mk_solver method

Z3_solver mk_solver(Z3_context c)

@name Solvers*/ /@{*/ / \brief Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.

If the solver is used in a non incremental way (i.e. no calls to #Z3_solver_push() or #Z3_solver_pop(), and no calls to #Z3_solver_assert() or #Z3_solver_assert_and_track() after checking satisfiability without an intervening #Z3_solver_reset()) then solver1 will be used. This solver will apply Z3's "default" tactic.

The "default" tactic will attempt to probe the logic used by the assertions and will apply a specialized tactic if one is supported. Otherwise the general (and-then simplify smt) tactic will be used.

If the solver is used in an incremental way then the combined solver will switch to using solver2 (which behaves similarly to the general "smt" tactic).

Note however it is possible to set the solver2_timeout, solver2_unknown, and ignore_solver1 parameters of the combined solver to change its behaviour.

The function #Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is \c Z3_L_TRUE) and model construction is enabled. The function #Z3_solver_get_model can also be used even if the result is \c Z3_L_UNDEF, but the returned model is not guaranteed to satisfy quantified assertions.

\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_simple_solver \sa Z3_mk_solver_for_logic \sa Z3_mk_solver_from_tactic

def_API('Z3_mk_solver', SOLVER, (_in(CONTEXT),))

Implementation

Z3_solver mk_solver(
  Z3_context c,
) {
  return _mk_solver(
    c,
  );
}