BitVecNum Class Reference

Inheritance diagram for BitVecNum:

Public Member Functions
int	getInt ()
long	getLong ()
BigInteger	getBigInteger ()
String	toString ()
String	toBinaryString ()
Public Member Functions inherited from BitVecExpr
int	getSortSize ()
Public Member Functions inherited from Expr< BitVecSort >
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 ()

Additional Inherited Members
Protected Member Functions inherited from Expr< BitVecSort >
	Expr (Context ctx, long obj)

Detailed Description

Bit-vector numerals

Definition at line 25 of file BitVecNum.java.

Member Function Documentation

getBigInteger()

BigInteger getBigInteger ( )

inline

Retrieve the BigInteger value.

Definition at line 58 of file BitVecNum.java.

    {
        return new BigInteger(this.toString());
    }

getInt()

int getInt ( )

inline

Retrieve the int value.

Exceptions

Z3Exception

Definition at line 32 of file BitVecNum.java.

    {
        Native.IntPtr res = new Native.IntPtr();
        if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
            throw new Z3Exception("Numeral is not an int");
        }
        return res.value;
    }

getLong()

long getLong ( )

inline

Retrieve the 64-bit int value.

Exceptions

Z3Exception

Definition at line 46 of file BitVecNum.java.

    {
        Native.LongPtr res = new Native.LongPtr();
        if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
            throw new Z3Exception("Numeral is not a long");
        }
        return res.value;
    }

toBinaryString()

String toBinaryString ( )

inline

Returns a binary string representation of the numeral.

Definition at line 75 of file BitVecNum.java.

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

toString()

String toString ( )

inline

Returns a decimal string representation of the numeral.

Definition at line 67 of file BitVecNum.java.

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

Referenced by BitVecNum.getBigInteger().