mk_solver_for_logic method

Z3_solver mk_solver_for_logic(
  1. Z3_context c,
  2. Z3_symbol logic
)

\brief Create a new solver customized for the given logic. It behaves like #Z3_mk_solver if the logic is unknown or unsupported.

\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.

\sa Z3_mk_solver \sa Z3_mk_simple_solver \sa Z3_mk_solver_from_tactic

def_API('Z3_mk_solver_for_logic', SOLVER, (_in(CONTEXT), _in(SYMBOL)))

Implementation

Z3_solver mk_solver_for_logic(
  Z3_context c,
  Z3_symbol logic,
) {
  return _mk_solver_for_logic(
    c,
    logic,
  );
}