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 ()
 
Statistics getStatistics ()
 
BoolExpr[] ParseFile (String file)
 
BoolExpr[] ParseString (String s)
 
- 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 245 of file Fixedpoint.java.

247  {
248  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
249  predicate.getNativeObject(), property.getNativeObject());
250  }
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 306 of file Fixedpoint.java.

307  {
308  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
309  return v.ToBoolExprArray();
310  }
Expr getCoverDelta ( int  level,
FuncDecl  predicate 
)
inline

Retrieve the cover of a predicate.

Exceptions
Z3Exception

Definition at line 234 of file Fixedpoint.java.

235  {
236  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
237  getNativeObject(), level, predicate.getNativeObject());
238  return (res == 0) ? null : Expr.create(getContext(), res);
239  }
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 223 of file Fixedpoint.java.

224  {
225  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
226  predicate.getNativeObject());
227  }
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  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
217  getNativeObject());
218  }
BoolExpr [] getRules ( )
inline

Retrieve set of rules added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 295 of file Fixedpoint.java.

296  {
297  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
298  return v.ToBoolExprArray();
299  }
Statistics getStatistics ( )
inline

Fixedpoint statistics.

Exceptions
Z3Exception

Definition at line 317 of file Fixedpoint.java.

318  {
319  return new Statistics(getContext(), Native.fixedpointGetStatistics(
320  getContext().nCtx(), getNativeObject()));
321  }
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 328 of file Fixedpoint.java.

329  {
330  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
331  return av.ToBoolExprArray();
332  }
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 339 of file Fixedpoint.java.

340  {
341  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
342  return av.ToBoolExprArray();
343  }
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:143
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:143
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 271 of file Fixedpoint.java.

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

Retrieve internal string representation of fixedpoint object.

Definition at line 255 of file Fixedpoint.java.

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

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

Definition at line 283 of file Fixedpoint.java.

284  {
285 
286  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
287  AST.arrayLength(queries), AST.arrayToNative(queries));
288  }
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  }