RatNum Class Reference

Inheritance diagram for RatNum:

Public Member Functions
IntNum	getNumerator ()
IntNum	getDenominator ()
BigInteger	getBigIntNumerator ()
BigInteger	getBigIntDenominator ()
long[]	getSmall ()
long[]	getRationalInt64 ()
String	toDecimalString (int precision)
String	toString ()

Detailed Description

Rational Numerals

Definition at line 25 of file RatNum.java.

Member Function Documentation

getBigIntDenominator()

BigInteger getBigIntDenominator ( )

inline

Converts the denominator of the rational to a BigInteger

Definition at line 57 of file RatNum.java.

    {
        IntNum n = getDenominator();
        return new BigInteger(n.toString());
    }

getBigIntNumerator()

BigInteger getBigIntNumerator ( )

inline

Converts the numerator of the rational to a BigInteger

Definition at line 48 of file RatNum.java.

    {
        IntNum n = getNumerator();
        return new BigInteger(n.toString());
    }

getDenominator()

IntNum getDenominator ( )

inline

The denominator of a rational numeral.

Definition at line 39 of file RatNum.java.

    {
        return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(),
                getNativeObject()));
    }

Referenced by RatNum.getBigIntDenominator().

getNumerator()

IntNum getNumerator ( )

inline

The numerator of a rational numeral.

Definition at line 30 of file RatNum.java.

    {
        return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(),
                getNativeObject()));
    }

Referenced by RatNum.getBigIntNumerator().

getRationalInt64()

long[] getRationalInt64 ( )

inline

Retrieve the numerator and denominator as 64-bit integers. Returns null if the value does not fit in 64-bit integers.

Returns

a two-element array [numerator, denominator], or null

Definition at line 82 of file RatNum.java.

    {
        Native.LongPtr num = new Native.LongPtr();
        Native.LongPtr den = new Native.LongPtr();
        if (!Native.getNumeralRationalInt64(getContext().nCtx(), getNativeObject(), num, den))
            return null;
        return new long[] { num.value, den.value };
    }

getSmall()

long[] getSmall ( )

inline

Retrieve the numerator and denominator as 64-bit integers. Throws if the value does not fit in 64-bit integers.

Returns

a two-element array [numerator, denominator]

Definition at line 68 of file RatNum.java.

    {
        Native.LongPtr num = new Native.LongPtr();
        Native.LongPtr den = new Native.LongPtr();
        if (!Native.getNumeralSmall(getContext().nCtx(), getNativeObject(), num, den))
            throw new Z3Exception("Numeral does not fit in int64");
        return new long[] { num.value, den.value };
    }

toDecimalString()

String toDecimalString ( int  precision )

inline

Returns a string representation in decimal notation. Remarks: The result has at most precision decimal places.

Definition at line 96 of file RatNum.java.

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

toString()

String toString ( )

inline

Returns a string representation of the numeral.

Definition at line 106 of file RatNum.java.

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