[−][src]Trait zdd::factory::ZddMaker
Provides safe node creation.
Required methods
fn mk_node(&self, lbl: Label, lft: Lft, rgt: Rgt) -> Zdd<Label>
The precise semantics of this function is as follows:
use zdd::* ; let consign = Factory::mk(7) ; let lbl = 0 ; let zero = consign.zero() ; let one = consign.one() ; let lft = zero.clone() ; let rgt = one.clone() ; let zdd1 = { let lft = consign.offset(&lft, &lbl) ; let rgt = consign.change(&rgt, &lbl) ; consign.union(lft, rgt) } ; let zdd2 = consign.mk_node(lbl, &lft, rgt) ; println!("zdd1 = {}", zdd1) ; println!("zdd2 = {}", zdd2) ; assert!(zdd1 == zdd2) ; let lbl = 1 ; let zdd1 = { let lft = consign.offset(&lft, &lbl) ; let rgt = consign.change(&zdd1, &lbl) ; consign.union(lft, rgt) } ; let zdd2 = consign.mk_node(lbl, lft, zdd2) ; println!("zdd1 = {}", zdd1) ; println!("zdd2 = {}", zdd2) ; assert!(zdd1 == zdd2) ; assert_eq!(zdd2.top().unwrap(), 0) ;
So, if lbl
is above all the labels in lft
and rgt
it corresponds to creating the node
Node(lbl, lft, rgt)
(modulo zdd creation rules regarding HasOne
and Zero
) with a
slight overhead.
If lbl
is not above all the labels in lft
and rgt
however (as is the case in the
second call of the example) the construction is safe: the resulting ZDD is well-formed. This
is not the intented usage though, which is why it has slightly weird semantics.
Providing the actual node creation function is way too dangerous as there's a lot of room for screwing up the ZDD well-formed-ness.