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 }
Microsoft.Z3.Fixedpoint.Assert
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 }
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:29
Z3_lbool
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

Statistics Statistics
| get

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 }
Microsoft.Z3.Fixedpoint.Statistics
Statistics Statistics
Fixedpoint statistics.
Definition: Fixedpoint.cs:280