Trait oxidd_core::function::TVLFunction

pub trait TVLFunction: Function {
    // Required methods
    fn new_var<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>;
    fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn u_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn not_edge<'id>(
        manager: &Self::Manager<'id>,
        edge: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn and_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn or_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn nand_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn nor_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn xor_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn equiv_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn imp_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn imp_strict_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;

    // Provided methods
    fn f<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn t<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn u<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn cofactors(&self) -> Option<(Self, Self, Self)> { ... }
    fn cofactor_true(&self) -> Option<Self> { ... }
    fn cofactor_unknown(&self) -> Option<Self> { ... }
    fn cofactor_false(&self) -> Option<Self> { ... }
    fn not(&self) -> AllocResult<Self> { ... }
    fn not_owned(self) -> AllocResult<Self> { ... }
    fn and(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn or(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn nand(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn nor(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn xor(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn equiv(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn imp(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn imp_strict(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn cofactors_edge<'a, 'id>(
        manager: &'a Self::Manager<'id>,
        f: &'a EdgeOfFunc<'id, Self>,
    ) -> Option<(Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>)> { ... }
    fn cofactors_node<'a, 'id>(
        tag: ETagOfFunc<'id, Self>,
        node: &'a INodeOfFunc<'id, Self>,
    ) -> (Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>) { ... }
    fn not_edge_owned<'id>(
        manager: &Self::Manager<'id>,
        edge: EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>> { ... }
    fn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self> { ... }
    fn ite_edge<'id>(
        manager: &Self::Manager<'id>,
        if_edge: &EdgeOfFunc<'id, Self>,
        then_edge: &EdgeOfFunc<'id, Self>,
        else_edge: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>> { ... }
}

Function of three valued logic

Required Methods

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

Get a fresh variable, i.e. a function that is true if the variable is true, false if the variable is false, and undefined otherwise. This adds a new level to a decision diagram.

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

Get the always false function ⊥ as edge

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

Get the always true function ⊤ as edge

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

Get the “unknown” function U as edge

fn not_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negation ¬edge, edge version

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

Compute the conjunction lhs ∧ rhs, edge version

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

Compute the disjunction lhs ∨ rhs, edge version

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

Compute the negated conjunction lhs ⊼ rhs, edge version

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

Compute the negated disjunction lhs ⊽ rhs, edge version

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

Compute the exclusive disjunction lhs ⊕ rhs, edge version

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

Compute the equivalence lhs ↔ rhs, edge version

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

Compute the implication lhs → rhs, edge version

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

Compute the strict implication lhs < rhs, edge version

Provided Methods

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

Get the always false function ⊥

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

Get the always true function ⊤

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

Get the “unknown” function U

fn cofactors(&self) -> Option<(Self, Self, Self)>

Get the cofactors (f_true, f_unknown, f_false) of self

Let f(x₀, …, xₙ) be represented by self, where x₀ is (currently) the top-most variable. Then f_true(x₁, …, xₙ) = f(⊤, x₁, …, xₙ) and f_false(x₁, …, xₙ) = f(⊥, x₁, …, xₙ).

Note that the domain of f is 𝔹ⁿ⁺¹ while the domain of f_true and f_false is 𝔹ⁿ.

Returns None iff self references a terminal node. If you only need f_true, f_unknown, or f_false, Self::cofactor_true, Self::cofactor_unknown, or Self::cofactor_false are slightly more efficient.

Locking behavior: acquires the manager’s lock for shared access.

fn cofactor_true(&self) -> Option<Self>

Get the cofactor f_true of self

This method is slightly more efficient than Self::cofactors in case f_unknown and f_false are not needed.

For a more detailed description, see Self::cofactors.

Returns None iff self references a terminal node.

Locking behavior: acquires the manager’s lock for shared access.

fn cofactor_unknown(&self) -> Option<Self>

Get the cofactor f_unknown of self

This method is slightly more efficient than Self::cofactors in case f_true and f_false are not needed.

For a more detailed description, see Self::cofactors.

Returns None iff self references a terminal node.

Locking behavior: acquires the manager’s lock for shared access.

fn cofactor_false(&self) -> Option<Self>

Get the cofactor f_false of self

This method is slightly more efficient than Self::cofactors in case f_true and f_unknown are not needed.

For a more detailed description, see Self::cofactors.

Returns None iff self references a terminal node.

Locking behavior: acquires the manager’s lock for shared access.

fn not(&self) -> AllocResult<Self>

Compute the negation ¬self

Locking behavior: acquires the manager’s lock for shared access.

fn not_owned(self) -> AllocResult<Self>

Compute the negation ¬self, owned version

Compared to Self::not(), this method does not need to clone the function, so when the implementation is using (e.g.) complemented edges, this might be a little bit faster than Self::not().

Locking behavior: acquires the manager’s lock for shared access.

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

Compute the conjunction self ∧ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the disjunction self ∨ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the negated conjunction self ⊼ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the negated disjunction self ⊽ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the exclusive disjunction self ⊕ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the equivalence self ↔ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the implication self → rhs (or self ≤ rhs)

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

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

Compute the strict implication self < rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn cofactors_edge<'a, 'id>( manager: &'a Self::Manager<'id>, f: &'a EdgeOfFunc<'id, Self>, ) -> Option<(Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>)>

Get the cofactors (f_true, f_unknown, f_false) of f, edge version

Returns None iff f references a terminal node. For more details on the semantics of f_true and f_false, see Self::cofactors.

fn cofactors_node<'a, 'id>( tag: ETagOfFunc<'id, Self>, node: &'a INodeOfFunc<'id, Self>, ) -> (Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>)

Get the cofactors (f_true, f_unknown, f_false) of node, assuming an incoming edge with EdgeTag

Returns None iff f references a terminal node. For more details on the semantics of f_true and f_false, see Self::cofactors.

Implementation note: The default implementation assumes that cofactor 0 corresponds to f_true, cofactor 1 corresponds to f_unknown, and cofactor 2 corresponds to f_false.

fn not_edge_owned<'id>( manager: &Self::Manager<'id>, edge: EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negation ¬edge, owned edge version

Compared to Self::not_edge(), this method does not need to clone the edge, so when the implementation is using (e.g.) complemented edges, this might be a little bit faster than Self::not_edge().

fn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self>

Compute if self { then_case } else { else_case }

This is equivalent to (self ∧ then_case) ∨ (¬self ∧ else_case) but possibly more efficient than computing all the conjunctions/disjunctions.

Locking behavior: acquires the manager’s lock for shared access.

Panics if self, then_case, and else_case don’t belong to the same manager.

fn ite_edge<'id>( manager: &Self::Manager<'id>, if_edge: &EdgeOfFunc<'id, Self>, then_edge: &EdgeOfFunc<'id, Self>, else_edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute if if_edge { then_edge } else { else_edge } (edge version)

This is equivalent to (self ∧ then_case) ∨ (¬self ∧ else_case) but possibly more efficient than computing all the conjunctions/disjunctions.

Object Safety

This trait is not object safe.

Implementors