18 package com.microsoft.z3;
57 return Expr.create(getContext(),
63 p.getNativeObject()));
109 for (
int i = 0; i < n; i++)
110 res[i] =
Expr.create(getContext(),
124 getContext().checkContextMatch(args);
126 throw new Z3Exception(
"Number of arguments does not match");
128 (
int) args.length,
Expr.arrayToNative(args)));
145 getContext().checkContextMatch(from);
146 getContext().checkContextMatch(to);
147 if (from.length != to.length)
148 throw new Z3Exception(
"Argument sizes do not match");
150 getNativeObject(), (
int) from.length,
Expr.arrayToNative(from),
151 Expr.arrayToNative(to)));
180 getContext().checkContextMatch(to);
182 getNativeObject(), (
int) to.length,
Expr.arrayToNative(to)));
197 if (getContext() == ctx)
211 return super.toString();
243 return Sort.create(getContext(),
2099 throw new Z3Exception(
"Term is not a bound variable.");
2125 void checkNativeObject(
long obj)
2130 throw new Z3Exception(
"Underlying object is not a term");
2131 super.checkNativeObject(obj);
2137 long obj =
Native.
mkApp(ctx.nCtx(), f.getNativeObject(),
2138 AST.arrayLength(arguments),
AST.arrayToNative(arguments));
2139 return create(ctx, obj);
2159 return new IntNum(ctx, obj);
2161 return new RatNum(ctx, obj);
2165 return new FPNum(ctx, obj);
2187 return new FPExpr(ctx, obj);
2193 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)
static final Z3_lbool fromInt(int v)