Trait haybale::backend::SolverRef

pub trait SolverRef: Clone + Deref<Target = Btor> {
    type BV: BV<SolverRef = Self>;
    type Array;
    fn new() -> Self;
    fn duplicate(&self) -> Self;
    fn match_bv(&self, bv: &Self::BV) -> Option<Self::BV>;
    fn match_array(&self, array: &Self::Array) -> Option<Self::Array>;
}

Trait for something which acts as a reference to a boolector::Btor (and possibly may carry other information as well).

This module provides an implementation of SolverRef for Rc<Btor>.

Associated Types

type BV: BV<SolverRef = Self>

type Array

Loading content...

Required methods

fn new() -> Self

Create a new Btor instance, initialize it as necessary, and return a SolverRef to it

fn duplicate(&self) -> Self

As opposed to clone() which merely clones the reference, this function produces a deep copy of the underlying solver instance

fn match_bv(&self, bv: &Self::BV) -> Option<Self::BV>

Given a BV originally created for any SolverRef, get the corresponding BV in this SolverRef. This is only guaranteed to work if the BV was created before the relevant SolverRef::duplicate() was called; that is, it is intended to be used to find the copied version of a given BV in the new SolverRef.

It's also fine to call this with a BV created for this SolverRef itself, in which case you'll just get back Some(bv.clone()).

fn match_array(&self, array: &Self::Array) -> Option<Self::Array>

Given an Array originally created for any SolverRef, get the corresponding Array in this SolverRef. This is only guaranteed to work if the Array was created before the relevant SolverRef::duplicate() was called; that is, it is intended to be used to find the copied version of a given Array in the new SolverRef.

It's also fine to call this with an Array created for this SolverRef itself, in which case you'll just get back Some(array.clone()).

Loading content...

Implementations on Foreign Types

impl SolverRef for Rc<Btor>

type BV = BV<Rc<Btor>>

type Array = Array<Rc<Btor>>

fn new() -> Self

fn duplicate(&self) -> Self

fn match_bv(&self, bv: &BV<Rc<Btor>>) -> Option<BV<Rc<Btor>>>

fn match_array(&self, array: &Array<Rc<Btor>>) -> Option<Array<Rc<Btor>>>

Loading content...

Implementors

Loading content...