Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Quantifier.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Quantifier.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Quantifiers
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-19
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 Quantifier : BoolExpr
30  {
34  public bool IsUniversal
35  {
36  get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; }
37  }
38 
42  public bool IsExistential
43  {
44  get { return !IsUniversal; }
45  }
46 
50  public uint Weight
51  {
52  get { return Native.Z3_get_quantifier_weight(Context.nCtx, NativeObject); }
53  }
54 
58  public uint NumPatterns
59  {
60  get { return Native.Z3_get_quantifier_num_patterns(Context.nCtx, NativeObject); }
61  }
62 
66  public Pattern[] Patterns
67  {
68  get
69  {
70  Contract.Ensures(Contract.Result<Pattern[]>() != null);
71 
72  uint n = NumPatterns;
73  Pattern[] res = new Pattern[n];
74  for (uint i = 0; i < n; i++)
75  res[i] = new Pattern(Context, Native.Z3_get_quantifier_pattern_ast(Context.nCtx, NativeObject, i));
76  return res;
77  }
78  }
79 
83  public uint NumNoPatterns
84  {
85  get { return Native.Z3_get_quantifier_num_no_patterns(Context.nCtx, NativeObject); }
86  }
87 
91  public Pattern[] NoPatterns
92  {
93  get
94  {
95  Contract.Ensures(Contract.Result<Pattern[]>() != null);
96 
97  uint n = NumNoPatterns;
98  Pattern[] res = new Pattern[n];
99  for (uint i = 0; i < n; i++)
100  res[i] = new Pattern(Context, Native.Z3_get_quantifier_no_pattern_ast(Context.nCtx, NativeObject, i));
101  return res;
102  }
103  }
104 
108  public uint NumBound
109  {
110  get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); }
111  }
112 
116  public Symbol[] BoundVariableNames
117  {
118  get
119  {
120  Contract.Ensures(Contract.Result<Symbol[]>() != null);
121 
122  uint n = NumBound;
123  Symbol[] res = new Symbol[n];
124  for (uint i = 0; i < n; i++)
125  res[i] = Symbol.Create(Context, Native.Z3_get_quantifier_bound_name(Context.nCtx, NativeObject, i));
126  return res;
127  }
128  }
129 
133  public Sort[] BoundVariableSorts
134  {
135  get
136  {
137  Contract.Ensures(Contract.Result<Sort[]>() != null);
138 
139  uint n = NumBound;
140  Sort[] res = new Sort[n];
141  for (uint i = 0; i < n; i++)
142  res[i] = Sort.Create(Context, Native.Z3_get_quantifier_bound_sort(Context.nCtx, NativeObject, i));
143  return res;
144  }
145  }
146 
150  public BoolExpr Body
151  {
152  get {
153  Contract.Ensures(Contract.Result<BoolExpr>() != null);
154 
155  return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); }
156  }
157 
158  #region Internal
159  [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
160  internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body,
161  uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
162  Symbol quantifierID = null, Symbol skolemID = null
163  )
164  : base(ctx)
165  {
166  Contract.Requires(ctx != null);
167  Contract.Requires(sorts != null);
168  Contract.Requires(names != null);
169  Contract.Requires(body != null);
170  Contract.Requires(sorts.Length == names.Length);
171  Contract.Requires(Contract.ForAll(sorts, s => s != null));
172  Contract.Requires(Contract.ForAll(names, n => n != null));
173  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
174  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
175 
176  Context.CheckContextMatch(patterns);
177  Context.CheckContextMatch(noPatterns);
178  Context.CheckContextMatch(sorts);
179  Context.CheckContextMatch(names);
180  Context.CheckContextMatch(body);
181 
182  if (sorts.Length != names.Length)
183  throw new Z3Exception("Number of sorts does not match number of names");
184 
185  IntPtr[] _patterns = AST.ArrayToNative(patterns);
186 
187  if (noPatterns == null && quantifierID == null && skolemID == null)
188  {
189  NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
190  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
191  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
192  Symbol.ArrayToNative(names),
193  body.NativeObject);
194  }
195  else
196  {
197  NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
198  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
199  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
200  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
201  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
202  Symbol.ArrayToNative(names),
203  body.NativeObject);
204  }
205  }
206 
207  [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
208  internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body,
209  uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
210  Symbol quantifierID = null, Symbol skolemID = null
211  )
212  : base(ctx)
213  {
214  Contract.Requires(ctx != null);
215  Contract.Requires(body != null);
216 
217  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
218  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
219  Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null));
220 
221  Context.CheckContextMatch(noPatterns);
222  Context.CheckContextMatch(patterns);
223  //Context.CheckContextMatch(bound);
224  Context.CheckContextMatch(body);
225 
226  if (noPatterns == null && quantifierID == null && skolemID == null)
227  {
228  NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
229  AST.ArrayLength(bound), AST.ArrayToNative(bound),
230  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
231  body.NativeObject);
232  }
233  else
234  {
235  NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
236  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
237  AST.ArrayLength(bound), AST.ArrayToNative(bound),
238  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
239  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
240  body.NativeObject);
241  }
242  }
243 
244 
245  internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
246 
247  #if DEBUG
248  internal override void CheckNativeObject(IntPtr obj)
249  {
250  if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
251  throw new Z3Exception("Underlying object is not a quantifier");
252  base.CheckNativeObject(obj);
253  }
254  #endif
255  #endregion
256  }
257 }
Generated on Thu Nov 22 2012 18:37:19 for Z3 by   doxygen 1.8.2