Data Structures | |
class | Handle |
Public Member Functions | |
String | getHelp () |
void | setParameters (Params value) |
ParamDescrs | getParameterDescriptions () |
void | Assert (BoolExpr ... constraints) |
void | Add (BoolExpr ... constraints) |
Handle | AssertSoft (BoolExpr constraint, int weight, String group) |
Status | Check (Expr... assumptions) |
void | Push () |
void | Pop () |
Model | getModel () |
BoolExpr[] | getUnsatCore () |
Handle | MkMaximize (Expr e) |
Handle | MkMinimize (Expr e) |
String | getReasonUnknown () |
String | toString () |
void | fromFile (String file) |
void | fromString (String s) |
BoolExpr[] | getAssertions () |
Expr[] | getObjectives () |
Statistics | getStatistics () |
Object for managing optimization context
Definition at line 27 of file Optimize.java.
|
inline |
|
inline |
Assert a constraint (or multiple) into the optimize solver.
Definition at line 58 of file Optimize.java.
Referenced by Optimize.Add().
|
inline |
Assert soft constraint
Return an objective which associates with the group of constraints.
Definition at line 152 of file Optimize.java.
|
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 164 of file Optimize.java.
|
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 333 of file Optimize.java.
|
inline |
Similar to FromFile. Instead it takes as argument a string.
Definition at line 341 of file Optimize.java.
|
inline |
The set of asserted formulas.
Definition at line 349 of file Optimize.java.
|
inline |
A string that describes all available optimize solver parameters.
Definition at line 32 of file Optimize.java.
|
inline |
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 216 of file Optimize.java.
|
inline |
The set of asserted formulas.
Definition at line 358 of file Optimize.java.
|
inline |
Retrieves parameter descriptions for Optimize solver.
Definition at line 50 of file Optimize.java.
|
inline |
Return a string the describes why the last to check returned unknown
Definition at line 315 of file Optimize.java.
|
inline |
Optimize statistics.
Definition at line 367 of file Optimize.java.
|
inline |
The unsat core of the last
. Remarks: The unsat core is a subset of
The result is empty if
was not invoked before, if its results was not
, or if core production is disabled.
Z3Exception |
Definition at line 235 of file Optimize.java.
|
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 246 of file Optimize.java.
|
inline |
Declare an arithmetical minimization objective. Similar to MkMaximize.
Definition at line 255 of file Optimize.java.
|
inline |
Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding Push.
Definition at line 204 of file Optimize.java.
|
inline |
Creates a backtracking point.
Definition at line 194 of file Optimize.java.
|
inline |
Sets the optimize solver parameters.
Z3Exception |
Definition at line 42 of file Optimize.java.
|
inline |
Print the context to a String (SMT-LIB parseable benchmark).
Definition at line 324 of file Optimize.java.