Public Member Functions | |
String | getHelp () |
void | setParameters (Params value) |
ParamDescrs | getParameterDescriptions () |
int | getNumScopes () |
void | push () |
void | pop () |
void | pop (int n) |
void | reset () |
void | interrupt () |
void | add (Expr< BoolSort >... constraints) |
void | assertAndTrack (Expr< BoolSort >[] constraints, Expr< BoolSort >[] ps) |
void | assertAndTrack (Expr< BoolSort > constraint, Expr< BoolSort > p) |
void | fromFile (String file) |
Load solver assertions from a file. More... | |
void | fromString (String str) |
Load solver assertions from a string. More... | |
int | getNumAssertions () |
BoolExpr[] | getAssertions () |
final Status | check (Expr< BoolSort >... assumptions) |
Status | check () |
Status | getConsequences (Expr< BoolSort >[] assumptions, Expr<?>[] variables, List< Expr< BoolSort >> consequences) |
Model | getModel () |
Expr<?> | getProof () |
BoolExpr[] | getUnsatCore () |
String | getReasonUnknown () |
Solver | translate (Context ctx) |
Statistics | getStatistics () |
String | toString () |
Additional Inherited Members | |
Static Public Member Functions inherited from Z3Object | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Solvers.
Definition at line 28 of file Solver.java.
Assert a multiple constraints into the solver.
Z3Exception |
Definition at line 126 of file Solver.java.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
Assert a constraint into the solver, 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 178 of file Solver.java.
Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps.
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
and the Boolean literals provided using check() with assumptions.
Definition at line 151 of file Solver.java.
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 256 of file Solver.java.
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 234 of file Solver.java.
|
inline |
Load solver assertions from a file.
Definition at line 190 of file Solver.java.
|
inline |
Load solver assertions from a string.
Definition at line 198 of file Solver.java.
|
inline |
|
inline |
Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is an implication of the form
relevant-assumptions Implies variable = value
where the relevant assumptions is a subset of the assumptions that are passed in and the equality on the right side of the implication indicates how a variable is fixed.
Definition at line 272 of file Solver.java.
|
inline |
A string that describes all available solver parameters.
Definition at line 32 of file Solver.java.
|
inline |
The model of the last
. Remarks: The result is
if
was not invoked before, if its results was not
, or if model production is not enabled.
Z3Exception |
Definition at line 294 of file Solver.java.
|
inline |
The number of assertions in the solver.
Z3Exception |
Definition at line 209 of file Solver.java.
|
inline |
The current number of backtracking points (scopes).
Definition at line 65 of file Solver.java.
|
inline |
Retrieves parameter descriptions for solver.
Z3Exception |
Definition at line 54 of file Solver.java.
|
inline |
The proof of the last
. Remarks: The result is
if
was not invoked before, if its results was not
, or if proof production is disabled.
Z3Exception |
Definition at line 313 of file Solver.java.
|
inline |
A brief justification of why the last call to
returned
.
Definition at line 343 of file Solver.java.
|
inline |
|
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 332 of file Solver.java.
|
inline |
Interrupt the execution of the solver object. Remarks: This ensures that the interrupt applies only to the given solver object and it applies only if it is running.
Definition at line 116 of file Solver.java.
|
inline |
Backtracks one backtracking point. Remarks: .
Definition at line 84 of file Solver.java.
|
inline |
Backtracks
backtracking points. Remarks: Note that an exception is thrown if
is not smaller than
Definition at line 96 of file Solver.java.
|
inline |
|
inline |
Resets the Solver. Remarks: This removes all assertions from the solver.
Definition at line 106 of file Solver.java.
|
inline |
|
inline |
A string representation of the solver.
Definition at line 372 of file Solver.java.
Create a clone of the current solver with respect to
.
Definition at line 352 of file Solver.java.
Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().