18 package com.microsoft.z3;
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)));
197 if (getContext() == ctx) {
213 return super.toString();
244 return Sort.create(getContext(),
2095 throw new Z3Exception(
"Term is not a bound variable.");
2110 void checkNativeObject(
long obj) {
2114 throw new Z3Exception(
"Underlying object is not a term");
2116 super.checkNativeObject(obj);
2122 long obj =
Native.
mkApp(ctx.nCtx(), f.getNativeObject(),
2123 AST.arrayLength(arguments),
AST.arrayToNative(arguments));
2124 return create(ctx, obj);
2144 return new IntNum(ctx, obj);
2146 return new RatNum(ctx, obj);
2150 return new FPNum(ctx, obj);
2174 return new FPExpr(ctx, obj);
2182 return new ReExpr(ctx, obj);
2186 return new Expr(ctx, obj);
boolean isEmptyRelation()
static int getBoolValue(long a0, long a1)
boolean isProofTransitivityStar()
boolean isProofModusPonens()
static long mkApp(long a0, long a1, int a2, long[] a3)
boolean isSetComplement()
boolean isProofElimUnusedVars()
boolean isProofMonotonicity()
static final Z3_ast_kind fromInt(int v)
static int getSortKind(long a0, long a1)
static final Z3_sort_kind fromInt(int v)
static int getAppNumArgs(long a0, long a1)
boolean isRelationSelect()
boolean isRelationStore()
boolean isBVRotateLeftExtended()
boolean isBVZeroExtension()
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
boolean isProofSkolemize()
boolean isConstantArray()
boolean isProofReflexivity()
boolean isProofIFFFalse()
boolean isBVShiftRightArithmetic()
boolean isProofPullQuantStar()
static long updateTerm(long a0, long a1, int a2, long[] a3)
static boolean isWellSorted(long a0, long a1)
boolean isBVRotateRight()
boolean isRelationProject()
boolean isProofCommutativity()
static boolean isNumeralAst(long a0, long a1)
boolean isRelationNegationFilter()
boolean isProofAndElimination()
static int getIndexValue(long a0, long a1)
Expr substitute(Expr from, Expr to)
boolean isSetDifference()
boolean isAlgebraicNumber()
boolean isRelationRename()
boolean isProofRewriteStar()
boolean isProofPushQuant()
boolean isRelationClone()
boolean isProofPullQuant()
boolean isRelationUnion()
boolean isProofHypothesis()
Z3_decl_kind getDeclKind()
boolean isRelationFilter()
boolean isProofTransitivity()
static long simplifyEx(long a0, long a1, long a2)
Z3_OP_PR_ELIM_UNUSED_VARS
boolean isProofOrElimination()
boolean isProofUnitResolution()
boolean isBVSignExtension()
boolean isBVShiftRightLogical()
Expr translate(Context ctx)
static boolean isApp(long a0, long a1)
static boolean isEqSort(long a0, long a1, long a2)
static long getAppArg(long a0, long a1, int a2)
boolean isRelationWiden()
boolean isProofDefIntro()
boolean isProofSymmetry()
boolean isFiniteDomainLT()
boolean isProofQuantIntro()
Z3_OP_PR_MODUS_PONENS_OEQ
static int getAstKind(long a0, long a1)
Expr substituteVars(Expr[] to)
boolean isProofModusPonensOEQ()
boolean isProofDefAxiom()
static long simplify(long a0, long a1)
boolean isProofDistributivity()
static long getAppDecl(long a0, long a1)
boolean isIsEmptyRelation()
boolean isArithmeticNumeral()
boolean isProofQuantInst()
boolean isRelationalJoin()
boolean isRelationComplement()
Expr(Context ctx, long obj)
static long mkBoolSort(long a0)
static long getSort(long a0, long a1)
Expr substitute(Expr[] from, Expr[] to)
static long substituteVars(long a0, long a1, int a2, long[] a3)
boolean isProofApplyDef()
boolean isProofAsserted()
boolean isBVRotateRightExtended()
Z3_OP_PR_TRANSITIVITY_STAR
boolean isProofTheoryLemma()
static long translate(long a0, long a1, long a2)
static boolean isAlgebraicNumber(long a0, long a1)
def String(name, ctx=None)
static final Z3_lbool fromInt(int v)