Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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  {
154  Contract.Ensures(Contract.Result<BoolExpr>() != null);
155 
156  return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
157  }
158  }
159 
160  #region Internal
161  [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
162  internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
163  : base(ctx)
164  {
165  Contract.Requires(ctx != null);
166  Contract.Requires(sorts != null);
167  Contract.Requires(names != null);
168  Contract.Requires(body != null);
169  Contract.Requires(sorts.Length == names.Length);
170  Contract.Requires(Contract.ForAll(sorts, s => s != null));
171  Contract.Requires(Contract.ForAll(names, n => n != null));
172  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
173  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
174 
175  Context.CheckContextMatch(patterns);
176  Context.CheckContextMatch(noPatterns);
177  Context.CheckContextMatch(sorts);
178  Context.CheckContextMatch(names);
179  Context.CheckContextMatch(body);
180 
181  if (sorts.Length != names.Length)
182  throw new Z3Exception("Number of sorts does not match number of names");
183 
184  if (noPatterns == null && quantifierID == null && skolemID == null)
185  {
186  NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
187  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
188  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
189  Symbol.ArrayToNative(names),
190  body.NativeObject);
191  }
192  else
193  {
194  NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
195  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
196  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
197  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
198  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
199  Symbol.ArrayToNative(names),
200  body.NativeObject);
201  }
202  }
203 
204  [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
205  internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
206  : base(ctx)
207  {
208  Contract.Requires(ctx != null);
209  Contract.Requires(body != null);
210 
211  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
212  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
213  Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null));
214 
215  Context.CheckContextMatch(noPatterns);
216  Context.CheckContextMatch(patterns);
217  //Context.CheckContextMatch(bound);
218  Context.CheckContextMatch(body);
219 
220  if (noPatterns == null && quantifierID == null && skolemID == null)
221  {
222  NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
223  AST.ArrayLength(bound), AST.ArrayToNative(bound),
224  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
225  body.NativeObject);
226  }
227  else
228  {
229  NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
230  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
231  AST.ArrayLength(bound), AST.ArrayToNative(bound),
232  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
233  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
234  body.NativeObject);
235  }
236  }
237 
238 
239  internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
240 
241 #if DEBUG
242  internal override void CheckNativeObject(IntPtr obj)
243  {
244  if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
245  throw new Z3Exception("Underlying object is not a quantifier");
246  base.CheckNativeObject(obj);
247  }
248 #endif
249  #endregion
250  }
251 }
static uint Z3_get_quantifier_num_no_patterns(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3494
static Z3_ast Z3_get_quantifier_no_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
Definition: Native.cs:3502
static uint Z3_get_quantifier_weight(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3470
Expressions are terms.
Definition: Expr.cs:29
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
static Z3_pattern Z3_get_quantifier_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
Definition: Native.cs:3486
static int Z3_is_quantifier_forall(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3462
static uint Z3_get_quantifier_num_bound(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3510
static IntPtr Z3_get_quantifier_bound_name(Z3_context a0, Z3_ast a1, uint a2)
Definition: Native.cs:3518
static uint Z3_get_quantifier_num_patterns(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3478
Quantifier expressions.
Definition: Quantifier.cs:29
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
static Z3_sort Z3_get_quantifier_bound_sort(Z3_context a0, Z3_ast a1, uint a2)
Definition: Native.cs:3526
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static Z3_ast Z3_mk_quantifier(Z3_context a0, int a1, uint a2, uint a3, [In] Z3_pattern[] a4, uint a5, [In] Z3_sort[] a6, [In] IntPtr[] a7, Z3_ast a8)
Definition: Native.cs:2846
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
static Z3_ast Z3_get_quantifier_body(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3534