Z3 |

Public Member Functions
RatNum Class Reference
Inheritance diagram for RatNum:

## Public Member Functions
IntNum | getNumerator ()
IntNum | getDenominator ()
BigInteger | getBigIntNumerator ()
BigInteger | getBigIntDenominator ()
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.

58 {
59 IntNum n = getDenominator();
60 return new BigInteger(n.toString());
61 }
com.microsoft.z3.RatNum.getDenominator
IntNum getDenominator()
Definition: RatNum.java:39

## ◆ getBigIntNumerator()

BigInteger getBigIntNumerator | ( |  | ) |
| inline

Converts the numerator of the rational to a BigInteger

Definition at line 48 of file RatNum.java.

49 {
50 IntNum n = getNumerator();
51 return new BigInteger(n.toString());
52 }
com.microsoft.z3.RatNum.getNumerator
IntNum getNumerator()
Definition: RatNum.java:30

## ◆ getDenominator()

IntNum getDenominator | ( |  | ) |
| inline

The denominator of a rational numeral.

Definition at line 39 of file RatNum.java.

40 {
41 return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(),
42 getNativeObject()));
43 }

Referenced by RatNum.getBigIntDenominator().

## ◆ getNumerator()

IntNum getNumerator | ( |  | ) |
| inline

The numerator of a rational numeral.

Definition at line 30 of file RatNum.java.

31 {
32 return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(),
33 getNativeObject()));
34 }

Referenced by RatNum.getBigIntNumerator().

## ◆ 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 68 of file RatNum.java.

69 {
70 return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
71 precision);
72 }

## ◆ toString()

String toString | ( |  | ) |
| inline

Returns a string representation of the numeral.

Definition at line 78 of file RatNum.java.

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