Public Member Functions | |
String | getHelp () |
void | setParameters (Params value) |
ParamDescrs | getParameterDescriptions () |
int | getNumScopes () |
void | push () |
void | pop () |
void | pop (int n) |
void | reset () |
void | add (BoolExpr... constraints) |
void | assertAndTrack (BoolExpr[] constraints, BoolExpr[] ps) |
void | assertAndTrack (BoolExpr constraint, BoolExpr p) |
int | getNumAssertions () |
BoolExpr [] | getAssertions () |
Status | check (Expr... assumptions) |
Status | check () |
Model | getModel () |
Expr | getProof () |
BoolExpr [] | getUnsatCore () |
String | getReasonUnknown () |
Solver | translate (Context ctx) |
Statistics | getStatistics () |
String | toString () |
Solvers.
Definition at line 25 of file Solver.java.
|
inline |
Assert a multiple constraints into the solver.
Z3Exception |
Definition at line 113 of file Solver.java.
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
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 137 of file Solver.java.
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 164 of file Solver.java.
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 202 of file Solver.java.
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 231 of file Solver.java.
|
inline |
|
inline |
A string that describes all available solver parameters.
Definition at line 29 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 245 of file Solver.java.
|
inline |
The number of assertions in the solver.
Z3Exception |
Definition at line 178 of file Solver.java.
|
inline |
The current number of backtracking points (scopes).
Definition at line 62 of file Solver.java.
|
inline |
Retrieves parameter descriptions for solver.
Z3Exception |
Definition at line 51 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 264 of file Solver.java.
|
inline |
A brief justification of why the last call to
returned
.
Definition at line 294 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 283 of file Solver.java.
|
inline |
Backtracks one backtracking point. Remarks: .
Definition at line 81 of file Solver.java.
|
inline |
Backtracks
backtracking points. Remarks: Note that an exception is thrown if
is not smaller than
Definition at line 93 of file Solver.java.
|
inline |
|
inline |
Resets the Solver. Remarks: This removes all assertions from the solver.
Definition at line 103 of file Solver.java.
|
inline |
|
inline |
A string representation of the solver.
Definition at line 323 of file Solver.java.
Create a clone of the current solver with respect to
.
Definition at line 303 of file Solver.java.