Inheritance diagram for Expr< R extends Sort >:

Public Member Functions
Expr< R >	simplify ()

Expr< R >	simplify (Params p)

FuncDecl< R >	getFuncDecl ()

Z3_lbool	getBoolValue ()

int	getNumArgs ()

Expr<?>[]	getArgs ()

Expr< R >	update (Expr<?>[] args)

Expr< R >	substitute (Expr<?>[] from, Expr<?>[] to)

Expr< R >	substitute (Expr<?> from, Expr<?> to)

Expr< R >	substituteVars (Expr<?>[] to)

Expr< R >	substituteFuns (FuncDecl<?>[] from, Expr<?>[] to)

Expr< R >	translate (Context ctx)

String	toString ()

boolean	isNumeral ()

double	getNumeralDouble ()

boolean	isWellSorted ()

R	getSort ()

boolean	isConst ()

boolean	isIntNum ()

boolean	isRatNum ()

boolean	isAlgebraicNumber ()

boolean	isGround ()

boolean	isLambda ()

boolean	isBool ()

boolean	isTrue ()

boolean	isFalse ()

boolean	isEq ()

boolean	isDistinct ()

boolean	isITE ()

boolean	isAnd ()

boolean	isOr ()

boolean	isIff ()

boolean	isXor ()

boolean	isNot ()

boolean	isImplies ()

boolean	isInt ()

boolean	isReal ()

boolean	isArithmeticNumeral ()

boolean	isLE ()

boolean	isGE ()

boolean	isLT ()

boolean	isGT ()

boolean	isAdd ()

boolean	isSub ()

boolean	isUMinus ()

boolean	isMul ()

boolean	isDiv ()

boolean	isIDiv ()

boolean	isRemainder ()

boolean	isModulus ()

boolean	isIntToReal ()

boolean	isRealToInt ()

boolean	isRealIsInt ()

boolean	isArray ()

boolean	isStore ()

boolean	isSelect ()

boolean	isConstantArray ()

boolean	isDefaultArray ()

boolean	isArrayMap ()

boolean	isAsArray ()

boolean	isSetUnion ()

boolean	isSetIntersect ()

boolean	isSetDifference ()

boolean	isSetComplement ()

boolean	isSetSubset ()

boolean	isBV ()

boolean	isBVNumeral ()

boolean	isBVBitOne ()

boolean	isBVBitZero ()

boolean	isBVUMinus ()

boolean	isBVAdd ()

boolean	isBVSub ()

boolean	isBVMul ()

boolean	isBVSDiv ()

boolean	isBVUDiv ()

boolean	isBVSRem ()

boolean	isBVURem ()

boolean	isBVSMod ()

boolean	isBVULE ()

boolean	isBVSLE ()

boolean	isBVUGE ()

boolean	isBVSGE ()

boolean	isBVULT ()

boolean	isBVSLT ()

boolean	isBVUGT ()

boolean	isBVSGT ()

boolean	isBVAND ()

boolean	isBVOR ()

boolean	isBVNOT ()

boolean	isBVXOR ()

boolean	isBVNAND ()

boolean	isBVNOR ()

boolean	isBVXNOR ()

boolean	isBVConcat ()

boolean	isBVSignExtension ()

boolean	isBVZeroExtension ()

boolean	isBVExtract ()

boolean	isBVRepeat ()

boolean	isBVReduceOR ()

boolean	isBVReduceAND ()

boolean	isBVComp ()

boolean	isBVShiftLeft ()

boolean	isBVShiftRightLogical ()

boolean	isBVShiftRightArithmetic ()

boolean	isBVRotateLeft ()

boolean	isBVRotateRight ()

boolean	isBVRotateLeftExtended ()

boolean	isBVRotateRightExtended ()

boolean	isIntToBV ()

boolean	isBVToInt ()

boolean	isBVCarry ()

boolean	isBVXOR3 ()

boolean	isLabel ()

boolean	isLabelLit ()

boolean	isString ()

String	getString ()

boolean	isConcat ()

boolean	isOEQ ()

boolean	isProofTrue ()

boolean	isProofAsserted ()

boolean	isProofGoal ()

boolean	isProofModusPonens ()

boolean	isProofReflexivity ()

boolean	isProofSymmetry ()

boolean	isProofTransitivity ()

boolean	isProofTransitivityStar ()

boolean	isProofMonotonicity ()

boolean	isProofQuantIntro ()

boolean	isProofDistributivity ()

boolean	isProofAndElimination ()

boolean	isProofOrElimination ()

boolean	isProofRewrite ()

boolean	isProofRewriteStar ()

boolean	isProofPullQuant ()

boolean	isProofPushQuant ()

boolean	isProofElimUnusedVars ()

boolean	isProofDER ()

boolean	isProofQuantInst ()

boolean	isProofHypothesis ()

boolean	isProofLemma ()

boolean	isProofUnitResolution ()

boolean	isProofIFFTrue ()

boolean	isProofIFFFalse ()

boolean	isProofCommutativity ()

boolean	isProofDefAxiom ()

boolean	isProofDefIntro ()

boolean	isProofApplyDef ()

