Function z3_sys::Z3_get_algebraic_number_lower

source · 
pub unsafe extern "C" fn Z3_get_algebraic_number_lower(
    c: Z3_context,
    a: Z3_ast,
    precision: c_uint
) -> Z3_ast
Expand description

Return a lower 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)

See also: