Z3
Data Structures | Public Member Functions | Properties
Fixedpoint Class Reference

Object for managing fixedpoints More...

+ Inheritance diagram for Fixedpoint:

Data Structures

class  DecRefQueue
 

Public Member Functions

void Assert (params BoolExpr[] constraints)
 Assert a constraint (or multiple) into the fixedpoint solver. More...
 
void Add (params BoolExpr[] constraints)
 Alias for Assert. More...
 
void RegisterRelation (FuncDecl f)
 Register predicate as recursive relation. More...
 
void AddRule (BoolExpr rule, Symbol name=null)
 Add rule into the fixedpoint solver. More...
 
void AddFact (FuncDecl pred, params uint[] args)
 Add table fact to the fixedpoint solver. More...
 
Status Query (BoolExpr query)
 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. More...
 
Status Query (params FuncDecl[] relations)
 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. More...
 
void UpdateRule (BoolExpr rule, Symbol name)
 Update named rule into in the fixedpoint solver. More...
 
Expr GetAnswer ()
 Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability. More...
 
string GetReasonUnknown ()
 Retrieve explanation why fixedpoint engine returned status Unknown. More...
 
uint GetNumLevels (FuncDecl predicate)
 Retrieve the number of levels explored for a given predicate. More...
 
Expr GetCoverDelta (int level, FuncDecl predicate)
 Retrieve the cover of a predicate. More...
 
void AddCover (int level, FuncDecl predicate, Expr property)
 Add property about the predicate. The property is added at level. More...
 
override string ToString ()
 Retrieve internal string representation of fixedpoint object. More...
 
void SetPredicateRepresentation (FuncDecl f, Symbol[] kinds)
 Instrument the Datalog engine on which table representation to use for recursive predicate. More...
 
string ToString (params BoolExpr[] queries)
 Convert benchmark given as set of axioms, rules and queries to a string. More...
 
BoolExpr[] ParseFile (string file)
 Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file. More...
 
BoolExpr[] ParseString (string s)
 Similar to ParseFile. Instead it takes as argument a string. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

string Help [get]
 A string that describes all available fixedpoint solver parameters. More...
 
Params Parameters [set]
 Sets the fixedpoint solver parameters. More...
 
ParamDescrs ParameterDescriptions [get]
 Retrieves parameter descriptions for Fixedpoint solver. More...
 
BoolExpr[] Rules [get]
 Retrieve set of rules added to fixedpoint context. More...
 
BoolExpr[] Assertions [get]
 Retrieve set of assertions added to fixedpoint context. More...
 
Statistics Statistics [get]
 Fixedpoint statistics. More...
 

Detailed Description

Object for managing fixedpoints

Definition at line 29 of file Fixedpoint.cs.

Member Function Documentation

◆ Add()

void Add ( params BoolExpr[]  constraints)
inline

Alias for Assert.


Definition at line 83 of file Fixedpoint.cs.

84 {
85 Assert(constraints);
86 }
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
Definition: Fixedpoint.cs:68

◆ AddCover()

void AddCover ( int  level,
FuncDecl  predicate,
Expr  property 
)
inline

Add property about the predicate. The property is added at level.


Definition at line 215 of file Fixedpoint.cs.

216 {
217 Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
218 }

◆ AddFact()

void AddFact ( FuncDecl  pred,
params uint[]  args 
)
inline

Add table fact to the fixedpoint solver.


Definition at line 113 of file Fixedpoint.cs.

114 {
115 Debug.Assert(pred != null);
116 Debug.Assert(args != null);
117
118 Context.CheckContextMatch(pred);
119 Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args);
120 }

◆ AddRule()

void AddRule ( BoolExpr  rule,
Symbol  name = null 
)
inline

Add rule into the fixedpoint solver.


Definition at line 102 of file Fixedpoint.cs.

103 {
104 Debug.Assert(rule != null);
105
106 Context.CheckContextMatch(rule);
107 Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
108 }

◆ Assert()

void Assert ( params BoolExpr[]  constraints)
inline

Assert a constraint (or multiple) into the fixedpoint solver.


Definition at line 68 of file Fixedpoint.cs.

69 {
70 Debug.Assert(constraints != null);
71 Debug.Assert(constraints.All(c => c != null));
72
73 Context.CheckContextMatch<BoolExpr>(constraints);
74 foreach (BoolExpr a in constraints)
75 {
76 Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject);
77 }
78 }

Referenced by Fixedpoint.Add().

◆ GetAnswer()

Expr GetAnswer ( )
inline

Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.


Definition at line 179 of file Fixedpoint.cs.

180 {
181 IntPtr ans = Native.Z3_fixedpoint_get_answer(Context.nCtx, NativeObject);
182 return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
183 }

◆ GetCoverDelta()

Expr GetCoverDelta ( int  level,
FuncDecl  predicate 
)
inline

