Struct Solver 

pub struct Solver { /* private fields */ }

Main interface to SMT solvers.

The Solver type is at the core of formally::smt, providing high-level access to backend solvers.

One can create a Solver in three ways, all accepting a Config reference to configure the solver:

• Solver::new() creates a solver with a default backend and a dedicated TermManager.
• Solver::with_backend() creates a solver with a given backend and a dedicated TermManager.
• Solver::with_manager() creates a solver over the given TermManager.

Solver is responsible to implement name lookup on terms used in definitions and assertions. A term such as term!(> p q) contains three unresolved symbols, ">", "p", and "q". Without name resolution the term would be unusable by the backends.

Solver implements Stack to provide the usual incremental interface of most SAT/SMT solvers.

Implementations

impl Solver

pub fn with_manager( config: &Config, manager: impl Into<Rc<TermManager>>, ) -> Result<Solver>

Create a Solver over a given TermManager.

Use this constructor to share the same TermManager among different solvers.

pub fn with_backend(config: &Config, backend: impl Backend) -> Result<Solver>

Create a Solver over a given Backend.

Backends provided by this crate are defined in formally::smt::backend.

pub fn with_backend_name<'a>( config: &Config, backend: impl Into<Identifier<'a>>, ) -> Result<Solver>

Create a Solver over the given Backend specified by name, if it exists.

Backends provided by this crate are defined in formally::smt::backend.

pub fn new(config: &Config) -> Result<Solver>

Create a Solver with a default backend and a dedicated TermManager.

pub fn logic(&self) -> &dyn Logic

Get the currently selected Logic.

pub fn config(&self, config: &Config) -> Result<()>

Set a new configuration for the solver.

Note that the logic field is ignored when changing configuration after construction.

pub fn env(&self) -> &Env

Get the Env object holding the current scopes for functions and sorts declared and defined in the solver.

pub fn pool(&self) -> &dyn TermPool

Return a reference to the TermPool of the underlying TermManager.

pub fn lookup<T: ToTerm>(&self, term: T, role: Role) -> Result<Term>

Convert a ToTerm object into a Term including name resolution and type checking.

This method uniques a ToTerm object into a Term using the TermPool of the underlying TermManager and then performs name resolution and type checking on the term.

The resulting term is guaranteed to be well typed and fully resolved.

Since terms can describe sorts as well, and SMT-LIBv2 defines two different namespaces for sorts and functions, the Role argument is needed to tell whether the term has to be interpreted as a sort or as a value term.

pub fn lookup_sort<S: ToSort>(&self, sort: &S) -> Result<Sort>

Convert a ToSort object into a Sort including name resolution and type checking.

This method uniques a ToSort object into a Sort and then performs name resolution and type checking on the sort.

The resulting sort is guaranteed to be well-formed and fully resolved.

pub fn lookup_var<S: ToSort>(&self, variable: &Variable<S>) -> Result<Variable>

Create a fully resolved Variable by looking up its sort.

This convenience method is equivalent to constructing a new Variable instance by calling Solver::lookup_sort() on the variable’s sort.

This method is needed to obtain a fully resolved Variable that can be used without further name resolution, but it is not needed when normally using variables to define functions that then refer to them by name.

Example:

 use formally::smt::*;

 let config = Config::default();
 let mut solver = Solver::new(&config)?;

 // we construct the variable directly.
 let x = Variable::new("x", sort!(Int));

 // here the variable `x` is moved and `lookup_var()` is called internally.
 let f = solver.define(Definition::function("f", [x], sort!(Int), term!(* x 2)));

 // here the variable is #expanded in the term so we need to do name resolution earlier
 let y = solver.lookup_var(&Variable::new("y", sort!(Int)))?;
 let g = solver.define(Definition::function("g", [y.clone()], sort!(Int), term!(* #y 2)));

 solver.require(term!(distinct (f 21) (g 21) 42))?;

 assert_eq!(solver.check()?, Answer::No);

pub fn lookup_binding<T: ToTerm>( &self, binding: Binding<Infer, T>, ) -> Result<Binding>

Create a fully resolved Binding by looking up its sort and term.

This convenience method is useful to infer automatically the sort of the binding from its defining term. It is designed to be used in pair with Binding::new().

pub fn declare<R: ToSort, B: ToSort>( &mut self, decl: Declaration<R, B>, ) -> Result<Declared>

Declare a function (or a constant, or a sort).

As explained in the overview, declare() registers a Declaration value in the suitable scope and returns a Declared object that immutably points to the registered Declaration object. The registered Declaration object is not equal to the one passed as argument, in general, because name resolution occurs.

Remember that constants are seen as functions with no arguments, and sorts as constants of the special sort Sort::sort(). See also Declaration::function(), Declaration::constant(), and Declaration::sort() for details.

pub fn define<V: ToSort, R: ToSort, B: ToTerm>( &mut self, def: Definition<V, R, B>, ) -> Result<Defined>

Define a function (or a constant, or a sort).

As explained in the overview, define() registers a Definition value in the suitable scope and returns a Defined object that immutably points to the registered Definition object. The registered Definition object is not equal to the one passed as argument, in general, because name resolution occurs.

Remember that constants are seen as functions with no arguments, and sorts as constants of the special sort Sort::sort(). See also Definition::function(), Definition::constant(), and Definition::sort() for details.

See also the documentation of Solver::lookup_var() to know when name lookup is needed to be done manually on the variables used in a definition.

pub fn require<T: ToTerm>(&mut self, term: T) -> Result<()>

Assert the given term to the current assertion stack

The term undergoes name resolution and must be well-typed and be of sort Core::Bool().

pub fn check(&mut self) -> Result<Answer>

Check the satisfiability of the current assertions.

The return value distinguishes between errors occurred during the solving process (Err(_)) and the case where no error occurred but the solver gave up on finding an answer (Ok(Answer::Unknown)).

pub fn model(&self) -> Result<Option<Model<'_>>>

Get a model of the current assertions, if they were found to be satisfiable.

The return value distinguishes between errors occurred while extracting the model from the backend (Err(_)), and the case where no error occurred but there is no model available (Ok(None)), for example because the last call to check() did not return Ok(Answer::Yes) or because model production was turned off in the solver’s Config.

Note that the representation of model values is still incomplete and only Boolean and numerical values can be currently extracted.

Trait Implementations

impl Stack for Solver

fn push(&mut self) -> Result<()>

Push a new frame in the assertions stack.

The assertion stack includes asserted terms and declared/defined entities. Currently, the :global-declarations option of SMT-LIBv2 is not supported.

fn pop_n(&mut self, n: usize) -> Result<()>

Pops a frame from the assertions stack, doing nothing if there is no frame to remove.

The assertion stack includes asserted terms and declared/defined entities. Currently, the :global-declarations option of SMT-LIBv2 is not supported.

fn pop(&mut self) -> Result<(), DiagnosticEmitted>

Shortcut for pop_n(1)