Refactors DecisionNNFBuilder into a TopDownBuilder trait and Standard impl

examples/bayesian_network_compiler.rs

@@ -6,7 +6,8 @@ use crate::rsdd::builder::BottomUpBuilder;
 use clap::Parser;
 use rsdd::builder::bdd::builder::BddBuilder;
 use rsdd::builder::cache::all_app::AllTable;
-use rsdd::builder::decision_nnf_builder::DecisionNNFBuilder;
+use rsdd::builder::decision_nnf::builder::DecisionNNFBuilder;
+use rsdd::builder::decision_nnf::standard::StandardDecisionNNFBuilder;
 use rsdd::builder::sdd::{builder::SddBuilder, compression::CompressionSddBuilder};
 use rsdd::repr::bdd::BddPtr;
 use rsdd::repr::ddnnf::DDNNFPtr;
@@ -303,7 +304,7 @@ fn compile_topdown(network: BayesianNetwork) {
     println!("############################\n\tCompiling topdown\n############################");
     let bn = BayesianNetworkCNF::new(&network);
     let order = VarOrder::linear_order(bn.cnf.num_vars());
-    let compiler = DecisionNNFBuilder::new(order);
+    let compiler = StandardDecisionNNFBuilder::new(order);
 
     println!("Compiling");
     let start = Instant::now();

examples/one_shot_benchmark.rs

@@ -3,6 +3,8 @@ extern crate rsdd;
 use clap::Parser;
 use rsdd::builder::bdd::builder::BddBuilder;
 use rsdd::builder::cache::lru_app::BddApplyTable;
+use rsdd::builder::decision_nnf::builder::DecisionNNFBuilder;
+use rsdd::builder::decision_nnf::standard::StandardDecisionNNFBuilder;
 use rsdd::plan::bdd_plan::BddPlan;
 use rsdd::repr::cnf::Cnf;
 use rsdd::repr::ddnnf::DDNNFPtr;
@@ -78,7 +80,7 @@ struct BenchResult {
 fn compile_topdown_nnf(str: String, _args: &Args) -> BenchResult {
     let cnf = Cnf::from_file(str);
     let order = VarOrder::linear_order(cnf.num_vars());
-    let builder = rsdd::builder::decision_nnf_builder::DecisionNNFBuilder::new(order);
+    let builder = StandardDecisionNNFBuilder::new(order);
     // let order = cnf.force_order();
     let ddnnf = builder.compile_cnf_topdown(&cnf);
     println!("num redundant: {}", builder.num_logically_redundant());

src/builder/decision_nnf_builder.rs → src/builder/decision_nnf/builder.rs

@@ -1,65 +1,27 @@
-//! Top-down decision DNNF compiler and manipulator
-
-use std::{cell::RefCell, collections::HashSet};
-
-use crate::{
-    backing_store::*,
-    repr::{
-        bdd::create_semantic_hash_map,
-        ddnnf::DDNNFPtr,
-        unit_prop::{DecisionResult, SATSolver},
-    },
-};
 use rustc_hash::FxHashMap;
 
 use crate::{
-    backing_store::bump_table::BackedRobinhoodTable,
+    builder::{
+        bdd::robdd::{BddPtr, DDNNFPtr},
+        TopDownBuilder,
+    },
     repr::{
-        bdd::{BddNode, BddPtr},
-        cnf::*,
-        var_label::{Literal, VarLabel},
-        var_order::VarOrder,
+        bdd::{BddNode, Literal, VarOrder},
+        cnf::Cnf,
+        unit_prop::{DecisionResult, SATSolver},
     },
 };
 
-pub struct DecisionNNFBuilder<'a> {
-    compute_table: RefCell<BackedRobinhoodTable<'a, BddNode<'a>>>,
-    order: VarOrder,
-}
+use crate::repr::var_label::VarLabel;
 
-impl<'a> DecisionNNFBuilder<'a> {
-    pub fn new(order: VarOrder) -> DecisionNNFBuilder<'a> {
-        DecisionNNFBuilder {
-            order,
-            compute_table: RefCell::new(BackedRobinhoodTable::new()),
-        }
-    }
+pub trait DecisionNNFBuilder<'a>: TopDownBuilder<'a, BddPtr<'a>> {
+    fn order(&'a self) -> &'a VarOrder;
 
     /// Normalizes and fetches a node from the store
-    fn get_or_insert(&'a self, bdd: BddNode<'a>) -> BddPtr<'a> {
-        // TODO make this safe
-        unsafe {
-            let tbl = &mut *self.compute_table.as_ptr();
-            if bdd.high.is_neg() {
-                let bdd = BddNode::new(bdd.var, bdd.low.neg(), bdd.high.neg());
-                BddPtr::new_compl(tbl.get_or_insert(bdd))
-            } else {
-                let bdd = BddNode::new(bdd.var, bdd.low, bdd.high);
-                BddPtr::new_reg(tbl.get_or_insert(bdd))
-            }
-        }
-    }
+    fn get_or_insert(&'a self, bdd: BddNode<'a>) -> BddPtr<'a>;
 
-    /// Get a pointer to the variable with label `lbl` and polarity `polarity`
-    pub fn var(&'a self, lbl: VarLabel, polarity: bool) -> BddPtr<'a> {
-        let bdd = BddNode::new(lbl, BddPtr::false_ptr(), BddPtr::true_ptr());
-        let r = self.get_or_insert(bdd);
-        if polarity {
-            r
-        } else {
-            r.neg()
-        }
-    }
+    /// counts number of redundant nodes allocated in internal table
+    fn num_logically_redundant(&self) -> usize;
 
     fn conjoin_implied(
         &'a self,
@@ -96,7 +58,7 @@ impl<'a> DecisionNNFBuilder<'a> {
         if level >= cnf.num_vars() || sat.is_sat() {
             return BddPtr::true_ptr();
         }
-        let cur_v = self.order.var_at_level(level);
+        let cur_v = self.order().var_at_level(level);
 
         // check if this literal is currently set in unit propagation; if
         // it is, skip it
@@ -158,7 +120,7 @@ impl<'a> DecisionNNFBuilder<'a> {
     }
 
     /// compile a decision DNNF top-down from a CNF
-    pub fn compile_cnf_topdown(&'a self, cnf: &Cnf) -> BddPtr<'a> {
+    fn compile_cnf_topdown(&'a self, cnf: &Cnf) -> BddPtr<'a> {
         let mut sat = match SATSolver::new(cnf.clone()) {
             Some(v) => v,
             None => return BddPtr::false_ptr(),
@@ -178,13 +140,6 @@ impl<'a> DecisionNNFBuilder<'a> {
         r
     }
 
-    /// Compute the Boolean function `f | var = value`
-    pub 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
-    }
-
     fn cond_helper(&'a self, bdd: BddPtr<'a>, lbl: VarLabel, value: bool) -> BddPtr<'a> {
         match bdd {
             BddPtr::PtrTrue | BddPtr::PtrFalse => bdd,
@@ -230,38 +185,27 @@ impl<'a> DecisionNNFBuilder<'a> {
             }
         }
     }
+}
 
-    pub fn num_logically_redundant(&self) -> usize {
-        let mut num_collisions = 0;
-        let mut seen_hashes = HashSet::new();
-        let map = create_semantic_hash_map::<10000000049>(self.order.num_vars());
-        for bdd in self.compute_table.borrow().iter() {
-            let h = BddPtr::new_reg(bdd).semantic_hash(&self.order, &map);
-            if seen_hashes.contains(&(h.value())) {
-                num_collisions += 1;
-            } else {
-                seen_hashes.insert(h.value());
-            }
+impl<'a, T> TopDownBuilder<'a, BddPtr<'a>> for T
+where
+    T: DecisionNNFBuilder<'a>,
+{
+    /// Get a pointer to the variable with label `lbl` and polarity `polarity`
+    fn var(&'a self, lbl: VarLabel, polarity: bool) -> BddPtr<'a> {
+        let bdd = BddNode::new(lbl, BddPtr::false_ptr(), BddPtr::true_ptr());
+        let r = self.get_or_insert(bdd);
+        if polarity {
+            r
+        } else {
+            r.neg()
         }
-        num_collisions
     }
-}
 
-// #[test]
-// fn test_dnnf() {
-//     let clauses = vec![
-//         vec![
-//             Literal::new(VarLabel::new(0), true),
-//             Literal::new(VarLabel::new(1), false),
-//         ],
-//         // vec![
-//         // Literal::new(VarLabel::new(0), false),
-//         // Literal::new(VarLabel::new(1), true)
-//         // ]
-//     ];
-//     let cnf = Cnf::new(clauses);
-//     let mut builder = DecisionNNFBuilder::new();
-//     let c2 = builder.from_cnf_topdown(&VarOrder::linear_order(cnf.num_vars()), &cnf);
-//     println!("c2: {}", c2.to_string_debug());
-//     assert!(false)
-// }
+    /// Compute the Boolean function `f | var = value`
+    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
+    }
+}

src/builder/decision_nnf/mod.rs

@@ -0,0 +1,2 @@
+pub mod builder;
+pub mod standard;

src/builder/decision_nnf/standard.rs

@@ -0,0 +1,61 @@
+use std::{cell::RefCell, collections::HashSet};
+
+use crate::{
+    backing_store::bump_table::BackedRobinhoodTable,
+    builder::{
+        bdd::robdd::{BddPtr, DDNNFPtr},
+        decision_nnf::builder::DecisionNNFBuilder,
+    },
+    repr::bdd::{create_semantic_hash_map, BddNode, VarOrder},
+};
+
+use crate::backing_store::UniqueTable;
+
+pub struct StandardDecisionNNFBuilder<'a> {
+    compute_table: RefCell<BackedRobinhoodTable<'a, BddNode<'a>>>,
+    order: VarOrder,
+}
+
+impl<'a> DecisionNNFBuilder<'a> for StandardDecisionNNFBuilder<'a> {
+    fn order(&'a self) -> &'a VarOrder {
+        &self.order
+    }
+
+    fn get_or_insert(&'a self, bdd: BddNode<'a>) -> BddPtr<'a> {
+        // TODO make this safe
+        unsafe {
+            let tbl = &mut *self.compute_table.as_ptr();
+            if bdd.high.is_neg() {
+                let bdd = BddNode::new(bdd.var, bdd.low.neg(), bdd.high.neg());
+                BddPtr::new_compl(tbl.get_or_insert(bdd))
+            } else {
+                let bdd = BddNode::new(bdd.var, bdd.low, bdd.high);
+                BddPtr::new_reg(tbl.get_or_insert(bdd))
+            }
+        }
+    }
+
+    fn num_logically_redundant(&self) -> usize {
+        let mut num_collisions = 0;
+        let mut seen_hashes = HashSet::new();
+        let map = create_semantic_hash_map::<10000000049>(self.order.num_vars());
+        for bdd in self.compute_table.borrow().iter() {
+            let h = BddPtr::new_reg(bdd).semantic_hash(&self.order, &map);
+            if seen_hashes.contains(&(h.value())) {
+                num_collisions += 1;
+            } else {
+                seen_hashes.insert(h.value());
+            }
+        }
+        num_collisions
+    }
+}
+
+impl<'a> StandardDecisionNNFBuilder<'a> {
+    pub fn new(order: VarOrder) -> StandardDecisionNNFBuilder<'a> {
+        StandardDecisionNNFBuilder {
+            order,
+            compute_table: RefCell::new(BackedRobinhoodTable::new()),
+        }
+    }
+}

src/builder/mod.rs

@@ -4,7 +4,7 @@
 pub mod cache;
 
 pub mod bdd;
-pub mod decision_nnf_builder;
+pub mod decision_nnf;
 pub mod sdd;
 
 use crate::repr::var_label::VarLabel;
@@ -49,3 +49,10 @@ pub trait BottomUpBuilder<'a, Ptr> {
     /// I.e., computes the logical function (exists v. (g <=> v) /\ f).
     fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr;
 }
+
+pub trait TopDownBuilder<'a, Ptr> {
+    fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr;
+
+    /// conditions f | v = value
+    fn condition(&'a self, a: Ptr, v: VarLabel, value: bool) -> Ptr;
+}

tests/test.rs

@@ -316,7 +316,6 @@ fn test_sdd_is_canonical() {
 
 #[cfg(test)]
 mod test_bdd_builder {
-    use crate::builder::decision_nnf_builder::DecisionNNFBuilder;
     use crate::repr::cnf::Cnf;
     use crate::repr::var_label::VarLabel;
     use crate::rsdd::builder::bdd::builder::BddBuilder;
@@ -325,6 +324,8 @@ mod test_bdd_builder {
     use rand::Rng;
     use rsdd::builder::cache::all_app::AllTable;
     use rsdd::builder::cache::lru_app::BddApplyTable;
+    use rsdd::builder::decision_nnf::builder::DecisionNNFBuilder;
+    use rsdd::builder::decision_nnf::standard::StandardDecisionNNFBuilder;
     use rsdd::builder::sdd::builder::SddBuilder;
     use rsdd::repr::bdd::BddPtr;
     use rsdd::repr::ddnnf::{create_semantic_hash_map, DDNNFPtr};
@@ -461,7 +462,7 @@ mod test_bdd_builder {
             let order = VarOrder::linear_order(c1.num_vars());
             let cnf1 = builder.compile_cnf(&c1);
 
-            let builder2 = DecisionNNFBuilder::new(order);
+            let builder2 = StandardDecisionNNFBuilder::new(order);
             let dnnf = builder2.compile_cnf_topdown(&c1);
 
             let bddwmc = super::repr::wmc::WmcParams::new_with_default(RealSemiring::zero(), RealSemiring::one(), weight_map);