Z3
Fixedpoint.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Fixedpoints.cs
7
8Abstract:
9
10 Z3 Managed API: Fixedpoints
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Linq;
23
24namespace Microsoft.Z3
25{
29 public class Fixedpoint : Z3Object
30 {
31
35 public string Help
36 {
37 get
38 {
39 return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject);
40 }
41 }
42
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 }
55
60 {
61 get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); }
62 }
63
64
68 public void Assert(params BoolExpr[] constraints)
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 }
79
83 public void Add(params BoolExpr[] constraints)
84 {
85 Assert(constraints);
86 }
87
92 {
93 Debug.Assert(f != null);
94
95 Context.CheckContextMatch(f);
96 Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject);
97 }
98
102 public void AddRule(BoolExpr rule, Symbol name = null)
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 }
109
113 public void AddFact(FuncDecl pred, params uint[] args)
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 }
121
128 public Status Query(BoolExpr query)
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 }
141
148 public Status Query(params FuncDecl[] relations)
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 }
163
167 public void UpdateRule(BoolExpr rule, Symbol name)
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 }
174
180 {
181 IntPtr ans = Native.Z3_fixedpoint_get_answer(Context.nCtx, NativeObject);
182 return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
183 }
184
188 public string GetReasonUnknown()
189 {
190
191 return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject);
192 }
193
197 public uint GetNumLevels(FuncDecl predicate)
198 {
199 return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
200 }
201
205 public Expr GetCoverDelta(int level, FuncDecl predicate)
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 }
210
215 public void AddCover(int level, FuncDecl predicate, Expr property)
216 {
217 Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
218 }
219
223 public override string ToString()
224 {
225 return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 0, null);
226 }
227
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 }
239
243 public string ToString(params BoolExpr[] queries)
244 {
245
246 return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
247 AST.ArrayLength(queries), AST.ArrayToNative(queries));
248 }
249
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 }
262
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 }
275
280 {
281 get
282 {
283
284 return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
285 }
286 }
287
293 public BoolExpr[] ParseFile(string file)
294 {
295 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
296 return av.ToBoolExprArray();
297 }
298
302 public BoolExpr[] ParseString(string s)
303 {
304 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
305 return av.ToBoolExprArray();
306 }
307
308
309 #region Internal
310 internal Fixedpoint(Context ctx, IntPtr obj)
311 : base(ctx, obj)
312 {
313 Debug.Assert(ctx != null);
314 }
315 internal Fixedpoint(Context ctx)
316 : base(ctx, Native.Z3_mk_fixedpoint(ctx.nCtx))
317 {
318 Debug.Assert(ctx != null);
319 }
320
321 internal class DecRefQueue : IDecRefQueue
322 {
323 public DecRefQueue() : base() { }
324 public DecRefQueue(uint move_limit) : base(move_limit) { }
325 internal override void IncRef(Context ctx, IntPtr obj)
326 {
327 Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
328 }
329
330 internal override void DecRef(Context ctx, IntPtr obj)
331 {
332 Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
333 }
334 };
335
336 internal override void IncRef(IntPtr o)
337 {
338 Context.Fixedpoint_DRQ.IncAndClear(Context, o);
339 base.IncRef(o);
340 }
341
342 internal override void DecRef(IntPtr o)
343 {
344 Context.Fixedpoint_DRQ.Add(o);
345 base.DecRef(o);
346 }
347 #endregion
348 }
349}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Vectors of ASTs.
Definition: ASTVector.cs:29
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:127
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Definition: Context.cs:4795
Expressions are terms.
Definition: Expr.cs:31
Object for managing fixedpoints
Definition: Fixedpoint.cs:30
BoolExpr[] Assertions
Retrieve set of assertions added to fixedpoint context.
Definition: Fixedpoint.cs:267
BoolExpr[] Rules
Retrieve set of rules added to fixedpoint context.
Definition: Fixedpoint.cs:254
string Help
A string that describes all available fixedpoint solver parameters.
Definition: Fixedpoint.cs:36
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
Definition: Fixedpoint.cs:68
void AddRule(BoolExpr rule, Symbol name=null)
Add rule into the fixedpoint solver.
Definition: Fixedpoint.cs:102
uint GetNumLevels(FuncDecl predicate)
Retrieve the number of levels explored for a given predicate.
Definition: Fixedpoint.cs:197
Status Query(params FuncDecl[] relations)
Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is a...
Definition: Fixedpoint.cs:148
Params Parameters
Sets the fixedpoint solver parameters.
Definition: Fixedpoint.cs:47
Statistics Statistics
Fixedpoint statistics.
Definition: Fixedpoint.cs:280
Expr GetCoverDelta(int level, FuncDecl predicate)
Retrieve the cover of a predicate.
Definition: Fixedpoint.cs:205
string GetReasonUnknown()
Retrieve explanation why fixedpoint engine returned status Unknown.
Definition: Fixedpoint.cs:188
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Fixedpoint solver.
Definition: Fixedpoint.cs:60
void RegisterRelation(FuncDecl f)
Register predicate as recursive relation.
Definition: Fixedpoint.cs:91
BoolExpr[] ParseString(string s)
Similar to ParseFile. Instead it takes as argument a string.
Definition: Fixedpoint.cs:302
override string ToString()
Retrieve internal string representation of fixedpoint object.
Definition: Fixedpoint.cs:223
Status Query(BoolExpr query)
Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the...
Definition: Fixedpoint.cs:128
void AddCover(int level, FuncDecl predicate, Expr property)
Add property about the predicate. The property is added at level.
Definition: Fixedpoint.cs:215
Expr GetAnswer()
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that...
Definition: Fixedpoint.cs:179
BoolExpr[] ParseFile(string file)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....
Definition: Fixedpoint.cs:293
void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition: Fixedpoint.cs:231
string ToString(params BoolExpr[] queries)
Convert benchmark given as set of axioms, rules and queries to a string.
Definition: Fixedpoint.cs:243
void UpdateRule(BoolExpr rule, Symbol name)
Update named rule into in the fixedpoint solver.
Definition: Fixedpoint.cs:167
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Fixedpoint.cs:83
void AddFact(FuncDecl pred, params uint[] args)
Add table fact to the fixedpoint solver.
Definition: Fixedpoint.cs:113
Function declarations.
Definition: FuncDecl.cs:31
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:30
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.