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 |
Rational Numerals
Definition at line 25 of file RatNum.java.
RatNum | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 87 of file RatNum.java.
{ super(ctx, obj); }
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(); } }