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  }

◆ 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
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 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  }

◆ 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
ruleimplication (Horn clause) representing rule
nameNullable 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  }
Z3_L_TRUE
Definition: z3_api.h:105
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:101
com.microsoft.z3.Fixedpoint.query
Status query(Expr< BoolSort > query)
Definition: Fixedpoint.java:121
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:28
Z3_L_FALSE
Definition: z3_api.h:103