boolean	isProofIFFOEQ ()

boolean	isProofNNFPos ()

boolean	isProofNNFNeg ()

boolean	isProofSkolemize ()

boolean	isProofModusPonensOEQ ()

boolean	isProofTheoryLemma ()

boolean	isRelation ()

boolean	isRelationStore ()

boolean	isEmptyRelation ()

boolean	isIsEmptyRelation ()

boolean	isRelationalJoin ()

boolean	isRelationUnion ()

boolean	isRelationWiden ()

boolean	isRelationProject ()

boolean	isRelationFilter ()

boolean	isRelationNegationFilter ()

boolean	isRelationRename ()

boolean	isRelationComplement ()

boolean	isRelationSelect ()

boolean	isRelationClone ()

boolean	isFiniteDomain ()

boolean	isFiniteDomainLT ()

int	getIndex ()

Public Member Functions inherited from AST
boolean	equals (Object o)

int	compareTo (AST other)

int	hashCode ()

int	getId ()

int	getDepth ()

Z3_ast_kind	getASTKind ()

boolean	isExpr ()

boolean	isApp ()

boolean	isVar ()

boolean	isQuantifier ()

boolean	isSort ()

boolean	isFuncDecl ()

String	getSExpr ()

Protected Member Functions
	Expr (Context ctx, long obj)

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)

static int	arrayLength (Z3Object[] a)

Detailed Description

Expressions are terms.

Definition at line 34 of file Expr.java.

Constructor & Destructor Documentation

◆ Expr()

Expr	(	Context	ctx,
		long	obj
	)

inlineprotected

Constructor for Expr

Exceptions

Z3Exception on error

Definition at line 2172 of file Expr.java.

                                          {
        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;
            }
        }
    }

Member Function Documentation

◆ getArgs()

Expr<?>[] getArgs ( )

inline

The arguments of the expression.

Exceptions

Z3Exception on error

Returns: an Expr[]

Definition at line 109 of file Expr.java.

    {
        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;
    }

Referenced by FuncInterp< R extends Sort >.toString().

◆ getBoolValue()

Z3_lbool getBoolValue ( )

inline

Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).

Exceptions

Z3Exception on error

Returns: a Z3_lbool

Definition at line 88 of file Expr.java.

    {
        return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
                getNativeObject()));
    }

◆ getFuncDecl()

FuncDecl< R > getFuncDecl ( )

inline

The function declaration of the function that is applied in this expression.

Returns: a FuncDecl

Exceptions

Z3Exception on error

Definition at line 76 of file Expr.java.

    {
        return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(),
                getNativeObject()));
    }

◆ getIndex()

int getIndex ( )

inline

The de-Bruijn index of a bound variable. Remarks: Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format. abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) abs1(x, x, n) = b_n abs1(y, x, n) = y abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Exceptions

Z3Exception on error

Returns: an int

Definition at line 2140 of file Expr.java.

    {
        if (!isVar()) {
            throw new Z3Exception("Term is not a bound variable.");
        }
 
        return Native.getIndexValue(getContext().nCtx(), getNativeObject());
    }

◆ getNumArgs()

int getNumArgs ( )

inline

The number of arguments of the expression.

Exceptions

Z3Exception on error

Returns: an int

Definition at line 99 of file Expr.java.

    {
        return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
    }

◆ getNumeralDouble()

double getNumeralDouble ( )

inline

Return the numeral value as a double. The expression must be a numeral or an algebraic number.

Definition at line 251 of file Expr.java.

    {
        return Native.getNumeralDouble(getContext().nCtx(), getNativeObject());
    }

◆ getSort()

R getSort ( )

inline

The Sort of the term.

Exceptions

Z3Exception on error

Returns: a sort

Definition at line 272 of file Expr.java.

    {
        return (R) Sort.create(getContext(),
                Native.getSort(getContext().nCtx(), getNativeObject()));
    }

◆ getString()

String getString ( )

inline

Retrieve string corresponding to string constant. Remark: the expression should be a string constant, (isString() should return true).

Exceptions

Z3Exception on error

Returns: a string

Definition at line 1345 of file Expr.java.

    {
        return Native.getString(getContext().nCtx(), getNativeObject());
    }

◆ isAdd()

boolean isAdd ( )

inline

Indicates whether the term is addition (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 537 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
    }

◆ isAlgebraicNumber()

boolean isAlgebraicNumber ( )

inline

Indicates whether the term is an algebraic number

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 313 of file Expr.java.

    {
        return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
    }

◆ isAnd()

boolean isAnd ( )

inline

Indicates whether the term is an n-ary conjunction

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 406 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
    }

◆ isArithmeticNumeral()

boolean isArithmeticNumeral ( )

inline

Indicates whether the term is an arithmetic numeral.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 487 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
    }

◆ isArray()

boolean isArray ( )

inline

Indicates whether the term is of an array sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 648 of file Expr.java.

    {
        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);
    }

◆ isArrayMap()

boolean isArrayMap ( )

inline

Indicates whether the term is an array map. Remarks: It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 705 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
    }

◆ isAsArray()

boolean isAsArray ( )

inline

Indicates whether the term is an as-array term. Remarks: An as-array term * is n array value that behaves as the function graph of the function * passed as parameter.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 716 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
    }

◆ isBool()

boolean isBool ( )

inline

Indicates whether the term has Boolean sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 343 of file Expr.java.

    {
        return (isExpr() && Native.isEqSort(getContext().nCtx(),
                Native.mkBoolSort(getContext().nCtx()),
                Native.getSort(getContext().nCtx(), getNativeObject())));
    }

◆ isBV()

boolean isBV ( )

inline

Indicates whether the terms is of bit-vector sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 776 of file Expr.java.

    {
        return Native.getSortKind(getContext().nCtx(),
                Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
                .toInt();
    }

◆ isBVAdd()

boolean isBVAdd ( )

inline

Indicates whether the term is a bit-vector addition (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 828 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
    }

◆ isBVAND()

boolean isBVAND ( )

inline

Indicates whether the term is a bit-wise AND

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1039 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
    }

◆ isBVBitOne()

boolean isBVBitOne ( )

inline

Indicates whether the term is a one-bit bit-vector with value one

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 798 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
    }

◆ isBVBitZero()

boolean isBVBitZero ( )

inline

Indicates whether the term is a one-bit bit-vector with value zero

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 808 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
    }

◆ isBVCarry()

boolean isBVCarry ( )

inline

Indicates whether the term is a bit-vector carry Remarks: Compute the * carry bit in a full-adder. The meaning is given by the equivalence (carry * l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1288 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
    }

◆ isBVComp()

boolean isBVComp ( )

inline

Indicates whether the term is a bit-vector comparison

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1179 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
    }

◆ isBVConcat()

boolean isBVConcat ( )

inline

Indicates whether the term is a bit-vector concatenation (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1109 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
    }

◆ isBVExtract()

boolean isBVExtract ( )

inline

Indicates whether the term is a bit-vector extraction

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1139 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
    }

◆ isBVMul()

boolean isBVMul ( )

inline

Indicates whether the term is a bit-vector multiplication (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 848 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
    }

◆ isBVNAND()

boolean isBVNAND ( )

inline

Indicates whether the term is a bit-wise NAND

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1079 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
    }

◆ isBVNOR()

boolean isBVNOR ( )

inline

Indicates whether the term is a bit-wise NOR

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1089 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
    }

◆ isBVNOT()

boolean isBVNOT ( )

inline

Indicates whether the term is a bit-wise NOT

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1059 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
    }

◆ isBVNumeral()

boolean isBVNumeral ( )

inline

Indicates whether the term is a bit-vector numeral

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 788 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
    }

◆ isBVOR()

boolean isBVOR ( )

inline

Indicates whether the term is a bit-wise OR

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1049 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
    }

◆ isBVReduceAND()

boolean isBVReduceAND ( )

inline

Indicates whether the term is a bit-vector reduce AND

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1169 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
    }

◆ isBVReduceOR()

boolean isBVReduceOR ( )

inline

Indicates whether the term is a bit-vector reduce OR

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1159 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
    }

◆ isBVRepeat()

boolean isBVRepeat ( )

inline

Indicates whether the term is a bit-vector repetition

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1149 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
    }

◆ isBVRotateLeft()

boolean isBVRotateLeft ( )

inline

Indicates whether the term is a bit-vector rotate left

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1219 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
    }

◆ isBVRotateLeftExtended()

boolean isBVRotateLeftExtended ( )

inline

Indicates whether the term is a bit-vector rotate left (extended) Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1241 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
    }

◆ isBVRotateRight()

boolean isBVRotateRight ( )

inline

Indicates whether the term is a bit-vector rotate right

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1229 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
    }

◆ isBVRotateRightExtended()

boolean isBVRotateRightExtended ( )

inline

Indicates whether the term is a bit-vector rotate right (extended) Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1253 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
    }

◆ isBVSDiv()

boolean isBVSDiv ( )

inline

Indicates whether the term is a bit-vector signed division (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 858 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
    }

◆ isBVSGE()

boolean isBVSGE ( )

inline

Indicates whether the term is a signed bit-vector greater-than-or-equal

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 989 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
    }

◆ isBVSGT()

boolean isBVSGT ( )

inline

Indicates whether the term is a signed bit-vector greater-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1029 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
    }

◆ isBVShiftLeft()

boolean isBVShiftLeft ( )

inline

Indicates whether the term is a bit-vector shift left

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1189 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
    }

◆ isBVShiftRightArithmetic()

boolean isBVShiftRightArithmetic ( )

inline

Indicates whether the term is a bit-vector arithmetic shift left

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1209 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
    }

◆ isBVShiftRightLogical()

boolean isBVShiftRightLogical ( )

inline

Indicates whether the term is a bit-vector logical shift right

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1199 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
    }

◆ isBVSignExtension()

boolean isBVSignExtension ( )

inline

Indicates whether the term is a bit-vector sign extension

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1119 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
    }

◆ isBVSLE()

boolean isBVSLE ( )

inline

Indicates whether the term is a signed bit-vector less-than-or-equal

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 968 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
    }

◆ isBVSLT()

