IntNum Class Reference

Inheritance diagram for IntNum:

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

---

Detailed Description

Integer Numerals

Definition at line 25 of file IntNum.java.

---

Constructor & Destructor Documentation

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

Definition at line 28 of file IntNum.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

BigInteger getBigInteger

(

)

throws Z3Exception [inline]

Retrieve the BigInteger value.

Definition at line 58 of file IntNum.java.

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

int getInt

(

)

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

long getInt64

(

)

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

String toString

(

)

[inline]

Returns a string representation of the numeral.

Reimplemented from Expr.

Definition at line 66 of file IntNum.java.

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

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