RatNum Class Reference

Inheritance diagram for RatNum:

Public Member Functions
IntNum	getNumerator () throws Z3Exception
IntNum	getDenominator () throws Z3Exception
BigInteger	getBigIntNumerator () throws Z3Exception
BigInteger	getBigIntDenominator () throws Z3Exception
String	toDecimalString (int precision) throws Z3Exception
String	toString ()
Package Functions
	RatNum (Context ctx, long obj) throws Z3Exception

---

Detailed Description

Rational Numerals

Definition at line 25 of file RatNum.java.

---

Constructor & Destructor Documentation

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

Definition at line 87 of file RatNum.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

BigInteger getBigIntDenominator

(

)

throws Z3Exception [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());
    }

BigInteger getBigIntNumerator

(

)

throws Z3Exception [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());
    }

IntNum getDenominator

(

)

throws Z3Exception [inline]

The denominator of a rational numeral.

Definition at line 39 of file RatNum.java.

Referenced by RatNum.getBigIntDenominator().

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

IntNum getNumerator

(

)

throws Z3Exception [inline]

The numerator of a rational numeral.

Definition at line 30 of file RatNum.java.

Referenced by RatNum.getBigIntNumerator().

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

String toDecimalString

(

int

precision

)

throws Z3Exception [inline]

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

Definition at line 67 of file RatNum.java.

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

String toString

(

)

[inline]

Returns a string representation of the numeral.

Reimplemented from Expr.

Definition at line 76 of file RatNum.java.

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