Function z3_sys::Z3_get_algebraic_number_upper[−][src]

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)

See also: