Trait BooleanVecSet

pub trait BooleanVecSet: Function {
    // Required methods
    fn new_singleton<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>;
    fn empty_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn base_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn subset0_edge<'id>(
        manager: &Self::Manager<'id>,
        set: &EdgeOfFunc<'id, Self>,
        var: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn subset1_edge<'id>(
        manager: &Self::Manager<'id>,
        set: &EdgeOfFunc<'id, Self>,
        var: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn change_edge<'id>(
        manager: &Self::Manager<'id>,
        set: &EdgeOfFunc<'id, Self>,
        var: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn union_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn intsec_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn diff_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;

    // Provided methods
    fn empty<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn base<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn subset0(&self, var: &Self) -> AllocResult<Self> { ... }
    fn subset1(&self, var: &Self) -> AllocResult<Self> { ... }
    fn change(&self, var: &Self) -> AllocResult<Self> { ... }
    fn union(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn intsec(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn diff(&self, rhs: &Self) -> AllocResult<Self> { ... }
}

Set of Boolean vectors

A Boolean function f: 𝔹ⁿ → 𝔹 may also be regarded as a set S ∈ 𝒫(𝔹ⁿ), where S = {v ∈ 𝔹ⁿ | f(v) = 1}. f is also called the characteristic function of S. We can even view a Boolean vector as a subset of some “Universe” U, so we also have S ∈ 𝒫(𝒫(U)). For example, let U = {a, b, c}. The function a is the set of all sets containing a, {a, ab, abc, ac} (for the sake of readability, we write ab for the set {a, b}). Conversely, the set {a} is the function a ∧ ¬b ∧ ¬c.

Counting the number of elements in a BoolVecSet is equivalent to counting the number of satisfying assignments of its characteristic function. Hence, you may use BooleanFunction::sat_count() for this task.

The functions of this trait can be implemented efficiently for ZBDDs.

As a user of this trait, you are probably most interested in methods like Self::union(), Self::intsec(), and Self::diff(). As an implementor, it suffices to implement the functions operating on edges.

Required Methods

fn new_singleton<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>

Add a new variable to the manager and get the corresponding singleton set

This adds a new level to the decision diagram.

fn empty_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>

Edge version of Self::empty()

fn base_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>

Edge version of Self::base()

fn subset0_edge<'id>( manager: &Self::Manager<'id>, set: &EdgeOfFunc<'id, Self>, var: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::subset0()

fn subset1_edge<'id>( manager: &Self::Manager<'id>, set: &EdgeOfFunc<'id, Self>, var: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::subset1()

fn change_edge<'id>( manager: &Self::Manager<'id>, set: &EdgeOfFunc<'id, Self>, var: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::change()

fn union_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the union lhs ∪ rhs, edge version

fn intsec_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the intersection lhs ∩ rhs, edge version

fn diff_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the set difference lhs ∖ rhs, edge version

Provided Methods

fn empty<'id>(manager: &Self::Manager<'id>) -> Self

Get the empty set ∅

This corresponds to the Boolean function ⊥.

fn base<'id>(manager: &Self::Manager<'id>) -> Self

Get the set {∅}

This corresponds to the Boolean function ¬x₁ ∧ … ∧ ¬xₙ

fn subset0(&self, var: &Self) -> AllocResult<Self>

Get the subset of self not containing var, formally {s ∈ self | var ∉ s}

var must be a singleton set, otherwise the result is unspecified. Ideally, the implementation panics.

Locking behavior: acquires a shared manager lock

Panics if self and var do not belong to the same manager.

fn subset1(&self, var: &Self) -> AllocResult<Self>

Get the subset of self containing var with var removed afterwards, formally {s ∖ {var} | s ∈ self ∧ var ∈ s}

var must be a singleton set, otherwise the result is unspecified. Ideally, the implementation panics.

Locking behavior: acquires a shared manager lock

Panics if self and var do not belong to the same manager.

fn change(&self, var: &Self) -> AllocResult<Self>

Swap subset0 and subset1 with respect to var, formally {s ∪ {var} | s ∈ self ∧ var ∉ s} ∪ {s ∖ {var} | s ∈ self ∧ var ∈ s}

var must be a singleton set, otherwise the result is unspecified. Ideally, the implementation panics.

Locking behavior: acquires a shared manager lock

Panics if self and var do not belong to the same manager.

fn union(&self, rhs: &Self) -> AllocResult<Self>

Compute the union self ∪ rhs

Locking behavior: acquires a shared manager lock

Panics if self and rhs do not belong to the same manager.

fn intsec(&self, rhs: &Self) -> AllocResult<Self>

Compute the intersection self ∩ rhs

Locking behavior: acquires a shared manager lock

Panics if self and rhs do not belong to the same manager.

fn diff(&self, rhs: &Self) -> AllocResult<Self>

Compute the set difference self ∖ rhs

Locking behavior: acquires a shared manager lock

Panics if self and rhs do not belong to the same manager.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors