optimize_get_lower_as_vector method

Z3_ast_vector optimize_get_lower_as_vector(
  1. Z3_context c,
  2. Z3_optimize o,
  3. int idx
)

\brief 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 \c a, \c b, \c c and encode the result of #Z3_optimize_get_lower \ccode{a * infinity + b + c * epsilon}.

\param c - context \param o - optimization context \param idx - index of optimization objective

\sa Z3_optimize_get_lower \sa Z3_optimize_get_upper \sa Z3_optimize_get_upper_as_vector

def_API('Z3_optimize_get_lower_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))

Implementation

Z3_ast_vector optimize_get_lower_as_vector(
  Z3_context c,
  Z3_optimize o,
  int idx,
) {
  return _optimize_get_lower_as_vector(
    c,
    o,
    idx,
  );
}