boolean isBVSLT ( )

inline

Indicates whether the term is a signed bit-vector less-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1009 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
    }

◆ isBVSMod()

boolean isBVSMod ( )

inline

Indicates whether the term is a bit-vector signed modulus

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 898 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
    }

◆ isBVSRem()

boolean isBVSRem ( )

inline

Indicates whether the term is a bit-vector signed remainder (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 878 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
    }

◆ isBVSub()

boolean isBVSub ( )

inline

Indicates whether the term is a bit-vector subtraction (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 838 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
    }

◆ isBVToInt()

boolean isBVToInt ( )

inline

Indicates whether the term is a coercion from bit-vector to integer

Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1277 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
    }

◆ isBVUDiv()

boolean isBVUDiv ( )

inline

Indicates whether the term is a bit-vector unsigned division (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 868 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
    }

◆ isBVUGE()

boolean isBVUGE ( )

inline

Indicates whether the term is an unsigned bit-vector greater-than-or-equal

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 979 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
    }

◆ isBVUGT()

boolean isBVUGT ( )

inline

Indicates whether the term is an unsigned bit-vector greater-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1019 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
    }

◆ isBVULE()

boolean isBVULE ( )

inline

Indicates whether the term is an unsigned bit-vector less-than-or-equal

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 958 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
    }

◆ isBVULT()

boolean isBVULT ( )

inline

Indicates whether the term is an unsigned bit-vector less-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 999 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
    }

◆ isBVUMinus()

boolean isBVUMinus ( )

inline

Indicates whether the term is a bit-vector unary minus

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 818 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
    }

◆ isBVURem()

boolean isBVURem ( )

inline

Indicates whether the term is a bit-vector unsigned remainder (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 888 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
    }

◆ isBVXNOR()

boolean isBVXNOR ( )

inline

Indicates whether the term is a bit-wise XNOR

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1099 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
    }

◆ isBVXOR()

boolean isBVXOR ( )

inline

Indicates whether the term is a bit-wise XOR

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1069 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
    }

◆ isBVXOR3()

boolean isBVXOR3 ( )

inline

Indicates whether the term is a bit-vector ternary XOR Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor * l1 l2) l3)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1299 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
    }

◆ isBVZeroExtension()

boolean isBVZeroExtension ( )

inline

Indicates whether the term is a bit-vector zero extension

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1129 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
    }

◆ isConcat()

boolean isConcat ( )

inline

TBD: sketch for #2522, 'Pointer' seems deprecated and instead approach seems to be around Set/Get CharArrayRegion and updating Native.cpp code generation to produce the char[].

public char[] getNativeString() { Native.IntPtr len = new Native.IntPtr(); long s = Native.getLstring(getContext().nCtx(), getNativeObject(), len); char[] result = new char[len.value]; Pointer ptr = Pointer.createConstant(s); for (int i = 0; i < len.value; ++i) result[i] = ptr.getChar(i); return result; } Check whether expression is a concatenation

Returns: a boolean

Definition at line 1370 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT;
    }

◆ isConst()

boolean isConst ( )

inline

Indicates whether the term represents a constant.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 283 of file Expr.java.

    {
        return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
    }

◆ isConstantArray()

boolean isConstantArray ( )

inline

Indicates whether the term is a constant array. Remarks: For example, * select(const(v),i) = v holds for every v and i. The function is * unary.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 682 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
    }

◆ isDefaultArray()

boolean isDefaultArray ( )

inline

Indicates whether the term is a default array. Remarks: For example default(const(v)) = v. The function is unary.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 693 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
    }

◆ isDistinct()

boolean isDistinct ( )

inline

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 386 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
    }

◆ isDiv()

boolean isDiv ( )

inline

Indicates whether the term is division (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 577 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
    }

◆ isEmptyRelation()

boolean isEmptyRelation ( )

inline

Indicates whether the term is an empty relation

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1950 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
    }

◆ isEq()

boolean isEq ( )

inline

Indicates whether the term is an equality predicate.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 375 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
    }

◆ isFalse()

boolean isFalse ( )

inline

Indicates whether the term is the constant false.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 365 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
    }

Referenced by Solver.cube().

◆ isFiniteDomain()

boolean isFiniteDomain ( )

inline

Indicates whether the term is of an array sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2104 of file Expr.java.

    {
        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
                .getSortKind(getContext().nCtx(),
                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
                .toInt());
    }

◆ isFiniteDomainLT()

boolean isFiniteDomainLT ( )

inline

Indicates whether the term is a less than predicate over a finite domain.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2117 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
    }

◆ isGE()

boolean isGE ( )

inline

Indicates whether the term is a greater-than-or-equal

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 507 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
    }

◆ isGround()

boolean isGround ( )

inline

Indicates whether the term is ground (contains no free variables).

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 323 of file Expr.java.

    {
        return Native.isGround(getContext().nCtx(), getNativeObject());
    }

◆ isGT()

boolean isGT ( )

inline

Indicates whether the term is a greater-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 527 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
    }

◆ isIDiv()

boolean isIDiv ( )

inline

Indicates whether the term is integer division (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 587 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
    }

◆ isIff()

