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.

Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().

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

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

§ addFact()

void addFact ( FuncDecl  pred,
int ...  args 
)
inline

Add table fact to the fixedpoint solver.

Exceptions
Z3Exception

Definition at line 105 of file Fixedpoint.java.

105  {
106  getContext().checkContextMatch(pred);
107  Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
108  pred.getNativeObject(), args.length, args);
109  }

§ addRule()

void addRule ( BoolExpr  rule,
Symbol  name 
)
inline

Add rule into the fixedpoint solver.

Parameters
nameNullable rule name.
Exceptions
Z3Exception

Definition at line 94 of file Fixedpoint.java.

94  {
95  getContext().checkContextMatch(rule);
96  Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
97  rule.getNativeObject(), AST.getNativeObject(name));
98  }

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

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

§ getAssertions()

BoolExpr [] getAssertions ( )
inline

Retrieve set of assertions added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 292 of file Fixedpoint.java.

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

§ getCoverDelta()

Expr getCoverDelta ( int  level,
FuncDecl  predicate 
)
inline

Retrieve the cover of a predicate.

Exceptions
Z3Exception

Definition at line 225 of file Fixedpoint.java.

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

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

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

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

206  {
207  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
208  getNativeObject());
209  }

§ getRules()

BoolExpr [] getRules ( )
inline

Retrieve set of rules added to fixedpoint context.

Exceptions
Z3Exception

Definition at line 281 of file Fixedpoint.java.

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

§ getStatistics()

Statistics getStatistics ( )
inline

Fixedpoint statistics.

Exceptions
Z3Exception

Definition at line 303 of file Fixedpoint.java.

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

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

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

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

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

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

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

§ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 163 of file Fixedpoint.java.

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

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

120  {
121  getContext().checkContextMatch(query);
122  Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
123  getNativeObject(), query.getNativeObject()));
124  switch (r)
125  {
126  case Z3_L_TRUE:
127  return Status.SATISFIABLE;
128  case Z3_L_FALSE:
129  return Status.UNSATISFIABLE;
130  default:
131  return Status.UNKNOWN;
132  }
133  }
Status query(BoolExpr query)
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
Status
Status values.
Definition: Status.cs:27

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

143  {
144  getContext().checkContextMatch(relations);
145  Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
146  .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
147  .arrayToNative(relations)));
148  switch (r)
149  {
150  case Z3_L_TRUE:
151  return Status.SATISFIABLE;
152  case Z3_L_FALSE:
153  return Status.UNSATISFIABLE;
154  default:
155  return Status.UNKNOWN;
156  }
157  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
Status
Status values.
Definition: Status.cs:27

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

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

§ toString() [1/2]

String toString ( )
inline

Retrieve internal string representation of fixedpoint object.

Definition at line 247 of file Fixedpoint.java.

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

§ toString() [2/2]

String toString ( BoolExpr []  queries)
inline

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

Definition at line 269 of file Fixedpoint.java.

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

§ updateRule()

void updateRule ( BoolExpr  rule,
Symbol  name 
)
inline

Update named rule into in the fixedpoint solver.

Parameters
nameNullable rule name.
Exceptions
Z3Exception

Definition at line 184 of file Fixedpoint.java.

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