Object for managing fixedpoints
Definition at line 25 of file Fixedpoint.java.
§ add()
Assert a constraint (or multiple) into the fixedpoint solver.
- Exceptions
-
Definition at line 65 of file Fixedpoint.java.
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
67 getContext().checkContextMatch(constraints);
68 for (BoolExpr a : constraints)
70 Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
§ addCover()
void addCover |
( |
int |
level, |
|
|
FuncDecl |
predicate, |
|
|
Expr |
property |
|
) |
| |
|
inline |
Add property
about the predicate
. The property is added at level
.
Definition at line 236 of file Fixedpoint.java.
239 Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
240 predicate.getNativeObject(),
property.getNativeObject());
§ addFact()
void addFact |
( |
FuncDecl |
pred, |
|
|
int ... |
args |
|
) |
| |
|
inline |
Add table fact to the fixedpoint solver.
- Exceptions
-
Definition at line 105 of file Fixedpoint.java.
106 getContext().checkContextMatch(pred);
107 Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
108 pred.getNativeObject(), args.length, args);
§ addRule()
Add rule into the fixedpoint solver.
- Parameters
-
- Exceptions
-
Definition at line 94 of file Fixedpoint.java.
95 getContext().checkContextMatch(rule);
96 Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
97 rule.getNativeObject(), AST.getNativeObject(name));
§ getAnswer()
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.
- Exceptions
-
Definition at line 196 of file Fixedpoint.java.
198 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
199 return (ans == 0) ? null : Expr.create(getContext(), ans);
§ getAssertions()
Retrieve set of assertions added to fixedpoint context.
- Exceptions
-
Definition at line 292 of file Fixedpoint.java.
294 ASTVector v =
new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
295 return v.ToBoolExprArray();
§ getCoverDelta()
Retrieve the cover of a predicate.
- Exceptions
-
Definition at line 225 of file Fixedpoint.java.
227 long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
228 getNativeObject(), level, predicate.getNativeObject());
229 return (res == 0) ? null : Expr.create(getContext(), res);
§ getHelp()
A string that describes all available fixedpoint solver parameters.
Definition at line 31 of file Fixedpoint.java.
33 return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
§ getNumLevels()
Retrieve the number of levels explored for a given predicate.
Definition at line 214 of file Fixedpoint.java.
216 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
217 predicate.getNativeObject());
§ getParameterDescriptions()
Retrieves parameter descriptions for Fixedpoint solver.
- Exceptions
-
Definition at line 54 of file Fixedpoint.java.
56 return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
§ getReasonUnknown()
String getReasonUnknown |
( |
| ) |
|
|
inline |
Retrieve explanation why fixedpoint engine returned status Unknown.
Definition at line 205 of file Fixedpoint.java.
207 return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
§ getRules()
Retrieve set of rules added to fixedpoint context.
- Exceptions
-
Definition at line 281 of file Fixedpoint.java.
283 ASTVector v =
new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
284 return v.ToBoolExprArray();
§ getStatistics()
Fixedpoint statistics.
- Exceptions
-
Definition at line 303 of file Fixedpoint.java.
305 return new Statistics(getContext(), Native.fixedpointGetStatistics(
306 getContext().nCtx(), getNativeObject()));
§ ParseFile()
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 314 of file Fixedpoint.java.
316 ASTVector av =
new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
317 return av.ToBoolExprArray();
§ ParseString()
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 325 of file Fixedpoint.java.
327 ASTVector av =
new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
328 return av.ToBoolExprArray();
§ pop()
Backtrack one backtracking point. Remarks: Note that an exception is thrown if
is called without a corresponding
- See also
- push
Definition at line 174 of file Fixedpoint.java.
175 Native.fixedpointPop(getContext().nCtx(), getNativeObject());
§ push()
Creates a backtracking point.
- See also
- pop
Definition at line 163 of file Fixedpoint.java.
164 Native.fixedpointPush(getContext().nCtx(), getNativeObject());
§ query() [1/2]
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.
- Exceptions
-
Definition at line 120 of file Fixedpoint.java.
121 getContext().checkContextMatch(
query);
123 getNativeObject(),
query.getNativeObject()));
127 return Status.SATISFIABLE;
129 return Status.UNSATISFIABLE;
Status query(BoolExpr query)
Z3_lbool
Lifted Boolean type: false, undefined, true.
§ query() [2/2]
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.
- Exceptions
-
Definition at line 143 of file Fixedpoint.java.
144 getContext().checkContextMatch(relations);
146 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
147 .arrayToNative(relations)));
151 return Status.SATISFIABLE;
153 return Status.UNSATISFIABLE;
Z3_lbool
Lifted Boolean type: false, undefined, true.
§ registerRelation()
Register predicate as recursive relation.
- Exceptions
-
Definition at line 80 of file Fixedpoint.java.
83 getContext().checkContextMatch(f);
84 Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
§ setParameters()
void setParameters |
( |
Params |
value | ) |
|
|
inline |
Sets the fixedpoint solver parameters.
- Exceptions
-
Definition at line 41 of file Fixedpoint.java.
44 getContext().checkContextMatch(value);
45 Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
§ setPredicateRepresentation()
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition at line 257 of file Fixedpoint.java.
260 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
261 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
262 Symbol.arrayToNative(kinds));
§ toString() [1/2]
Retrieve internal string representation of fixedpoint object.
Definition at line 247 of file Fixedpoint.java.
249 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
§ toString() [2/2]
Convert benchmark given as set of axioms, rules and queries to a string.
Definition at line 269 of file Fixedpoint.java.
272 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
273 AST.arrayLength(queries), AST.arrayToNative(queries));
§ updateRule()
Update named rule into in the fixedpoint solver.
- Parameters
-
- Exceptions
-
Definition at line 184 of file Fixedpoint.java.
185 getContext().checkContextMatch(rule);
186 Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
187 rule.getNativeObject(), AST.getNativeObject(name));