Function z3_sys::Z3_mk_simple_solver [−][src]
pub unsafe extern "C" fn Z3_mk_simple_solver(
c: Z3_context
) -> Z3_solver
Expand description
Create a new incremental solver.
This is equivalent to applying the “smt” tactic.
Unlike Z3_mk_solver()
this solver
- Does not attempt to apply any logic specific tactics.
- Does not change its behaviour based on whether it used incrementally/non-incrementally.
Note that these differences can result in very different performance
compared to Z3_mk_solver()
.
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
.