Z3
Public Member Functions
Fixedpoint Class Reference
+ Inheritance diagram for Fixedpoint:

Public Member Functions

String getHelp ()
 
void setParameters (Params value)
 
ParamDescrs getParameterDescriptions ()
 
void add (BoolExpr...constraints)
 
void registerRelation (FuncDecl f)
 
void addRule (BoolExpr rule, Symbol name)
 
void addFact (FuncDecl pred, int...args)
 
Status query (BoolExpr query)
 
Status query (FuncDecl[] relations)
 
void push ()
 
void pop ()
 
void updateRule (BoolExpr rule, Symbol name)
 
Expr getAnswer ()
 
String getReasonUnknown ()
 
int getNumLevels (FuncDecl predicate)
 
Expr getCoverDelta (int level, FuncDecl predicate)
 
void addCover (int level, FuncDecl predicate, Expr property)
 
String toString ()
 
void setPredicateRepresentation (FuncDecl f, Symbol[] kinds)
 
String toString (BoolExpr[] queries)
 
BoolExpr[] getRules ()
 
BoolExpr[] getAssertions ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Object for managing fixedpoints

Definition at line 25 of file Fixedpoint.java.

Member Function Documentation

void add ( BoolExpr...  constraints)
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 
)
inline

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

Definition at line 246 of file Fixedpoint.java.

248  {
249  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
250  predicate.getNativeObject(), property.getNativeObject());
251  }
void addFact ( FuncDecl  pred,
int...  args 
)
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 
)
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 ( )
inline

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

Exceptions
Z3Exception

Definition at line 205 of file Fixedpoint.java.

206  {
207  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
208  return (ans == 0) ? null : Expr.create(getContext(), ans);
209  }
BoolExpr [] getAssertions ( )
inline

Retrieve set of assertions added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 313 of file Fixedpoint.java.

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

Retrieve the cover of a predicate.

Exceptions
Z3Exception

Definition at line 235 of file Fixedpoint.java.

236  {
237  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
238  getNativeObject(), level, predicate.getNativeObject());
239  return (res == 0) ? null : Expr.create(getContext(), res);
240  }
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  }
int getNumLevels ( FuncDecl  predicate)
inline

Retrieve the number of levels explored for a given predicate.

Definition at line 224 of file Fixedpoint.java.

225  {
226  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
227  predicate.getNativeObject());
228  }
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  }
String getReasonUnknown ( )
inline

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 214 of file Fixedpoint.java.

215  {
216 
217  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
218  getNativeObject());
219  }
BoolExpr [] getRules ( )
inline

Retrieve set of rules added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 296 of file Fixedpoint.java.

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

Backtrack one backtracking point. Remarks: Note that an exception is thrown if

is called without a corresponding

See also
push

Definition at line 181 of file Fixedpoint.java.

182  {
183  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
184  }
void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 169 of file Fixedpoint.java.

170  {
171  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
172  }
Status query ( BoolExpr  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 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  }
Status query(BoolExpr query)
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
Status
Status values.
Definition: Status.cs:27
Status query ( FuncDecl[]  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 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)
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)
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 
)
inline

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

Definition at line 272 of file Fixedpoint.java.

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

Retrieve internal string representation of fixedpoint object.

Definition at line 256 of file Fixedpoint.java.

257  {
258  try
259  {
260  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
261  0, null);
262  } catch (Z3Exception e)
263  {
264  return "Z3Exception: " + e.getMessage();
265  }
266  }
String toString ( BoolExpr[]  queries)
inline

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

Definition at line 284 of file Fixedpoint.java.

285  {
286 
287  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
288  AST.arrayLength(queries), AST.arrayToNative(queries));
289  }
void updateRule ( BoolExpr  rule,
Symbol  name 
)
inline

Update named rule into in the fixedpoint solver.

Exceptions
Z3Exception

Definition at line 191 of file Fixedpoint.java.

192  {
193 
194  getContext().checkContextMatch(rule);
195  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
196  rule.getNativeObject(), AST.getNativeObject(name));
197  }