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