Go to the documentation of this file.
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");
147 getContext().checkContextMatch(from);
148 getContext().checkContextMatch(to);
149 if (from.length != to.length) {
150 throw new Z3Exception(
"Argument sizes do not match");
182 getContext().checkContextMatch(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);
Z3_OP_PR_TRANSITIVITY_STAR
static long getAppArg(long a0, long a1, int a2)
static int getSortKind(long a0, long a1)
static String getString(long a0, long a1)
boolean isProofQuantIntro()
boolean isProofApplyDef()
boolean isArithmeticNumeral()
boolean isProofAndElimination()
static long updateTerm(long a0, long a1, int a2, long[] a3)
boolean isProofTransitivityStar()
static long substituteVars(long a0, long a1, int a2, long[] a3)
Expr substitute(Expr[] from, Expr[] to)
static int getAppNumArgs(long a0, long a1)
static boolean isAlgebraicNumber(long a0, long a1)
Z3_OP_PR_ELIM_UNUSED_VARS
static final Z3_lbool fromInt(int v)
static boolean isWellSorted(long a0, long a1)
boolean isRelationFilter()
boolean isProofDefIntro()
boolean isSetComplement()
boolean isProofPushQuant()
static boolean isNumeralAst(long a0, long a1)
boolean isProofTransitivity()
static long simplify(long a0, long a1)
boolean isBVZeroExtension()
boolean isBVRotateLeftExtended()
boolean isProofSkolemize()
boolean isBVShiftRightLogical()
boolean isProofAsserted()
boolean isProofModusPonens()
boolean isAlgebraicNumber()
boolean isProofIFFFalse()
boolean isRelationRename()
static long getSort(long a0, long a1)
boolean isProofMonotonicity()
boolean isBVRotateRight()
boolean isEmptyRelation()
boolean isSetDifference()
boolean isRelationProject()
boolean isRelationClone()
boolean isRelationalJoin()
boolean isProofElimUnusedVars()
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
boolean isProofOrElimination()
Expr translate(Context ctx)
boolean isProofModusPonensOEQ()
static long mkBoolSort(long a0)
static long getAppDecl(long a0, long a1)
static int getBoolValue(long a0, long a1)
Expr substitute(Expr from, Expr to)
static long simplifyEx(long a0, long a1, long a2)
boolean isBVSignExtension()
boolean isProofQuantInst()
boolean isProofUnitResolution()
boolean isFiniteDomainLT()
static boolean isString(long a0, long a1)
static int getAstKind(long a0, long a1)
boolean isIsEmptyRelation()
boolean isProofReflexivity()
boolean isProofCommutativity()
boolean isRelationNegationFilter()
boolean isRelationUnion()
boolean isRelationComplement()
Expr(Context ctx, long obj)
boolean isProofPullQuant()
boolean isRelationStore()
static int getIndexValue(long a0, long a1)
static boolean isApp(long a0, long a1)
boolean isProofDistributivity()
boolean isBVShiftRightArithmetic()
boolean isBVRotateRightExtended()
boolean isProofSymmetry()
boolean isProofHypothesis()
Z3_decl_kind getDeclKind()
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
boolean isProofRewriteStar()
static long[] arrayToNative(Z3Object[] a)
boolean isProofTheoryLemma()
Z3_decl_kind
The different kinds of interpreted function kinds.
boolean isConstantArray()
Expr substituteVars(Expr[] to)
Z3_OP_PR_MODUS_PONENS_OEQ
boolean isProofDefAxiom()
boolean isRelationWiden()
boolean isRelationSelect()
static boolean isEqSort(long a0, long a1, long a2)
def String(name, ctx=None)