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) |
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 () |
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 26 of file Solver.java.
|
inline |
Assert a multiple constraints into the solver.
Z3Exception |
Definition at line 114 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 166 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 139 of file Solver.java.
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 250 of file Solver.java.
Referenced by Solver.check().
|
inline |
Checks whether the assertions in the solver are consistent or not. Remarks:
Definition at line 221 of file Solver.java.
|
inline |
Load solver assertions from a file.
Definition at line 178 of file Solver.java.
|
inline |
Load solver assertions from a string.
Definition at line 186 of file Solver.java.
|
inline |
The set of asserted formulas.
Z3Exception |
Definition at line 208 of file Solver.java.
|
inline |
A string that describes all available solver parameters.
Definition at line 30 of file Solver.java.
|
inline |
The model of the last Check
. Remarks: The result is null
if Check
was not invoked before, if its results was not SATISFIABLE
, or if model production is not enabled.
Z3Exception |
Definition at line 264 of file Solver.java.
|
inline |
The number of assertions in the solver.
Z3Exception |
Definition at line 197 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 Check
. Remarks: The result is null
if Check
was not invoked before, if its results was not UNSATISFIABLE
, or if proof production is disabled.
Z3Exception |
Definition at line 283 of file Solver.java.
|
inline |
A brief justification of why the last call to Check
returned UNKNOWN
.
Definition at line 313 of file Solver.java.
|
inline |
Solver statistics.
Z3Exception |
Definition at line 332 of file Solver.java.
|
inline |
The unsat core of the last Check
. Remarks: The unsat core is a subset of Assertions
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 302 of file Solver.java.
|
inline |
Backtracks one backtracking point. Remarks: .
Definition at line 82 of file Solver.java.
Referenced by Solver.pop().
|
inline |
Backtracks n
backtracking points. Remarks: Note that an exception is thrown if n
is not smaller than NumScopes
Definition at line 94 of file Solver.java.
|
inline |
Creates a backtracking point.
Definition at line 73 of file Solver.java.
|
inline |
Resets the Solver. Remarks: This removes all assertions from the solver.
Definition at line 104 of file Solver.java.
|
inline |
Sets the solver parameters.
Z3Exception |
Definition at line 40 of file Solver.java.
|
inline |
A string representation of the solver.
Definition at line 342 of file Solver.java.
Create a clone of the current solver with respect toctx
.
Definition at line 322 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__().