Trait oxidd_core::function::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 set of subsets 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 set of subsets of self 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 change(&self, var: &Self) -> AllocResult<Self>

Get the set of subsets derived from self by adding var to the subsets that do not contain var, and removing var from the subsets that contain 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.

Object Safety

This trait is not object safe.

Implementors