Z3
Data Structures | Public Member Functions | Properties
Optimize Class Reference

Object for managing optimizization context More...

+ Inheritance diagram for Optimize:

Data Structures

class  DecRefQueue
 
class  Handle
 Handle to objectives returned by objective functions. More...
 

Public Member Functions

void Assert (params BoolExpr[] constraints)
 Assert a constraint (or multiple) into the optimize solver. More...
 
void Assert (IEnumerable< BoolExpr > constraints)
 Assert a constraint (or multiple) into the optimize solver. More...
 
void Add (params BoolExpr[] constraints)
 Alias for Assert. More...
 
void Add (IEnumerable< BoolExpr > constraints)
 Alias for Assert. More...
 
Handle AssertSoft (BoolExpr constraint, uint weight, string group)
 Assert soft constraint More...
 
Status Check ()
 Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives. More...
 
void Push ()
 Creates a backtracking point. More...
 
void Pop ()
 Backtrack one backtracking point. More...
 
Handle MkMaximize (ArithExpr e)
 Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check. More...
 
Handle MkMinimize (ArithExpr e)
 Declare an arithmetical minimization objective. Similar to MkMaximize. More...
 
override string ToString ()
 Print the context to a string (SMT-LIB parseable benchmark). More...
 
void FromFile (string file)
 Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context. More...
 
void FromString (string s)
 Similar to FromFile. Instead it takes as argument a string. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

string Help [get]
 A string that describes all available optimize solver parameters. More...
 
Params Parameters [set]
 Sets the optimize solver parameters. More...
 
ParamDescrs ParameterDescriptions [get]
 Retrieves parameter descriptions for Optimize solver. More...
 
Model Model [get]
 The model of the last Check. More...
 
String ReasonUnknown [get]
 Return a string the describes why the last to check returned unknown More...
 
BoolExpr [] Assertions [get]
 The set of asserted formulas. More...
 
Expr [] Objectives [get]
 The set of asserted formulas. More...
 
Statistics Statistics [get]
 Optimize statistics. More...
 

Detailed Description

Object for managing optimizization context

Definition at line 30 of file Optimize.cs.

Member Function Documentation

◆ Add() [1/2]

void Add ( params BoolExpr []  constraints)
inline

Alias for Assert.

Definition at line 84 of file Optimize.cs.

85  {
86  AddConstraints(constraints);
87  }

◆ Add() [2/2]

void Add ( IEnumerable< BoolExpr constraints)
inline

Alias for Assert.

Definition at line 92 of file Optimize.cs.

93  {
94  AddConstraints(constraints);
95  }

◆ Assert() [1/2]

void Assert ( params BoolExpr []  constraints)
inline

Assert a constraint (or multiple) into the optimize solver.

Definition at line 68 of file Optimize.cs.

69  {
70  AddConstraints(constraints);
71  }

◆ Assert() [2/2]

void Assert ( IEnumerable< BoolExpr constraints)
inline

Assert a constraint (or multiple) into the optimize solver.

Definition at line 76 of file Optimize.cs.

77  {
78  AddConstraints(constraints);
79  }

◆ AssertSoft()

Handle AssertSoft ( BoolExpr  constraint,
uint  weight,
string  group 
)
inline

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 155 of file Optimize.cs.

156  {
157  Context.CheckContextMatch(constraint);
158  Symbol s = Context.MkSymbol(group);
159  return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
160  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

◆ Check()

Status Check ( )
inline

Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives.

Definition at line 169 of file Optimize.cs.

170  {
171  Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
172  switch (r)
173  {
174  case Z3_lbool.Z3_L_TRUE:
175  return Status.SATISFIABLE;
176  case Z3_lbool.Z3_L_FALSE:
177  return Status.UNSATISFIABLE;
178  default:
179  return Status.UNKNOWN;
180  }
181  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
Status
Status values.
Definition: Status.cs:27

◆ FromFile()

void FromFile ( string  file)
inline

Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context.

Definition at line 283 of file Optimize.cs.

284  {
285  Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
286  }

◆ FromString()

void FromString ( string  s)
inline

Similar to FromFile. Instead it takes as argument a string.

Definition at line 291 of file Optimize.cs.

292  {
293  Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
294  }

◆ MkMaximize()

Handle MkMaximize ( ArithExpr  e)
inline

Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check.

Definition at line 227 of file Optimize.cs.

228  {
229  return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
230  }

◆ MkMinimize()

Handle MkMinimize ( ArithExpr  e)
inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 236 of file Optimize.cs.

237  {
238  return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
239  }

◆ Pop()

void Pop ( )
inline

Backtrack one backtracking point.

Note that an exception is thrown if Pop is called without a corresponding Push

See also
Push

Definition at line 197 of file Optimize.cs.

198  {
199  Native.Z3_optimize_pop(Context.nCtx, NativeObject);
200  }

◆ Push()

void Push ( )
inline

Creates a backtracking point.

See also
Pop

Definition at line 187 of file Optimize.cs.

188  {
189  Native.Z3_optimize_push(Context.nCtx, NativeObject);
190  }

◆ ToString()

override string ToString ( )
inline

Print the context to a string (SMT-LIB parseable benchmark).

Definition at line 274 of file Optimize.cs.

275  {
276  return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
277  }

Property Documentation

◆ Assertions

BoolExpr [] Assertions
get

The set of asserted formulas.

Definition at line 300 of file Optimize.cs.

300  {
301  get
302  {
303  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
304 
305  ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
306  return assertions.ToBoolExprArray();
307  }
308  }

◆ Help

string Help
get

A string that describes all available optimize solver parameters.

Definition at line 36 of file Optimize.cs.

36  {
37  get
38  {
39  Contract.Ensures(Contract.Result<string>() != null);
40  return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
41  }
42  }

◆ Model

Model Model
get

The model of the last Check.

The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Definition at line 211 of file Optimize.cs.

211  {
212  get
213  {
214  IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
215  if (x == IntPtr.Zero)
216  return null;
217  else
218  return new Model(Context, x);
219  }
220  }
Model Model
The model of the last Check.
Definition: Optimize.cs:211

◆ Objectives

Expr [] Objectives
get

The set of asserted formulas.

Definition at line 314 of file Optimize.cs.

314  {
315  get
316  {
317  Contract.Ensures(Contract.Result<Expr[]>() != null);
318 
319  ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
320  return objectives.ToExprArray();
321  }
322  }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Optimize solver.

Definition at line 61 of file Optimize.cs.

61  {
62  get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
63  }

◆ Parameters

Params Parameters
set

Sets the optimize solver parameters.

Definition at line 48 of file Optimize.cs.

48  {
49  set
50  {
51  Contract.Requires(value != null);
52  Context.CheckContextMatch(value);
53  Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
54  }
55  }

◆ ReasonUnknown

String ReasonUnknown
get

Return a string the describes why the last to check returned unknown

Definition at line 262 of file Optimize.cs.

262  {
263  get
264  {
265  Contract.Ensures(Contract.Result<string>() != null);
266  return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
267  }
268  }

◆ Statistics

Optimize statistics.

Definition at line 329 of file Optimize.cs.

329  {
330  get
331  {
332  Contract.Ensures(Contract.Result<Statistics>() != null);
333 
334  return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
335  }
336  }
Statistics Statistics
Optimize statistics.
Definition: Optimize.cs:329