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.
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 238 of file Fixedpoint.java.
241 Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
242 predicate.getNativeObject(),
property.getNativeObject());
◆ addFact()
void addFact |
( |
FuncDecl |
pred, |
|
|
int ... |
args |
|
) |
| |
|
inline |
Add table fact to the fixedpoint solver.
- Exceptions
-
Definition at line 106 of file Fixedpoint.java.
107 getContext().checkContextMatch(pred);
108 Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
109 pred.getNativeObject(), args.length, args);
◆ addRule()
Add rule into the fixedpoint solver.
- Parameters
-
rule | implication (Horn clause) representing rule |
name | Nullable rule name. |
- Exceptions
-
Definition at line 95 of file Fixedpoint.java.
96 getContext().checkContextMatch(rule);
97 Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
98 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 198 of file Fixedpoint.java.
200 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
201 return (ans == 0) ? null : Expr.create(getContext(), ans);
◆ getAssertions()
Retrieve set of assertions added to fixedpoint context.
- Exceptions
-
Definition at line 294 of file Fixedpoint.java.
296 ASTVector v =
new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
297 return v.ToBoolExprArray();
◆ getCoverDelta()
Retrieve the cover of a predicate.
- Exceptions
-
Definition at line 227 of file Fixedpoint.java.
229 long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
230 getNativeObject(), level, predicate.getNativeObject());
231 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 216 of file Fixedpoint.java.
218 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
219 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 207 of file Fixedpoint.java.
209 return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
◆ getRules()
Retrieve set of rules added to fixedpoint context.
- Exceptions
-
Definition at line 283 of file Fixedpoint.java.
285 ASTVector v =
new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
286 return v.ToBoolExprArray();
◆ getStatistics()
Fixedpoint statistics.
- Exceptions
-
Definition at line 305 of file Fixedpoint.java.
307 return new Statistics(getContext(), Native.fixedpointGetStatistics(
308 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 316 of file Fixedpoint.java.
318 ASTVector av =
new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
319 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 327 of file Fixedpoint.java.
329 ASTVector av =
new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
330 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 175 of file Fixedpoint.java.
176 Native.fixedpointPop(getContext().nCtx(), getNativeObject());
◆ push()
Creates a backtracking point.
- See also
- pop
Definition at line 164 of file Fixedpoint.java.
165 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 121 of file Fixedpoint.java.
122 getContext().checkContextMatch(
query);
124 getNativeObject(),
query.getNativeObject()));
128 return Status.SATISFIABLE;
130 return Status.UNSATISFIABLE;
132 return Status.UNKNOWN;
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 144 of file Fixedpoint.java.
145 getContext().checkContextMatch(relations);
147 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
148 .arrayToNative(relations)));
152 return Status.SATISFIABLE;
154 return Status.UNSATISFIABLE;
156 return Status.UNKNOWN;
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 259 of file Fixedpoint.java.
262 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
263 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
264 Symbol.arrayToNative(kinds));
◆ toString() [1/2]
Retrieve internal string representation of fixedpoint object.
Definition at line 249 of file Fixedpoint.java.
251 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 271 of file Fixedpoint.java.
274 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
275 AST.arrayLength(queries), AST.arrayToNative(queries));
◆ updateRule()
Update named rule into in the fixedpoint solver.
- Parameters
-
rule | implication (Horn clause) representing rule |
name | Nullable rule name. |
- Exceptions
-
Definition at line 186 of file Fixedpoint.java.
187 getContext().checkContextMatch(rule);
188 Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
189 rule.getNativeObject(), AST.getNativeObject(name));