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 (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 Push ()
 Creates a backtracking point. More...
 
void Pop ()
 Backtrack one backtracking point. 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 (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

void Add ( params BoolExpr[]  constraints)
inline

Alias for Assert.

Definition at line 84 of file Fixedpoint.cs.

85  {
86  Assert(constraints);
87  }
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
Definition: Fixedpoint.cs:69
void AddCover ( int  level,
FuncDecl  predicate,
Expr  property 
)
inline

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

Definition at line 237 of file Fixedpoint.cs.

238  {
239  Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
240  }
void AddFact ( FuncDecl  pred,
params uint[]  args 
)
inline

Add table fact to the fixedpoint solver.

Definition at line 114 of file Fixedpoint.cs.

115  {
116  Contract.Requires(pred != null);
117  Contract.Requires(args != null);
118 
119  Context.CheckContextMatch(pred);
120  Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args);
121  }
void AddRule ( BoolExpr  rule,
Symbol  name = null 
)
inline

Add rule into the fixedpoint solver.

Definition at line 103 of file Fixedpoint.cs.

104  {
105  Contract.Requires(rule != null);
106 
107  Context.CheckContextMatch(rule);
108  Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
109  }
void Assert ( params BoolExpr[]  constraints)
inline

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

Definition at line 69 of file Fixedpoint.cs.

70  {
71  Contract.Requires(constraints != null);
72  Contract.Requires(Contract.ForAll(constraints, c => c != null));
73 
74  Context.CheckContextMatch(constraints);
75  foreach (BoolExpr a in constraints)
76  {
77  Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject);
78  }
79  }
Expr GetAnswer ( )
inline

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

Definition at line 200 of file Fixedpoint.cs.

201  {
202  IntPtr ans = Native.Z3_fixedpoint_get_answer(Context.nCtx, NativeObject);
203  return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
204  }
Expr GetCoverDelta ( int  level,
FuncDecl  predicate 
)
inline

Retrieve the cover of a predicate.

Definition at line 227 of file Fixedpoint.cs.

228  {
229  IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject);
230  return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
231  }
uint GetNumLevels ( FuncDecl  predicate)
inline

Retrieve the number of levels explored for a given predicate.

Definition at line 219 of file Fixedpoint.cs.

220  {
221  return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
222  }
string GetReasonUnknown ( )
inline

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 209 of file Fixedpoint.cs.

210  {
211  Contract.Ensures(Contract.Result<string>() != null);
212 
213  return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject);
214  }
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 318 of file Fixedpoint.cs.

319  {
320  ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
321  return av.ToBoolExprArray();
322  }
BoolExpr [] ParseString ( string  s)
inline

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

Definition at line 327 of file Fixedpoint.cs.

328  {
329  ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
330  return av.ToBoolExprArray();
331  }
void Pop ( )
inline

Backtrack one backtracking point.

Note that an exception is thrown if Pop is called without a corresponding Push

See also
Push

Definition at line 179 of file Fixedpoint.cs.

180  {
181  Native.Z3_fixedpoint_pop(Context.nCtx, NativeObject);
182  }
void Push ( )
inline

Creates a backtracking point.

See also
Pop

Definition at line 169 of file Fixedpoint.cs.

170  {
171  Native.Z3_fixedpoint_push(Context.nCtx, NativeObject);
172  }
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 129 of file Fixedpoint.cs.

130  {
131  Contract.Requires(query != null);
132 
133  Context.CheckContextMatch(query);
134  Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject);
135  switch (r)
136  {
137  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
138  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
139  default: return Status.UNKNOWN;
140  }
141  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
Status
Status values.
Definition: Status.cs:27
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
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.

Definition at line 149 of file Fixedpoint.cs.

150  {
151  Contract.Requires(relations != null);
152  Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
153 
154  Context.CheckContextMatch(relations);
155  Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
156  AST.ArrayLength(relations), AST.ArrayToNative(relations));
157  switch (r)
158  {
159  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
160  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
161  default: return Status.UNKNOWN;
162  }
163  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
Status
Status values.
Definition: Status.cs:27
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
void RegisterRelation ( FuncDecl  f)
inline

Register predicate as recursive relation.

Definition at line 92 of file Fixedpoint.cs.

93  {
94  Contract.Requires(f != null);
95 
96  Context.CheckContextMatch(f);
97  Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject);
98  }
void SetPredicateRepresentation ( FuncDecl  f,
Symbol[]  kinds 
)
inline

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

Definition at line 253 of file Fixedpoint.cs.

254  {
255  Contract.Requires(f != null);
256 
257  Native.Z3_fixedpoint_set_predicate_representation(Context.nCtx, NativeObject,
258  f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
259 
260  }
override string ToString ( )
inline

Retrieve internal string representation of fixedpoint object.

Definition at line 245 of file Fixedpoint.cs.

246  {
247  return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 0, null);
248  }
string ToString ( BoolExpr[]  queries)
inline

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

Definition at line 265 of file Fixedpoint.cs.

266  {
267 
268  return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
269  AST.ArrayLength(queries), AST.ArrayToNative(queries));
270  }
void UpdateRule ( BoolExpr  rule,
Symbol  name 
)
inline

Update named rule into in the fixedpoint solver.

Definition at line 188 of file Fixedpoint.cs.

189  {
190  Contract.Requires(rule != null);
191 
192  Context.CheckContextMatch(rule);
193  Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
194  }

Property Documentation

BoolExpr [] Assertions
get

Retrieve set of assertions added to fixedpoint context.

Definition at line 290 of file Fixedpoint.cs.

string Help
get

A string that describes all available fixedpoint solver parameters.

Definition at line 36 of file Fixedpoint.cs.

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Fixedpoint solver.

Definition at line 61 of file Fixedpoint.cs.

Params Parameters
set

Sets the fixedpoint solver parameters.

Definition at line 48 of file Fixedpoint.cs.

BoolExpr [] Rules
get

Retrieve set of rules added to fixedpoint context.

Definition at line 276 of file Fixedpoint.cs.

Fixedpoint statistics.

Definition at line 304 of file Fixedpoint.cs.