diff --git a/examples/bayesian_network_compiler.rs b/examples/bayesian_network_compiler.rs index 842e4f18..0a126ffe 100755 --- a/examples/bayesian_network_compiler.rs +++ b/examples/bayesian_network_compiler.rs @@ -6,7 +6,7 @@ use crate::rsdd::builder::BottomUpBuilder; use clap::Parser; use rsdd::builder::cache::all_app::AllTable; use rsdd::builder::decision_nnf_builder::DecisionNNFBuilder; -use rsdd::builder::sdd_builder; +use rsdd::builder::sdd_builder::{self, SddBuilder}; use rsdd::repr::ddnnf::DDNNFPtr; use rsdd::repr::dtree::DTree; use rsdd::repr::robdd::BddPtr; diff --git a/src/builder/bdd_builder.rs b/src/builder/bdd_builder.rs index eaf3c802..def82a0c 100644 --- a/src/builder/bdd_builder.rs +++ b/src/builder/bdd_builder.rs @@ -84,7 +84,7 @@ impl BddManagerStats { } } -pub trait BddBuilder<'a>: BottomUpBuilder<'a, Ptr = BddPtr<'a>> { +pub trait BddBuilder<'a>: BottomUpBuilder<'a, BddPtr<'a>> { fn eq_bdd(&self, a: BddPtr, b: BddPtr) -> bool; fn get_or_insert(&'a self, bdd: BddNode<'a>) -> BddPtr<'a>; @@ -114,22 +114,22 @@ pub trait BddBuilder<'a>: BottomUpBuilder<'a, Ptr = BddPtr<'a>> { } } -impl<'a, T> BottomUpBuilder<'a> for T +impl<'a, T> BottomUpBuilder<'a, BddPtr<'a>> for T where T: BddBuilder<'a>, { - type Ptr = BddPtr<'a>; + // type Ptr = BddPtr<'a>; - fn true_ptr(&self) -> Self::Ptr { + fn true_ptr(&self) -> BddPtr<'a> { BddPtr::true_ptr() } - fn false_ptr(&self) -> Self::Ptr { + fn false_ptr(&self) -> BddPtr<'a> { BddPtr::false_ptr() } /// Get a pointer to the variable with label `lbl` and polarity `polarity` - fn var(&'a self, label: VarLabel, polarity: bool) -> Self::Ptr { + fn var(&'a self, label: VarLabel, polarity: bool) -> BddPtr<'a> { let bdd = BddNode::new(label, BddPtr::false_ptr(), BddPtr::true_ptr()); let r = self.get_or_insert(bdd); if polarity { @@ -153,30 +153,30 @@ where /// let a_and_not_a = man.and(a, a.neg()); /// assert!(a_and_not_a.is_false()); /// ``` - fn and(&'a self, f: Self::Ptr, g: Self::Ptr) -> Self::Ptr { + fn and(&'a self, f: BddPtr<'a>, g: BddPtr<'a>) -> BddPtr<'a> { self.ite(f, g, BddPtr::false_ptr()) } - fn negate(&'a self, f: Self::Ptr) -> Self::Ptr { + fn negate(&'a self, f: BddPtr<'a>) -> BddPtr<'a> { f.neg() } /// if f then g else h - fn ite(&'a self, f: Self::Ptr, g: Self::Ptr, h: Self::Ptr) -> Self::Ptr { + fn ite(&'a self, f: BddPtr<'a>, g: BddPtr<'a>, h: BddPtr<'a>) -> BddPtr<'a> { self.ite_helper(f, g, h) } /// Compute the Boolean function `f iff g` - fn iff(&'a self, f: Self::Ptr, g: Self::Ptr) -> Self::Ptr { + fn iff(&'a self, f: BddPtr<'a>, g: BddPtr<'a>) -> BddPtr<'a> { self.ite(f, g, g.neg()) } - fn xor(&'a self, f: Self::Ptr, g: Self::Ptr) -> Self::Ptr { + fn xor(&'a self, f: BddPtr<'a>, g: BddPtr<'a>) -> BddPtr<'a> { self.ite(f, g.neg(), g) } /// Existentially quantifies out the variable `lbl` from `f` - fn exists(&'a self, bdd: Self::Ptr, lbl: VarLabel) -> Self::Ptr { + fn exists(&'a self, bdd: BddPtr<'a>, lbl: VarLabel) -> BddPtr<'a> { // TODO this can be optimized by specializing it let v1 = self.condition(bdd, lbl, true); let v2 = self.condition(bdd, lbl, false); @@ -184,14 +184,14 @@ where } /// Compute the Boolean function `f | var = value` - fn condition(&'a self, bdd: Self::Ptr, lbl: VarLabel, value: bool) -> Self::Ptr { + fn condition(&'a self, bdd: BddPtr<'a>, lbl: VarLabel, value: bool) -> BddPtr<'a> { let r = self.cond_helper(bdd, lbl, value); bdd.clear_scratch(); r } /// Compose `g` into `f` by substituting for `lbl` - fn compose(&'a self, f: Self::Ptr, lbl: VarLabel, g: Self::Ptr) -> Self::Ptr { + fn compose(&'a self, f: BddPtr<'a>, lbl: VarLabel, g: BddPtr<'a>) -> BddPtr<'a> { // TODO this can be optimized with a specialized implementation to make // it a single traversal let var = self.var(lbl, true); diff --git a/src/builder/mod.rs b/src/builder/mod.rs index 9713cd71..416dd4e7 100644 --- a/src/builder/mod.rs +++ b/src/builder/mod.rs @@ -10,41 +10,41 @@ pub mod bdd_plan; pub mod decision_nnf_builder; pub mod sdd_builder; -pub trait BottomUpBuilder<'a> { - type Ptr; +pub trait BottomUpBuilder<'a, Ptr> { + // type Ptr; // constants --- can elide the input lifetimes - fn true_ptr(&self) -> Self::Ptr; - fn false_ptr(&self) -> Self::Ptr; + fn true_ptr(&self) -> Ptr; + fn false_ptr(&self) -> Ptr; - fn var(&'a self, label: VarLabel, polarity: bool) -> Self::Ptr; + fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr; // primitive operations - fn and(&'a self, a: Self::Ptr, b: Self::Ptr) -> Self::Ptr; + fn and(&'a self, a: Ptr, b: Ptr) -> Ptr; /// Compute the Boolean function `f || g` /// by default, or is defined using de morgan's law as and - fn or(&'a self, a: Self::Ptr, b: Self::Ptr) -> Self::Ptr { + fn or(&'a self, a: Ptr, b: Ptr) -> Ptr { self.negate(self.and(self.negate(a), self.negate(b))) } - fn negate(&'a self, f: Self::Ptr) -> Self::Ptr; + fn negate(&'a self, f: Ptr) -> Ptr; /// if f then g else h - fn ite(&'a self, f: Self::Ptr, g: Self::Ptr, h: Self::Ptr) -> Self::Ptr; + fn ite(&'a self, f: Ptr, g: Ptr, h: Ptr) -> Ptr; /// if and only if (i.e., Boolean equality) - fn iff(&'a self, a: Self::Ptr, b: Self::Ptr) -> Self::Ptr; + fn iff(&'a self, a: Ptr, b: Ptr) -> Ptr; /// logical exclusive-or - fn xor(&'a self, a: Self::Ptr, b: Self::Ptr) -> Self::Ptr; + fn xor(&'a self, a: Ptr, b: Ptr) -> Ptr; /// existentially quantifies `v` out of `f` - fn exists(&'a self, f: Self::Ptr, v: VarLabel) -> Self::Ptr; + fn exists(&'a self, f: Ptr, v: VarLabel) -> Ptr; /// conditions f | v = value - fn condition(&'a self, a: Self::Ptr, v: VarLabel, value: bool) -> Self::Ptr; + fn condition(&'a self, a: Ptr, v: VarLabel, value: bool) -> Ptr; /// compose g into f for variable v /// I.e., computes the logical function (exists v. (g <=> v) /\ f). - fn compose(&'a self, f: Self::Ptr, lbl: VarLabel, g: Self::Ptr) -> Self::Ptr; + fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr; } diff --git a/src/builder/sdd_builder.rs b/src/builder/sdd_builder.rs index 74be5a72..67113075 100644 --- a/src/builder/sdd_builder.rs +++ b/src/builder/sdd_builder.rs @@ -53,293 +53,38 @@ impl Default for SddStats { } } -// pub trait SddBuilder<'a>: BottomUpBuilder<'a> { -// type SddPtr: PartialEq; +// pub trait SddBottomUpBuilder<'a>: BottomUpBuilder<'a, Ptr=SddPtr<'a>> {} -// fn sdd_eq(&'a self, a: Self::SddPtr, b: Self::SddPtr) -> bool { -// a == b -// } -// } - -// impl<'a, T> BottomUpBuilder<'a> for T where T: SddBuilder<'a> { -// type Ptr = T::SddPtr; - -// fn negate(&'a self, f: Self::Ptr) -> Self::Ptr { -// f.neg() -// } -// } - -pub struct SddManager<'a> { - vtree: VTreeManager, - stats: SddStats, - should_compress: bool, - // tables - bdd_tbl: RefCell>>, - sdd_tbl: RefCell>>, - // caches - ite_cache: RefCell>>, - app_cache: RefCell, SddPtr<'a>>>, -} - -impl<'a> BottomUpBuilder<'a> for SddManager<'a> { - type Ptr = SddPtr<'a>; - - fn true_ptr(&self) -> Self::Ptr { - SddPtr::PtrTrue - } - - fn false_ptr(&self) -> Self::Ptr { - SddPtr::PtrFalse - } - - fn var(&'a self, label: VarLabel, polarity: bool) -> Self::Ptr { - SddPtr::Var(label, polarity) - } - - fn negate(&'a self, f: Self::Ptr) -> Self::Ptr { - f.neg() - } - - fn and(&'a self, a: Self::Ptr, b: Self::Ptr) -> Self::Ptr { - // println!("and a: {}\nb: {}", self.print_sdd(a), self.print_sdd(b)); - // first, check for a base case - match (a, b) { - (a, b) if self.is_true(a) => return b, - (a, b) if self.is_true(b) => return a, - (a, _) if self.is_false(a) => return SddPtr::false_ptr(), - (_, b) if self.is_false(b) => return SddPtr::false_ptr(), - (a, b) if self.sdd_eq(a, b) => return a, - (a, b) if self.sdd_eq(a, b.neg()) => return SddPtr::false_ptr(), - _ => (), - }; - - // normalize so `a` is always prime if possible - let (a, b) = if self.get_vtree_idx(a) == self.get_vtree_idx(b) - || self - .vtree - .is_prime_index(self.get_vtree_idx(a), self.get_vtree_idx(b)) - { - (a, b) - } else { - (b, a) - }; - - { - let app_cache = self.app_cache.borrow(); - // check if we have this application cached - if let Some(x) = app_cache.get(&SddAnd::new(a, b)) { - // self.stats.num_app_cache_hits += 1; - return *x; - } - } - - let av = self.get_vtree_idx(a); - let bv = self.get_vtree_idx(b); - let lca = self.vtree.lca(av, bv); - - // now we determine the current iterator for primes and subs - // consider the following example vtree: - // 3 - // 1 5 - // 0 2 4 6 - // 4 cases: - // 1. `a` and `b` have the same vtree - // 2. The lca is `a` - // 3. The lca is `b` - // 4. The lca is a shared parent equal to neither - // we can only conjoin two SDD nodes if they are normalized with respect - // to the same vtree; the following code does this for each of the - // above cases. - let r = if av == bv { - self.and_cartesian(a, b, lca) - } else if lca == av { - self.and_sub_desc(a, b) - } else if lca == bv { - self.and_prime_desc(b, a) - } else { - self.and_indep(a, b, lca) - }; - - // cache and return - self.app_cache.borrow_mut().insert(SddAnd::new(a, b), r); - r - } - - fn or(&'a self, a: Self::Ptr, b: Self::Ptr) -> Self::Ptr { - self.and(a.neg(), b.neg()).neg() - } - - /// Computes `f | var = value` - /// TODO: This is highly inefficient, will re-traverse nodes, needs a cache - /// TODO : this can bail out early by checking the vtree - fn condition(&'a self, f: Self::Ptr, lbl: VarLabel, value: bool) -> Self::Ptr { - // self.stats.num_rec += 1; - match f { - SddPtr::PtrTrue | SddPtr::PtrFalse => f, - SddPtr::Var(label, polarity) => { - if label == lbl { - if polarity == value { - SddPtr::PtrTrue - } else { - SddPtr::PtrFalse - } - } else { - f - } - } - // if f.is_bdd() { - // if f.topvar() == lbl { - // if !f.is_compl() == value { - // return f.high(); - // } else { - // return f.low(); - // } - // } else { - // let l = self.condition(f.low(), lbl, value); - // let h = self.condition(f.high(), lbl, value); - // return self.unique_bdd(BinarySDD::new(f.topvar(), l, h)); - // } - // } - _ => { - let mut v = Vec::new(); - // f is a node; recurse and compress the result - for a in f.node_iter() { - let prime = a.prime(); - let sub = a.sub(); - let newp = self.condition(prime, lbl, value); - let sub = if f.is_neg() { sub.neg() } else { sub }; - if self.is_false(newp) { - continue; - }; - let news = self.condition(sub, lbl, value); - if self.is_true(newp) { - return news; - } - v.push(SddAnd::new(newp, news)); - } - self.canonicalize(v, f.vtree()) - } - } - } - - /// Computes the SDD representing the logical function `if f then g else h` - fn ite(&'a self, f: Self::Ptr, g: Self::Ptr, h: Self::Ptr) -> Self::Ptr { - let ite = Ite::new(|a, b| self.vtree.is_prime(a, b), f, g, h); - if let Ite::IteConst(f) = ite { - return f; - } - - let hash = self.ite_cache.borrow().hash(&ite); - if let Some(v) = self.ite_cache.borrow().get(ite, hash) { - return v; - } - - // TODO make this a primitive operation - let fg = self.and(f, g); - let negfh = self.and(f.neg(), h); - let r = self.or(fg, negfh); - self.ite_cache.borrow_mut().insert(ite, r, hash); - r - } - - /// Computes the SDD representing the logical function `f <=> g` - fn iff(&'a self, f: Self::Ptr, g: Self::Ptr) -> Self::Ptr { - self.ite(f, g, g.neg()) - } - - /// Computes the SDD representing the logical function `f xor g` - fn xor(&'a self, f: Self::Ptr, g: Self::Ptr) -> Self::Ptr { - self.ite(f, g.neg(), g) - } - - /// Existentially quantifies out the variable `lbl` from `f` - fn exists(&'a self, sdd: Self::Ptr, lbl: VarLabel) -> Self::Ptr { - // TODO this can be optimized by specializing it - let v1 = self.condition(sdd, lbl, true); - let v2 = self.condition(sdd, lbl, false); - self.or(v1, v2) - } - - /// Compose `g` into `f` by substituting for `lbl` - fn compose(&'a self, _f: Self::Ptr, _lbl: VarLabel, _g: Self::Ptr) -> Self::Ptr { - panic!("not impl") - // TODO this can be optimized with a specialized implementation to make - // it a single traversal - // let var = self.var(lbl, true); - // let iff = self.iff(var, g); - // let a = self.and(iff, f); - // self.exists(a, lbl) - } -} - -impl<'a> SddManager<'a> { - pub fn new(vtree: VTree) -> SddManager<'a> { - let vtree_man = VTreeManager::new(vtree); - SddManager { - stats: SddStats::new(), - ite_cache: RefCell::new(AllTable::new()), - app_cache: RefCell::new(HashMap::new()), - bdd_tbl: RefCell::new(BackedRobinhoodTable::new()), - sdd_tbl: RefCell::new(BackedRobinhoodTable::new()), - vtree: vtree_man, - should_compress: true, - } - } +pub trait SddBuilder<'a>: BottomUpBuilder<'a, SddPtr<'a>> { + // internal data structures + fn get_vtree_manager(&self) -> &VTreeManager; - pub fn set_compression(&mut self, b: bool) { - self.should_compress = b - } + fn app_cache_get(&self, and: &SddAnd<'a>) -> Option>; + fn app_cache_insert(&self, and: SddAnd<'a>, ptr: SddPtr<'a>); - pub fn get_vtree_root(&self) -> &VTree { - self.vtree.vtree_root() - } + fn ite_cache_hash(&self, ite: &Ite) -> u64; + fn ite_cache_get(&self, ite: Ite>, hash: u64) -> Option; + fn ite_cache_insert(&self, ite: Ite>, res: SddPtr<'a>, hash: u64); - pub fn get_vtree_manager(&self) -> &VTreeManager { - &self.vtree - } + fn get_or_insert_bdd(&'a self, bdd: BinarySDD<'a>) -> &BinarySDD<'a>; + fn get_or_insert_sdd(&'a self, or: SddOr<'a>) -> &SddOr<'a>; + fn node_iter(&self) -> Vec; - pub fn num_vars(&self) -> usize { - self.vtree.num_vars() - } + // equality + fn sdd_eq(&'a self, a: SddPtr<'a>, b: SddPtr<'a>) -> bool; - /// Canonicalizes the list of (prime, sub) terms in-place - /// `node`: a list of (prime, sub) pairs - fn compress(&'a self, node: &mut Vec>) { - // self.stats.num_compr += 1; - for i in 0..node.len() { - // see if we can compress i - let mut j = i + 1; - while j < node.len() { - if self.sdd_eq(node[i].sub(), node[j].sub()) { - // self.stats.num_compr_and += 1; - // compress j into i and remove j from the node list - node[i] = SddAnd::new(self.or(node[i].prime(), node[j].prime()), node[i].sub()); - node.swap_remove(j); - } else { - j += 1; - } - } - } + fn is_true(&'a self, a: SddPtr<'a>) -> bool { + self.sdd_eq(a, SddPtr::PtrTrue) } - pub fn get_vtree(&self, ptr: SddPtr) -> &VTree { - match ptr { - SddPtr::Var(lbl, _) => { - let idx = self.vtree.get_varlabel_idx(lbl); - self.vtree.get_idx(idx) - } - SddPtr::Compl(_) | SddPtr::Reg(_) => self.vtree.get_idx(ptr.vtree()), - _ => panic!("called vtree on constant"), - } + fn is_false(&'a self, a: SddPtr<'a>) -> bool { + self.sdd_eq(a, SddPtr::PtrFalse) } - pub fn get_vtree_idx(&self, ptr: SddPtr) -> VTreeIndex { - match ptr { - SddPtr::Var(lbl, _) => self.vtree.get_varlabel_idx(lbl), - SddPtr::BDD(_) | SddPtr::ComplBDD(_) | SddPtr::Compl(_) | SddPtr::Reg(_) => ptr.vtree(), - _ => panic!("called vtree on constant"), - } - } + // compression & canonicalization + fn set_compression(&mut self, b: bool); + fn compress(&'a self, node: &mut Vec>); + fn canonicalize(&'a self, node: Vec>, table: VTreeIndex) -> SddPtr<'a>; fn unique_or(&'a self, mut node: Vec>, table: VTreeIndex) -> SddPtr<'a> { // check if it is a BDD; if it is, return that @@ -364,98 +109,47 @@ impl<'a> SddManager<'a> { } } - unsafe { - let tbl = &mut *self.sdd_tbl.as_ptr(); - - node.sort_by_key(|a| a.prime()); - if node[0].sub().is_neg() || self.is_false(node[0].sub()) || node[0].sub().is_neg_var() - { - for x in node.iter_mut() { - *x = SddAnd::new(x.prime(), x.sub().neg()); - } - SddPtr::Reg(tbl.get_or_insert(SddOr::new(node, table))).neg() - } else { - SddPtr::Reg(tbl.get_or_insert(SddOr::new(node, table))) + node.sort_by_key(|a| a.prime()); + if node[0].sub().is_neg() || self.is_false(node[0].sub()) || node[0].sub().is_neg_var() { + for x in node.iter_mut() { + *x = SddAnd::new(x.prime(), x.sub().neg()); } + SddPtr::Reg(self.get_or_insert_sdd(SddOr::new(node, table))).neg() + } else { + SddPtr::Reg(self.get_or_insert_sdd(SddOr::new(node, table))) } } fn unique_bdd(&'a self, bdd: BinarySDD<'a>) -> SddPtr<'a> { - unsafe { - let tbl = &mut *self.bdd_tbl.as_ptr(); - if bdd.high() == bdd.low() { - return bdd.high(); - } - if self.is_false(bdd.high()) && self.is_true(bdd.low()) { - return SddPtr::Var(bdd.label(), false); - } - if self.is_true(bdd.high()) && self.is_false(bdd.low()) { - return SddPtr::Var(bdd.label(), true); - } - - if bdd.high().is_neg() || self.is_false(bdd.high()) || bdd.high().is_neg_var() { - let low = bdd.low().neg(); - let high = bdd.high().neg(); - let neg_bdd = BinarySDD::new(bdd.label(), low, high, bdd.vtree()); + if bdd.high() == bdd.low() { + return bdd.high(); + } + if self.is_false(bdd.high()) && self.is_true(bdd.low()) { + return SddPtr::Var(bdd.label(), false); + } + if self.is_true(bdd.high()) && self.is_false(bdd.low()) { + return SddPtr::Var(bdd.label(), true); + } - let unique = tbl.get_or_insert(neg_bdd); + if bdd.high().is_neg() || self.is_false(bdd.high()) || bdd.high().is_neg_var() { + let low = bdd.low().neg(); + let high = bdd.high().neg(); + let neg_bdd = BinarySDD::new(bdd.label(), low, high, bdd.vtree()); - return SddPtr::BDD(unique).neg(); - } + let unique = self.get_or_insert_bdd(neg_bdd); - SddPtr::BDD(tbl.get_or_insert(bdd)) + return SddPtr::BDD(unique).neg(); } + + SddPtr::BDD(self.get_or_insert_bdd(bdd)) } - #[inline] - fn canonicalize_base_case(&'a self, node: &Vec>) -> Option> { - if node.is_empty() { - return Some(SddPtr::true_ptr()); - } - if node.len() == 1 { - if self.is_true(node[0].prime()) { - return Some(node[0].sub()); - } - - if self.is_false(node[0].sub()) { - return Some(SddPtr::false_ptr()); - } - } - if node.len() == 2 { - if self.is_true(node[0].sub()) && self.is_false(node[1].sub()) { - return Some(node[0].prime()); - } else if self.is_false(node[0].sub()) && self.is_true(node[1].sub()) { - return Some(node[1].prime()); - } - } - None - } - - /// Returns a canonicalized SDD pointer from a list of (prime, sub) pairs - fn canonicalize(&'a self, mut node: Vec>, table: VTreeIndex) -> SddPtr<'a> { - // check for base cases before compression - if let Some(sdd) = self.canonicalize_base_case(&node) { - return sdd; - } - - if self.should_compress { - self.compress(&mut node); - - // check for a base case after compression (compression can sometimes - // reduce node counts to a base case) - if let Some(sdd) = self.canonicalize_base_case(&node) { - return sdd; - } - } - - self.unique_or(node, table) - } - + // calc /// conjoin two SDDs that are in independent vtrees /// a is prime to b fn and_indep(&'a self, a: SddPtr<'a>, b: SddPtr<'a>, lca: VTreeIndex) -> SddPtr<'a> { // check if this is a right-linear fragment and construct the relevant SDD type - if self.vtree.get_idx(lca).is_right_linear() { + if self.get_vtree_manager().get_idx(lca).is_right_linear() { // a is a right-linear decision for b; construct a binary decision let bdd = if a.is_neg_var() { BinarySDD::new(a.get_var_label(), b, SddPtr::false_ptr(), lca) @@ -587,7 +281,7 @@ impl<'a> SddManager<'a> { // check if a and b are both binary SDDs; if so, we apply BDD conjunction here if let SddPtr::BDD(or) | SddPtr::ComplBDD(or) = a { - if self.vtree.get_idx(lca).is_right_linear() { + if self.get_vtree_manager().get_idx(lca).is_right_linear() { let l = self.and(a.low(), b.low()); let h = self.and(a.high(), b.high()); return self.unique_bdd(BinarySDD::new(or.label(), l, h, lca)); @@ -648,201 +342,525 @@ impl<'a> SddManager<'a> { } } - // canonicalize - self.canonicalize(r, lca) + // canonicalize + self.canonicalize(r, lca) + } + + // helpers + + fn get_vtree_root(&self) -> &VTree { + self.get_vtree_manager().vtree_root() + } + + fn num_vars(&self) -> usize { + self.get_vtree_manager().num_vars() + } + + fn get_vtree(&self, ptr: SddPtr) -> &VTree { + match ptr { + SddPtr::Var(lbl, _) => { + let idx = self.get_vtree_manager().get_varlabel_idx(lbl); + self.get_vtree_manager().get_idx(idx) + } + SddPtr::Compl(_) | SddPtr::Reg(_) => self.get_vtree_manager().get_idx(ptr.vtree()), + _ => panic!("called vtree on constant"), + } + } + + fn get_vtree_idx(&self, ptr: SddPtr) -> VTreeIndex { + match ptr { + SddPtr::Var(lbl, _) => self.get_vtree_manager().get_varlabel_idx(lbl), + SddPtr::BDD(_) | SddPtr::ComplBDD(_) | SddPtr::Compl(_) | SddPtr::Reg(_) => ptr.vtree(), + _ => panic!("called vtree on constant"), + } + } + + /// compile an SDD from an input CNF + /// #[allow(clippy::wrong_self_convention)] // this is a naming thing; consider renaming in the future + fn from_cnf(&'a self, cnf: &Cnf) -> SddPtr<'a> { + let mut cvec: Vec = Vec::with_capacity(cnf.clauses().len()); + if cnf.clauses().is_empty() { + return SddPtr::true_ptr(); + } + // check if there is an empty clause -- if so, UNSAT + if cnf.clauses().iter().any(|x| x.is_empty()) { + return SddPtr::false_ptr(); + } + + // sort the clauses based on a best-effort bottom-up ordering of clauses + let mut cnf_sorted = cnf.clauses().to_vec(); + cnf_sorted.sort_by(|c1, c2| { + // order the clause with the first-most variable last + let fst1 = c1 + .iter() + .max_by(|l1, l2| { + if self + .get_vtree_manager() + .is_prime_var(l1.get_label(), l2.get_label()) + { + Ordering::Less + } else { + Ordering::Equal + } + }) + .unwrap(); + let fst2 = c2 + .iter() + .max_by(|l1, l2| { + if self + .get_vtree_manager() + .is_prime_var(l1.get_label(), l2.get_label()) + { + Ordering::Less + } else { + Ordering::Equal + } + }) + .unwrap(); + if self + .get_vtree_manager() + .is_prime_var(fst1.get_label(), fst2.get_label()) + { + Ordering::Less + } else { + Ordering::Equal + } + }); + + for lit_vec in cnf_sorted.iter() { + let (vlabel, val) = (lit_vec[0].get_label(), lit_vec[0].get_polarity()); + let mut bdd = SddPtr::Var(vlabel, val); + for lit in lit_vec { + let (vlabel, val) = (lit.get_label(), lit.get_polarity()); + let var = SddPtr::Var(vlabel, val); + bdd = self.or(bdd, var); + } + cvec.push(bdd); + } + // now cvec has a list of all the clauses; collapse it down + let r = self.from_cnf_helper(&cvec); + match r { + None => SddPtr::true_ptr(), + Some(x) => x, + } + } + + #[allow(clippy::wrong_self_convention)] // this is a naming thing; consider renaming in the future + fn from_cnf_helper(&'a self, vec: &[SddPtr<'a>]) -> Option> { + if vec.is_empty() { + None + } else if vec.len() == 1 { + Some(vec[0]) + } else { + let (l, r) = vec.split_at(vec.len() / 2); + let sub_l = self.from_cnf_helper(l); + let sub_r = self.from_cnf_helper(r); + match (sub_l, sub_r) { + (None, None) => None, + (Some(v), None) | (None, Some(v)) => Some(v), + (Some(l), Some(r)) => Some(self.and(l, r)), + } + } + } + + fn from_logical_expr(&mut self, _expr: &LogicalExpr) -> SddPtr { + panic!("not impl") + // match expr { + // &LogicalExpr::Literal(lbl, polarity) => self.var(VarLabel::new(lbl as u64), polarity), + // &LogicalExpr::Not(ref e) => { + // let e = self.from_logical_expr(e); + // e.neg() + // } + // &LogicalExpr::And(ref l, ref r) => { + // let r1 = self.from_logical_expr(l); + // let r2 = self.from_logical_expr(r); + // self.and(r1, r2) + // } + // &LogicalExpr::Or(ref l, ref r) => { + // let r1 = self.from_logical_expr(l); + // let r2 = self.from_logical_expr(r); + // self.or(r1, r2) + // } + // &LogicalExpr::Xor(ref l, ref r) => { + // let r1 = self.from_logical_expr(l); + // let r2 = self.from_logical_expr(r); + // self.xor(r1, r2) + // } + // &LogicalExpr::Iff(ref l, ref r) => { + // let r1 = self.from_logical_expr(l); + // let r2 = self.from_logical_expr(r); + // self.iff(r1, r2) + // } + // &LogicalExpr::Ite { + // ref guard, + // ref thn, + // ref els, + // } => { + // let g = self.from_logical_expr(guard); + // let thn = self.from_logical_expr(thn); + // let els = self.from_logical_expr(els); + // self.ite(g, thn, els) + // } + // } + } + + fn print_sdd(&'a self, ptr: SddPtr<'a>) -> String { + use pretty::*; + fn helper(ptr: SddPtr) -> Doc<'static, BoxDoc<'static>> { + match ptr { + SddPtr::PtrTrue => Doc::from("T"), + SddPtr::PtrFalse => Doc::from("F"), + SddPtr::Var(label, polarity) => Doc::from(format!( + "{}{}", + if polarity { "" } else { "!" }, + label.value() + )), + SddPtr::BDD(bdd) | SddPtr::ComplBDD(bdd) => { + let l = helper(bdd.low()); + let h = helper(bdd.high()); + let mut doc: Doc = Doc::from(""); + doc = doc.append(Doc::newline()).append( + (Doc::from(format!("ITE {:?} {}", ptr, bdd.label().value())) + .append(Doc::newline()) + .append(h.append(Doc::newline()).append(l))) + .nest(2), + ); + doc + } + SddPtr::Reg(or) | SddPtr::Compl(or) => { + let mut doc: Doc = Doc::from(""); + for a in or.nodes.iter() { + let sub = a.sub(); + let prime = a.prime(); + let s = if ptr.is_neg() { sub.neg() } else { sub }; + let new_s1 = helper(prime); + let new_s2 = helper(s); + doc = doc.append(Doc::newline()).append( + (Doc::from("/\\") + .append(Doc::newline()) + .append(new_s1.append(Doc::newline()).append(new_s2))) + .nest(2), + ); + } + let d = Doc::from(format!("\\/ {:?}", ptr)); + d.append(doc.nest(2)) + } + } + } + let d = helper(ptr); + let mut w = Vec::new(); + d.render(10, &mut w).unwrap(); + String::from_utf8(w).unwrap() + } + + fn stats(&self) -> &SddStats; + fn num_logically_redundant(&self) -> usize; +} + +impl<'a, T> BottomUpBuilder<'a, SddPtr<'a>> for T +where + T: SddBuilder<'a>, +{ + #[inline] + fn true_ptr(&self) -> SddPtr<'a> { + SddPtr::PtrTrue + } + + #[inline] + fn false_ptr(&self) -> SddPtr<'a> { + SddPtr::PtrFalse + } + + #[inline] + fn var(&'a self, label: VarLabel, polarity: bool) -> SddPtr<'a> { + SddPtr::Var(label, polarity) + } + + #[inline] + fn negate(&'a self, f: SddPtr<'a>) -> SddPtr<'a> { + f.neg() + } + + fn and(&'a self, a: SddPtr<'a>, b: SddPtr<'a>) -> SddPtr<'a> { + // println!("and a: {}\nb: {}", self.print_sdd(a), self.print_sdd(b)); + // first, check for a base case + match (a, b) { + (a, b) if self.is_true(a) => return b, + (a, b) if self.is_true(b) => return a, + (a, _) if self.is_false(a) => return SddPtr::false_ptr(), + (_, b) if self.is_false(b) => return SddPtr::false_ptr(), + (a, b) if self.sdd_eq(a, b) => return a, + (a, b) if self.sdd_eq(a, b.neg()) => return SddPtr::false_ptr(), + _ => (), + }; + + // normalize so `a` is always prime if possible + let (a, b) = if self.get_vtree_idx(a) == self.get_vtree_idx(b) + || self + .get_vtree_manager() + .is_prime_index(self.get_vtree_idx(a), self.get_vtree_idx(b)) + { + (a, b) + } else { + (b, a) + }; + + // check if we have this application cached + if let Some(x) = self.app_cache_get(&SddAnd::new(a, b)) { + // self.stats.num_app_cache_hits += 1; + return x; + } + + let av = self.get_vtree_idx(a); + let bv = self.get_vtree_idx(b); + let lca = self.get_vtree_manager().lca(av, bv); + + // now we determine the current iterator for primes and subs + // consider the following example vtree: + // 3 + // 1 5 + // 0 2 4 6 + // 4 cases: + // 1. `a` and `b` have the same vtree + // 2. The lca is `a` + // 3. The lca is `b` + // 4. The lca is a shared parent equal to neither + // we can only conjoin two SDD nodes if they are normalized with respect + // to the same vtree; the following code does this for each of the + // above cases. + let r = if av == bv { + self.and_cartesian(a, b, lca) + } else if lca == av { + self.and_sub_desc(a, b) + } else if lca == bv { + self.and_prime_desc(b, a) + } else { + self.and_indep(a, b, lca) + }; + + // cache and return + self.app_cache_insert(SddAnd::new(a, b), r); + r + } + + // fn or(&'a self, a: SddPtr<'a>, b: SddPtr<'a>) -> SddPtr<'a> { + // self.and(a.neg(), b.neg()).neg() + // } + + /// Computes `f | var = value` + /// TODO: This is highly inefficient, will re-traverse nodes, needs a cache + /// TODO : this can bail out early by checking the vtree + fn condition(&'a self, f: SddPtr<'a>, lbl: VarLabel, value: bool) -> SddPtr<'a> { + // self.stats.num_rec += 1; + match f { + SddPtr::PtrTrue | SddPtr::PtrFalse => f, + SddPtr::Var(label, polarity) => { + if label == lbl { + if polarity == value { + SddPtr::PtrTrue + } else { + SddPtr::PtrFalse + } + } else { + f + } + } + // if f.is_bdd() { + // if f.topvar() == lbl { + // if !f.is_compl() == value { + // return f.high(); + // } else { + // return f.low(); + // } + // } else { + // let l = self.condition(f.low(), lbl, value); + // let h = self.condition(f.high(), lbl, value); + // return self.unique_bdd(BinarySDD::new(f.topvar(), l, h)); + // } + // } + _ => { + let mut v = Vec::new(); + // f is a node; recurse and compress the result + for a in f.node_iter() { + let prime = a.prime(); + let sub = a.sub(); + let newp = self.condition(prime, lbl, value); + let sub = if f.is_neg() { sub.neg() } else { sub }; + if self.is_false(newp) { + continue; + }; + let news = self.condition(sub, lbl, value); + if self.is_true(newp) { + return news; + } + v.push(SddAnd::new(newp, news)); + } + self.canonicalize(v, f.vtree()) + } + } + } + + /// Computes the SDD representing the logical function `if f then g else h` + fn ite(&'a self, f: SddPtr<'a>, g: SddPtr<'a>, h: SddPtr<'a>) -> SddPtr<'a> { + let ite = Ite::new(|a, b| self.get_vtree_manager().is_prime(a, b), f, g, h); + if let Ite::IteConst(f) = ite { + return f; + } + + let hash = self.ite_cache_hash(&ite); + if let Some(v) = self.ite_cache_get(ite, hash) { + return v; + } + + // TODO make this a primitive operation + let fg = self.and(f, g); + let negfh = self.and(f.neg(), h); + let r = self.or(fg, negfh); + self.ite_cache_insert(ite, r, hash); + r + } + + /// Computes the SDD representing the logical function `f <=> g` + fn iff(&'a self, f: SddPtr<'a>, g: SddPtr<'a>) -> SddPtr<'a> { + self.ite(f, g, g.neg()) + } + + /// Computes the SDD representing the logical function `f xor g` + fn xor(&'a self, f: SddPtr<'a>, g: SddPtr<'a>) -> SddPtr<'a> { + self.ite(f, g.neg(), g) + } + + /// Existentially quantifies out the variable `lbl` from `f` + fn exists(&'a self, sdd: SddPtr<'a>, lbl: VarLabel) -> SddPtr<'a> { + // TODO this can be optimized by specializing it + let v1 = self.condition(sdd, lbl, true); + let v2 = self.condition(sdd, lbl, false); + self.or(v1, v2) + } + + /// Compose `g` into `f` by substituting for `lbl` + fn compose(&'a self, _f: SddPtr<'a>, _lbl: VarLabel, _g: SddPtr<'a>) -> SddPtr<'a> { + panic!("not impl") + // TODO this can be optimized with a specialized implementation to make + // it a single traversal + // let var = self.var(lbl, true); + // let iff = self.iff(var, g); + // let a = self.and(iff, f); + // self.exists(a, lbl) + } +} + +pub struct SddManager<'a> { + vtree: VTreeManager, + stats: SddStats, + should_compress: bool, + // tables + bdd_tbl: RefCell>>, + sdd_tbl: RefCell>>, + // caches + ite_cache: RefCell>>, + app_cache: RefCell, SddPtr<'a>>>, +} + +impl<'a> SddBuilder<'a> for SddManager<'a> { + #[inline] + fn get_vtree_manager(&self) -> &VTreeManager { + &self.vtree } - fn print_sdd_internal(&'a self, ptr: SddPtr<'a>) -> String { - // self.canonicalizer.borrow().on_sdd_print_dump_state(ptr); - use pretty::*; - fn helper(ptr: SddPtr) -> Doc<'static, BoxDoc<'static>> { - match ptr { - SddPtr::PtrTrue => Doc::from("T"), - SddPtr::PtrFalse => Doc::from("F"), - SddPtr::Var(label, polarity) => Doc::from(format!( - "{}{}", - if polarity { "" } else { "!" }, - label.value() - )), - SddPtr::BDD(bdd) | SddPtr::ComplBDD(bdd) => { - let l = helper(bdd.low()); - let h = helper(bdd.high()); - let mut doc: Doc = Doc::from(""); - doc = doc.append(Doc::newline()).append( - (Doc::from(format!("ITE {:?} {}", ptr, bdd.label().value())) - .append(Doc::newline()) - .append(h.append(Doc::newline()).append(l))) - .nest(2), - ); - doc - } - SddPtr::Reg(or) | SddPtr::Compl(or) => { - let mut doc: Doc = Doc::from(""); - for a in or.nodes.iter() { - let sub = a.sub(); - let prime = a.prime(); - let s = if ptr.is_neg() { sub.neg() } else { sub }; - let new_s1 = helper(prime); - let new_s2 = helper(s); - doc = doc.append(Doc::newline()).append( - (Doc::from("/\\") - .append(Doc::newline()) - .append(new_s1.append(Doc::newline()).append(new_s2))) - .nest(2), - ); - } - let d = Doc::from(format!("\\/ {:?}", ptr)); - d.append(doc.nest(2)) - } - } - } - let d = helper(ptr); - let mut w = Vec::new(); - d.render(10, &mut w).unwrap(); - String::from_utf8(w).unwrap() + #[inline] + fn app_cache_get(&self, and: &SddAnd<'a>) -> Option> { + // TODO: check if this is right? + self.app_cache.borrow().get(and).cloned() } - pub fn print_sdd(&'a self, ptr: SddPtr<'a>) -> String { - self.print_sdd_internal(ptr) + #[inline] + fn app_cache_insert(&self, and: SddAnd<'a>, ptr: SddPtr<'a>) { + self.app_cache.borrow_mut().insert(and, ptr); } - pub fn sdd_eq(&'a self, a: SddPtr<'a>, b: SddPtr<'a>) -> bool { - a == b + #[inline] + fn ite_cache_hash(&self, ite: &Ite) -> u64 { + self.ite_cache.borrow().hash(ite) } - pub fn is_true(&'a self, a: SddPtr<'a>) -> bool { - self.sdd_eq(a, SddPtr::PtrTrue) + #[inline] + fn ite_cache_get(&self, ite: Ite>, hash: u64) -> Option { + self.ite_cache.borrow().get(ite, hash) } - pub fn is_false(&'a self, a: SddPtr<'a>) -> bool { - self.sdd_eq(a, SddPtr::PtrFalse) + #[inline] + fn ite_cache_insert(&self, ite: Ite>, res: SddPtr<'a>, hash: u64) { + self.ite_cache.borrow_mut().insert(ite, res, hash) } - /// compile an SDD from an input CNF - /// #[allow(clippy::wrong_self_convention)] // this is a naming thing; consider renaming in the future - pub fn from_cnf(&'a self, cnf: &Cnf) -> SddPtr<'a> { - let mut cvec: Vec = Vec::with_capacity(cnf.clauses().len()); - if cnf.clauses().is_empty() { - return SddPtr::true_ptr(); + #[inline] + fn get_or_insert_bdd(&'a self, bdd: BinarySDD<'a>) -> &BinarySDD<'a> { + unsafe { + let tbl = &mut *self.bdd_tbl.as_ptr(); + tbl.get_or_insert(bdd) } - // check if there is an empty clause -- if so, UNSAT - if cnf.clauses().iter().any(|x| x.is_empty()) { - return SddPtr::false_ptr(); + } + + #[inline] + fn get_or_insert_sdd(&'a self, or: SddOr<'a>) -> &SddOr<'a> { + unsafe { + let tbl = &mut *self.sdd_tbl.as_ptr(); + tbl.get_or_insert(or) } + } - // sort the clauses based on a best-effort bottom-up ordering of clauses - let mut cnf_sorted = cnf.clauses().to_vec(); - cnf_sorted.sort_by(|c1, c2| { - // order the clause with the first-most variable last - let fst1 = c1 - .iter() - .max_by(|l1, l2| { - if self.vtree.is_prime_var(l1.get_label(), l2.get_label()) { - Ordering::Less - } else { - Ordering::Equal - } - }) - .unwrap(); - let fst2 = c2 - .iter() - .max_by(|l1, l2| { - if self.vtree.is_prime_var(l1.get_label(), l2.get_label()) { - Ordering::Less - } else { - Ordering::Equal - } - }) - .unwrap(); - if self.vtree.is_prime_var(fst1.get_label(), fst2.get_label()) { - Ordering::Less - } else { - Ordering::Equal - } - }); + #[inline] + fn sdd_eq(&'a self, a: SddPtr<'a>, b: SddPtr<'a>) -> bool { + a == b + } - for lit_vec in cnf_sorted.iter() { - let (vlabel, val) = (lit_vec[0].get_label(), lit_vec[0].get_polarity()); - let mut bdd = SddPtr::Var(vlabel, val); - for lit in lit_vec { - let (vlabel, val) = (lit.get_label(), lit.get_polarity()); - let var = SddPtr::Var(vlabel, val); - bdd = self.or(bdd, var); - } - cvec.push(bdd); - } - // now cvec has a list of all the clauses; collapse it down - let r = self.from_cnf_helper(&cvec); - match r { - None => SddPtr::true_ptr(), - Some(x) => x, - } + #[inline] + fn set_compression(&mut self, b: bool) { + self.should_compress = b } - #[allow(clippy::wrong_self_convention)] // this is a naming thing; consider renaming in the future - fn from_cnf_helper(&'a self, vec: &[SddPtr<'a>]) -> Option> { - if vec.is_empty() { - None - } else if vec.len() == 1 { - Some(vec[0]) - } else { - let (l, r) = vec.split_at(vec.len() / 2); - let sub_l = self.from_cnf_helper(l); - let sub_r = self.from_cnf_helper(r); - match (sub_l, sub_r) { - (None, None) => None, - (Some(v), None) | (None, Some(v)) => Some(v), - (Some(l), Some(r)) => Some(self.and(l, r)), + /// Canonicalizes the list of (prime, sub) terms in-place + /// `node`: a list of (prime, sub) pairs + fn compress(&'a self, node: &mut Vec>) { + // self.stats.num_compr += 1; + for i in 0..node.len() { + // see if we can compress i + let mut j = i + 1; + while j < node.len() { + if self.sdd_eq(node[i].sub(), node[j].sub()) { + // self.stats.num_compr_and += 1; + // compress j into i and remove j from the node list + node[i] = SddAnd::new(self.or(node[i].prime(), node[j].prime()), node[i].sub()); + node.swap_remove(j); + } else { + j += 1; + } } } } - pub fn from_logical_expr(&mut self, _expr: &LogicalExpr) -> SddPtr { - panic!("not impl") - // match expr { - // &LogicalExpr::Literal(lbl, polarity) => self.var(VarLabel::new(lbl as u64), polarity), - // &LogicalExpr::Not(ref e) => { - // let e = self.from_logical_expr(e); - // e.neg() - // } - // &LogicalExpr::And(ref l, ref r) => { - // let r1 = self.from_logical_expr(l); - // let r2 = self.from_logical_expr(r); - // self.and(r1, r2) - // } - // &LogicalExpr::Or(ref l, ref r) => { - // let r1 = self.from_logical_expr(l); - // let r2 = self.from_logical_expr(r); - // self.or(r1, r2) - // } - // &LogicalExpr::Xor(ref l, ref r) => { - // let r1 = self.from_logical_expr(l); - // let r2 = self.from_logical_expr(r); - // self.xor(r1, r2) - // } - // &LogicalExpr::Iff(ref l, ref r) => { - // let r1 = self.from_logical_expr(l); - // let r2 = self.from_logical_expr(r); - // self.iff(r1, r2) - // } - // &LogicalExpr::Ite { - // ref guard, - // ref thn, - // ref els, - // } => { - // let g = self.from_logical_expr(guard); - // let thn = self.from_logical_expr(thn); - // let els = self.from_logical_expr(els); - // self.ite(g, thn, els) - // } - // } - } + /// Returns a canonicalized SDD pointer from a list of (prime, sub) pairs + fn canonicalize(&'a self, mut node: Vec>, table: VTreeIndex) -> SddPtr<'a> { + // check for base cases before compression + if let Some(sdd) = self.canonicalize_base_case(&node) { + return sdd; + } - pub fn stats(&self) -> &SddStats { - &self.stats + if self.should_compress { + self.compress(&mut node); + + // check for a base case after compression (compression can sometimes + // reduce node counts to a base case) + if let Some(sdd) = self.canonicalize_base_case(&node) { + return sdd; + } + } + + self.unique_or(node, table) } - pub fn node_iter(&self) -> Vec { + fn node_iter(&self) -> Vec { let binding = self.bdd_tbl.borrow_mut(); let bdds = binding.iter().map(SddPtr::BDD); let binding = self.sdd_tbl.borrow_mut(); @@ -850,9 +868,13 @@ impl<'a> SddManager<'a> { bdds.chain(sdds).collect() } + fn stats(&self) -> &SddStats { + &self.stats + } + /// computes the number of logically redundant nodes allocated by the /// manager (nodes that have the same semantic hash) - pub fn num_logically_redundant(&self) -> usize { + fn num_logically_redundant(&self) -> usize { let mut s: HashSet = HashSet::new(); let hasher = create_semantic_hash_map::<100000000063>(self.num_vars() + 1000); // TODO FIX THIS BADNESS let mut num_collisions = 0; @@ -867,6 +889,45 @@ impl<'a> SddManager<'a> { } } +impl<'a> SddManager<'a> { + pub fn new(vtree: VTree) -> SddManager<'a> { + let vtree_man = VTreeManager::new(vtree); + SddManager { + stats: SddStats::new(), + ite_cache: RefCell::new(AllTable::new()), + app_cache: RefCell::new(HashMap::new()), + bdd_tbl: RefCell::new(BackedRobinhoodTable::new()), + sdd_tbl: RefCell::new(BackedRobinhoodTable::new()), + vtree: vtree_man, + should_compress: true, + } + } + + #[inline] + fn canonicalize_base_case(&'a self, node: &Vec>) -> Option> { + if node.is_empty() { + return Some(SddPtr::true_ptr()); + } + if node.len() == 1 { + if self.is_true(node[0].prime()) { + return Some(node[0].sub()); + } + + if self.is_false(node[0].sub()) { + return Some(SddPtr::false_ptr()); + } + } + if node.len() == 2 { + if self.is_true(node[0].sub()) && self.is_false(node[1].sub()) { + return Some(node[0].prime()); + } else if self.is_false(node[0].sub()) && self.is_true(node[1].sub()) { + return Some(node[1].prime()); + } + } + None + } +} + // check that (a \/ b) /\ a === a #[test] fn simple_equality() { diff --git a/src/wasm/mod.rs b/src/wasm/mod.rs index 5060cc5d..cda787bc 100644 --- a/src/wasm/mod.rs +++ b/src/wasm/mod.rs @@ -1,6 +1,6 @@ use crate::builder::bdd_builder::{BddManager, BddPtr}; use crate::builder::cache::lru_app::BddApplyTable; -use crate::builder::sdd_builder::SddManager; +use crate::builder::sdd_builder::{SddBuilder, SddManager}; use crate::repr::dtree::DTree; use crate::repr::robdd::VarOrder; use crate::repr::{cnf::Cnf, var_label::VarLabel, vtree::VTree}; diff --git a/tests/test.rs b/tests/test.rs index 40d1bf1a..f7320c88 100644 --- a/tests/test.rs +++ b/tests/test.rs @@ -8,7 +8,7 @@ use crate::repr::cnf::Cnf; use crate::repr::var_label::VarLabel; use rsdd::builder::bdd_builder::BddManager; use rsdd::builder::cache::all_app::AllTable; -use rsdd::builder::sdd_builder::SddManager; +use rsdd::builder::sdd_builder::{SddBuilder, SddManager}; use rsdd::repr::robdd::BddPtr; use rsdd::repr::vtree::VTree; use rsdd::*; @@ -323,6 +323,7 @@ mod test_bdd_manager { use rand::Rng; use rsdd::builder::cache::all_app::AllTable; use rsdd::builder::cache::lru_app::BddApplyTable; + use rsdd::builder::sdd_builder::SddBuilder; use rsdd::repr::ddnnf::{create_semantic_hash_map, DDNNFPtr}; use rsdd::repr::dtree::DTree; use rsdd::repr::model::PartialModel; @@ -698,6 +699,7 @@ mod test_sdd_manager { use rand::seq::SliceRandom; use rand::SeedableRng; use rsdd::builder::cache::all_app::AllTable; + use rsdd::builder::sdd_builder::SddBuilder; use rsdd::repr::ddnnf::{create_semantic_hash_map, DDNNFPtr}; use rsdd::repr::dtree::DTree; use rsdd::repr::robdd::BddPtr;