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()));
173 setNativeObject(Native.mkQuantifierEx(ctx.nCtx(),
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()));
184 Quantifier(Context ctx,
boolean isForall,
Expr[] bound,
Expr body,
185 int weight, Pattern[] patterns,
Expr[] noPatterns,
186 Symbol quantifierID, Symbol skolemID)
throws Z3Exception
190 getContext().checkContextMatch(noPatterns);
191 getContext().checkContextMatch(patterns);
193 getContext().checkContextMatch(body);
195 if (noPatterns == null && quantifierID == null && skolemID == null)
197 setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
198 (isForall) ?
true :
false, weight, AST.arrayLength(bound),
199 AST.arrayToNative(bound), AST.arrayLength(patterns),
200 AST.arrayToNative(patterns), body.getNativeObject()));
203 setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
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()));
213 Quantifier(Context ctx,
long obj)
throws Z3Exception
218 void checkNativeObject(
long obj)
throws Z3Exception
220 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_QUANTIFIER_AST
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)
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 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()
Sort[] getBoundVariableSorts()
static boolean isQuantifierForall(long a0, long a1)