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()));
154 getContext().checkContextMatch(patterns);
155 getContext().checkContextMatch(noPatterns);
156 getContext().checkContextMatch(sorts);
157 getContext().checkContextMatch(names);
158 getContext().checkContextMatch(body);
160 if (sorts.length != names.length)
162 "Number of sorts does not match number of names");
164 if (noPatterns == null && quantifierID == null && skolemID == null)
167 :
false, weight,
AST.arrayLength(patterns),
AST 168 .arrayToNative(patterns),
AST.arrayLength(sorts),
AST 169 .arrayToNative(sorts),
Symbol.arrayToNative(names), body
170 .getNativeObject()));
174 (isForall) ?
true :
false, weight,
AST.getNativeObject(quantifierID),
175 AST.getNativeObject(skolemID),
176 AST.arrayLength(patterns),
AST.arrayToNative(patterns),
177 AST.arrayLength(noPatterns),
AST.arrayToNative(noPatterns),
178 AST.arrayLength(sorts),
AST.arrayToNative(sorts),
179 Symbol.arrayToNative(names),
180 body.getNativeObject()));
190 getContext().checkContextMatch(noPatterns);
191 getContext().checkContextMatch(patterns);
193 getContext().checkContextMatch(body);
195 if (noPatterns == null && quantifierID == null && skolemID == null)
198 (isForall) ?
true :
false, weight,
AST.arrayLength(bound),
199 AST.arrayToNative(bound),
AST.arrayLength(patterns),
200 AST.arrayToNative(patterns), body.getNativeObject()));
204 (isForall) ?
true :
false, weight,
205 AST.getNativeObject(quantifierID),
206 AST.getNativeObject(skolemID),
AST.arrayLength(bound),
207 AST.arrayToNative(bound),
AST.arrayLength(patterns),
208 AST.arrayToNative(patterns),
AST.arrayLength(noPatterns),
209 AST.arrayToNative(noPatterns), body.getNativeObject()));
218 void checkNativeObject(
long obj)
222 throw new Z3Exception(
"Underlying object is not a quantifier");
223 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 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)