Expr.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.lang.reflect.Type;
import java.lang.reflect.ParameterizedType;
 
import com.microsoft.z3.enumerations.Z3_ast_kind;
import com.microsoft.z3.enumerations.Z3_decl_kind;
import com.microsoft.z3.enumerations.Z3_lbool;
import com.microsoft.z3.enumerations.Z3_sort_kind;
 
/* using System; */
 
@SuppressWarnings("unchecked")
public class Expr<R extends Sort> extends AST
{
    public Expr<R> simplify()
    {
        return simplify(null);
    }
 
    public Expr<R> simplify(Params p)
    {
 
        if (p == null) {
            return (Expr<R>) Expr.create(getContext(),
                Native.simplify(getContext().nCtx(), getNativeObject()));
        }
        else {
            return (Expr<R>) Expr.create(
                getContext(),
                Native.simplifyEx(getContext().nCtx(), getNativeObject(),
                    p.getNativeObject()));
        }
    }
 
    public FuncDecl<R> getFuncDecl()
    {
        return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(),
                getNativeObject()));
    }
 
    public Z3_lbool getBoolValue()
    {
        return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
                getNativeObject()));
    }
 
    public int getNumArgs()
    {
        return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
    }
 
    public Expr<?>[] getArgs()
    {
        int n = getNumArgs();
        Expr<?>[] res = new Expr[n];
        for (int i = 0; i < n; i++) {
            res[i] = Expr.create(getContext(),
                Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
        }
        return res;
    }
 
    public Expr<R> update(Expr<?>[] args)
    {
        getContext().checkContextMatch(args);
        if (isApp() && args.length != getNumArgs()) {
            throw new Z3Exception("Number of arguments does not match");
        }
        return (Expr<R>) Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
                args.length, Expr.arrayToNative(args)));
    }
 
    public Expr<R> substitute(Expr<?>[] from, Expr<?>[] to)
    {
        getContext().checkContextMatch(from);
        getContext().checkContextMatch(to);
        if (from.length != to.length) {
            throw new Z3Exception("Argument sizes do not match");
        }
        return (Expr<R>) Expr.create(getContext(), Native.substitute(getContext().nCtx(),
                getNativeObject(), from.length, Expr.arrayToNative(from),
                Expr.arrayToNative(to)));
    }
 
    public Expr<R> substitute(Expr<?> from, Expr<?> to)
    {
        return substitute(new Expr[] { from }, new Expr[] { to });
    }
 
    public Expr<R> substituteVars(Expr<?>[] to)
    {
 
        getContext().checkContextMatch(to);
        return (Expr<R>) Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
                getNativeObject(), to.length, Expr.arrayToNative(to)));
    }
 
    public Expr<R> substituteFuns(FuncDecl<?>[] from, Expr<?>[] to)
    {
        getContext().checkContextMatch(from);
        getContext().checkContextMatch(to);
        if (from.length != to.length) {
            throw new Z3Exception("Arrays 'from' and 'to' must have the same length");
        }
        return (Expr<R>) Expr.create(getContext(), Native.substituteFuns(getContext().nCtx(),
                getNativeObject(), from.length, AST.arrayToNative(from),
                Expr.arrayToNative(to)));
    }
 
    public Expr<R> translate(Context ctx)
    {
        return (Expr<R>) super.translate(ctx);
    }
 
    @Override
    public String toString()
    {
        return super.toString();
    }
 
    public boolean isNumeral()
    {
        return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
    }
 
    public double getNumeralDouble()
    {
        return Native.getNumeralDouble(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isWellSorted()
    {
        return Native.isWellSorted(getContext().nCtx(), getNativeObject());
    }
 
    public R getSort()
    {
        return (R) Sort.create(getContext(),
                Native.getSort(getContext().nCtx(), getNativeObject()));
    }
 
    public boolean isConst()
    {
        return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
    }
 
    public boolean isIntNum()
    {
        return isNumeral() && isInt();
    }
 
    public boolean isRatNum()
    {
        return isNumeral() && isReal();
    }
 
    public boolean isAlgebraicNumber()
    {
        return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isGround()
    {
        return Native.isGround(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isLambda()
    {
        return Native.isLambda(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isBool()
    {
        return (isExpr() && Native.isEqSort(getContext().nCtx(),
                Native.mkBoolSort(getContext().nCtx()),
                Native.getSort(getContext().nCtx(), getNativeObject())));
    }
 
    public boolean isTrue()
    {
            return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
    }
 
    public boolean isFalse()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
    }
 
    public boolean isEq()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
    }
 
    public boolean isDistinct()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
    }
 
    public boolean isITE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
    }
 
    public boolean isAnd()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
    }
 
    public boolean isOr()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
    }
 
    public boolean isIff()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
    }
 
    public boolean isXor()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
    }
 
    public boolean isNot()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
    }
 
    public boolean isImplies()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
    }
 
    public boolean isInt()
    {
        return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
    }
 
    public boolean isReal()
    {
        return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
    }
 
    public boolean isArithmeticNumeral()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
    }
 
    public boolean isLE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
    }
 
    public boolean isGE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
    }
 
    public boolean isLT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
    }
 
    public boolean isGT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
    }
 
    public boolean isAdd()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
    }
 
    public boolean isSub()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
    }
 
    public boolean isUMinus()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
    }
 
    public boolean isMul()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
    }
 
    public boolean isDiv()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
    }
 
    public boolean isIDiv()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
    }
 
    public boolean isRemainder()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
    }
 
    public boolean isModulus()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
    }
 
    public boolean isIntToReal()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
    }
 
    public boolean isRealToInt()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
    }
 
    public boolean isRealIsInt()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
    }
 
    public boolean isArray()
    {
        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
                .fromInt(Native.getSortKind(getContext().nCtx(),
                        Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
    }
 
    public boolean isStore()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
    }
 
    public boolean isSelect()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
    }
 
    public boolean isConstantArray()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
    }
 
    public boolean isDefaultArray()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
    }
 
    public boolean isArrayMap()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
    }
 
    public boolean isAsArray()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
    }
 
    public boolean isSetUnion()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
    }
 
    public boolean isSetIntersect()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
    }
 
    public boolean isSetDifference()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
    }
 
    public boolean isSetComplement()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
    }
 
    public boolean isSetSubset()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
    }
 
    public boolean isBV()
    {
        return Native.getSortKind(getContext().nCtx(),
                Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
                .toInt();
    }
 
    public boolean isBVNumeral()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
    }
 
    public boolean isBVBitOne()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
    }
 
    public boolean isBVBitZero()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
    }
 
    public boolean isBVUMinus()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
    }
 
    public boolean isBVAdd()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
    }
 
    public boolean isBVSub()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
    }
 
    public boolean isBVMul()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
    }
 
    public boolean isBVSDiv()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
    }
 
    public boolean isBVUDiv()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
    }
 
    public boolean isBVSRem()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
    }
 
    public boolean isBVURem()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
    }
 
    public boolean isBVSMod()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
    }
 
    boolean isBVSDiv0()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
    }
 
    boolean isBVUDiv0()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
    }
 
    boolean isBVSRem0()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
    }
 
    boolean isBVURem0()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
    }
 
    boolean isBVSMod0()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
    }
 
    public boolean isBVULE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
    }
 
    public boolean isBVSLE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
    }
 
    public boolean isBVUGE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
    }
 
    public boolean isBVSGE()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
    }
 
    public boolean isBVULT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
    }
 
    public boolean isBVSLT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
    }
 
    public boolean isBVUGT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
    }
 
    public boolean isBVSGT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
    }
 
    public boolean isBVAND()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
    }
 
    public boolean isBVOR()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
    }
 
    public boolean isBVNOT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
    }
 
    public boolean isBVXOR()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
    }
 
    public boolean isBVNAND()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
    }
 
    public boolean isBVNOR()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
    }
 
    public boolean isBVXNOR()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
    }
 
    public boolean isBVConcat()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
    }
 
    public boolean isBVSignExtension()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
    }
 
    public boolean isBVZeroExtension()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
    }
 
    public boolean isBVExtract()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
    }
 
    public boolean isBVRepeat()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
    }
 
    public boolean isBVReduceOR()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
    }
 
    public boolean isBVReduceAND()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
    }
 
    public boolean isBVComp()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
    }
 
    public boolean isBVShiftLeft()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
    }
 
    public boolean isBVShiftRightLogical()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
    }
 
    public boolean isBVShiftRightArithmetic()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
    }
 
    public boolean isBVRotateLeft()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
    }
 
    public boolean isBVRotateRight()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
    }
 
    public boolean isBVRotateLeftExtended()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
    }
 
    public boolean isBVRotateRightExtended()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
    }
 
    public boolean isIntToBV()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
    }
 
    public boolean isBVToInt()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
    }
 
    public boolean isBVCarry()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
    }
 
    public boolean isBVXOR3()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
    }
 
    public boolean isLabel()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
    }
 
    public boolean isLabelLit()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
    }
 
    public boolean isString() 
    {
        return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
    }
 
    public String getString()
    {
        return Native.getString(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isConcat() 
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT;
    }
 
    public boolean isOEQ()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
    }
 
    public boolean isProofTrue()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
    }
 
    public boolean isProofAsserted()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
    }
 
    public boolean isProofGoal()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
    }
 
    public boolean isProofModusPonens()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
    }
 
    public boolean isProofReflexivity()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
    }
 
    public boolean isProofSymmetry()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
    }
 
    public boolean isProofTransitivity()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
    }
 
    public boolean isProofTransitivityStar()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
    }
 
    public boolean isProofMonotonicity()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
    }
 
    public boolean isProofQuantIntro()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
    }
 
    public boolean isProofDistributivity()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
    }
 
    public boolean isProofAndElimination()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
    }
 
    public boolean isProofOrElimination()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
    }
 
    public boolean isProofRewrite()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
    }
 
    public boolean isProofRewriteStar()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
    }
 
    public boolean isProofPullQuant()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
    }
 
 
    public boolean isProofPushQuant()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
    }
 
    public boolean isProofElimUnusedVars()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
    }
 
    public boolean isProofDER()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
    }
 
    public boolean isProofQuantInst()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
    }
 
    public boolean isProofHypothesis()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
    }
 
    public boolean isProofLemma()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
    }
 
    public boolean isProofUnitResolution()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
    }
 
    public boolean isProofIFFTrue()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
    }
 
    public boolean isProofIFFFalse()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
    }
 
    public boolean isProofCommutativity()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
    }
 
    public boolean isProofDefAxiom()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
    }
 
    public boolean isProofDefIntro()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
    }
 
    public boolean isProofApplyDef()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
    }
 
    public boolean isProofIFFOEQ()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
    }
 
    public boolean isProofNNFPos()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
    }
 
    public boolean isProofNNFNeg()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
    }
 
 
    public boolean isProofSkolemize()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
    }
 
    public boolean isProofModusPonensOEQ()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
    }
 
    public boolean isProofTheoryLemma()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
    }
 
    public boolean isRelation()
    {
        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
                .getSortKind(getContext().nCtx(),
                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
                .toInt());
    }
 
    public boolean isRelationStore()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
    }
 
    public boolean isEmptyRelation()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
    }
 
    public boolean isIsEmptyRelation()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
    }
 
    public boolean isRelationalJoin()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
    }
 
    public boolean isRelationUnion()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
    }
 
    public boolean isRelationWiden()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
    }
 
    public boolean isRelationProject()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
    }
 
    public boolean isRelationFilter()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
    }
 
    public boolean isRelationNegationFilter()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
    }
 
    public boolean isRelationRename()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
    }
 
    public boolean isRelationComplement()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
    }
 
    public boolean isRelationSelect()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
    }
 
    public boolean isRelationClone()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
    }
 
    public boolean isFiniteDomain()
    {
        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
                .getSortKind(getContext().nCtx(),
                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
                .toInt());
    }
 
    public boolean isFiniteDomainLT()
    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
    }
 
    public int getIndex()
    {
        if (!isVar()) {
            throw new Z3Exception("Term is not a bound variable.");
        }
 
        return Native.getIndexValue(getContext().nCtx(), getNativeObject());
    }
 
    private Class sort = null;
 
    public <S extends R> Expr<S> distillSort(Class<S> newSort) {
        if (sort != null && !newSort.isAssignableFrom(sort)) {
            throw new Z3Exception(
                    String.format("Cannot distill expression of sort %s to %s.", sort.getName(), newSort.getName()));
        }
 
        return (Expr<S>) ((Expr<?>) this);
    }
 
    protected Expr(Context ctx, long obj) {
        super(ctx, obj);
        Type superclass = getClass().getGenericSuperclass();
        if (superclass instanceof ParameterizedType) {
            Type argType = ((ParameterizedType) superclass).getActualTypeArguments()[0];
            if (argType instanceof Class) {
                this.sort = (Class) argType;
            }
        }
    }
 
    @Override
    void checkNativeObject(long obj) {
        if (!Native.isApp(getContext().nCtx(), obj) && 
            Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
            Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
            throw new Z3Exception("Underlying object is not a term");
        }
        super.checkNativeObject(obj);
    }
 
    static <U extends Sort> Expr<U> create(Context ctx, FuncDecl<U> f, Expr<?> ... arguments)
    {
        long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
                AST.arrayLength(arguments), AST.arrayToNative(arguments));
        return (Expr<U>) create(ctx, obj);
    }
 
    // TODO generify, but it conflicts with AST.create
    static Expr<?> create(Context ctx, long obj)
    {
        Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
        if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) {
                        // a quantifier AST is a lambda iff it is neither a forall nor an exists. 
            boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
            if (isLambda) {
               return new Lambda(ctx, obj);
            } else {
               return new Quantifier(ctx, obj);
            }
                }
        long s = Native.getSort(ctx.nCtx(), obj);
        Z3_sort_kind sk = Z3_sort_kind
                .fromInt(Native.getSortKind(ctx.nCtx(), s));
 
        if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
            return new AlgebraicNum(ctx, obj);
 
        if (Native.isNumeralAst(ctx.nCtx(), obj))
        {
            switch (sk)
            {
            case Z3_INT_SORT:
                return new IntNum(ctx, obj);
            case Z3_REAL_SORT:
                return new RatNum(ctx, obj);
            case Z3_BV_SORT:
                return new BitVecNum(ctx, obj);
            case Z3_FLOATING_POINT_SORT:
                return new FPNum(ctx, obj);
            case Z3_ROUNDING_MODE_SORT:
                return new FPRMNum(ctx, obj);
            case Z3_FINITE_DOMAIN_SORT:
                return new FiniteDomainNum(ctx, obj);
            default:
            }
        }
 
        switch (sk)
        {
        case Z3_BOOL_SORT:
            return new BoolExpr(ctx, obj);
        case Z3_INT_SORT:
            return new IntExpr(ctx, obj);
        case Z3_REAL_SORT:
            return new RealExpr(ctx, obj);
        case Z3_BV_SORT:
            return new BitVecExpr(ctx, obj);
        case Z3_ARRAY_SORT:
            return new ArrayExpr<>(ctx, obj);
        case Z3_DATATYPE_SORT:
            return new DatatypeExpr<>(ctx, obj);
        case Z3_FLOATING_POINT_SORT:
            return new FPExpr(ctx, obj);
        case Z3_ROUNDING_MODE_SORT:
            return new FPRMExpr(ctx, obj);
        case Z3_FINITE_DOMAIN_SORT:
            return new FiniteDomainExpr(ctx, obj);
        case Z3_SEQ_SORT:
            return new SeqExpr<>(ctx, obj);
        case Z3_RE_SORT:
            return new ReExpr<>(ctx, obj);
        default:
        }
 
        return new Expr<>(ctx, obj);
    }
}