Function z3_sys::Z3_mk_solver [−][src]
pub unsafe extern "C" fn Z3_mk_solver(c: Z3_context) -> Z3_solver
Expand 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
.