cond

Author: SHoltzen

src/builder/bdd/robdd.rs

@@ -84,11 +84,11 @@ impl<'a, T: IteTable<'a, BddPtr<'a>> + Default> BddBuilder<'a> for RobddBuilder<
 
 
     fn cond_helper(&'a self, bdd: BddPtr<'a>, lbl: VarLabel, value: bool) -> BddPtr<'a> {
-        bdd.clear_scratch();
+        // bdd.clear_scratch();
         let r = self.cond_with_alloc(bdd, lbl, value, &mut HashMap::new());
         // outer call clears the scratch. very messy.
-        bdd.clear_scratch();
-        r.clear_scratch();
+        // bdd.clear_scratch();
+        // r.clear_scratch();
         r
     }
 }

src/repr/bdd.rs

@@ -403,7 +403,7 @@ impl<'a> BddPtr<'a> {
                     };
                     let l_s = print_bdd_helper(l_p);
                     let h_s = print_bdd_helper(h_p);
-                    format!("({}, scratch: {:?}, {}, {})", node.var.value(), node.data, h_s, l_s)
+                    format!("({}, {}, {})", node.var.value(),  h_s, l_s)
                 }
             }
         }

src/repr/cnf.rs

@@ -265,7 +265,6 @@ impl Cnf {
     pub fn new(clauses: &[Vec<Literal>]) -> Cnf {
         let clauses: Vec<Vec<Literal>> = clauses
             .iter()
-            .filter(|clause| !clause.is_empty())
             .map(|clause| {
                 let mut clause = clause.clone();
                 clause.sort_by_key(|a| a.label().value());
@@ -552,30 +551,24 @@ impl Cnf {
     }
 
     /// Updates the CNF to a new CNF that results from conditioning on the supplied literal
-    pub fn condition(&mut self, lit: Literal) -> Cnf {
-        let new_cnf: Vec<Vec<Literal>> = self
-            .clauses()
-            .iter()
-            .filter_map(|clause| {
-                // first, check if there is a true literal -- if there is, filter out this clause
-                if clause
-                    .iter()
-                    .any(|outer| outer.label() == lit.label() && outer.polarity() == lit.polarity())
-                {
-                    None
+    pub fn condition(&self, lit: Literal) -> Cnf {
+        let mut new_cnf  : Vec<Vec<Literal>> = Vec::new();
+        'cnf: for clause in self.clauses.iter() {
+            let mut new_clause = Vec::new();
+            'clause: for l in clause.iter() {
+                if l.label() == lit.label() && l.polarity() == lit.polarity() {
+                    // skip over this whole clause
+                    continue 'cnf
+                } else if l.label() == lit.label() && l.polarity() != lit.polarity() {
+                    // skip over this literal 
+                    continue 'clause
                 } else {
-                    // next, filter out clauses with false literals
-                    let filtered: Vec<Literal> = clause
-                        .iter()
-                        .filter(|outer| {
-                            !(lit.label() == outer.label() && lit.polarity() != outer.polarity())
-                        })
-                        .copied()
-                        .collect();
-                    Some(filtered)
+                    // push the literal
+                    new_clause.push(*l);
                 }
-            })
-            .collect();
+            }
+            new_cnf.push(new_clause);
+        }
         Cnf::new(&new_cnf)
     }
 
@@ -730,3 +723,12 @@ fn test_cnf_wmc() {
     ]);
     assert_eq!(cnf.wmc(&WmcParams::new(weights)), FiniteField::new(3));
 }
+
+#[test]
+fn test_cond() {
+    let v = vec![vec![
+        Literal::new(VarLabel::new(0), false),
+    ]];
+    let cnf = Cnf::new(&v);
+    println!("{:?}", cnf.condition(Literal::new(VarLabel::new(0), true)));
+}

tests/test.rs

@@ -283,6 +283,7 @@ mod test_bdd_builder {
     use rsdd::repr::BddPtr;
     use rsdd::repr::Cnf;
     use rsdd::repr::DTree;
+    use rsdd::repr::Literal;
     use rsdd::repr::PartialModel;
     use rsdd::repr::VTree;
     use rsdd::repr::VarLabel;
@@ -311,6 +312,21 @@ mod test_bdd_builder {
         }
     }
 
+    quickcheck! {
+        fn test_cond(c: Cnf, i : u64) -> bool {
+            let builder = super::RobddBuilder::<AllIteTable<BddPtr>>::new_with_linear_order(16);
+            let cnf = builder.compile_cnf(&c);
+            let cond_var = VarLabel::new(i % 4);
+            let cnf_cond = c.condition(Literal::new(cond_var, true));
+            let bdd1 = builder.condition(cnf, cond_var, true);
+            let bdd2 = builder.compile_cnf(&cnf_cond);
+            println!("cnf: {}\ncond var: {:?}\ncond cnf: {}\ncond cnf debug: {:?}\ncond bdd: {}\ncond cnf bdd: {}\neq? {}\n", 
+                c, cond_var, cnf_cond, cnf_cond, bdd1.to_string_debug(), bdd2.to_string_debug(), bdd1 == bdd2);
+            bdd1 == bdd2
+        }
+    }
+
+
     quickcheck! {
         /// check that every node in the BDD has a unique semantic hash
         fn qc_bdd_canonicity(c1: Cnf) -> TestResult {