Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines