IntNum Class Reference

Inheritance diagram for IntNum:

Public Member Functions
int	getInt ()
long	getInt64 ()
int	getUint ()
long	getUint64 ()
BigInteger	getBigInteger ()
String	toString ()

Detailed Description

Integer Numerals

Definition at line 25 of file IntNum.java.

Member Function Documentation

getBigInteger()

BigInteger getBigInteger ( )

inline

Retrieve the BigInteger value.

Definition at line 85 of file IntNum.java.

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

getInt()

int getInt ( )

inline

Retrieve the int value.

Definition at line 36 of file IntNum.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;
    }

getInt64()

long getInt64 ( )

inline

Retrieve the 64-bit int value.

Definition at line 47 of file IntNum.java.

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

getUint()

int getUint ( )

inline

Retrieve the unsigned 32-bit value. The returned Java int holds the raw bit pattern; use Integer.toUnsignedLong(v) for unsigned interpretation.

Definition at line 60 of file IntNum.java.

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

getUint64()

long getUint64 ( )

inline

Retrieve the unsigned 64-bit value. The returned Java long holds the raw bit pattern; use Long.toUnsignedString(v) or getBigInteger() for values exceeding Long.MAX_VALUE.

Definition at line 74 of file IntNum.java.

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

toString()

String toString ( )

inline

Returns a string representation of the numeral.

Definition at line 93 of file IntNum.java.

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

Referenced by RatNum.getBigIntDenominator(), IntNum.getBigInteger(), and RatNum.getBigIntNumerator().