IntNum Class Reference

Inheritance diagram for IntNum:

Public Member Functions
int	getInt ()
long	getInt64 ()
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 58 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;
    }

toString()

String toString ( )

inline

Returns a string representation of the numeral.

Definition at line 66 of file IntNum.java.

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

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