pub unsafe extern "C" fn Z3_mk_solver(c: Z3_context) -> Z3_solverExpand description
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.