18package com.microsoft.z3;
20import java.lang.reflect.Type;
21import java.lang.reflect.ParameterizedType;
23import com.microsoft.z3.enumerations.Z3_ast_kind;
24import com.microsoft.z3.enumerations.Z3_decl_kind;
25import com.microsoft.z3.enumerations.Z3_lbool;
26import com.microsoft.z3.enumerations.Z3_sort_kind;
33@SuppressWarnings(
"unchecked")
60 Native.simplify(getContext().nCtx(), getNativeObject()));
65 Native.simplifyEx(getContext().nCtx(), getNativeObject(),
66 p.getNativeObject()));
78 return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(),
90 return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
101 return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
111 int n = getNumArgs();
113 for (
int i = 0; i < n; i++) {
114 res[i] =
Expr.create(getContext(),
115 Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
129 getContext().checkContextMatch(args);
130 if (isApp() && args.length != getNumArgs()) {
131 throw new Z3Exception(
"Number of arguments does not match");
133 return (
Expr<R>)
Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
151 getContext().checkContextMatch(from);
152 getContext().checkContextMatch(to);
153 if (from.length != to.length) {
154 throw new Z3Exception(
"Argument sizes do not match");
156 return (
Expr<R>)
Expr.create(getContext(), Native.substitute(getContext().nCtx(),
186 getContext().checkContextMatch(to);
187 return (
Expr<R>)
Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
210 return super.toString();
220 return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
231 return Native.isWellSorted(getContext().nCtx(), getNativeObject());
241 return (R)
Sort.create(getContext(),
242 Native.getSort(getContext().nCtx(), getNativeObject()));
252 return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
262 return isNumeral() && isInt();
272 return isNumeral() && isReal();
282 return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
292 return (isExpr() && Native.isEqSort(getContext().nCtx(),
293 Native.mkBoolSort(getContext().nCtx()),
294 Native.getSort(getContext().nCtx(), getNativeObject())));
304 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_TRUE;
314 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_FALSE;
324 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_EQ;
335 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_DISTINCT;
345 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ITE;
355 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_AND;
365 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_OR;
376 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_IFF;
386 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_XOR;
396 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_NOT;
406 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_IMPLIES;
416 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) ==
Z3_sort_kind.Z3_INT_SORT.toInt();
426 return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) ==
Z3_sort_kind.Z3_REAL_SORT.toInt();
436 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ANUM;
446 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_LE;
456 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_GE;
466 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_LT;
476 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_GT;
486 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ADD;
496 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SUB;
506 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_UMINUS;
516 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_MUL;
526 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_DIV;
536 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_IDIV;
546 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_REM;
556 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_MOD;
566 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_TO_REAL;
576 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_TO_INT;
587 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_IS_INT;
597 return (Native.isApp(getContext().nCtx(), getNativeObject()) &&
Z3_sort_kind
598 .fromInt(Native.getSortKind(getContext().nCtx(),
599 Native.getSort(getContext().nCtx(), getNativeObject()))) ==
Z3_sort_kind.Z3_ARRAY_SORT);
610 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_STORE;
620 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SELECT;
631 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_CONST_ARRAY;
642 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
654 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ARRAY_MAP;
665 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_AS_ARRAY;
675 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SET_UNION;
685 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SET_INTERSECT;
695 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
705 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
715 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SET_SUBSET;
725 return Native.getSortKind(getContext().nCtx(),
726 Native.getSort(getContext().nCtx(), getNativeObject())) ==
Z3_sort_kind.Z3_BV_SORT
737 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BNUM;
747 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BIT1;
757 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BIT0;
767 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BNEG;
777 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BADD;
787 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSUB;
797 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BMUL;
807 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSDIV;
817 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BUDIV;
827 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSREM;
837 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BUREM;
847 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSMOD;
857 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSDIV0;
867 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BUDIV0;
877 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSREM0;
887 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BUREM0;
897 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSMOD0;
907 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ULEQ;
917 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SLEQ;
928 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_UGEQ;
938 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SGEQ;
948 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ULT;
958 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SLT;
968 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_UGT;
978 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SGT;
988 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BAND;
998 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BOR;
1008 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BNOT;
1018 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BXOR;
1028 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BNAND;
1038 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BNOR;
1048 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BXNOR;
1058 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_CONCAT;
1068 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SIGN_EXT;
1078 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ZERO_EXT;
1088 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_EXTRACT;
1098 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_REPEAT;
1108 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BREDOR;
1118 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BREDAND;
1128 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BCOMP;
1138 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BSHL;
1148 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BLSHR;
1158 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BASHR;
1168 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ROTATE_LEFT;
1178 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
1190 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
1202 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
1214 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_INT2BV;
1226 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_BV2INT;
1237 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_CARRY;
1248 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_XOR3;
1261 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_LABEL;
1274 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_LABEL_LIT;
1283 return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
1294 return Native.getString(getContext().nCtx(), getNativeObject());
1319 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_SEQ_CONCAT;
1331 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_OEQ;
1341 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_TRUE;
1351 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_ASSERTED;
1362 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_GOAL;
1376 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
1391 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
1403 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_SYMMETRY;
1415 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
1435 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
1450 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
1461 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
1480 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
1491 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_AND_ELIM;
1502 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
1522 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_REWRITE;
1538 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
1550 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
1565 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
1581 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
1597 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_DER;
1609 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_QUANT_INST;
1621 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
1637 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_LEMMA;
1648 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
1660 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
1672 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
1689 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
1715 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
1738 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
1750 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
1762 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
1790 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_NNF_POS;
1809 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_NNF_NEG;
1827 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
1840 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
1862 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
1872 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1873 .getSortKind(getContext().nCtx(),
1874 Native.getSort(getContext().nCtx(), getNativeObject())) ==
Z3_sort_kind.Z3_RELATION_SORT
1889 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_STORE;
1899 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_EMPTY;
1909 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
1919 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_JOIN;
1931 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_UNION;
1943 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_WIDEN;
1956 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_PROJECT;
1971 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_FILTER;
1991 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
2003 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_RENAME;
2013 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
2027 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_SELECT;
2043 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_RA_CLONE;
2053 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
2054 .getSortKind(getContext().nCtx(),
2055 Native.getSort(getContext().nCtx(), getNativeObject())) ==
Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
2066 return isApp() && getFuncDecl().getDeclKind() ==
Z3_decl_kind.Z3_OP_FD_LT;
2090 throw new Z3Exception(
"Term is not a bound variable.");
2093 return Native.getIndexValue(getContext().nCtx(), getNativeObject());
2096 private Class sort =
null;
2106 public <S extends R>
Expr<S> distillSort(Class<S> newSort) {
2107 if (sort !=
null && !newSort.isAssignableFrom(sort)) {
2109 String.format(
"Cannot distill expression of sort %s to %s.", sort.getName(), newSort.getName()));
2112 return (Expr<S>) ((Expr<?>)
this);
2121 Type superclass = getClass().getGenericSuperclass();
2122 if (superclass instanceof ParameterizedType) {
2123 Type argType = ((ParameterizedType) superclass).getActualTypeArguments()[0];
2124 if (argType instanceof Class) {
2125 this.sort = (Class) argType;
2131 void checkNativeObject(
long obj) {
2132 if (!Native.isApp(getContext().nCtx(), obj) &&
2133 Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_VAR_AST.toInt() &&
2134 Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
2135 throw new Z3Exception(
"Underlying object is not a term");
2137 super.checkNativeObject(obj);
2140 static <U extends Sort> Expr<U> create(Context ctx, FuncDecl<U> f, Expr<?> ... arguments)
2142 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2143 AST.arrayLength(arguments), AST.arrayToNative(arguments));
2144 return (Expr<U>) create(ctx, obj);
2148 static Expr<?> create(Context ctx,
long obj)
2152 return new Quantifier(ctx, obj);
2153 long s = Native.getSort(ctx.nCtx(), obj);
2155 .fromInt(Native.getSortKind(ctx.nCtx(), s));
2157 if (Native.isAlgebraicNumber(ctx.nCtx(), obj))
2158 return new AlgebraicNum(ctx, obj);
2160 if (Native.isNumeralAst(ctx.nCtx(), obj))
2165 return new IntNum(ctx, obj);
2167 return new RatNum(ctx, obj);
2169 return new BitVecNum(ctx, obj);
2171 return new FPNum(ctx, obj);
2173 return new FPRMNum(ctx, obj);
2175 return new FiniteDomainNum(ctx, obj);
2183 return new BoolExpr(ctx, obj);
2185 return new IntExpr(ctx, obj);
2187 return new RealExpr(ctx, obj);
2189 return new BitVecExpr(ctx, obj);
2191 return new ArrayExpr<>(ctx, obj);
2193 return new DatatypeExpr<>(ctx, obj);
2195 return new FPExpr(ctx, obj);
2197 return new FPRMExpr(ctx, obj);
2199 return new FiniteDomainExpr(ctx, obj);
2201 return new SeqExpr<>(ctx, obj);
2203 return new ReExpr<>(ctx, obj);
2207 return new Expr<>(ctx, obj);
boolean isConstantArray()
Expr(Context ctx, long obj)
boolean isProofHypothesis()
boolean isProofTransitivityStar()
boolean isProofAsserted()
boolean isBVRotateRightExtended()
Expr< R > substitute(Expr<?>[] from, Expr<?>[] to)
boolean isRelationFilter()
boolean isEmptyRelation()
Expr< R > substituteVars(Expr<?>[] to)
boolean isRelationalJoin()
boolean isProofApplyDef()
Expr< R > simplify(Params p)
boolean isProofQuantIntro()
boolean isProofReflexivity()
boolean isProofModusPonensOEQ()
boolean isProofTransitivity()
boolean isProofPullQuant()
boolean isProofOrElimination()
boolean isProofIFFFalse()
boolean isProofQuantInst()
boolean isProofPushQuant()
boolean isRelationUnion()
boolean isProofTheoryLemma()
boolean isBVRotateLeftExtended()
boolean isProofSkolemize()
boolean isRelationClone()
boolean isProofElimUnusedVars()
boolean isProofSymmetry()
boolean isProofMonotonicity()
boolean isBVZeroExtension()
Expr< R > translate(Context ctx)
boolean isAlgebraicNumber()
boolean isSetDifference()
boolean isProofAndElimination()
boolean isProofDefIntro()
boolean isBVRotateRight()
boolean isSetComplement()
boolean isArithmeticNumeral()
boolean isBVShiftRightArithmetic()
boolean isFiniteDomainLT()
FuncDecl< R > getFuncDecl()
boolean isIsEmptyRelation()
Expr< R > update(Expr<?>[] args)
boolean isProofUnitResolution()
boolean isBVShiftRightLogical()
boolean isRelationProject()
boolean isRelationNegationFilter()
boolean isRelationWiden()
boolean isRelationSelect()
boolean isProofDefAxiom()
boolean isProofModusPonens()
boolean isRelationStore()
boolean isProofRewriteStar()
boolean isProofDistributivity()
boolean isRelationRename()
boolean isBVSignExtension()
boolean isProofCommutativity()
Expr< R > substitute(Expr<?> from, Expr<?> to)
boolean isRelationComplement()
static long[] arrayToNative(Z3Object[] a)
def simplify(a, *arguments, **keywords)
Utils.
def String(name, ctx=None)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Z3_decl_kind
The different kinds of interpreted function kinds.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Z3_lbool
Lifted Boolean type: false, undefined, true.