34 public bool IsUniversal
36 get {
return Native.Z3_is_quantifier_forall(
Context.nCtx, NativeObject) != 0; }
42 public bool IsExistential
44 get {
return !IsUniversal; }
52 get {
return Native.Z3_get_quantifier_weight(
Context.nCtx, NativeObject); }
58 public uint NumPatterns
60 get {
return Native.Z3_get_quantifier_num_patterns(
Context.nCtx, NativeObject); }
70 Contract.Ensures(Contract.Result<
Pattern[]>() != null);
74 for (uint i = 0; i < n; i++)
83 public uint NumNoPatterns
85 get {
return Native.Z3_get_quantifier_num_no_patterns(
Context.nCtx, NativeObject); }
95 Contract.Ensures(Contract.Result<
Pattern[]>() != null);
97 uint n = NumNoPatterns;
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));
110 get {
return Native.Z3_get_quantifier_num_bound(
Context.nCtx, NativeObject); }
116 public Symbol[] BoundVariableNames
120 Contract.Ensures(Contract.Result<
Symbol[]>() != null);
124 for (uint i = 0; i < n; i++)
125 res[i] =
Symbol.Create(
Context, Native.Z3_get_quantifier_bound_name(
Context.nCtx, NativeObject, i));
133 public Sort[] BoundVariableSorts
137 Contract.Ensures(Contract.Result<
Sort[]>() != null);
141 for (uint i = 0; i < n; i++)
142 res[i] =
Sort.Create(
Context, Native.Z3_get_quantifier_bound_sort(
Context.nCtx, NativeObject, i));
154 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
163 : base(ctx, IntPtr.Zero)
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));
179 Context.CheckContextMatch(body);
181 if (sorts.Length != names.Length)
182 throw new Z3Exception(
"Number of sorts does not match number of names");
184 if (noPatterns == null && quantifierID == null && skolemID == null)
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),
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),
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, IntPtr.Zero)
208 Contract.Requires(ctx != null);
209 Contract.Requires(body != null);
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));
218 Context.CheckContextMatch(body);
220 if (noPatterns == null && quantifierID == null && skolemID == null)
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),
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),
239 internal Quantifier(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
242 internal override void CheckNativeObject(IntPtr obj)
245 throw new Z3Exception(
"Underlying object is not a quantifier");
246 base.CheckNativeObject(obj);
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
The abstract syntax tree (AST) class.
Symbols are used to name several term and type constructors.