Trait haybale::backend::SolverRef

pub trait SolverRef: Clone + Deref<Target = Btor> {
    type BV: BV<SolverRef = Self>;
    type Array;

    // Required methods
    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>.

Required Associated Types

type BV: BV<SolverRef = Self>

type Array

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

Object Safety

This trait is not object safe.

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>>>

Implementors