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  }

◆ 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  }

◆ 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  }
com.microsoft.z3.RatNum.getDenominator
IntNum getDenominator()
Definition: RatNum.java:39
com.microsoft.z3.RatNum.getNumerator
IntNum getNumerator()
Definition: RatNum.java:30