Struct TermManager 

pub struct TermManager { /* private fields */ }

Type that manages the backend’s “term manager” (or “context”) and subterm sharing.

Most SMT APIs separate the “term manager” (also called “context”), responsible for managing subterm sharing and the creation and lifetime management of term objects, from the “solver”, which is responsible for the actual reasoning.

formally::smt does the same, where TermManager manages subterm sharing (through an underlying instance of TermPool) and a handle to the underlying backend’s term manager (e.g. TermManager in cvc5 or Z3_context in Z3).

The handle to the underlying backend’s manager performs the conversion from Term to the internal representation of terms of the backend (e.g. Z3_ast in Z3).

A term manager is mainly used by giving a reference to it to one or more Solver instances. Solvers built on the same manager can use the same terms which will be converted to the underlying backend’s representation only once, saving time.

Example:

 use formally::{smt::{*, backends::z3::Z3}};

 let manager = Rc::new(TermManager::with_backend(Z3)?);
 let config = Config::new();
 let mut slv1 = Solver::with_manager(&config, manager.clone())?;
 let mut slv2 = Solver::with_manager(&config, manager)?;

 let x1 = slv1.declare(Declaration::constant("x", sort!(Int)))?;
 let x2 = slv2.declare(Declaration::constant("x", sort!(Int)))?;

 // Equivalent declarations/definitions result in the same `Declared`/`Defined` objects
 assert_eq!(x1, x2);

 let t1 = slv1.lookup(term!(* x x), Role::Function)?;
 let t2 = slv2.lookup(term!(* x x), Role::Function)?;

 // Equivalent terms result into the same [Term] objects
 assert_eq!(t1, t2);

Since most SMT APIs are not threadsafe, TermManager is not Send nor Sync and must therefore be accessed and used by a single thread only. However, one can construct it using TermManager::with_pool() and passing a DashPool instance, which is a concurrent TermPool that allows to at least share the same terms among different threads.

Implementations

impl TermManager

pub fn new() -> Result<TermManager>

Construct a TermManager with the default backend (if any is available).

pub fn with_backend_name<'a>( backend: impl Into<Identifier<'a>>, ) -> Result<TermManager>

Construct a TermManager over a given Backend looked up by name, if it exists.

pub fn with_backend(backend: impl Backend) -> Result<TermManager>

Construct a TermManager over a given Backend.

pub fn with_pool( backend: impl Backend, pool: Rc<dyn TermPool>, ) -> Result<TermManager>

Construct a TermManager over a given Backend and TermPool.

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

Return a reference to the underlying TermPool.

Trait Implementations

impl Clone for TermManager

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TermManager

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

Formats the value using the given formatter.