21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
34 public bool IsUniversal
42 public bool IsExistential
44 get {
return !IsUniversal; }
58 public uint NumPatterns
70 Contract.Ensures(Contract.Result<
Pattern[]>() != null);
74 for (uint i = 0; i < n; i++)
83 public uint NumNoPatterns
95 Contract.Ensures(Contract.Result<
Pattern[]>() != null);
97 uint n = NumNoPatterns;
99 for (uint i = 0; i < n; i++)
116 public Symbol[] BoundVariableNames
120 Contract.Ensures(Contract.Result<
Symbol[]>() != null);
124 for (uint i = 0; i < n; i++)
133 public Sort[] BoundVariableSorts
137 Contract.Ensures(Contract.Result<
Sort[]>() != null);
141 for (uint i = 0; i < n; i++)
154 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
161 [ContractVerification(
false)]
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));
175 Context.CheckContextMatch(patterns);
176 Context.CheckContextMatch(noPatterns);
177 Context.CheckContextMatch(sorts);
178 Context.CheckContextMatch(names);
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)
187 AST.ArrayLength(patterns),
AST.ArrayToNative(patterns),
188 AST.ArrayLength(sorts),
AST.ArrayToNative(sorts),
189 Symbol.ArrayToNative(names),
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),
204 [ContractVerification(
false)]
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));
215 Context.CheckContextMatch(noPatterns);
216 Context.CheckContextMatch(patterns);
218 Context.CheckContextMatch(body);
220 if (noPatterns == null && quantifierID == null && skolemID == null)
223 AST.ArrayLength(bound),
AST.ArrayToNative(bound),
224 AST.ArrayLength(patterns),
AST.ArrayToNative(patterns),
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);
static uint Z3_get_quantifier_num_no_patterns(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_get_quantifier_no_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
static uint Z3_get_quantifier_weight(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_mk_quantifier_const_ex(Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_app[] a6, uint a7, [In] Z3_pattern[] a8, uint a9, [In] Z3_ast[] a10, Z3_ast a11)
static Z3_pattern Z3_get_quantifier_pattern_ast(Z3_context a0, Z3_ast a1, uint a2)
static int Z3_is_quantifier_forall(Z3_context a0, Z3_ast a1)
static uint Z3_get_quantifier_num_bound(Z3_context a0, Z3_ast a1)
static IntPtr Z3_get_quantifier_bound_name(Z3_context a0, Z3_ast a1, uint a2)
static uint Z3_get_quantifier_num_patterns(Z3_context a0, Z3_ast a1)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
static Z3_sort Z3_get_quantifier_bound_sort(Z3_context a0, Z3_ast a1, uint a2)
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
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)
The abstract syntax tree (AST) class.
static Z3_ast Z3_mk_quantifier_const(Z3_context a0, int a1, uint a2, uint a3, [In] Z3_app[] a4, uint a5, [In] Z3_pattern[] a6, Z3_ast a7)
Symbols are used to name several term and type constructors.
static Z3_ast Z3_mk_quantifier_ex(Z3_context a0, int a1, uint a2, IntPtr a3, IntPtr a4, uint a5, [In] Z3_pattern[] a6, uint a7, [In] Z3_ast[] a8, uint a9, [In] Z3_sort[] a10, [In] IntPtr[] a11, Z3_ast a12)
static Z3_ast Z3_get_quantifier_body(Z3_context a0, Z3_ast a1)