Object for managing optimizization context More...
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... | |
![]() | |
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... | |
Object for managing optimizization context
Definition at line 30 of file Optimize.cs.
|
inline |
Alias for Assert.
Definition at line 84 of file Optimize.cs.
|
inline |
Alias for Assert.
Definition at line 92 of file Optimize.cs.
|
inline |
Assert a constraint (or multiple) into the optimize solver.
Definition at line 68 of file Optimize.cs.
|
inline |
Assert a constraint (or multiple) into the optimize solver.
Definition at line 76 of file Optimize.cs.
Assert soft constraint
Return an objective which associates with the group of constraints.
Definition at line 155 of file Optimize.cs.
|
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.
|
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.
|
inline |
Similar to FromFile. Instead it takes as argument a string.
Definition at line 291 of file Optimize.cs.
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.
Declare an arithmetical minimization objective. Similar to MkMaximize.
Definition at line 236 of file Optimize.cs.
|
inline |
Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding Push
Definition at line 197 of file Optimize.cs.
|
inline |
|
inline |
Print the context to a string (SMT-LIB parseable benchmark).
Definition at line 274 of file Optimize.cs.
|
get |
The set of asserted formulas.
Definition at line 300 of file Optimize.cs.
|
get |
A string that describes all available optimize solver parameters.
Definition at line 36 of file Optimize.cs.
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.
|
get |
The set of asserted formulas.
Definition at line 314 of file Optimize.cs.
|
get |
Retrieves parameter descriptions for Optimize solver.
Definition at line 61 of file Optimize.cs.
|
set |
Sets the optimize solver parameters.
Definition at line 48 of file Optimize.cs.
|
get |
Return a string the describes why the last to check returned unknown
Definition at line 262 of file Optimize.cs.
|
get |
Optimize statistics.
Definition at line 329 of file Optimize.cs.