boolean isIff ( )

inline

Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 427 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
    }

◆ isImplies()

boolean isImplies ( )

inline

Indicates whether the term is an implication

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 457 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
    }

◆ isInt()

boolean isInt ( )

inline

Indicates whether the term is of integer sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 467 of file Expr.java.

    {
        return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
    }

◆ isIntNum()

boolean isIntNum ( )

inline

Indicates whether the term is an integer numeral.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 293 of file Expr.java.

    {
        return isNumeral() && isInt();
    }

◆ isIntToBV()

boolean isIntToBV ( )

inline

Indicates whether the term is a coercion from integer to bit-vector

Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1265 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
    }

◆ isIntToReal()

boolean isIntToReal ( )

inline

Indicates whether the term is a coercion of integer to real (unary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 617 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
    }

◆ isIsEmptyRelation()

boolean isIsEmptyRelation ( )

inline

Indicates whether the term is a test for the emptiness of a relation

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1960 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
    }

◆ isITE()

boolean isITE ( )

inline

Indicates whether the term is a ternary if-then-else term

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 396 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
    }

◆ isLabel()

boolean isLabel ( )

inline

Indicates whether the term is a label (used by the Boogie Verification condition generator). Remarks: The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1312 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
    }

◆ isLabelLit()

boolean isLabelLit ( )

inline

Indicates whether the term is a label literal (used by the Boogie Verification condition generator). Remarks: A label literal has a set of string parameters. It takes no arguments.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1325 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
    }

◆ isLambda()

boolean isLambda ( )

inline

Indicates whether the term is a lambda expression.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 333 of file Expr.java.

    {
        return Native.isLambda(getContext().nCtx(), getNativeObject());
    }

◆ isLE()

boolean isLE ( )

inline

Indicates whether the term is a less-than-or-equal

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 497 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
    }

◆ isLT()

boolean isLT ( )

inline

Indicates whether the term is a less-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 517 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
    }

◆ isModulus()

boolean isModulus ( )

inline

Indicates whether the term is modulus (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 607 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
    }

◆ isMul()

boolean isMul ( )

inline

Indicates whether the term is multiplication (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 567 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
    }

◆ isNot()

boolean isNot ( )

inline

Indicates whether the term is a negation

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 447 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
    }

◆ isNumeral()

boolean isNumeral ( )

inline

Indicates whether the term is a numeral

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 242 of file Expr.java.

    {
        return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
    }

◆ isOEQ()

boolean isOEQ ( )

inline

Indicates whether the term is a binary equivalence modulo namings. Remarks: This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1382 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
    }

◆ isOr()

boolean isOr ( )

inline

Indicates whether the term is an n-ary disjunction

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 416 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
    }

◆ isProofAndElimination()

boolean isProofAndElimination ( )

inline

Indicates whether the term is a proof by elimination of AND Remarks: * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and * l_1 ... l_n) [and-elim T1]: l_i

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1542 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
    }

◆ isProofApplyDef()

boolean isProofApplyDef ( )

inline

Indicates whether the term is a proof for application of a definition Remarks: [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1801 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
    }

◆ isProofAsserted()

boolean isProofAsserted ( )

inline

Indicates whether the term is a proof for a fact asserted by the user.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1402 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
    }

◆ isProofCommutativity()

boolean isProofCommutativity ( )

inline

Indicates whether the term is a proof by commutativity Remarks: [comm]: (= (f a b) (f b a))

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1740 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
    }

◆ isProofDefAxiom()

boolean isProofDefAxiom ( )

inline

Indicates whether the term is a proof for Tseitin-like axioms Remarks: Proof object used to justify Tseitin's like axioms:

(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)

This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1766 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
    }

◆ isProofDefIntro()

boolean isProofDefIntro ( )

inline

Indicates whether the term is a proof for introduction of a name Remarks: Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:

When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n) e))

or: [def-intro]: (or (not n) e) when e only occurs positively.

When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))

Otherwise: [def-intro]: (= n e)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1789 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
    }

◆ isProofDER()

boolean isProofDER ( )

inline

Indicates whether the term is a proof for destructive equality resolution Remarks: A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1648 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
    }

◆ isProofDistributivity()

boolean isProofDistributivity ( )

inline

Indicates whether the term is a distributivity proof object. Remarks: Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.

This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1531 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
    }

◆ isProofElimUnusedVars()

boolean isProofElimUnusedVars ( )

inline

Indicates whether the term is a proof for elimination of unused variables. Remarks: A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))

It is used to justify the elimination of unused variables. This proof object has no antecedents.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1632 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
    }

◆ isProofGoal()

boolean isProofGoal ( )

inline

Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1413 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
    }

◆ isProofHypothesis()

boolean isProofHypothesis ( )

inline

Indicates whether the term is a hypothesis marker. Remarks: Mark a hypothesis in a natural deduction style proof.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1672 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
    }

◆ isProofIFFFalse()

boolean isProofIFFFalse ( )

inline

Indicates whether the term is a proof by iff-false Remarks: T1: (not p) [iff-false T1]: (iff p false)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1723 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
    }

◆ isProofIFFOEQ()

