Z3
Fixedpoint.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Fixedpoints.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Fixedpoints
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Fixedpoint : Z3Object
30  {
31 
35  public string Help
36  {
37  get
38  {
39  Contract.Ensures(Contract.Result<string>() != null);
40  return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject);
41  }
42  }
43 
47  public Params Parameters
48  {
49  set
50  {
51  Contract.Requires(value != null);
52  Context.CheckContextMatch(value);
53  Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject);
54  }
55  }
56 
60  public ParamDescrs ParameterDescriptions
61  {
62  get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); }
63  }
64 
65 
69  public void Assert(params BoolExpr[] constraints)
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  }
80 
84  public void Add(params BoolExpr[] constraints)
85  {
86  Assert(constraints);
87  }
88 
92  public void RegisterRelation(FuncDecl f)
93  {
94  Contract.Requires(f != null);
95 
96  Context.CheckContextMatch(f);
97  Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject);
98  }
99 
103  public void AddRule(BoolExpr rule, Symbol name = null)
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  }
110 
114  public void AddFact(FuncDecl pred, params uint[] args)
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  }
122 
129  public Status Query(BoolExpr query)
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  }
142 
149  public Status Query(FuncDecl[] relations)
150  {
151  Contract.Requires(relations != null);
152  Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
153 
154  Context.CheckContextMatch(relations);
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  }
164 
169  public void Push()
170  {
171  Native.Z3_fixedpoint_push(Context.nCtx, NativeObject);
172  }
173 
179  public void Pop()
180  {
181  Native.Z3_fixedpoint_pop(Context.nCtx, NativeObject);
182  }
183 
184 
188  public void UpdateRule(BoolExpr rule, Symbol name)
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  }
195 
200  public Expr GetAnswer()
201  {
202  IntPtr ans = Native.Z3_fixedpoint_get_answer(Context.nCtx, NativeObject);
203  return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
204  }
205 
209  public string GetReasonUnknown()
210  {
211  Contract.Ensures(Contract.Result<string>() != null);
212 
213  return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject);
214  }
215 
219  public uint GetNumLevels(FuncDecl predicate)
220  {
221  return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
222  }
223 
227  public Expr GetCoverDelta(int level, FuncDecl predicate)
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  }
232 
237  public void AddCover(int level, FuncDecl predicate, Expr property)
238  {
239  Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
240  }
241 
245  public override string ToString()
246  {
247  return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 0, null);
248  }
249 
254  {
255  Contract.Requires(f != null);
256 
258  f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
259 
260  }
261 
265  public string ToString(BoolExpr[] queries)
266  {
267 
268  return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
269  AST.ArrayLength(queries), AST.ArrayToNative(queries));
270  }
271 
275  public BoolExpr[] Rules
276  {
277  get
278  {
279  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
280 
281  ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
282  return av.ToBoolExprArray();
283  }
284  }
285 
289  public BoolExpr[] Assertions
290  {
291  get
292  {
293  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
294 
295  ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
296  return av.ToBoolExprArray();
297  }
298  }
299 
303  public Statistics Statistics
304  {
305  get
306  {
307  Contract.Ensures(Contract.Result<Statistics>() != null);
308 
309  return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
310  }
311  }
312 
318  public BoolExpr[] ParseFile(string file)
319  {
320  ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
321  return av.ToBoolExprArray();
322  }
323 
327  public BoolExpr[] ParseString(string s)
328  {
329  ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
330  return av.ToBoolExprArray();
331  }
332 
333 
334  #region Internal
335  internal Fixedpoint(Context ctx, IntPtr obj)
336  : base(ctx, obj)
337  {
338  Contract.Requires(ctx != null);
339  }
340  internal Fixedpoint(Context ctx)
341  : base(ctx, Native.Z3_mk_fixedpoint(ctx.nCtx))
342  {
343  Contract.Requires(ctx != null);
344  }
345 
346  internal class DecRefQueue : IDecRefQueue
347  {
348  public DecRefQueue() : base() { }
349  public DecRefQueue(uint move_limit) : base(move_limit) { }
350  internal override void IncRef(Context ctx, IntPtr obj)
351  {
352  Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
353  }
354 
355  internal override void DecRef(Context ctx, IntPtr obj)
356  {
357  Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
358  }
359  };
360 
361  internal override void IncRef(IntPtr o)
362  {
363  Context.Fixedpoint_DRQ.IncAndClear(Context, o);
364  base.IncRef(o);
365  }
366 
367  internal override void DecRef(IntPtr o)
368  {
369  Context.Fixedpoint_DRQ.Add(o);
370  base.DecRef(o);
371  }
372  #endregion
373  }
374 }
static void Z3_fixedpoint_dec_ref(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4346
static void Z3_fixedpoint_push(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4521
string ToString(BoolExpr[] queries)
Convert benchmark given as set of axioms, rules and queries to a string.
Definition: Fixedpoint.cs:265
static Z3_ast Z3_fixedpoint_get_answer(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4390
using System
static void Z3_fixedpoint_register_relation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
Definition: Native.cs:4444
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Fixedpoint.cs:84
Boolean expressions
Definition: BoolExpr.cs:31
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:29
void UpdateRule(BoolExpr rule, Symbol name)
Update named rule into in the fixedpoint solver.
Definition: Fixedpoint.cs:188
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
Definition: Fixedpoint.cs:69
static void Z3_fixedpoint_set_params(Z3_context a0, Z3_fixedpoint a1, Z3_params a2)
Definition: Native.cs:4474
Expr GetCoverDelta(int level, FuncDecl predicate)
Retrieve the cover of a predicate.
Definition: Fixedpoint.cs:227
static Z3_stats Z3_fixedpoint_get_statistics(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4436
static int Z3_fixedpoint_query(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
Definition: Native.cs:4374
static void Z3_fixedpoint_pop(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4528
string GetReasonUnknown()
Retrieve explanation why fixedpoint engine returned status Unknown.
Definition: Fixedpoint.cs:209
void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition: Fixedpoint.cs:253
static void Z3_fixedpoint_assert(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
Definition: Native.cs:4367
Vectors of ASTs.
Definition: ASTVector.cs:28
static void Z3_fixedpoint_set_predicate_representation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] IntPtr[] a4)
Definition: Native.cs:4451
Expressions are terms.
Definition: Expr.cs:29
BoolExpr[] ParseString(string s)
Similar to ParseFile. Instead it takes as argument a string.
Definition: Fixedpoint.cs:327
static void Z3_fixedpoint_add_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
Definition: Native.cs:4353
BoolExpr[] ParseFile(string file)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
Definition: Fixedpoint.cs:318
static void Z3_fixedpoint_update_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
Definition: Native.cs:4406
static int Z3_fixedpoint_query_relations(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_func_decl[] a3)
Definition: Native.cs:4382
static string Z3_fixedpoint_get_help(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4481
static void Z3_fixedpoint_add_fact(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] uint[] a4)
Definition: Native.cs:4360
static void Z3_fixedpoint_add_cover(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3, Z3_ast a4)
Definition: Native.cs:4429
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
void AddCover(int level, FuncDecl predicate, Expr property)
Add property about the predicate. The property is added at level.
Definition: Fixedpoint.cs:237
static Z3_ast_vector Z3_fixedpoint_get_rules(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4458
static Z3_ast_vector Z3_fixedpoint_get_assertions(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4466
Status Query(FuncDecl[] relations)
Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is a...
Definition: Fixedpoint.cs:149
Status
Status values.
Definition: Status.cs:27
static void Z3_fixedpoint_inc_ref(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4339
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:129
static string Z3_fixedpoint_get_reason_unknown(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4398
Expr GetAnswer()
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that...
Definition: Fixedpoint.cs:200
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
static Z3_ast_vector Z3_fixedpoint_from_file(Z3_context a0, Z3_fixedpoint a1, string a2)
Definition: Native.cs:4513
void AddFact(FuncDecl pred, params uint[] args)
Add table fact to the fixedpoint solver.
Definition: Fixedpoint.cs:114
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
static Z3_fixedpoint Z3_mk_fixedpoint(Z3_context a0)
Definition: Native.cs:4331
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Definition: Context.cs:4534
static Z3_ast_vector Z3_fixedpoint_from_string(Z3_context a0, Z3_fixedpoint a1, string a2)
Definition: Native.cs:4505
The abstract syntax tree (AST) class.
Definition: AST.cs:31
uint GetNumLevels(FuncDecl predicate)
Retrieve the number of levels explored for a given predicate.
Definition: Fixedpoint.cs:219
Object for managing fixedpoints
Definition: Fixedpoint.cs:29
void Pop()
Backtrack one backtracking point.
Definition: Fixedpoint.cs:179
void RegisterRelation(FuncDecl f)
Register predicate as recursive relation.
Definition: Fixedpoint.cs:92
void Push()
Creates a backtracking point.
Definition: Fixedpoint.cs:169
static uint Z3_fixedpoint_get_num_levels(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
Definition: Native.cs:4413
void AddRule(BoolExpr rule, Symbol name=null)
Add rule into the fixedpoint solver.
Definition: Fixedpoint.cs:103
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
static string Z3_fixedpoint_to_string(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:4497
override string ToString()
Retrieve internal string representation of fixedpoint object.
Definition: Fixedpoint.cs:245
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Status Query(BoolExpr query)
Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the...
Definition: Fixedpoint.cs:129
static Z3_ast Z3_fixedpoint_get_cover_delta(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3)
Definition: Native.cs:4421
Function declarations.
Definition: FuncDecl.cs:29
static Z3_param_descrs Z3_fixedpoint_get_param_descrs(Z3_context a0, Z3_fixedpoint a1)
Definition: Native.cs:4489