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