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)
 

Detailed Description

Object for managing fixedpoints

Definition at line 25 of file Fixedpoint.java.

Member Function Documentation

§ add()

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  }

§ 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.

240  {
241  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
242  predicate.getNativeObject(), property.getNativeObject());
243  }

§ addFact()

void addFact ( FuncDecl  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 ( BoolExpr  rule,
Symbol  name 
)
inline

Add rule into the fixedpoint solver.

Parameters
ruleimplication (Horn clause) representing rule
nameNullable 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 198 of file Fixedpoint.java.

199  {
200  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
201  return (ans == 0) ? null : Expr.create(getContext(), ans);
202  }

§ getAssertions()

BoolExpr [] getAssertions ( )
inline

Retrieve set of assertions added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 294 of file Fixedpoint.java.

295  {
296  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
297  return v.ToBoolExprArray();
298  }

§ getCoverDelta()

Expr getCoverDelta ( int  level,
FuncDecl  predicate 
)
inline

Retrieve the cover of a predicate.

Exceptions
Z3Exception

Definition at line 227 of file Fixedpoint.java.

228  {
229  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
230  getNativeObject(), level, predicate.getNativeObject());
231  return (res == 0) ? null : Expr.create(getContext(), res);
232  }

§ 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  predicate)
inline

Retrieve the number of levels explored for a given predicate.

Definition at line 216 of file Fixedpoint.java.

217  {
218  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
219  predicate.getNativeObject());
220  }

§ 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 207 of file Fixedpoint.java.

208  {
209  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
210  getNativeObject());
211  }

§ getRules()

BoolExpr [] getRules ( )
inline

Retrieve set of rules added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 283 of file Fixedpoint.java.

284  {
285  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
286  return v.ToBoolExprArray();
287  }

§ getStatistics()

Statistics getStatistics ( )
inline

Fixedpoint statistics.

Exceptions
Z3Exception

Definition at line 305 of file Fixedpoint.java.

306  {
307  return new Statistics(getContext(), Native.fixedpointGetStatistics(
308  getContext().nCtx(), getNativeObject()));
309  }

§ 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 316 of file Fixedpoint.java.

317  {
318  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
319  return av.ToBoolExprArray();
320  }

§ 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 327 of file Fixedpoint.java.

328  {
329  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
330  return av.ToBoolExprArray();
331  }

§ pop()

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 175 of file Fixedpoint.java.

175  {
176  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
177  }

§ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 164 of file Fixedpoint.java.

164  {
165  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
166  }

§ query() [1/2]

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 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  }
Status query(BoolExpr query)
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:98

§ query() [2/2]

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 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  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:98

§ registerRelation()

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  }

§ 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  f,
Symbol []  kinds 
)
inline

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

Definition at line 259 of file Fixedpoint.java.

260  {
261 
262  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
263  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
264  Symbol.arrayToNative(kinds));
265 
266  }

§ toString() [1/2]

String toString ( )
inline

Retrieve internal string representation of fixedpoint object.

Definition at line 249 of file Fixedpoint.java.

250  {
251  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
252  0, null);
253  }

§ toString() [2/2]

String toString ( BoolExpr []  queries)
inline

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

Definition at line 271 of file Fixedpoint.java.

272  {
273 
274  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
275  AST.arrayLength(queries), AST.arrayToNative(queries));
276  }

§ updateRule()

void updateRule ( BoolExpr  rule,
Symbol  name 
)
inline

Update named rule into in the fixedpoint solver.

Parameters
ruleimplication (Horn clause) representing rule
nameNullable rule name.
Exceptions
Z3Exception

Definition at line 186 of file Fixedpoint.java.

186  {
187  getContext().checkContextMatch(rule);
188  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
189  rule.getNativeObject(), AST.getNativeObject(name));
190  }