18 package com.microsoft.z3;
69 for (
int i = 0; i < n; i++)
71 getContext().nCtx(), getNativeObject(), i));
93 for (
int i = 0; i < n; i++)
95 getContext().nCtx(), getNativeObject(), i));
116 for (
int i = 0; i < n; i++)
118 getContext().nCtx(), getNativeObject(), i));
131 for (
int i = 0; i < n; i++)
133 getContext().nCtx(), getNativeObject(), i));
145 .nCtx(), getNativeObject()));
173 ctx.checkContextMatch(patterns);
174 ctx.checkContextMatch(noPatterns);
175 ctx.checkContextMatch(sorts);
176 ctx.checkContextMatch(names);
177 ctx.checkContextMatch(body);
179 if (sorts.length != names.length) {
181 "Number of sorts does not match number of names");
185 if (noPatterns ==
null && quantifierID ==
null && skolemID ==
null) {
187 .arrayToNative(patterns),
AST.arrayLength(sorts),
AST
188 .arrayToNative(sorts),
Symbol.arrayToNative(names), body
192 (isForall), weight,
AST.getNativeObject(quantifierID),
193 AST.getNativeObject(skolemID),
194 AST.arrayLength(patterns),
AST.arrayToNative(patterns),
195 AST.arrayLength(noPatterns),
AST.arrayToNative(noPatterns),
196 AST.arrayLength(sorts),
AST.arrayToNative(sorts),
197 Symbol.arrayToNative(names),
198 body.getNativeObject());
218 ctx.checkContextMatch(noPatterns);
219 ctx.checkContextMatch(patterns);
220 ctx.checkContextMatch(body);
223 if (noPatterns ==
null && quantifierID ==
null && skolemID ==
null) {
225 isForall, weight,
AST.arrayLength(bound),
226 AST.arrayToNative(bound),
AST.arrayLength(patterns),
227 AST.arrayToNative(patterns), body.getNativeObject());
231 AST.getNativeObject(quantifierID),
232 AST.getNativeObject(skolemID),
AST.arrayLength(bound),
233 AST.arrayToNative(bound),
AST.arrayLength(patterns),
234 AST.arrayToNative(patterns),
AST.arrayLength(noPatterns),
235 AST.arrayToNative(noPatterns), body.getNativeObject());
246 void checkNativeObject(
long obj) {
247 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_QUANTIFIER_AST
249 throw new Z3Exception(
"Underlying object is not a quantifier");
251 super.checkNativeObject(obj);