Public Member Functions | |
String | getHelp () throws Z3Exception |
void | setParameters (Params value) throws Z3Exception |
ParamDescrs | getParameterDescriptions () throws Z3Exception |
void | add (BoolExpr...constraints) throws Z3Exception |
void | registerRelation (FuncDecl f) throws Z3Exception |
void | addRule (BoolExpr rule, Symbol name) throws Z3Exception |
void | addFact (FuncDecl pred, int...args) throws Z3Exception |
Status | query (BoolExpr query) throws Z3Exception |
Status | query (FuncDecl[] relations) throws Z3Exception |
void | push () throws Z3Exception |
void | pop () throws Z3Exception |
void | updateRule (BoolExpr rule, Symbol name) throws Z3Exception |
Expr | getAnswer () throws Z3Exception |
String | getReasonUnknown () throws Z3Exception |
int | getNumLevels (FuncDecl predicate) throws Z3Exception |
Expr | getCoverDelta (int level, FuncDecl predicate) throws Z3Exception |
void | addCover (int level, FuncDecl predicate, Expr property) throws Z3Exception |
String | toString () |
void | setPredicateRepresentation (FuncDecl f, Symbol[] kinds) throws Z3Exception |
String | toString (BoolExpr[] queries) throws Z3Exception |
BoolExpr[] | getRules () throws Z3Exception |
BoolExpr[] | getAssertions () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () throws Z3Exception |
Object for managing fixedpoints
Definition at line 25 of file Fixedpoint.java.
|
inline |
Assert a constraint (or multiple) into the fixedpoint solver.
Z3Exception |
Definition at line 65 of file Fixedpoint.java.
|
inline |
Add property
about the predicate
. The property is added at level
.
Definition at line 243 of file Fixedpoint.java.
|
inline |
Add table fact to the fixedpoint solver.
Z3Exception |
Definition at line 106 of file Fixedpoint.java.
|
inline |
Add rule into the fixedpoint solver.
Z3Exception |
Definition at line 93 of file Fixedpoint.java.
|
inline |
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.
Z3Exception |
Definition at line 202 of file Fixedpoint.java.
|
inline |
Retrieve set of assertions added to fixedpoint context.
Z3Exception |
Definition at line 310 of file Fixedpoint.java.
|
inline |
Retrieve the cover of a predicate.
Z3Exception |
Definition at line 232 of file Fixedpoint.java.
|
inline |
A string that describes all available fixedpoint solver parameters.
Definition at line 31 of file Fixedpoint.java.
|
inline |
Retrieve the number of levels explored for a given predicate.
Definition at line 221 of file Fixedpoint.java.
|
inline |
Retrieves parameter descriptions for Fixedpoint solver.
Z3Exception |
Definition at line 54 of file Fixedpoint.java.
|
inline |
Retrieve explanation why fixedpoint engine returned status Unknown.
Definition at line 211 of file Fixedpoint.java.
|
inline |
Retrieve set of rules added to fixedpoint context.
Z3Exception |
Definition at line 293 of file Fixedpoint.java.
|
inline |
Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding
Definition at line 178 of file Fixedpoint.java.
|
inline |
|
inline |
Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the recursively defined relations. The query is satisfiable if there is an instance of the query variables and a derivation for it. The query is unsatisfiable if there are no derivations satisfying the query variables.
Z3Exception |
Definition at line 122 of file Fixedpoint.java.
|
inline |
Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is an instance of some relation that is non-empty. The query is unsatisfiable if there are no derivations satisfying any of the relations.
Z3Exception |
Definition at line 147 of file Fixedpoint.java.
|
inline |
Register predicate as recursive relation.
Z3Exception |
Definition at line 80 of file Fixedpoint.java.
|
inline |
Sets the fixedpoint solver parameters.
Z3Exception |
Definition at line 41 of file Fixedpoint.java.
|
inline |
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition at line 269 of file Fixedpoint.java.
|
inline |
Retrieve internal string representation of fixedpoint object.
Definition at line 253 of file Fixedpoint.java.
|
inline |
Convert benchmark given as set of axioms, rules and queries to a string.
Definition at line 281 of file Fixedpoint.java.
|
inline |
Update named rule into in the fixedpoint solver.
Z3Exception |
Definition at line 188 of file Fixedpoint.java.