Struct Solver

pub struct Solver<'st, B> { /* private fields */ }

The Solver type is the primary entrypoint to interaction with the solver. Checking for validity of a set of assertions requires:

// 1. Set up storage (TODO: document)
let st = smtlib::Storage::new();
// 2. Set up the backend (in this case z3)
let backend = smtlib::backend::z3_binary::Z3Binary::new("z3")?;
// 3. Set up the solver
let mut solver = smtlib::Solver::new(&st, backend)?;
// 4. Declare the necessary constants
let x = Int::new_const(&st, "x");
// 5. Add assertions to the solver
solver.assert(x._eq(12))?;
// 6. Check for validity, and optionally construct a model
let sat_res = solver.check_sat_with_model()?;
// 7. In this case we expect sat, and thus want to extract the model
let model = sat_res.expect_sat()?;
// 8. Interpret the result by extract the values of constants which
//    satisfy the assertions.
match model.eval(x) {
    Some(x) => println!("This is the value of x: {x}"),
    None => panic!("Oh no! This should never happen, as x was part of an assert"),
}

Implementations

impl<'st, B> Solver<'st, B>

where B: Backend,

pub fn new(st: &'st Storage, backend: B) -> Result<Self, Error>

Construct a new solver provided with the backend to use.

The read more about which backends are available, check out the documentation of the backend module.

pub fn st(&self) -> &'st Storage

Get the smtlib storage.

pub fn set_logger(&mut self, logger: impl Logger)

Set the logger for the solver. This is useful for debugging or tracing purposes.

pub fn set_timeout(&mut self, ms: usize) -> Result<(), Error>

Set the timeout for the solver. The timeout is in milliseconds.

pub fn set_logic(&mut self, logic: Logic) -> Result<(), Error>

Explicitly sets the logic for the solver. For some backends this is not required, as they will infer what ever logic fits the current program.

To read more about logics read the documentation of Logic.

pub fn run_command( &mut self, cmd: Command<'st>, ) -> Result<GeneralResponse<'st>, Error>

Runs the given command on the solver, and returns the result.

pub fn assert(&mut self, b: Bool<'st>) -> Result<(), Error>

Adds the constraint of b as an assertion to the solver. To check for satisfiability call Solver::check_sat or Solver::check_sat_with_model.

pub fn check_sat(&mut self) -> Result<SatResult, Error>

Checks for satisfiability of the assertions sent to the solver using Solver::assert.

If you are interested in producing a model satisfying the assertions check out Solver::check_sat.

pub fn check_sat_with_model(&mut self) -> Result<SatResultWithModel<'st>, Error>

Checks for satisfiability of the assertions sent to the solver using Solver::assert, and produces a model in case of sat.

If you are not interested in the produced model, check out Solver::check_sat.

pub fn get_model(&mut self) -> Result<Model<'st>, Error>

Produces the model for satisfying the assertions. If you are looking to retrieve a model after calling Solver::check_sat, consider using Solver::check_sat_with_model instead.

NOTE: This must only be called after having called Solver::check_sat and it returning SatResult::Sat.

pub fn declare_fun(&mut self, fun: &Fun<'st>) -> Result<(), Error>

Declares a function to the solver. For more details refer to the funs module.

pub fn simplify(&mut self, t: Dynamic<'st>) -> Result<&'st Term<'st>, Error>

Simplifies the given term

pub fn scope<T>( &mut self, f: impl FnOnce(&mut Solver<'st, B>) -> Result<T, Error>, ) -> Result<T, Error>

Start a new scope, execute the given closure, and then pop the scope.

A scope is a way to group a set of assertions together, and then later rollback all the assertions to the state before the scope was started.

Trait Implementations

impl<'st, B: Debug> Debug for Solver<'st, B>

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

Formats the value using the given formatter.