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§
Sourcefn new_var<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>
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.
Sourcefn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>
fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>
Get the always false function ⊥
as edge
Sourcefn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>
fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>
Get the always true function ⊤
as edge
Sourcefn u_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>
fn u_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>
Get the “unknown” function U
as edge
Sourcefn not_edge<'id>(
manager: &Self::Manager<'id>,
edge: &EdgeOfFunc<'id, Self>,
) -> AllocResult<EdgeOfFunc<'id, Self>>
fn not_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>
Compute the negation ¬edge
, edge version
Sourcefn and_edge<'id>(
manager: &Self::Manager<'id>,
lhs: &EdgeOfFunc<'id, Self>,
rhs: &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>>
Compute the conjunction lhs ∧ rhs
, edge version
Sourcefn or_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>>
Compute the disjunction lhs ∨ rhs
, edge version
Sourcefn nand_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>>
Compute the negated conjunction lhs ⊼ rhs
, edge version
Sourcefn nor_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>>
Compute the negated disjunction lhs ⊽ rhs
, edge version
Sourcefn xor_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>>
Compute the exclusive disjunction lhs ⊕ rhs
, edge version
Sourcefn equiv_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>>
Compute the equivalence lhs ↔ rhs
, edge version
Sourcefn imp_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>>
Compute the implication lhs → rhs
, edge version
Sourcefn imp_strict_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>>
Compute the strict implication lhs < rhs
, edge version
Provided Methods§
Sourcefn cofactors(&self) -> Option<(Self, Self, Self)>
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.
Sourcefn cofactor_true(&self) -> Option<Self>
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.
Sourcefn cofactor_unknown(&self) -> Option<Self>
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.
Sourcefn cofactor_false(&self) -> Option<Self>
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.
Sourcefn not(&self) -> AllocResult<Self>
fn not(&self) -> AllocResult<Self>
Compute the negation ¬self
Locking behavior: acquires the manager’s lock for shared access.
Sourcefn not_owned(self) -> AllocResult<Self>
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.
Sourcefn and(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn or(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn nand(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn nor(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn xor(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn equiv(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn imp(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn imp_strict(&self, rhs: &Self) -> AllocResult<Self>
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.
Sourcefn 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_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
.
Sourcefn 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 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
.
Sourcefn not_edge_owned<'id>(
manager: &Self::Manager<'id>,
edge: EdgeOfFunc<'id, Self>,
) -> AllocResult<EdgeOfFunc<'id, Self>>
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()
.
Sourcefn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self>
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.
Sourcefn 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 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.