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