18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_ast_kind;
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);
static boolean isQuantifierForall(long a0, long a1)
static long getQuantifierNoPatternAst(long a0, long a1, int a2)
static int getQuantifierWeight(long a0, long a1)
static long getQuantifierBody(long a0, long a1)
static int getQuantifierNumPatterns(long a0, long a1)
static long mkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11)
static long getQuantifierPatternAst(long a0, long a1, int a2)
static long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
static long getQuantifierBoundName(long a0, long a1, int a2)
static boolean isQuantifierExists(long a0, long a1)
static long mkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12)
static long getQuantifierBoundSort(long a0, long a1, int a2)
static long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
static int getQuantifierNumNoPatterns(long a0, long a1)
static int getQuantifierNumBound(long a0, long a1)
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Quantifier translate(Context ctx)
Sort[] getBoundVariableSorts()
Symbol[] getBoundVariableNames()
static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Pattern[] getNoPatterns()
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.