Z3
Public Member Functions
Fixedpoint Class Reference
+ 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
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

Object for managing fixedpoints

Definition at line 25 of file Fixedpoint.java.

Member Function Documentation

void add ( BoolExpr...  constraints) throws Z3Exception
inline

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

Exceptions
Z3Exception

Definition at line 65 of file Fixedpoint.java.

66  {
67  getContext().checkContextMatch(constraints);
68  for (BoolExpr a : constraints)
69  {
70  Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
71  a.getNativeObject());
72  }
73  }
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.

245  {
246  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
247  predicate.getNativeObject(), property.getNativeObject());
248  }
void addFact ( FuncDecl  pred,
int...  args 
) throws Z3Exception
inline

Add table fact to the fixedpoint solver.

Exceptions
Z3Exception

Definition at line 106 of file Fixedpoint.java.

107  {
108  getContext().checkContextMatch(pred);
109  Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
110  pred.getNativeObject(), (int) args.length, args);
111  }
void addRule ( BoolExpr  rule,
Symbol  name 
) throws Z3Exception
inline

Add rule into the fixedpoint solver.

Exceptions
Z3Exception

Definition at line 93 of file Fixedpoint.java.

94  {
95 
96  getContext().checkContextMatch(rule);
97  Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
98  rule.getNativeObject(), AST.getNativeObject(name));
99  }
Expr getAnswer ( ) throws Z3Exception
inline

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

Exceptions
Z3Exception

Definition at line 202 of file Fixedpoint.java.

203  {
204  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
205  return (ans == 0) ? null : Expr.create(getContext(), ans);
206  }
BoolExpr [] getAssertions ( ) throws Z3Exception
inline

Retrieve set of assertions added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 310 of file Fixedpoint.java.

311  {
312 
313  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
314  getContext().nCtx(), getNativeObject()));
315  int n = v.size();
316  BoolExpr[] res = new BoolExpr[n];
317  for (int i = 0; i < n; i++)
318  res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
319  return res;
320  }
Expr getCoverDelta ( int  level,
FuncDecl  predicate 
) throws Z3Exception
inline

Retrieve the cover of a predicate.

Exceptions
Z3Exception

Definition at line 232 of file Fixedpoint.java.

233  {
234  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
235  getNativeObject(), level, predicate.getNativeObject());
236  return (res == 0) ? null : Expr.create(getContext(), res);
237  }
String getHelp ( ) throws Z3Exception
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  }
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.

222  {
223  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
224  predicate.getNativeObject());
225  }
ParamDescrs getParameterDescriptions ( ) throws Z3Exception
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  }
String getReasonUnknown ( ) throws Z3Exception
inline

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 211 of file Fixedpoint.java.

212  {
213 
214  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
215  getNativeObject());
216  }
BoolExpr [] getRules ( ) throws Z3Exception
inline

Retrieve set of rules added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 293 of file Fixedpoint.java.

294  {
295 
296  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
297  getContext().nCtx(), getNativeObject()));
298  int n = v.size();
299  BoolExpr[] res = new BoolExpr[n];
300  for (int i = 0; i < n; i++)
301  res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
302  return res;
303  }
void pop ( ) throws Z3Exception
inline

Backtrack one backtracking point.

Note that an exception is thrown if Pop is called without a corresponding

Push
See also
Push

Definition at line 178 of file Fixedpoint.java.

179  {
180  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
181  }
void push ( ) throws Z3Exception
inline

Creates a backtracking point.

See also
Pop

Definition at line 168 of file Fixedpoint.java.

169  {
170  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
171  }
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.

Exceptions
Z3Exception

Definition at line 122 of file Fixedpoint.java.

123  {
124 
125  getContext().checkContextMatch(query);
126  Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
127  getNativeObject(), query.getNativeObject()));
128  switch (r)
129  {
130  case Z3_L_TRUE:
131  return Status.SATISFIABLE;
132  case Z3_L_FALSE:
133  return Status.UNSATISFIABLE;
134  default:
135  return Status.UNKNOWN;
136  }
137  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
Status
Status values.
Definition: Status.cs:27
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.

Exceptions
Z3Exception

Definition at line 147 of file Fixedpoint.java.

148  {
149 
150  getContext().checkContextMatch(relations);
151  Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
152  .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
153  .arrayToNative(relations)));
154  switch (r)
155  {
156  case Z3_L_TRUE:
157  return Status.SATISFIABLE;
158  case Z3_L_FALSE:
159  return Status.UNSATISFIABLE;
160  default:
161  return Status.UNKNOWN;
162  }
163  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
Status
Status values.
Definition: Status.cs:27
void registerRelation ( FuncDecl  f) throws Z3Exception
inline

Register predicate as recursive relation.

Exceptions
Z3Exception

Definition at line 80 of file Fixedpoint.java.

81  {
82 
83  getContext().checkContextMatch(f);
84  Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
85  f.getNativeObject());
86  }
void setParameters ( Params  value) throws Z3Exception
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  }
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.

270  {
271 
272  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
273  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
274  Symbol.arrayToNative(kinds));
275 
276  }
String toString ( )
inline

Retrieve internal string representation of fixedpoint object.

Definition at line 253 of file Fixedpoint.java.

254  {
255  try
256  {
257  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
258  0, null);
259  } catch (Z3Exception e)
260  {
261  return "Z3Exception: " + e.getMessage();
262  }
263  }
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.

282  {
283 
284  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
285  AST.arrayLength(queries), AST.arrayToNative(queries));
286  }
void updateRule ( BoolExpr  rule,
Symbol  name 
) throws Z3Exception
inline

Update named rule into in the fixedpoint solver.

Exceptions
Z3Exception

Definition at line 188 of file Fixedpoint.java.

189  {
190 
191  getContext().checkContextMatch(rule);
192  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
193  rule.getNativeObject(), AST.getNativeObject(name));
194  }