optimize_get_objectives method

Z3_ast_vector optimize_get_objectives(
  1. Z3_context c,
  2. Z3_optimize o
)

\brief Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form \ccode{(+ (if f1 w1 0) (if f2 w2 0) ...)} If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.

def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))

Implementation

Z3_ast_vector optimize_get_objectives(
  Z3_context c,
  Z3_optimize o,
) {
  return _optimize_get_objectives(
    c,
    o,
  );
}