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.