Z3 |

Public Member Functions
Fixedpoint Class Reference
Inheritance diagram for Fixedpoint:

## 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)

## Detailed Description

Object for managing fixedpoints

Definition at line 25 of file Fixedpoint.java.

## Member Function Documentation

## ◆ add()

final void add | ( | Expr< BoolSort >... | constraints | ) |
| inline

Assert a constraint (or multiple) into the fixedpoint solver.

Exceptions

  Z3Exception |

Definition at line 66 of file Fixedpoint.java.

67 {
68 getContext().checkContextMatch(constraints);
69 for (Expr<BoolSort> a : constraints)
70 {
71 Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
72 a.getNativeObject());
73 }
74 }

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

## ◆ addCover()

void addCover | ( | int | level,
|  | FuncDecl< BoolSort > | predicate,
|  | Expr<?> | property
| ) |  |
| inline

Add `property` about the `predicate`. The property is added at `level`.

Definition at line 219 of file Fixedpoint.java.

221 {
222 Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
223 predicate.getNativeObject(), property.getNativeObject());
224 }

## ◆ addFact()

void addFact | ( | FuncDecl< BoolSort > | pred,
|  | int ... | args
| ) |  |
| inline

Add table fact to the fixedpoint solver.

Exceptions

  Z3Exception |

Definition at line 106 of file Fixedpoint.java.

106 {
107 getContext().checkContextMatch(pred);
108 Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
109 pred.getNativeObject(), args.length, args);
110 }

## ◆ addRule()

void addRule | ( | Expr< BoolSort > | rule,
|  | Symbol | name
| ) |  |
| inline

Add rule into the fixedpoint solver.

Parameters

  rule | implication (Horn clause) representing rule
  name | Nullable rule name.

Exceptions

  Z3Exception |

Definition at line 95 of file Fixedpoint.java.

95 {
96 getContext().checkContextMatch(rule);
97 Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
98 rule.getNativeObject(), AST.getNativeObject(name));
99 }

## ◆ getAnswer()

Expr<?> getAnswer | ( |  | ) |
| inline

Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.

Exceptions

  Z3Exception |

Definition at line 179 of file Fixedpoint.java.

180 {
181 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
182 return (ans == 0) ? null : Expr.create(getContext(), ans);
183 }

## ◆ getAssertions()

BoolExpr[] getAssertions | ( |  | ) |
| inline

Retrieve set of assertions added to fixedpoint context.

Exceptions

  Z3Exception |

Definition at line 273 of file Fixedpoint.java.

274 {
275 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
276 return v.ToBoolExprArray();
277 }

## ◆ getCoverDelta()

Expr<?> getCoverDelta | ( | int | level,
|  | FuncDecl< BoolSort > | predicate
| ) |  |
| inline

Retrieve the cover of a predicate.

Exceptions

  Z3Exception |

Definition at line 208 of file Fixedpoint.java.

209 {
210 long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
211 getNativeObject(), level, predicate.getNativeObject());
212 return (res == 0) ? null : Expr.create(getContext(), res);
213 }

## ◆ getHelp()

String getHelp | ( |  | ) |
| inline

A string that describes all available fixedpoint solver parameters.

Definition at line 31 of file Fixedpoint.java.

32 {
33 return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
34 }

## ◆ getNumLevels()

int getNumLevels | ( | FuncDecl< BoolSort > | predicate | ) |
| inline

Retrieve the number of levels explored for a given predicate.

Definition at line 197 of file Fixedpoint.java.

198 {
199 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
200 predicate.getNativeObject());
201 }

## ◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions | ( |  | ) |
| inline

Retrieves parameter descriptions for Fixedpoint solver.

Exceptions

  Z3Exception |

Definition at line 54 of file Fixedpoint.java.

55 {
56 return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
58 }

## ◆ getReasonUnknown()

String getReasonUnknown | ( |  | ) |
| inline

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 188 of file Fixedpoint.java.

189 {
190 return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
191 getNativeObject());
192 }

## ◆ getRules()

BoolExpr[] getRules | ( |  | ) |
| inline

Retrieve set of rules added to fixedpoint context.

Exceptions

  Z3Exception |

Definition at line 262 of file Fixedpoint.java.

