|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
Z3
|
|
Inheritance diagram for Fixedpoint: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));
}
1.7.6.1