boolean isProofIFFOEQ ( )

inline

Indicates whether the term is a proof iff-oeq Remarks: T1: (iff p q) [iff~ T1]: (~ p q)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1813 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
    }

◆ isProofIFFTrue()

boolean isProofIFFTrue ( )

inline

Indicates whether the term is a proof by iff-true Remarks: T1: p [iff-true T1]: (iff p true)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1711 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
    }

◆ isProofLemma()

boolean isProofLemma ( )

inline

Indicates whether the term is a proof by lemma Remarks: T1: false [lemma T1]: (or (not l_1) ... (not l_n))

This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1688 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
    }

◆ isProofModusPonens()

boolean isProofModusPonens ( )

inline

Indicates whether the term is proof via modus ponens Remarks: Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a proof for (iff p q).

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1427 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
    }

◆ isProofModusPonensOEQ()

boolean isProofModusPonensOEQ ( )

inline

Indicates whether the term is a proof by modus ponens for equi-satisfiability. Remarks: Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1891 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
    }

◆ isProofMonotonicity()

boolean isProofMonotonicity ( )

inline

Indicates whether the term is a monotonicity proof object. Remarks: T1: (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are suppressed to save space.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1501 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
    }

◆ isProofNNFNeg()

boolean isProofNNFNeg ( )

inline

Indicates whether the term is a proof for a negative NNF step Remarks: Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2')))

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1860 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
    }

◆ isProofNNFPos()

boolean isProofNNFPos ( )

inline

Indicates whether the term is a proof for a positive NNF step Remarks: Proof for a (positive) NNF step. Example:

T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'

r_2)))

The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x R) q) (forall (x R) q_new))

(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1841 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
    }

◆ isProofOrElimination()

boolean isProofOrElimination ( )

inline

Indicates whether the term is a proof by elimination of not-or Remarks: * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1553 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
    }

◆ isProofPullQuant()

boolean isProofPullQuant ( )

inline

Indicates whether the term is a proof for pulling quantifiers out. Remarks: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1601 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
    }

◆ isProofPushQuant()

boolean isProofPushQuant ( )

inline

Indicates whether the term is a proof for pushing quantifiers in. Remarks: A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ... (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1616 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
    }

◆ isProofQuantInst()

boolean isProofQuantInst ( )

inline

Indicates whether the term is a proof for quantifier instantiation

Remarks: A proof of (or (not (forall (x) (P x))) (P a))

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1660 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
    }

◆ isProofQuantIntro()

boolean isProofQuantIntro ( )

inline

Indicates whether the term is a quant-intro proof Remarks: Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q))

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1512 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
    }

◆ isProofReflexivity()

boolean isProofReflexivity ( )

inline

Indicates whether the term is a proof for (R t t), where R is a reflexive relation. Remarks: This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1442 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
    }

◆ isProofRewrite()

boolean isProofRewrite ( )

inline

Indicates whether the term is a proof by rewriting Remarks: A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.

This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.

Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1573 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
    }

◆ isProofRewriteStar()

boolean isProofRewriteStar ( )

inline

Indicates whether the term is a proof by rewriting Remarks: A proof for rewriting an expression t into an expression s. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is used in a few cases . The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1589 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
    }

◆ isProofSkolemize()

boolean isProofSkolemize ( )

inline

Indicates whether the term is a proof for a Skolemization step Remarks: Proof for:

(p x y)) (p (sk y) y))

This proof object has no antecedents.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1878 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
    }

◆ isProofSymmetry()

boolean isProofSymmetry ( )

inline

Indicates whether the term is proof by symmetricity of a relation

Remarks: Given an symmetric relation R and a proof for (R t s), produces * a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the * antecedent of this proof object.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1454 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
    }

◆ isProofTheoryLemma()

boolean isProofTheoryLemma ( )

inline

Indicates whether the term is a proof for theory lemma Remarks: Generic proof for theory lemmas.

The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are: - farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - triangle-eq - Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1913 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
    }

◆ isProofTransitivity()

boolean isProofTransitivity ( )

inline

Indicates whether the term is a proof by transitivity of a relation

Remarks: Given a transitive relation R, and proofs for (R t s) and (R s * u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: * (R t u)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1466 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
    }

◆ isProofTransitivityStar()

boolean isProofTransitivityStar ( )

inline

Indicates whether the term is a proof by condensed transitivity of a relation Remarks: Condensed transitivity proof. It combines several symmetry and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.

Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1486 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
    }

◆ isProofTrue()

boolean isProofTrue ( )

inline

Indicates whether the term is a Proof for the expression 'true'.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1392 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
    }

◆ isProofUnitResolution()

boolean isProofUnitResolution ( )

inline

Indicates whether the term is a proof by unit resolution Remarks: T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... R(n+1): (not l_n) * [unit-resolution T1 ... R(n+1)]: (or l_1' ... l_m')

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1699 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
    }

◆ isRatNum()

boolean isRatNum ( )

inline

Indicates whether the term is a real numeral.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 303 of file Expr.java.

    {
        return isNumeral() && isReal();
    }

◆ isReal()

boolean isReal ( )

inline

