Public Member Functions | |
String | getHelp () |
void | setParameters (Params value) |
ParamDescrs | getParameterDescriptions () |
final void | add (Expr< BoolSort >... constraints) |
void | registerRelation (FuncDecl< BoolSort > f) |
void | addRule (Expr< BoolSort > rule, Symbol name) |
void | addFact (FuncDecl< BoolSort > pred, int ... args) |
Status | query (Expr< BoolSort > query) |
Status | query (FuncDecl< BoolSort >[] relations) |
void | updateRule (Expr< BoolSort > rule, Symbol name) |
Expr<?> | getAnswer () |
String | getReasonUnknown () |
int | getNumLevels (FuncDecl< BoolSort > predicate) |
Expr<?> | getCoverDelta (int level, FuncDecl< BoolSort > predicate) |
void | addCover (int level, FuncDecl< BoolSort > predicate, Expr<?> property) |
String | toString () |
void | setPredicateRepresentation (FuncDecl< BoolSort > f, Symbol[] kinds) |
String | toString (Expr< BoolSort >[] queries) |
BoolExpr[] | getRules () |
BoolExpr[] | getAssertions () |
Statistics | getStatistics () |
BoolExpr[] | ParseFile (String file) |
BoolExpr[] | ParseString (String s) |
Additional Inherited Members | |
Static Public Member Functions inherited from Z3Object | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Object for managing fixedpoints
Definition at line 25 of file Fixedpoint.java.
Assert a constraint (or multiple) into the fixedpoint solver.
Z3Exception |
Definition at line 66 of file Fixedpoint.java.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
Add property
about the predicate
. The property is added at level
.
Definition at line 219 of file Fixedpoint.java.
Add table fact to the fixedpoint solver.
Z3Exception |
Definition at line 106 of file Fixedpoint.java.
Add rule into the fixedpoint solver.
rule | implication (Horn clause) representing rule |
name | Nullable rule name. |
Z3Exception |
Definition at line 95 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 179 of file Fixedpoint.java.
|
inline |
Retrieve set of assertions added to fixedpoint context.
Z3Exception |
Definition at line 273 of file Fixedpoint.java.
Retrieve the cover of a predicate.
Z3Exception |
Definition at line 208 of file Fixedpoint.java.
|
inline |
A string that describes all available fixedpoint solver parameters.
Definition at line 31 of file Fixedpoint.java.
Retrieve the number of levels explored for a given predicate.
Definition at line 197 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 188 of file Fixedpoint.java.
|
inline |
Retrieve set of rules added to fixedpoint context.
Z3Exception |
Definition at line 262 of file Fixedpoint.java.
|
inline |
|
inline |
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.
Definition at line 295 of file Fixedpoint.java.
|
inline |
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.
Definition at line 306 of file Fixedpoint.java.
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 121 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 144 of file Fixedpoint.java.
Register predicate as recursive relation.
Z3Exception |
Definition at line 81 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 240 of file Fixedpoint.java.
|
inline |
Retrieve internal string representation of fixedpoint object.
Definition at line 230 of file Fixedpoint.java.
Convert benchmark given as set of axioms, rules and queries to a string.
Definition at line 251 of file Fixedpoint.java.
Update named rule into in the fixedpoint solver.
rule | implication (Horn clause) representing rule |
name | Nullable rule name. |
Z3Exception |
Definition at line 167 of file Fixedpoint.java.