Trait TVLFunction

Source
pub trait TVLFunction: Function {
Show 35 methods // 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>> { ... }
}
Expand description

Function of three valued logic

Required Methods§

Source

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.

Source

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

Get the always false function as edge

Source

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

Get the always true function as edge

Source

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

Get the “unknown” function U as edge

Source

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

Compute the negation ¬edge, edge version

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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§

Source

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

Get the always false function

Source

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

Get the always true function

Source

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

Get the “unknown” function U

Source

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 ftrue(x₁, …, xₙ) = f(⊤, x₁, …, xₙ) and ffalse(x₁, …, xₙ) = f(⊥, x₁, …, xₙ).

Note that the domain of f is 𝔹ⁿ⁺¹ while the domain of ftrue and ffalse 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.

Source

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.

Source

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.

Source

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.

Source

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

Compute the negation ¬self

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

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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().

Source

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.

Source

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.

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§