Public Member Functions | |
String | getHelp () |
void | setParameters (Params value) |
ParamDescrs | getParameterDescriptions () |
void | add (BoolExpr...constraints) |
void | registerRelation (FuncDecl f) |
void | addRule (BoolExpr rule, Symbol name) |
void | addFact (FuncDecl pred, int...args) |
Status | query (BoolExpr query) |
Status | query (FuncDecl[] relations) |
void | push () |
void | pop () |
void | updateRule (BoolExpr rule, Symbol name) |
Expr | getAnswer () |
String | getReasonUnknown () |
int | getNumLevels (FuncDecl predicate) |
Expr | getCoverDelta (int level, FuncDecl predicate) |
void | addCover (int level, FuncDecl predicate, Expr property) |
String | toString () |
void | setPredicateRepresentation (FuncDecl f, Symbol[] kinds) |
String | toString (BoolExpr[] queries) |
BoolExpr[] | getRules () |
BoolExpr[] | getAssertions () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
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.
Add property
about the predicate
. The property is added at level
.
Definition at line 246 of file Fixedpoint.java.
|
inline |
Add table fact to the fixedpoint solver.
Z3Exception |
Definition at line 106 of file Fixedpoint.java.
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 205 of file Fixedpoint.java.
|
inline |
Retrieve set of assertions added to fixedpoint context.
Z3Exception |
Definition at line 313 of file Fixedpoint.java.
Retrieve the cover of a predicate.
Z3Exception |
Definition at line 235 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 224 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 214 of file Fixedpoint.java.
|
inline |
Retrieve set of rules added to fixedpoint context.
Z3Exception |
Definition at line 296 of file Fixedpoint.java.
|
inline |
Backtrack one backtracking point. Remarks: Note that an exception is thrown if
is called without a corresponding
Definition at line 181 of file Fixedpoint.java.
|
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.
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.
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition at line 272 of file Fixedpoint.java.
|
inline |
Retrieve internal string representation of fixedpoint object.
Definition at line 256 of file Fixedpoint.java.
|
inline |
Convert benchmark given as set of axioms, rules and queries to a string.
Definition at line 284 of file Fixedpoint.java.
Update named rule into in the fixedpoint solver.
Z3Exception |
Definition at line 191 of file Fixedpoint.java.