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()));
160 ctx.checkContextMatch(patterns);
161 ctx.checkContextMatch(noPatterns);
162 ctx.checkContextMatch(sorts);
163 ctx.checkContextMatch(names);
164 ctx.checkContextMatch(body);
166 if (sorts.length != names.length) {
168 "Number of sorts does not match number of names");
172 if (noPatterns == null && quantifierID == null && skolemID == null) {
174 .arrayToNative(patterns),
AST.arrayLength(sorts),
AST 175 .arrayToNative(sorts),
Symbol.arrayToNative(names), body
179 (isForall), weight,
AST.getNativeObject(quantifierID),
180 AST.getNativeObject(skolemID),
181 AST.arrayLength(patterns),
AST.arrayToNative(patterns),
182 AST.arrayLength(noPatterns),
AST.arrayToNative(noPatterns),
183 AST.arrayLength(sorts),
AST.arrayToNative(sorts),
184 Symbol.arrayToNative(names),
185 body.getNativeObject());
205 ctx.checkContextMatch(noPatterns);
206 ctx.checkContextMatch(patterns);
207 ctx.checkContextMatch(body);
210 if (noPatterns == null && quantifierID == null && skolemID == null) {
212 isForall, weight,
AST.arrayLength(bound),
213 AST.arrayToNative(bound),
AST.arrayLength(patterns),
214 AST.arrayToNative(patterns), body.getNativeObject());
218 AST.getNativeObject(quantifierID),
219 AST.getNativeObject(skolemID),
AST.arrayLength(bound),
220 AST.arrayToNative(bound),
AST.arrayLength(patterns),
221 AST.arrayToNative(patterns),
AST.arrayLength(noPatterns),
222 AST.arrayToNative(noPatterns), body.getNativeObject());
233 void checkNativeObject(
long obj) {
236 throw new Z3Exception(
"Underlying object is not a quantifier");
238 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)
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 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)
Sort [] getBoundVariableSorts()
static int getAstKind(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 boolean isQuantifierForall(long a0, long a1)