Data Structures | |
class | Handle |
Public Member Functions | |
String | getHelp () |
void | setParameters (Params value) |
ParamDescrs | getParameterDescriptions () |
void | Assert (Expr< BoolSort > ... constraints) |
void | Add (Expr< BoolSort > ... constraints) |
void | AssertAndTrack (Expr< BoolSort > constraint, Expr< BoolSort > p) |
Handle<?> | AssertSoft (Expr< BoolSort > constraint, int weight, String group) |
Status | Check (Expr< BoolSort >... assumptions) |
void | Push () |
void | Pop () |
Model | getModel () |
BoolExpr[] | getUnsatCore () |
String | getReasonUnknown () |
String | toString () |
void | fromFile (String file) |
void | fromString (String s) |
BoolExpr[] | getAssertions () |
Expr<?>[] | getObjectives () |
Statistics | getStatistics () |
Additional Inherited Members | |
![]() | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Object for managing optimization context
Definition at line 28 of file Optimize.java.
Alias for Assert.
Definition at line 71 of file Optimize.java.
Assert a constraint (or multiple) into the optimize solver.
Definition at line 59 of file Optimize.java.
Assert a constraint into the optimizer, and track it (in the unsat) core using the Boolean constant p.
Remarks: This API is an alternative to check
with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using assertAndTrack
and the Boolean literals provided using check
with assumptions.
Definition at line 89 of file Optimize.java.
Assert soft constraint
Return an objective which associates with the group of constraints.
Definition at line 175 of file Optimize.java.
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 187 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 356 of file Optimize.java.
|
inline |
Similar to FromFile. Instead it takes as argument a string.
Definition at line 364 of file Optimize.java.
|
inline |
The set of asserted formulas.
Definition at line 372 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 239 of file Optimize.java.
|
inline |
The set of asserted formulas.
Definition at line 381 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 338 of file Optimize.java.
|
inline |
Optimize statistics.
Definition at line 390 of file Optimize.java.
|
inline |
The unsat core of the last Check
. Remarks: The unsat core is a subset of Assumptions
The result is empty if Check
was not invoked before, if its results was not UNSATISFIABLE
, or if core production is disabled.
Z3Exception |
Definition at line 258 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 227 of file Optimize.java.
|
inline |
Creates a backtracking point.
Definition at line 217 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 347 of file Optimize.java.