[−][src]Trait zdd::factory::ZddMaker

pub trait ZddMaker<Label: Eq + Hash + Clone, Lft, Rgt> {
    fn mk_node(&self, lbl: Label, lft: Lft, rgt: Rgt) -> Zdd<Label>;
}

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.

Loading content...

Implementors

impl<'a, 'b, Label: Ord + Eq + Hash + Clone> ZddMaker<Label, &'a HConsed<ZddTree<Label>>, &'b HConsed<ZddTree<Label>>> for Factory<Label>[src]

impl<'a, Label: Ord + Eq + Hash + Clone> ZddMaker<Label, &'a HConsed<ZddTree<Label>>, HConsed<ZddTree<Label>>> for Factory<Label>[src]

impl<'a, Label: Ord + Eq + Hash + Clone> ZddMaker<Label, HConsed<ZddTree<Label>>, &'a HConsed<ZddTree<Label>>> for Factory<Label>[src]

impl<Label: Ord + Eq + Hash + Clone> ZddMaker<Label, HConsed<ZddTree<Label>>, HConsed<ZddTree<Label>>> for Factory<Label>[src]

Loading content...