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 Add (params 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...
 
String getReasonUnknown ()
 Return a string the describes why the last to check returned unknown More...
 
override string ToString ()
 Print the context to a string (SMT-LIB parseable benchmark). 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...
 
Statistics Statistics [get]
 Optimize statistics. More...
 

Detailed Description

Object for managing optimizization context

Definition at line 30 of file Optimize.cs.

Member Function Documentation

void Add ( params BoolExpr[]  constraints)
inline

Alias for Assert.

Definition at line 83 of file Optimize.cs.

84  {
85  Assert(constraints);
86  }
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the optimize solver.
Definition: Optimize.cs:68
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  Contract.Requires(constraints != null);
71  Contract.Requires(Contract.ForAll(constraints, c => c != null));
72 
73  Context.CheckContextMatch(constraints);
74  foreach (BoolExpr a in constraints)
75  {
76  Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
77  }
78  }
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 132 of file Optimize.cs.

133  {
134  Context.CheckContextMatch(constraint);
135  Symbol s = Context.MkSymbol(group);
136  return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
137  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
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 146 of file Optimize.cs.

147  {
148  Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
149  switch (r)
150  {
151  case Z3_lbool.Z3_L_TRUE:
152  return Status.SATISFIABLE;
153  case Z3_lbool.Z3_L_FALSE:
154  return Status.UNSATISFIABLE;
155  default:
156  return Status.UNKNOWN;
157  }
158  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
Status
Status values.
Definition: Status.cs:27
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
String getReasonUnknown ( )
inline

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

Definition at line 238 of file Optimize.cs.

239  {
240  Contract.Ensures(Contract.Result<string>() != null);
241  return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
242  }
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 204 of file Optimize.cs.

205  {
206  return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
207  }
Handle MkMinimize ( ArithExpr  e)
inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 213 of file Optimize.cs.

214  {
215  return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
216  }
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 174 of file Optimize.cs.

175  {
176  Native.Z3_optimize_pop(Context.nCtx, NativeObject);
177  }
void Push ( )
inline

Creates a backtracking point.

See also
Pop

Definition at line 164 of file Optimize.cs.

165  {
166  Native.Z3_optimize_push(Context.nCtx, NativeObject);
167  }
override string ToString ( )
inline

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

Definition at line 248 of file Optimize.cs.

249  {
250  return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
251  }

Property Documentation

string Help
get

A string that describes all available optimize solver parameters.

Definition at line 36 of file Optimize.cs.

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 188 of file Optimize.cs.

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Optimize solver.

Definition at line 61 of file Optimize.cs.

Params Parameters
set

Sets the optimize solver parameters.

Definition at line 48 of file Optimize.cs.

Optimize statistics.

Definition at line 257 of file Optimize.cs.