Trait TVLFunction 

pub trait TVLFunction: Function {
    // Required methods
    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 var_edge<'id>(
        manager: &Self::Manager<'id>,
        var: VarNo,
    ) -> AllocResult<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>>;
    fn eval_edge<'id>(
        manager: &Self::Manager<'id>,
        edge: &EdgeOfFunc<'id, Self>,
        args: impl IntoIterator<Item = (VarNo, Option<bool>)>,
    ) -> Option<bool>;

    // 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 var<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<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>> { ... }
    fn eval(
        &self,
        args: impl IntoIterator<Item = (VarNo, Option<bool>)>,
    ) -> Option<bool> { ... }
}

Function of three valued logic

Required Methods

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

Edge version of Self::var()

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

fn eval_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, args: impl IntoIterator<Item = (VarNo, Option<bool>)>, ) -> Option<bool>

Edge version of Self::eval()

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

Get the function that is true if the variable is true, false if the variable is false, and undefined otherwise

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

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.

fn eval( &self, args: impl IntoIterator<Item = (VarNo, Option<bool>)>, ) -> Option<bool>

Evaluate this function

args consists of pairs (variable, value) and determines the valuation for all variables in the function’s domain. The order is irrelevant (except that if the valuation for a variable is given multiple times, the last value counts).

Should there be a decision node for a variable not part of the domain, then unknown is used as the decision value.

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

Panics if any variable number in args is larger that the number of variables in the containing 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