Struct z3::Solver

pub struct Solver<'ctx> { /* private fields */ }

(Incremental) solver, possibly specialized by a particular tactic or logic.

Implementations

impl<'ctx> Solver<'ctx>

pub fn new(ctx: &Context) -> Solver<'_>

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 Z3_L_TRUE) and model construction is enabled. The function 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.

pub fn assert(&self, ast: &Ast<'ctx>)

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:

• Solver::assert_and_track()

pub fn assert_and_track(&self, ast: &Ast<'ctx>, p: &Ast<'ctx>)

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().

Preconditions:

• a must be a Boolean expression
• p must be a Boolean constant (aka variable).

See also:

• Solver::assert()

pub fn reset(&self)

Remove all assertions from the solver.

pub fn check(&self) -> bool

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 Z3_L_TRUE) and model construction is enabled. Note that if the call returns Z3_L_UNDEF, 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 Z3_L_FALSE).

See also:

• Config::set_model_generation()
• Config::set_proof_generation()
• Solver::check_assumptions()

pub fn check_assumptions(&self, assumptions: &[Ast<'ctx>]) -> bool

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:

• Solver::check()

pub fn push(&self)

Create a backtracking point.

The solver contains a stack of assertions.

See also:

• Solver::pop()

pub fn pop(&self, n: u32)

Backtrack n backtracking points.

See also:

• Solver::push()

pub fn get_model(&self) -> Model<'ctx>

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) -> Ast<'ctx>

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:

• Config::set_proof_generation()

Trait Implementations

impl<'ctx> Display for Solver<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for Solver<'ctx>

fn drop(&mut self)

Executes the destructor for this type.