Public Member Functions | |
RatNum | toUpper (int precision) throws Z3Exception |
RatNum | toLower (int precision) throws Z3Exception |
String | toDecimal (int precision) throws Z3Exception |
Package Functions | |
AlgebraicNum (Context ctx, long obj) throws Z3Exception |
Algebraic numbers
Definition at line 23 of file AlgebraicNum.java.
AlgebraicNum | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 65 of file AlgebraicNum.java.
{ super(ctx, obj); }
String toDecimal | ( | int | precision | ) | throws Z3Exception [inline] |
Returns a string representation in decimal notation. The result has at most precision decimal places.
Definition at line 58 of file AlgebraicNum.java.
{ return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(), precision); }
RatNum toLower | ( | int | precision | ) | throws Z3Exception [inline] |
Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision .
precision |
Definition at line 47 of file AlgebraicNum.java.
{ return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext() .nCtx(), getNativeObject(), precision)); }
RatNum toUpper | ( | int | precision | ) | throws Z3Exception [inline] |
Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision .
precision | the precision of the result |
Definition at line 33 of file AlgebraicNum.java.
{ return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext() .nCtx(), getNativeObject(), precision)); }