Module Z3.Arithmetic.Real.AlgebraicNumber

module AlgebraicNumber: sig .. end

Algebraic Numbers

val to_upper : Expr.expr -> int -> Expr.expr

Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision. Arithmetic.is_algebraic_number

Returns A numeral Expr of sort Real

val to_lower : Expr.expr -> int -> Expr.expr

Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. Arithmetic.is_algebraic_number

Returns A numeral Expr of sort Real

val to_decimal_string : Expr.expr -> int -> string

Returns a string representation in decimal notation. The result has at most as many decimal places as the int argument provided.

val numeral_to_string : Expr.expr -> string

Returns a string representation of a numeral.