Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
AlgebraicNum Class Reference
+ Inheritance diagram for AlgebraicNum:

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

Detailed Description

Algebraic numbers

Definition at line 23 of file AlgebraicNum.java.


Constructor & Destructor Documentation

AlgebraicNum ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 65 of file AlgebraicNum.java.

        {
                super(ctx, obj);

        }

Member Function Documentation

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 .

See also:
Expr.IsAlgebraicNumber
Parameters:
precision
Returns:
A numeral Expr of sort Real

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 .

See also:
Expr.IsAlgebraicNumber
Parameters:
precisionthe precision of the result
Returns:
A numeral Expr of sort Real

Definition at line 33 of file AlgebraicNum.java.

        {

                return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
                                .nCtx(), getNativeObject(), precision));
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines