Function z3_sys::Z3_optimize_get_objectives

pub unsafe extern "C" fn Z3_optimize_get_objectives(
    c: Z3_context, 
    o: Z3_optimize
) -> Z3_ast_vector

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 (+ (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.