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