optimize_assert_soft method

int optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id,)

\brief Assert soft constraint to the optimization context. \param c - context \param o - optimization context \param a - formula \param weight - a penalty for violating soft constraint. Negative weights convert into rewards. \param id - optional identifier to group soft constraints

\sa Z3_optimize_assert \sa Z3_optimize_assert_and_track

def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))

Implementation

int optimize_assert_soft(
  Z3_context c,
  Z3_optimize o,
  Z3_ast a,
  Z3_string weight,
  Z3_symbol id,
) {
  return _optimize_assert_soft(
    c,
    o,
    a,
    weight,
    id,
  );
}