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)
 

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 }

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

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

Referenced by Fixedpoint.query().

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