Function z3_sys::Z3_get_algebraic_number_upper
source · pub unsafe extern "C" fn Z3_get_algebraic_number_upper(
c: Z3_context,
a: Z3_ast,
precision: c_uint
) -> Z3_ast
Expand description
Return an upper bound for the given real algebraic number.
The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.
Preconditions:
Z3_is_algebraic_number(c, a)