Fix a bug in mk_dnf/mk_cnf that manifests if the input contains dupli…

…cate clauses.
sybila · Sep 18, 2024 · c24deec · c24deec
1 parent 25ab8d3
commit c24deec
Show file tree

Hide file tree

Showing 2 changed files with 62 additions and 4 deletions.
diff --git a/src/_impl_bdd/_impl_cnf.rs b/src/_impl_bdd/_impl_cnf.rs
@@ -12,8 +12,13 @@ impl Bdd {
                 if cnf.is_empty() {
                     return ctx.mk_true();
                 }
-                if cnf.len() == 1 {
-                    return ctx.mk_disjunctive_clause(cnf[0]);
+                if var == ctx.num_vars() || cnf.len() == 1 {
+                    let c = cnf[0];
+                    // At this point, all remaining clauses should just be duplicates.
+                    for cx in &cnf[1..] {
+                        assert_eq!(*cx, c);
+                    }
+                    return ctx.mk_disjunctive_clause(c);
                 }
 
                 // If we ever get to this point, the dnf should be always either empty,
@@ -181,3 +186,37 @@ impl Bdd {
         result
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use crate::{BddPartialValuation, BddVariable, BddVariableSet};
+
+    #[test]
+    pub fn bad_mk_cnf() {
+        let ctx = BddVariableSet::new_anonymous(60);
+        let variables = ctx.variables();
+        let mut clauses = Vec::new();
+        for i in 0..30 {
+            let mut c = BddPartialValuation::empty();
+            c[variables[2 * i]] = Some(true);
+            c[variables[2 * i + 1]] = Some(true);
+            clauses.push(c);
+        }
+
+        assert_eq!(ctx.mk_cnf(&clauses).size(), 62);
+    }
+
+    #[test]
+    pub fn bad_mk_cnf_2() {
+        // Extracted from AEON.py test.
+        let ctx = BddVariableSet::new_anonymous(3);
+        let a_true = (BddVariable::from_index(0), true);
+        let b_false = (BddVariable::from_index(1), false);
+        let clauses = vec![
+            BddPartialValuation::from_values(&[a_true, b_false]),
+            BddPartialValuation::from_values(&[a_true, b_false]),
+        ];
+
+        assert_eq!(ctx.mk_cnf(&clauses).size(), 4);
+    }
+}
diff --git a/src/_impl_bdd/_impl_dnf.rs b/src/_impl_bdd/_impl_dnf.rs
@@ -13,8 +13,13 @@ impl Bdd {
                 if dnf.is_empty() {
                     return Bdd::mk_false(num_vars);
                 }
-                if dnf.len() == 1 {
-                    return Bdd::mk_partial_valuation(num_vars, dnf[0]);
+                if var == num_vars || dnf.len() == 1 {
+                    let c = dnf[0];
+                    // At this point, all remaining clauses should just be duplicates.
+                    for cx in &dnf[1..] {
+                        assert_eq!(*cx, c);
+                    }
+                    return Bdd::mk_partial_valuation(num_vars, c);
                 }
 
                 // If we ever get to this point, the dnf should be always either empty,
@@ -451,4 +456,18 @@ mod tests {
 
         assert_eq!(ctx.mk_dnf(&clauses).size(), 62);
     }
+
+    #[test]
+    pub fn bad_mk_dnf_2() {
+        // Extracted from AEON.py test.
+        let ctx = BddVariableSet::new_anonymous(3);
+        let a_true = (BddVariable::from_index(0), true);
+        let b_false = (BddVariable::from_index(1), false);
+        let clauses = vec![
+            BddPartialValuation::from_values(&[a_true, b_false]),
+            BddPartialValuation::from_values(&[a_true, b_false]),
+        ];
+
+        assert_eq!(ctx.mk_dnf(&clauses).size(), 4);
+    }
 }