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 |
Package Functions | |
Fixedpoint (Context ctx, long obj) throws Z3Exception | |
Fixedpoint (Context ctx) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
Object for managing fixedpoints
Definition at line 25 of file Fixedpoint.java.
Fixedpoint | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 322 of file Fixedpoint.java.
{ super(ctx, obj); }
Fixedpoint | ( | Context | ctx | ) | throws Z3Exception [inline, package] |
Definition at line 327 of file Fixedpoint.java.
{ super(ctx, Native.mkFixedpoint(ctx.nCtx())); }
void add | ( | BoolExpr... | constraints | ) | throws Z3Exception [inline] |
Assert a constraint (or multiple) into the fixedpoint solver.
Z3Exception |
Definition at line 65 of file Fixedpoint.java.
{ getContext().checkContextMatch(constraints); for (BoolExpr a : constraints) { Native.fixedpointAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject()); } }
void addCover | ( | int | level, |
FuncDecl | predicate, | ||
Expr | property | ||
) | throws Z3Exception [inline] |
Add property
about the predicate
. The property is added at level
.
Definition at line 243 of file Fixedpoint.java.
{ Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level, predicate.getNativeObject(), property.getNativeObject()); }
void addFact | ( | FuncDecl | pred, |
int... | args | ||
) | throws Z3Exception [inline] |
Add table fact to the fixedpoint solver.
Z3Exception |
Definition at line 106 of file Fixedpoint.java.
{ getContext().checkContextMatch(pred); Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(), pred.getNativeObject(), (int) args.length, args); }
void addRule | ( | BoolExpr | rule, |
Symbol | name | ||
) | throws Z3Exception [inline] |
Add rule into the fixedpoint solver.
Z3Exception |
Definition at line 93 of file Fixedpoint.java.
{ getContext().checkContextMatch(rule); Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(), rule.getNativeObject(), AST.getNativeObject(name)); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 338 of file Fixedpoint.java.
{ getContext().fixedpoint_DRQ().add(o); super.decRef(o); }
Expr getAnswer | ( | ) | throws Z3Exception [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.
{ long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject()); return (ans == 0) ? null : Expr.create(getContext(), ans); }
BoolExpr [] getAssertions | ( | ) | throws Z3Exception [inline] |
Retrieve set of assertions added to fixedpoint context.
Z3Exception |
Definition at line 310 of file Fixedpoint.java.
{ ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( getContext().nCtx(), getNativeObject())); int n = v.size(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); return res; }
Expr getCoverDelta | ( | int | level, |
FuncDecl | predicate | ||
) | throws Z3Exception [inline] |
Retrieve the cover of a predicate.
Z3Exception |
Definition at line 232 of file Fixedpoint.java.
{ long res = Native.fixedpointGetCoverDelta(getContext().nCtx(), getNativeObject(), level, predicate.getNativeObject()); return (res == 0) ? null : Expr.create(getContext(), res); }
String getHelp | ( | ) | throws Z3Exception [inline] |
A string that describes all available fixedpoint solver parameters.
Definition at line 31 of file Fixedpoint.java.
{ return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject()); }
int getNumLevels | ( | FuncDecl | predicate | ) | throws Z3Exception [inline] |
Retrieve the number of levels explored for a given predicate.
Definition at line 221 of file Fixedpoint.java.
{ return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(), predicate.getNativeObject()); }
ParamDescrs getParameterDescriptions | ( | ) | throws Z3Exception [inline] |
Retrieves parameter descriptions for Fixedpoint solver.
Z3Exception |
Definition at line 54 of file Fixedpoint.java.
{ return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs( getContext().nCtx(), getNativeObject())); }
String getReasonUnknown | ( | ) | throws Z3Exception [inline] |
Retrieve explanation why fixedpoint engine returned status Unknown.
Definition at line 211 of file Fixedpoint.java.
{ return Native.fixedpointGetReasonUnknown(getContext().nCtx(), getNativeObject()); }
BoolExpr [] getRules | ( | ) | throws Z3Exception [inline] |
Retrieve set of rules added to fixedpoint context.
Z3Exception |
Definition at line 293 of file Fixedpoint.java.
{ ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( getContext().nCtx(), getNativeObject())); int n = v.size(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); return res; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 332 of file Fixedpoint.java.
{ getContext().fixedpoint_DRQ().incAndClear(getContext(), o); super.incRef(o); }
void pop | ( | ) | throws Z3Exception [inline] |
Backtrack one backtracking point. Note that an exception is thrown if Pop is called without a corresponding Push
Definition at line 178 of file Fixedpoint.java.
{ Native.fixedpointPop(getContext().nCtx(), getNativeObject()); }
void push | ( | ) | throws Z3Exception [inline] |
Creates a backtracking point.
Definition at line 168 of file Fixedpoint.java.
{ Native.fixedpointPush(getContext().nCtx(), getNativeObject()); }
Status query | ( | BoolExpr | query | ) | throws Z3Exception [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.
{ getContext().checkContextMatch(query); Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(), getNativeObject(), query.getNativeObject())); switch (r) { case Z3_L_TRUE: return Status.SATISFIABLE; case Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } }
Status query | ( | FuncDecl[] | relations | ) | throws Z3Exception [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.
{ getContext().checkContextMatch(relations); Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext() .nCtx(), getNativeObject(), AST.arrayLength(relations), AST .arrayToNative(relations))); switch (r) { case Z3_L_TRUE: return Status.SATISFIABLE; case Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } }
void registerRelation | ( | FuncDecl | f | ) | throws Z3Exception [inline] |
Register predicate as recursive relation.
Z3Exception |
Definition at line 80 of file Fixedpoint.java.
{ getContext().checkContextMatch(f); Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(), f.getNativeObject()); }
void setParameters | ( | Params | value | ) | throws Z3Exception [inline] |
Sets the fixedpoint solver parameters.
Z3Exception |
Definition at line 41 of file Fixedpoint.java.
{ getContext().checkContextMatch(value); Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject()); }
void setPredicateRepresentation | ( | FuncDecl | f, |
Symbol[] | kinds | ||
) | throws Z3Exception [inline] |
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition at line 269 of file Fixedpoint.java.
{ Native.fixedpointSetPredicateRepresentation(getContext().nCtx(), getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds), Symbol.arrayToNative(kinds)); }
String toString | ( | ) | [inline] |
Retrieve internal string representation of fixedpoint object.
Definition at line 253 of file Fixedpoint.java.
{ try { return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), 0, null); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }
String toString | ( | BoolExpr[] | queries | ) | throws Z3Exception [inline] |
Convert benchmark given as set of axioms, rules and queries to a string.
Definition at line 281 of file Fixedpoint.java.
{ return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), AST.arrayLength(queries), AST.arrayToNative(queries)); }
void updateRule | ( | BoolExpr | rule, |
Symbol | name | ||
) | throws Z3Exception [inline] |
Update named rule into in the fixedpoint solver.
Z3Exception |
Definition at line 188 of file Fixedpoint.java.
{ getContext().checkContextMatch(rule); Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(), rule.getNativeObject(), AST.getNativeObject(name)); }