Indicates whether the term is of sort real.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 477 of file Expr.java.

    {
        return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
    }

◆ isRealIsInt()

boolean isRealIsInt ( )

inline

Indicates whether the term is a check that tests whether a real is integral (unary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 638 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
    }

◆ isRealToInt()

boolean isRealToInt ( )

inline

Indicates whether the term is a coercion of real to integer (unary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 627 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
    }

◆ isRelation()

boolean isRelation ( )

inline

Indicates whether the term is of an array sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1923 of file Expr.java.

    {
        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
                .getSortKind(getContext().nCtx(),
                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
                .toInt());
    }

◆ isRelationalJoin()

boolean isRelationalJoin ( )

inline

Indicates whether the term is a relational join

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1970 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
    }

◆ isRelationClone()

boolean isRelationClone ( )

inline

Indicates whether the term is a relational clone (copy) Remarks: Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind isRelationUnion to perform destructive updates to the first argument.

See also: #isRelationUnion

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2094 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
    }

◆ isRelationComplement()

boolean isRelationComplement ( )

inline

Indicates whether the term is the complement of a relation

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2064 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
    }

◆ isRelationFilter()

boolean isRelationFilter ( )

inline

Indicates whether the term is a relation filter Remarks: Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2022 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
    }

◆ isRelationNegationFilter()

boolean isRelationNegationFilter ( )

inline

Indicates whether the term is an intersection of a relation with the negation of another. Remarks: Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2042 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
    }

◆ isRelationProject()

boolean isRelationProject ( )

inline

Indicates whether the term is a projection of columns (provided as numbers in the parameters). Remarks: The function takes one argument.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2007 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
    }

◆ isRelationRename()

boolean isRelationRename ( )

inline

Indicates whether the term is the renaming of a column in a relation Remarks: The function takes one argument. The parameters contain the renaming as a cycle.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2054 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
    }

◆ isRelationSelect()

boolean isRelationSelect ( )

inline

Indicates whether the term is a relational select Remarks: Check if a record is an element of the relation. The function takes n+1 arguments, where the first argument is a relation, and the remaining n arguments correspond to a record.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2078 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
    }

◆ isRelationStore()

boolean isRelationStore ( )

inline

Indicates whether the term is an relation store Remarks: Insert a record into a relation. The function takes n+1 arguments, where the first argument is the relation and the remaining n elements correspond to the n columns of the relation.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1940 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
    }

◆ isRelationUnion()

boolean isRelationUnion ( )

inline

Indicates whether the term is the union or convex hull of two relations.

Remarks: The function takes two arguments.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1982 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
    }

◆ isRelationWiden()

boolean isRelationWiden ( )

inline

Indicates whether the term is the widening of two relations Remarks: The function takes two arguments.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 1994 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
    }

◆ isRemainder()

boolean isRemainder ( )

inline

Indicates whether the term is remainder (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 597 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
    }

◆ isSelect()

boolean isSelect ( )

inline

Indicates whether the term is an array select.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 671 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
    }

◆ isSetComplement()

boolean isSetComplement ( )

inline

Indicates whether the term is set complement

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 756 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
    }

◆ isSetDifference()

boolean isSetDifference ( )

inline

Indicates whether the term is set difference

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 746 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
    }

◆ isSetIntersect()

boolean isSetIntersect ( )

inline

Indicates whether the term is set intersection

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 736 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
    }

◆ isSetSubset()

boolean isSetSubset ( )

inline

Indicates whether the term is set subset

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 766 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
    }

◆ isSetUnion()

boolean isSetUnion ( )

inline

Indicates whether the term is set union

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 726 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
    }

◆ isStore()

boolean isStore ( )

inline

Indicates whether the term is an array store. Remarks: It satisfies * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store * takes at least 3 arguments.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 661 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
    }

◆ isString()

boolean isString ( )

inline

Check whether expression is a string constant.

Returns: a boolean

Definition at line 1334 of file Expr.java.

    {
        return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
    }

◆ isSub()

boolean isSub ( )

inline

Indicates whether the term is subtraction (binary)

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 547 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
    }

◆ isTrue()

boolean isTrue ( )

inline

Indicates whether the term is the constant true.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 355 of file Expr.java.

    {
            return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
    }

◆ isUMinus()

boolean isUMinus ( )

inline

Indicates whether the term is a unary minus

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 557 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
    }

◆ isWellSorted()

boolean isWellSorted ( )

inline

Indicates whether the term is well-sorted.

Exceptions

Z3Exception on error

Returns: True if the term is well-sorted, false otherwise.

Definition at line 262 of file Expr.java.

    {
        return Native.isWellSorted(getContext().nCtx(), getNativeObject());
    }

◆ isXor()

boolean isXor ( )

inline

Indicates whether the term is an exclusive or

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 437 of file Expr.java.

    {
        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
    }

◆ simplify() [1/2]

Expr< R > simplify ( )

inline

Returns a simplified version of the expression

Returns: Expr

Exceptions

Z3Exception on error

Definition at line 41 of file Expr.java.

    {
        return simplify(null);
    }

◆ simplify() [2/2]

Expr< R > simplify ( Params p )

inline

