Function z3_sys::Z3_mk_solver_from_tactic

pub unsafe extern "C" fn Z3_mk_solver_from_tactic(
    c: Z3_context,
    t: Z3_tactic
) -> Z3_solver

Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_solver_push and Z3_solver_pop, but it will always solve each Z3_solver_check from scratch.

NOTE: 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.

See also:

• Z3_mk_solver
• Z3_mk_simple_solver
• Z3_mk_solver_for_logic