Function z3_sys::Z3_mk_solver

pub unsafe extern "C" fn Z3_mk_solver(c: Z3_context) -> Z3_solver

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 Z3_L_TRUE) and model construction is enabled. The function Z3_solver_get_model can also be used even if the result is Z3_L_UNDEF, but the returned model is not guaranteed to satisfy quantified assertions.

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.