Z3 |

Public Member Functions
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.

59 {
60 return new BigInteger(this.toString());
61 }
com.microsoft.z3.BitVecNum.toString
String toString()
Definition: BitVecNum.java:67

## ◆ getInt()

int getInt | ( |  | ) |
| inline

Retrieve the int value.

Exceptions

  Z3Exception |

Definition at line 32 of file BitVecNum.java.

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

## ◆ getLong()

long getLong | ( |  | ) |
| inline

Retrieve the 64-bit int value.

Exceptions

  Z3Exception |

Definition at line 46 of file BitVecNum.java.

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

## ◆ toBinaryString()

String toBinaryString | ( |  | ) |
| inline

Returns a binary string representation of the numeral.

Definition at line 75 of file BitVecNum.java.

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

## ◆ toString()

String toString | ( |  | ) |
| inline

Returns a decimal string representation of the numeral.

Definition at line 67 of file BitVecNum.java.

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

Referenced by BitVecNum.getBigInteger().