18 package com.microsoft.z3;
50 return Expr.create(getContext(),
56 p.getNativeObject()));
94 for (
int i = 0; i < n; i++)
95 res[i] =
Expr.create(getContext(),
107 getContext().checkContextMatch(args);
109 throw new Z3Exception(
"Number of arguments does not match");
111 (
int) args.length,
Expr.arrayToNative(args)));
125 getContext().checkContextMatch(from);
126 getContext().checkContextMatch(to);
127 if (from.length != to.length)
128 throw new Z3Exception(
"Argument sizes do not match");
130 getNativeObject(), (
int) from.length,
Expr.arrayToNative(from),
131 Expr.arrayToNative(to)));
153 getContext().checkContextMatch(to);
155 getNativeObject(), (
int) to.length,
Expr.arrayToNative(to)));
168 if (getContext() == ctx)
182 return super.toString();
208 return Sort.create(getContext(),
717 boolean IsBVUDiv0() throws Z3Exception
725 boolean IsBVSRem0() throws Z3Exception
733 boolean IsBVURem0() throws Z3Exception
741 boolean IsBVSMod0() throws Z3Exception
822 public boolean isBVOR() throws Z3Exception
1058 public boolean isOEQ() throws Z3Exception
1730 throw new Z3Exception(
"Term is not a bound variable.");
1755 void checkNativeObject(
long obj)
throws Z3Exception
1760 throw new Z3Exception(
"Underlying object is not a term");
1761 super.checkNativeObject(obj);
1764 static Expr create(Context ctx, FuncDecl f,
Expr ... arguments)
1767 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
1768 AST.arrayLength(arguments), AST.arrayToNative(arguments));
1769 return create(ctx, obj);
1772 static Expr create(Context ctx,
long obj)
throws Z3Exception
1776 return new Quantifier(ctx, obj);
1777 long s = Native.getSort(ctx.nCtx(), obj);
1779 .fromInt(Native.getSortKind(ctx.nCtx(), s));
1781 if (Native.isAlgebraicNumber(ctx.nCtx(), obj))
1782 return new AlgebraicNum(ctx, obj);
1784 if (Native.isNumeralAst(ctx.nCtx(), obj))
1789 return new IntNum(ctx, obj);
1791 return new RatNum(ctx, obj);
1793 return new BitVecNum(ctx, obj);
1803 return new IntExpr(ctx, obj);
1805 return new RealExpr(ctx, obj);
1807 return new BitVecExpr(ctx, obj);
1809 return new ArrayExpr(ctx, obj);
1811 return new DatatypeExpr(ctx, obj);
1815 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 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_decl_kind
The different kinds of interpreted function kinds.
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)