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 }

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

◆ 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 }
Status query(Expr< BoolSort > query)
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
@ Z3_L_TRUE
Definition: z3_api.h:105
@ Z3_L_FALSE
Definition: z3_api.h:103

Referenced by Fixedpoint.query().

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