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 () |
Statistics | getStatistics () |
String | toString () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
Solvers.
Definition at line 25 of file Solver.java.
|
inline |
Assert a multiple constraints into the solver.
Z3Exception |
Definition at line 114 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 AssertAndTrack and the Boolean literals provided using Check with assumptions.
Definition at line 138 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 163 of file Solver.java.
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 201 of file Solver.java.
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 229 of file Solver.java.
|
inline |
|
inline |
A string that describes all available solver parameters.
Definition at line 30 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 243 of file Solver.java.
|
inline |
The number of assertions in the solver.
Z3Exception |
Definition at line 177 of file Solver.java.
|
inline |
The current number of backtracking points (scopes).
Definition at line 63 of file Solver.java.
|
inline |
Retrieves parameter descriptions for solver.
Z3Exception |
Definition at line 52 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 261 of file Solver.java.
|
inline |
A brief justification of why the last call to
returned
.
Definition at line 290 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 279 of file Solver.java.
|
inline |
Backtracks one backtracking point. Remarks: .
Definition at line 82 of file Solver.java.
|
inline |
Backtracks
backtracking points. Remarks: Note that an exception is thrown if
is not smaller than
Definition at line 94 of file Solver.java.
|
inline |
|
inline |
Resets the Solver. Remarks: This removes all assertions from the solver.
Definition at line 104 of file Solver.java.
|
inline |
|
inline |
A string representation of the solver.
Definition at line 310 of file Solver.java.