Returns a simplified version of the expression A set of parameters

Parameters

p	a Params object to configure the simplifier

See also: Context::SimplifyHelp

Returns: an Expr

Exceptions

Z3Exception on error

Definition at line 55 of file Expr.java.

    {
 
        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()));
        }
    }

◆ substitute() [1/2]

Expr< R > substitute	(	Expr<?>	from,
		Expr<?>	to
	)

inline

Substitute every occurrence of from in the expression with to.

See also: Expr::substitute(Expr[],Expr[])

Exceptions

Z3Exception on error

Returns: an Expr

Definition at line 168 of file Expr.java.

    {
        return substitute(new Expr[] { from }, new Expr[] { to });
    }

◆ substitute() [2/2]

Expr< R > substitute	(	Expr<?>[]	from,
		Expr<?>[]	to
	)

inline

Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs. Remarks: The result is the new expression. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].

Exceptions

Z3Exception on error

Returns: an Expr

Definition at line 149 of file Expr.java.

    {
        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)));
    }

◆ substituteFuns()

Expr< R > substituteFuns	(	FuncDecl<?>[]	from,
		Expr<?>[]	to
	)

inline

Substitute functions in from with the expressions in to. The expressions in to can have free variables. The free variable in to[i] at de-Bruijn index 0 refers to the first argument of from[i], the free variable at index 1 corresponds to the second argument, and so on. Remarks: The arrays from and to must have the same size.

Parameters

from	Array of function declarations to be substituted
to	Array of expressions to substitute with

Exceptions

Z3Exception on error

Returns: an Expr

Definition at line 203 of file Expr.java.

    {
        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)));
    }

◆ substituteVars()

Expr< R > substituteVars ( Expr<?>[] to )

inline

Substitute the free variables in the expression with the expressions in to Remarks: For every i smaller than * num_exprs, the variable with de-Bruijn index i * is replaced with term to[i].

Exceptions

Z3Exception	on error
Z3Exception	on error

Returns: an Expr

Definition at line 183 of file Expr.java.

    {
 
        getContext().checkContextMatch(to);
        return (Expr<R>) Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
                getNativeObject(), to.length, Expr.arrayToNative(to)));
    }

◆ toString()

String toString ( )

inline

Returns a string representation of the expression.

Reimplemented from AST.

Definition at line 232 of file Expr.java.

    {
        return super.toString();
    }

Referenced by Optimize.AssertSoft().

◆ translate()

Expr< R > translate ( Context ctx )

inline

Translates (copies) the term to the Context ctx.

Parameters

ctx A context

Returns: A copy of the term which is associated with ctx

Exceptions

Z3Exception on error

Reimplemented from AST.

Definition at line 223 of file Expr.java.

    {
        return (Expr<R>) super.translate(ctx);
    }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Expr< R extends Sort >.translate().

◆ update()

Expr< R > update ( Expr<?>[] args )

inline

Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments.

Parameters

args arguments

Exceptions

Z3Exception on error

Definition at line 127 of file Expr.java.

    {
        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 Member Functions

Protected Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Expr()

Member Function Documentation

◆ getArgs()

◆ getBoolValue()

◆ getFuncDecl()

◆ getIndex()

◆ getNumArgs()

◆ getNumeralDouble()

◆ getSort()

◆ getString()

◆ isAdd()

◆ isAlgebraicNumber()

◆ isAnd()

◆ isArithmeticNumeral()

◆ isArray()

◆ isArrayMap()

◆ isAsArray()

◆ isBool()

◆ isBV()

◆ isBVAdd()

◆ isBVAND()

◆ isBVBitOne()

◆ isBVBitZero()

◆ isBVCarry()

◆ isBVComp()

◆ isBVConcat()

◆ isBVExtract()

◆ isBVMul()

◆ isBVNAND()

◆ isBVNOR()

◆ isBVNOT()

◆ isBVNumeral()

◆ isBVOR()

◆ isBVReduceAND()

◆ isBVReduceOR()

◆ isBVRepeat()

◆ isBVRotateLeft()

◆ isBVRotateLeftExtended()

◆ isBVRotateRight()

◆ isBVRotateRightExtended()

◆ isBVSDiv()

◆ isBVSGE()

◆ isBVSGT()

◆ isBVShiftLeft()

◆ isBVShiftRightArithmetic()

◆ isBVShiftRightLogical()

◆ isBVSignExtension()

◆ isBVSLE()

◆ isBVSLT()

◆ isBVSMod()

◆ isBVSRem()

◆ isBVSub()

◆ isBVToInt()

◆ isBVUDiv()

◆ isBVUGE()

◆ isBVUGT()

◆ isBVULE()

◆ isBVULT()

◆ isBVUMinus()

◆ isBVURem()

◆ isBVXNOR()

◆ isBVXOR()

◆ isBVXOR3()

◆ isBVZeroExtension()

◆ isConcat()

◆ isConst()

◆ isConstantArray()

◆ isDefaultArray()

◆ isDistinct()

◆ isDiv()

◆ isEmptyRelation()

◆ isEq()

◆ isFalse()

◆ isFiniteDomain()

◆ isFiniteDomainLT()