Trait BooleanVecSet 

pub trait BooleanVecSet: Function {
    // Required methods
    fn singleton_edge<'id>(
        manager: &Self::Manager<'id>,
        var: VarNo,
    ) -> AllocResult<EdgeOfFunc<'id, 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: VarNo,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn subset1_edge<'id>(
        manager: &Self::Manager<'id>,
        set: &EdgeOfFunc<'id, Self>,
        var: VarNo,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn change_edge<'id>(
        manager: &Self::Manager<'id>,
        set: &EdgeOfFunc<'id, Self>,
        var: VarNo,
    ) -> 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 singleton<'id>(
        manager: &Self::Manager<'id>,
        var: VarNo,
    ) -> AllocResult<Self> { ... }
    fn empty<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn base<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn subset0(&self, var: VarNo) -> AllocResult<Self> { ... }
    fn subset1(&self, var: VarNo) -> AllocResult<Self> { ... }
    fn change(&self, var: VarNo) -> 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 BooleanVecSet 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 singleton_edge<'id>( manager: &Self::Manager<'id>, var: VarNo, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::singleton()

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: VarNo, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::subset0()

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

Edge version of Self::subset1()

fn change_edge<'id>( manager: &Self::Manager<'id>, set: &EdgeOfFunc<'id, Self>, var: VarNo, ) -> 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 singleton<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<Self>

Get the singleton set {var}

Panics if var is greater or equal to the number of variables in manager.

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: VarNo) -> AllocResult<Self>

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

Locking behavior: acquires a shared manager lock

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

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

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

Locking behavior: acquires a shared manager lock

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

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

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

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