Z3
Quantifier.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Quantifier.cs
7
8Abstract:
9
10 Z3 Managed API: Quantifiers
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-19
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Linq;
23
24namespace Microsoft.Z3
25{
29 public class Quantifier : BoolExpr
30 {
34 public bool IsUniversal
35 {
36 get { return 0 != Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); }
37 }
38
42 public bool IsExistential
43 {
44 get { return 0 != Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); }
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
67 {
68 get
69 {
70
71 uint n = NumPatterns;
72 Pattern[] res = new Pattern[n];
73 for (uint i = 0; i < n; i++)
74 res[i] = new Pattern(Context, Native.Z3_get_quantifier_pattern_ast(Context.nCtx, NativeObject, i));
75 return res;
76 }
77 }
78
82 public uint NumNoPatterns
83 {
84 get { return Native.Z3_get_quantifier_num_no_patterns(Context.nCtx, NativeObject); }
85 }
86
91 {
92 get
93 {
94
95 uint n = NumNoPatterns;
96 Pattern[] res = new Pattern[n];
97 for (uint i = 0; i < n; i++)
98 res[i] = new Pattern(Context, Native.Z3_get_quantifier_no_pattern_ast(Context.nCtx, NativeObject, i));
99 return res;
100 }
101 }
102
106 public uint NumBound
107 {
108 get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); }
109 }
110
115 {
116 get
117 {
118
119 uint n = NumBound;
120 Symbol[] res = new Symbol[n];
121 for (uint i = 0; i < n; i++)
122 res[i] = Symbol.Create(Context, Native.Z3_get_quantifier_bound_name(Context.nCtx, NativeObject, i));
123 return res;
124 }
125 }
126
131 {
132 get
133 {
134
135 uint n = NumBound;
136 Sort[] res = new Sort[n];
137 for (uint i = 0; i < n; i++)
138 res[i] = Sort.Create(Context, Native.Z3_get_quantifier_bound_sort(Context.nCtx, NativeObject, i));
139 return res;
140 }
141 }
142
146 public Expr Body
147 {
148 get
149 {
150
151 return Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
152 }
153 }
154
161 {
162 return (Quantifier)base.Translate(ctx);
163 }
164
165 #region Internal
166 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)
167 : base(ctx, IntPtr.Zero)
168 {
169 Debug.Assert(ctx != null);
170 Debug.Assert(sorts != null);
171 Debug.Assert(names != null);
172 Debug.Assert(body != null);
173 Debug.Assert(sorts.Length == names.Length);
174 Debug.Assert(sorts.All(s => s != null));
175 Debug.Assert(names.All(n => n != null));
176 Debug.Assert(patterns == null || patterns.All(p => p != null));
177 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
178
179 Context.CheckContextMatch<Pattern>(patterns);
180 Context.CheckContextMatch<Expr>(noPatterns);
181 Context.CheckContextMatch<Sort>(sorts);
182 Context.CheckContextMatch<Symbol>(names);
183 Context.CheckContextMatch(body);
184
185 if (sorts.Length != names.Length)
186 throw new Z3Exception("Number of sorts does not match number of names");
187
188 if (noPatterns == null && quantifierID == null && skolemID == null)
189 {
190 NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight,
191 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
192 AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
193 Symbol.ArrayToNative(names),
194 body.NativeObject);
195 }
196 else
197 {
198 NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (byte)(isForall ? 1 : 0), weight,
199 AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
200 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
201 AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
202 AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
203 Symbol.ArrayToNative(names),
204 body.NativeObject);
205 }
206 }
207
208 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)
209 : base(ctx, IntPtr.Zero)
210 {
211 Debug.Assert(ctx != null);
212 Debug.Assert(body != null);
213
214 Debug.Assert(patterns == null || patterns.All(p => p != null));
215 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
216 Debug.Assert(bound == null || bound.All(n => n != null));
217
218 Context.CheckContextMatch<Expr>(noPatterns);
219 Context.CheckContextMatch<Pattern>(patterns);
220 //Context.CheckContextMatch(bound);
221 Context.CheckContextMatch(body);
222
223 if (noPatterns == null && quantifierID == null && skolemID == null)
224 {
225 NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight,
226 AST.ArrayLength(bound), AST.ArrayToNative(bound),
227 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
228 body.NativeObject);
229 }
230 else
231 {
232 NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (byte)(isForall ? 1 : 0), weight,
233 AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
234 AST.ArrayLength(bound), AST.ArrayToNative(bound),
235 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
236 AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
237 body.NativeObject);
238 }
239 }
240
241
242 internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
243
244#if DEBUG
245 internal override void CheckNativeObject(IntPtr obj)
246 {
247 if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
248 throw new Z3Exception("Underlying object is not a quantifier");
249 base.CheckNativeObject(obj);
250 }
251#endif
252 #endregion
253 }
254}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expressions are terms.
Definition: Expr.cs:31
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1821
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
Quantifier expressions.
Definition: Quantifier.cs:30
Pattern[] Patterns
The patterns.
Definition: Quantifier.cs:67
uint NumNoPatterns
The number of no-patterns.
Definition: Quantifier.cs:83
uint Weight
The weight of the quantifier.
Definition: Quantifier.cs:51
bool IsUniversal
Indicates whether the quantifier is universal.
Definition: Quantifier.cs:35
Pattern[] NoPatterns
The no-patterns.
Definition: Quantifier.cs:91
new Quantifier Translate(Context ctx)
Translates (copies) the quantifier to the Context ctx .
Definition: Quantifier.cs:160
uint NumBound
The number of bound variables.
Definition: Quantifier.cs:107
Symbol[] BoundVariableNames
The symbols for the bound variables.
Definition: Quantifier.cs:115
Sort[] BoundVariableSorts
The sorts of the bound variables.
Definition: Quantifier.cs:131
uint NumPatterns
The number of patterns.
Definition: Quantifier.cs:59
Expr Body
The body of the quantifier.
Definition: Quantifier.cs:147
bool IsExistential
Indicates whether the quantifier is existential.
Definition: Quantifier.cs:43
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180