263 {
264 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
265 return v.ToBoolExprArray();
266 }

## ◆ getStatistics()

Statistics getStatistics | ( |  | ) |
| inline

Fixedpoint statistics.

Exceptions

  Z3Exception |

Definition at line 284 of file Fixedpoint.java.

285 {
286 return new Statistics(getContext(), Native.fixedpointGetStatistics(
287 getContext().nCtx(), getNativeObject()));
288 }

## ◆ ParseFile()

BoolExpr[] ParseFile | ( | String | file | ) |
| 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.

296 {
297 ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
298 return av.ToBoolExprArray();
299 }

## ◆ ParseString()

BoolExpr[] ParseString | ( | String | s | ) |
| 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.

307 {
308 ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
309 return av.ToBoolExprArray();
310 }

## ◆ query() [1/2]

Status query | ( | Expr< BoolSort > | query | ) |
| 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.

Exceptions

  Z3Exception |

Definition at line 121 of file Fixedpoint.java.

121 {
122 getContext().checkContextMatch(query);
123 Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
124 getNativeObject(), query.getNativeObject()));
125 switch (r)
126 {
127 case Z3_L_TRUE:
128 return Status.SATISFIABLE;
129 case Z3_L_FALSE:
130 return Status.UNSATISFIABLE;
131 default:
132 return Status.UNKNOWN;
133 }
134 }
com.microsoft.z3.Fixedpoint.query
Status query(Expr< BoolSort > query)
Definition: Fixedpoint.java:121
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:105
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:103

Referenced by Fixedpoint.query().

## ◆ query() [2/2]

Status query | ( | FuncDecl< BoolSort >[] | relations | ) |
| 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.

Exceptions

  Z3Exception |

Definition at line 144 of file Fixedpoint.java.

144 {
145 getContext().checkContextMatch(relations);
146 Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
147 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
148 .arrayToNative(relations)));
149 switch (r)
150 {
151 case Z3_L_TRUE:
152 return Status.SATISFIABLE;
153 case Z3_L_FALSE:
154 return Status.UNSATISFIABLE;
155 default:
156 return Status.UNKNOWN;
157 }
158 }

## ◆ registerRelation()

void registerRelation | ( | FuncDecl< BoolSort > | f | ) |
| inline

Register predicate as recursive relation.

Exceptions

  Z3Exception |

Definition at line 81 of file Fixedpoint.java.

82 {
83 getContext().checkContextMatch(f);
84 Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
85 f.getNativeObject());
86 }

## ◆ setParameters()

void setParameters | ( | Params | value | ) |
| inline

Sets the fixedpoint solver parameters.

Exceptions

  Z3Exception |

Definition at line 41 of file Fixedpoint.java.

42 {
43
44 getContext().checkContextMatch(value);
45 Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
47 }

## ◆ setPredicateRepresentation()

void setPredicateRepresentation | ( | FuncDecl< BoolSort > | f,
|  | Symbol[] | kinds
| ) |  |
| inline

Instrument the Datalog engine on which table representation to use for recursive predicate.

Definition at line 240 of file Fixedpoint.java.

241 {
242 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
243 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
244 Symbol.arrayToNative(kinds));
245
246 }

## ◆ toString() [1/2]

String toString | ( |  | ) |
| inline

Retrieve internal string representation of fixedpoint object.

Definition at line 230 of file Fixedpoint.java.

231 {
232 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
233 0, null);
234 }

## ◆ toString() [2/2]

String toString | ( | Expr< BoolSort >[] | queries | ) |
| inline

Convert benchmark given as set of axioms, rules and queries to a string.

Definition at line 251 of file Fixedpoint.java.

252 {
253 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
254 AST.arrayLength(queries), AST.arrayToNative(queries));
255 }

## ◆ updateRule()

void updateRule | ( | Expr< BoolSort > | rule,
|  | Symbol | name
| ) |  |
| inline

Update named rule into in the fixedpoint solver.

Parameters

  rule | implication (Horn clause) representing rule
  name | Nullable rule name.

Exceptions

  Z3Exception |

Definition at line 167 of file Fixedpoint.java.

167 {
168 getContext().checkContextMatch(rule);
169 Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
170 rule.getNativeObject(), AST.getNativeObject(name));
171 }