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  }

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

◆ 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 267 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 36 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 60 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 47 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 254 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 280 of file Fixedpoint.cs.

280  {
281  get
282  {
283 
284  return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
285  }
286  }
Microsoft.Z3.Fixedpoint.Assert
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
Definition: Fixedpoint.cs:68
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:101
Microsoft.Z3.Fixedpoint.Statistics
Statistics Statistics
Fixedpoint statistics.
Definition: Fixedpoint.cs:280
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:28