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:

precision

the 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));
        }