[−][src]Struct z3::Solver
(Incremental) solver, possibly specialized by a particular tactic or logic.
Implementations
impl<'ctx> Solver<'ctx>
[src]
pub fn new(ctx: &Context) -> Solver<'_>
[src]
Create a new solver. This solver is a "combined solver"
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
Solver::push()
or Solver::pop()
, and no calls to
Solver::assert()
or Solver::assert_and_track()
after checking
satisfiability without an intervening 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 Solver::get_model()
retrieves a model if the
assertions is satisfiable (i.e., the result is
SatResult::Sat
) and model construction is enabled.
The function Solver::get_model()
can also be used even
if the result is SatResult::Unknown
, but the returned model
is not guaranteed to satisfy quantified assertions.
pub fn translate<'dest_ctx>(
&self,
dest: &'dest_ctx Context
) -> Solver<'dest_ctx>
[src]
&self,
dest: &'dest_ctx Context
) -> Solver<'dest_ctx>
pub fn get_context(&self) -> &'ctx Context
[src]
Get this solver's context.
pub fn assert(&self, ast: &Bool<'ctx>)
[src]
Assert a constraint into the solver.
The functions Solver::check()
and
Solver::check_assumptions()
should be
used to check whether the logical context is consistent or not.
See also:
pub fn assert_and_track(&self, ast: &Bool<'ctx>, p: &Bool<'ctx>)
[src]
Assert a constraint a
into the solver, and track it (in the
unsat) core using the Boolean constant p
.
This API is an alternative to
Solver::check_assumptions()
for extracting unsat cores. Both APIs can be used in the same solver.
The unsat core will contain a combination of the Boolean variables
provided using Solver::assert_and_track()
and the Boolean literals provided using
Solver::check_assumptions()
.
See also:
pub fn reset(&self)
[src]
Remove all assertions from the solver.
pub fn check(&self) -> SatResult
[src]
Check whether the assertions in a given solver are consistent or not.
The function Solver::get_model()
retrieves a model if the assertions is satisfiable (i.e., the
result is SatResult::Sat
) and model construction is enabled.
Note that if the call returns SatResult::Unknown
, Z3 does not
ensure that calls to Solver::get_model()
succeed and any models produced in this case are not guaranteed
to satisfy the assertions.
The function Solver::get_proof()
retrieves a proof if proof generation was enabled when the context
was created, and the assertions are unsatisfiable (i.e., the result
is SatResult::Unsat
).
See also:
pub fn check_assumptions(&self, assumptions: &[Bool<'ctx>]) -> SatResult
[src]
Check whether the assertions in the given solver and optional assumptions are consistent or not.
The function
Solver::get_unsat_core()
retrieves the subset of the assumptions used in the
unsatisfiability proof produced by Z3.
See also:
pub fn get_unsat_core(&self) -> Vec<Bool<'ctx>>
[src]
Return a subset of the assumptions provided to either the last
check_assumptions
call, or- sequence of
assert_and_track
calls followed by acheck
call.
These are the assumptions Z3 used in the unsatisfiability proof. Assumptions are available in Z3. They are used to extract unsatisfiable cores. They may be also used to "retract" assumptions. Note that, assumptions are not really "soft constraints", but they can be used to implement them.
See also:
pub fn push(&self)
[src]
pub fn pop(&self, n: u32)
[src]
pub fn get_model(&self) -> Option<Model<'ctx>>
[src]
Retrieve the model for the last Solver::check()
or Solver::check_assumptions()
The error handler is invoked if a model is not available because
the commands above were not invoked for the given solver, or if
the result was Z3_L_FALSE
.
pub fn get_proof(&self) -> Option<impl Ast<'ctx>>
[src]
Retrieve the proof for the last Solver::check()
or Solver::check_assumptions()
The error handler is invoked if proof generation is not enabled,
or if the commands above were not invoked for the given solver,
or if the result was different from Z3_L_FALSE
.
See also:
pub fn get_reason_unknown(&self) -> Option<String>
[src]
Return a brief justification for an "unknown" result (i.e., SatResult::Unknown
) for
the commands Solver::check()
and
Solver::check_assumptions()
pub fn set_params(&self, params: &Params<'ctx>)
[src]
Set the current solver using the given parameters.
Trait Implementations
impl<'ctx> Debug for Solver<'ctx>
[src]
impl<'ctx> Display for Solver<'ctx>
[src]
impl<'ctx> Drop for Solver<'ctx>
[src]
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for Solver<'ctx>
impl<'ctx> !Send for Solver<'ctx>
impl<'ctx> !Sync for Solver<'ctx>
impl<'ctx> Unpin for Solver<'ctx>
impl<'ctx> UnwindSafe for Solver<'ctx>
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,