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 >	translate (Context ctx)

String	toString ()

boolean	isNumeral ()

boolean	isWellSorted ()

R	getSort ()

boolean	isConst ()

boolean	isIntNum ()

boolean	isRatNum ()

boolean	isAlgebraicNumber ()

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 ()

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

◆ getSort()

R getSort ( )

inline

The Sort of the term.

Exceptions

Z3Exception on error

Returns: a sort

Definition at line 239 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 1292 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 484 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 280 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 353 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 434 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 595 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 652 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 663 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 290 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 723 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 775 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 986 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 745 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 755 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 1235 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 1126 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 1056 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 1086 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 795 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 1026 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 1036 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 1006 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 735 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 996 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 1116 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 1106 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 1096 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 1166 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 1188 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 1176 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 1200 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 805 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 936 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 976 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 1136 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 1156 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 1146 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 1066 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 915 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 956 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 845 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 825 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 785 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 1224 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 815 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 926 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 966 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 905 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 946 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 765 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 835 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 1046 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 1016 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 1246 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 1076 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 1317 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 250 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 629 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 640 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 333 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 524 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 1897 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 322 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 312 of file Expr.java.

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

◆ isFiniteDomain()

boolean isFiniteDomain ( )

inline

Indicates whether the term is of an array sort.

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2051 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 2064 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 454 of file Expr.java.

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

◆ isGT()

boolean isGT ( )

inline

Indicates whether the term is a greater-than

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 474 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 534 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 374 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 404 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 414 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 260 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 1212 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 564 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 1907 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 343 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 1259 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 1272 of file Expr.java.

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

◆ isLE()

boolean isLE ( )

inline

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

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 444 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 464 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 554 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 514 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 394 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 218 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 1329 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 363 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 1489 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 1748 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 1349 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 1687 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 1713 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 1736 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 1595 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 1478 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 1579 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 1360 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 1619 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 1670 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 1760 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 1658 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 1635 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 1374 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 1838 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 1448 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 1807 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 1788 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 1500 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 1548 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 1563 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 1607 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 1459 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 1389 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 1520 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 1536 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 1825 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 1401 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 1860 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 1413 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 1433 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 1339 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 1646 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 270 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 424 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 585 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 574 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 1870 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 1917 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

com.microsoft.z3.Expr.isRelationUnion

boolean isRelationUnion()

Definition: Expr.java:1929

to perform destructive updates to the first argument.

See also: isRelationUnion

Exceptions

Z3Exception on error

Returns: a boolean

Definition at line 2041 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 2011 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 1969 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 1989 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 1954 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 2001 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 2025 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 1887 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 1929 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 1941 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 544 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 618 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 703 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 693 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 683 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 713 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 673 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 608 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 1281 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 494 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 302 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 504 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 229 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 384 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)));
     }

◆ 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 208 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 199 of file Expr.java.

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

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__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()

◆ 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()

◆ isGE()