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)));
206 return super.toString();
237 return Sort.create(getContext(),
2117 throw new Z3Exception(
"Term is not a bound variable.");
2132 void checkNativeObject(
long obj) {
2136 throw new Z3Exception(
"Underlying object is not a term");
2138 super.checkNativeObject(obj);
2141 static Expr create(Context ctx, FuncDecl f,
Expr ... arguments)
2144 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
2145 AST.arrayLength(arguments), AST.arrayToNative(arguments));
2146 return create(ctx, obj);
2149 static Expr create(Context ctx,
long obj)
2153 return new Quantifier(ctx, obj);
2154 long s = Native.getSort(ctx.nCtx(), obj);
2156 .fromInt(Native.getSortKind(ctx.nCtx(), s));
2158 if (Native.isAlgebraicNumber(ctx.nCtx(), obj))
2159 return new AlgebraicNum(ctx, obj);
2161 if (Native.isNumeralAst(ctx.nCtx(), obj))
2166 return new IntNum(ctx, obj);
2168 return new RatNum(ctx, obj);
2170 return new BitVecNum(ctx, obj);
2172 return new FPNum(ctx, obj);
2174 return new FPRMNum(ctx, obj);
2176 return new FiniteDomainNum(ctx, obj);
2184 return new BoolExpr(ctx, obj);
2186 return new IntExpr(ctx, obj);
2188 return new RealExpr(ctx, obj);
2190 return new BitVecExpr(ctx, obj);
2192 return new ArrayExpr(ctx, obj);
2194 return new DatatypeExpr(ctx, obj);
2196 return new FPExpr(ctx, obj);
2198 return new FPRMExpr(ctx, obj);
2200 return new FiniteDomainExpr(ctx, obj);
2202 return new SeqExpr(ctx, obj);
2204 return new ReExpr(ctx, obj);
2208 return new Expr(ctx, obj);
boolean isEmptyRelation()
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
static int getBoolValue(long a0, long a1)
boolean isProofTransitivityStar()
boolean isProofModusPonens()
boolean isSetComplement()
boolean isProofElimUnusedVars()
boolean isProofMonotonicity()
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()
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
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 String getString(long a0, long a1)
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()
static boolean isString(long a0, long a1)
boolean isBVRotateRightExtended()
Z3_decl_kind
The different kinds of interpreted function kinds.
Z3_OP_PR_TRANSITIVITY_STAR
boolean isProofTheoryLemma()
static boolean isAlgebraicNumber(long a0, long a1)
def String(name, ctx=None)
static final Z3_lbool fromInt(int v)