Function z3_sys::Z3_optimize_get_lower_as_vector [−][src]
pub unsafe extern "C" fn Z3_optimize_get_lower_as_vector(
c: Z3_context,
o: Z3_optimize,
idx: c_uint
) -> Z3_ast_vector
Expand description
Retrieve lower bound value or approximation for the i’th optimization objective.
The returned vector is of length 3. It always contains numerals.
The three numerals are coefficients a, b, c and encode the result of Z3_optimize_get_lower
a * infinity + b + c * epsilon.
c
: - contexto
: - optimization contextidx
: - index of optimization objective