21using System.Diagnostics;
36 get {
return 0 != Native.Z3_is_quantifier_forall(
Context.nCtx, NativeObject); }
44 get {
return 0 != Native.Z3_is_quantifier_exists(
Context.nCtx, NativeObject); }
52 get {
return Native.Z3_get_quantifier_weight(
Context.nCtx, NativeObject); }
60 get {
return Native.Z3_get_quantifier_num_patterns(
Context.nCtx, NativeObject); }
73 for (uint i = 0; i < n; i++)
84 get {
return Native.Z3_get_quantifier_num_no_patterns(
Context.nCtx, NativeObject); }
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));
108 get {
return Native.Z3_get_quantifier_num_bound(
Context.nCtx, NativeObject); }
121 for (uint i = 0; i < n; i++)
122 res[i] =
Symbol.Create(
Context, Native.Z3_get_quantifier_bound_name(
Context.nCtx, NativeObject, i));
137 for (uint i = 0; i < n; i++)
138 res[i] =
Sort.Create(
Context, Native.Z3_get_quantifier_bound_sort(
Context.nCtx, NativeObject, i));
151 return Expr.Create(
Context, Native.Z3_get_quantifier_body(
Context.nCtx, NativeObject));
167 : base(ctx, IntPtr.Zero)
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));
183 Context.CheckContextMatch(body);
185 if (sorts.Length != names.Length)
186 throw new Z3Exception(
"Number of sorts does not match number of names");
188 if (noPatterns ==
null && quantifierID ==
null && skolemID ==
null)
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),
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),
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)
211 Debug.Assert(ctx !=
null);
212 Debug.Assert(body !=
null);
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));
218 Context.CheckContextMatch<
Expr>(noPatterns);
219 Context.CheckContextMatch<Pattern>(patterns);
221 Context.CheckContextMatch(body);
223 if (noPatterns ==
null && quantifierID ==
null && skolemID ==
null)
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),
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),
242 internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
245 internal override void CheckNativeObject(IntPtr obj)
248 throw new Z3Exception(
"Underlying object is not a quantifier");
249 base.CheckNativeObject(obj);
The abstract syntax tree (AST) class.
The main interaction with Z3 happens via the Context.
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Pattern[] Patterns
The patterns.
uint NumNoPatterns
The number of no-patterns.
uint Weight
The weight of the quantifier.
bool IsUniversal
Indicates whether the quantifier is universal.
Pattern[] NoPatterns
The no-patterns.
new Quantifier Translate(Context ctx)
Translates (copies) the quantifier to the Context ctx .
uint NumBound
The number of bound variables.
Symbol[] BoundVariableNames
The symbols for the bound variables.
Sort[] BoundVariableSorts
The sorts of the bound variables.
uint NumPatterns
The number of patterns.
Expr Body
The body of the quantifier.
bool IsExistential
Indicates whether the quantifier is existential.
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.
The exception base class for error reporting from Z3
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.