Retrieve the cover of a predicate.


Definition at line 205 of file Fixedpoint.cs.

206 {
207 IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject);
208 return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
209 }

◆ GetNumLevels()

uint GetNumLevels ( FuncDecl  predicate)
inline

Retrieve the number of levels explored for a given predicate.


Definition at line 197 of file Fixedpoint.cs.

198 {
199 return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
200 }

◆ GetReasonUnknown()

string GetReasonUnknown ( )
inline

Retrieve explanation why fixedpoint engine returned status Unknown.


Definition at line 188 of file Fixedpoint.cs.

189 {
190
191 return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject);
192 }

◆ 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 293 of file Fixedpoint.cs.

294 {
295 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
296 return av.ToBoolExprArray();
297 }

◆ ParseString()

BoolExpr[] ParseString ( string  s)
inline

Similar to ParseFile. Instead it takes as argument a string.

Definition at line 302 of file Fixedpoint.cs.

303 {
304 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
305 return av.ToBoolExprArray();
306 }

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


Definition at line 128 of file Fixedpoint.cs.

129 {
130 Debug.Assert(query != null);
131
132 Context.CheckContextMatch(query);
133 Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject);
134 switch (r)
135 {
136 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
137 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
138 default: return Status.UNKNOWN;
139 }
140 }
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

◆ Query() [2/2]

Status Query ( params 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.


Definition at line 148 of file Fixedpoint.cs.

149 {
150 Debug.Assert(relations != null);
151 Debug.Assert(relations.All(rel => rel != null));
152
153 Context.CheckContextMatch<FuncDecl>(relations);
154 Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
155 AST.ArrayLength(relations), AST.ArrayToNative(relations));
156 switch (r)
157 {
158 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
159 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
160 default: return Status.UNKNOWN;
161 }
162 }

◆ RegisterRelation()

void RegisterRelation ( FuncDecl  f)
inline

Register predicate as recursive relation.


Definition at line 91 of file Fixedpoint.cs.

92 {
93 Debug.Assert(f != null);
94
95 Context.CheckContextMatch(f);
96 Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject);
97 }

◆ SetPredicateRepresentation()

void SetPredicateRepresentation ( FuncDecl  f,
Symbol[]  kinds 
)
inline

Instrument the Datalog engine on which table representation to use for recursive predicate.


Definition at line 231 of file Fixedpoint.cs.

232 {
233 Debug.Assert(f != null);
234
235 Native.Z3_fixedpoint_set_predicate_representation(Context.nCtx, NativeObject,
236 f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
237
238 }

◆ ToString() [1/2]

override string ToString ( )
inline

Retrieve internal string representation of fixedpoint object.


Definition at line 223 of file Fixedpoint.cs.

224 {
225 return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 0, null);
226 }

◆ ToString() [2/2]

string ToString ( params BoolExpr[]  queries)
inline

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


Definition at line 243 of file Fixedpoint.cs.

244 {
245
246 return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
247 AST.ArrayLength(queries), AST.ArrayToNative(queries));
248 }

◆ UpdateRule()

void UpdateRule ( BoolExpr  rule,
Symbol  name 
)
inline

Update named rule into in the fixedpoint solver.


Definition at line 167 of file Fixedpoint.cs.

168 {
169 Debug.Assert(rule != null);
170
171 Context.CheckContextMatch(rule);
172 Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
173 }

Property Documentation

◆ Assertions

BoolExpr [] Assertions
get

Retrieve set of assertions added to fixedpoint context.


Definition at line 266 of file Fixedpoint.cs.

267 {
268 get
269 {
270
271 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
272 return av.ToBoolExprArray();
273 }
274 }

◆ Help

string Help
get

A string that describes all available fixedpoint solver parameters.

Definition at line 35 of file Fixedpoint.cs.

36 {
37 get
38 {
39 return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject);
40 }
41 }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Fixedpoint solver.

Definition at line 59 of file Fixedpoint.cs.

60 {
61 get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); }
62 }

◆ Parameters

Params Parameters
set

Sets the fixedpoint solver parameters.

Definition at line 46 of file Fixedpoint.cs.

47 {
48 set
49 {
50 Debug.Assert(value != null);
51 Context.CheckContextMatch(value);
52 Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject);
53 }
54 }

◆ Rules

BoolExpr [] Rules
get

Retrieve set of rules added to fixedpoint context.


Definition at line 253 of file Fixedpoint.cs.

254 {
255 get
256 {
257
258 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
259 return av.ToBoolExprArray();
260 }
261 }

◆ Statistics

Fixedpoint statistics.

Definition at line 279 of file Fixedpoint.cs.

280 {
281 get
282 {
283
284 return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
285 }
286 }
Statistics Statistics
Fixedpoint statistics.
Definition: Fixedpoint.cs:280