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 () |
void | Push () |
void | Pop () |
Model | getModel () |
Handle | MkMaximize (ArithExpr e) |
Handle | MkMinimize (ArithExpr e) |
String | getReasonUnknown () |
String | toString () |
Statistics | getStatistics () |
Object for managing optimizization context
Definition at line 28 of file Optimize.java.
|
inline |
|
inline |
Assert a constraint (or multiple) into the optimize solver.
Definition at line 59 of file Optimize.java.
Referenced by Optimize.Add().
Assert soft constraint
Return an objective which associates with the group of constraints.
Definition at line 130 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 144 of file Optimize.java.
|
inline |
A string that describes all available optimize solver parameters.
Definition at line 33 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 184 of file Optimize.java.
|
inline |
Retrieves parameter descriptions for Optimize solver.
Definition at line 51 of file Optimize.java.
|
inline |
Return a string the describes why the last to check returned unknown
Definition at line 233 of file Optimize.java.
|
inline |
Optimize statistics.
Definition at line 252 of file Optimize.java.
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 199 of file Optimize.java.
Declare an arithmetical minimization objective. Similar to MkMaximize.
Definition at line 208 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 172 of file Optimize.java.
|
inline |
Creates a backtracking point.
Definition at line 160 of file Optimize.java.
|
inline |
Sets the optimize solver parameters.
Z3Exception |
Definition at line 43 of file Optimize.java.
|
inline |
Print the context to a String (SMT-LIB parseable benchmark).
Definition at line 244 of file Optimize.java.