18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21import com.microsoft.z3.enumerations.Z3_decl_kind;
22import com.microsoft.z3.enumerations.Z3_lbool;
23import com.microsoft.z3.enumerations.Z3_sort_kind;
55 return Expr.create(getContext(),
62 p.getNativeObject()));
109 for (
int i = 0; i < n; i++) {
110 res[i] =
Expr.create(getContext(),
125 getContext().checkContextMatch(args);
127 throw new Z3Exception(
"Number of arguments does not match");
130 args.length,
Expr.arrayToNative(args)));
147 getContext().checkContextMatch(from);
148 getContext().checkContextMatch(to);
149 if (from.length != to.length) {
150 throw new Z3Exception(
"Argument sizes do not match");
153 getNativeObject(), from.length,
Expr.arrayToNative(from),
154 Expr.arrayToNative(to)));
182 getContext().checkContextMatch(to);
184 getNativeObject(), to.length,
Expr.arrayToNative(to)));
206 return super.toString();
237 return Sort.create(getContext(),
1869 .getSortKind(getContext().nCtx(),
2050 .getSortKind(getContext().nCtx(),
2086 throw new Z3Exception(
"Term is not a bound variable.");
2101 void checkNativeObject(
long obj) {
2105 throw new Z3Exception(
"Underlying object is not a term");
2107 super.checkNativeObject(obj);
2110 static Expr create(Context ctx, FuncDecl f,
Expr ... arguments)
2113 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2114 AST.arrayLength(arguments), AST.arrayToNative(arguments));
2115 return create(ctx, obj);
2118 static Expr create(Context ctx,
long obj)
2122 return new Quantifier(ctx, obj);
2123 long s = Native.getSort(ctx.nCtx(), obj);
2125 .fromInt(Native.getSortKind(ctx.nCtx(), s));
2127 if (Native.isAlgebraicNumber(ctx.nCtx(), obj))
2128 return new AlgebraicNum(ctx, obj);
2130 if (Native.isNumeralAst(ctx.nCtx(), obj))
2135 return new IntNum(ctx, obj);
2137 return new RatNum(ctx, obj);
2139 return new BitVecNum(ctx, obj);
2141 return new FPNum(ctx, obj);
2143 return new FPRMNum(ctx, obj);
2145 return new FiniteDomainNum(ctx, obj);
2153 return new BoolExpr(ctx, obj);
2155 return new IntExpr(ctx, obj);
2157 return new RealExpr(ctx, obj);
2159 return new BitVecExpr(ctx, obj);
2161 return new ArrayExpr(ctx, obj);
2163 return new DatatypeExpr(ctx, obj);
2165 return new FPExpr(ctx, obj);
2167 return new FPRMExpr(ctx, obj);
2169 return new FiniteDomainExpr(ctx, obj);
2171 return new SeqExpr(ctx, obj);
2173 return new ReExpr(ctx, obj);
2177 return new Expr(ctx, obj);
Expr substituteVars(Expr[] to)
boolean isConstantArray()
Expr(Context ctx, long obj)
boolean isProofHypothesis()
boolean isProofTransitivityStar()
boolean isProofAsserted()
boolean isBVRotateRightExtended()
boolean isRelationFilter()
boolean isEmptyRelation()
Expr substitute(Expr from, Expr to)
boolean isRelationalJoin()
boolean isProofApplyDef()
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()
Expr translate(Context ctx)
boolean isBVZeroExtension()
boolean isAlgebraicNumber()
boolean isSetDifference()
boolean isProofAndElimination()
boolean isProofDefIntro()
boolean isBVRotateRight()
boolean isSetComplement()
boolean isArithmeticNumeral()
boolean isBVShiftRightArithmetic()
boolean isFiniteDomainLT()
boolean isIsEmptyRelation()
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 substitute(Expr[] from, Expr[] to)
boolean isRelationComplement()
Z3_decl_kind getDeclKind()
static long getAppDecl(long a0, long a1)
static boolean isNumeralAst(long a0, long a1)
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
static int getAppNumArgs(long a0, long a1)
static int getSortKind(long a0, long a1)
static long updateTerm(long a0, long a1, int a2, long[] a3)
static long simplify(long a0, long a1)
static boolean isAlgebraicNumber(long a0, long a1)
static int getAstKind(long a0, long a1)
static boolean isString(long a0, long a1)
static boolean isApp(long a0, long a1)
static boolean isWellSorted(long a0, long a1)
static String getString(long a0, long a1)
static long mkBoolSort(long a0)
static long simplifyEx(long a0, long a1, long a2)
static long getAppArg(long a0, long a1, int a2)
static long substituteVars(long a0, long a1, int a2, long[] a3)
static long getSort(long a0, long a1)
static int getBoolValue(long a0, long a1)
static boolean isEqSort(long a0, long a1, long a2)
static int getIndexValue(long a0, long a1)
Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_MODUS_PONENS_OEQ
static final Z3_lbool fromInt(int v)
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).