BitVecNum Class Reference

Inheritance diagram for BitVecNum:

Public Member Functions
int	getInt () throws Z3Exception
long	getLong () throws Z3Exception
BigInteger	getBigInteger ()
String	toString ()
Package Functions
	BitVecNum (Context ctx, long obj) throws Z3Exception

---

Detailed Description

Bit-vector numerals

Definition at line 25 of file BitVecNum.java.

---

Constructor & Destructor Documentation

BitVecNum	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 75 of file BitVecNum.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

BigInteger getBigInteger

(

)

[inline]

Retrieve the BigInteger value.

Definition at line 56 of file BitVecNum.java.

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

int getInt

(

)

throws Z3Exception [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) ^ true)
            throw new Z3Exception("Numeral is not an int");
        return res.value;
    }

long getLong

(

)

throws Z3Exception [inline]

Retrieve the 64-bit int value.

Exceptions:

Z3Exception

Definition at line 45 of file BitVecNum.java.

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

String toString

(

)

[inline]

Returns a string representation of the numeral.

Reimplemented from Expr.

Definition at line 64 of file BitVecNum.java.

Referenced by BitVecNum.getBigInteger().

    {
        try
        {
            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }