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: - context
  • o: - optimization context
  • idx: - index of optimization objective

See also: