18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_ast_kind;
32 return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
40 return Native.isQuantifierExists(getContext().nCtx(), getNativeObject());
48 return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
57 .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
69 for (
int i = 0; i < n; i++)
70 res[i] =
new Pattern(getContext(), Native.getQuantifierPatternAst(
71 getContext().nCtx(), getNativeObject(), i));
80 return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
93 for (
int i = 0; i < n; i++)
94 res[i] =
new Pattern(getContext(), Native.getQuantifierNoPatternAst(
95 getContext().nCtx(), getNativeObject(), i));
104 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
116 for (
int i = 0; i < n; i++)
117 res[i] =
Symbol.create(getContext(), Native.getQuantifierBoundName(
118 getContext().nCtx(), getNativeObject(), i));
131 for (
int i = 0; i < n; i++)
132 res[i] =
Sort.create(getContext(), Native.getQuantifierBoundSort(
133 getContext().nCtx(), getNativeObject(), i));
144 return (
BoolExpr)
Expr.create(getContext(), Native.getQuantifierBody(getContext()
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) {
191 nativeObj = Native.mkQuantifierEx(ctx.
nCtx(),
192 (isForall), weight,
AST.getNativeObject(quantifierID),
193 AST.getNativeObject(skolemID),
198 body.getNativeObject());
218 ctx.checkContextMatch(noPatterns);
219 ctx.checkContextMatch(patterns);
220 ctx.checkContextMatch(body);
223 if (noPatterns ==
null && quantifierID ==
null && skolemID ==
null) {
224 nativeObj = Native.mkQuantifierConst(ctx.
nCtx(),
229 nativeObj = Native.mkQuantifierConstEx(ctx.
nCtx(),
231 AST.getNativeObject(quantifierID),
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 Quantifier of(Context ctx, boolean isForall, Expr<?>[] bound, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Quantifier translate(Context ctx)
Sort[] getBoundVariableSorts()
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Symbol[] getBoundVariableNames()
Pattern[] getNoPatterns()
static long[] arrayToNative(Z3Object[] a)
static int arrayLength(Z3Object[] a)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.