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 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)
 

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()

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

221  {
222  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
223  predicate.getNativeObject(), property.getNativeObject());
224  }

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

276  {
277  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
278  return v.ToBoolExprArray();
279  }

◆ getCoverDelta()

Expr getCoverDelta ( int  level,
FuncDecl  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  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 264 of file Fixedpoint.java.

265  {
266  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
267  return v.ToBoolExprArray();
268  }

◆ getStatistics()

Statistics getStatistics ( )
inline

Fixedpoint statistics.

Exceptions
Z3Exception

Definition at line 286 of file Fixedpoint.java.

287  {
288  return new Statistics(getContext(), Native.fixedpointGetStatistics(
289  getContext().nCtx(), getNativeObject()));
290  }

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

298  {
299  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
300  return av.ToBoolExprArray();
301  }

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

309  {
310  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
311  return av.ToBoolExprArray();
312  }

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

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

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

241  {
242 
243  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
244  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
245  Symbol.arrayToNative(kinds));
246 
247  }

◆ 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 ( BoolExpr[]  queries)
inline

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

Definition at line 252 of file Fixedpoint.java.

253  {
254 
255  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
256  AST.arrayLength(queries), AST.arrayToNative(queries));
257  }

◆ 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 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
@ Z3_L_TRUE
Definition: z3_api.h:103
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:100
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:101
com.microsoft.z3.Fixedpoint.query
Status query(BoolExpr query)
Definition: Fixedpoint.java:121