Fix a minor bug with handling of constants in mk_cnf and mk_dnf.

sybila · Jan 23, 2024 · b06beed · b06beed
1 parent 0f7d561
commit b06beed
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 5 deletions.
diff --git a/src/_impl_bdd/_impl_cnf.rs b/src/_impl_bdd/_impl_cnf.rs
@@ -13,7 +13,7 @@ impl Bdd {
         // can be found there.
 
         if cnf.is_empty() {
-            Bdd::mk_true(num_vars);
+            return Bdd::mk_true(num_vars);
         }
 
         fn build_recursive(
@@ -79,9 +79,12 @@ impl Bdd {
         node_cache.insert(BddNode::mk_one(num_vars), BddPointer::one());
 
         let cnf = Vec::from_iter(cnf.iter());
-        build_recursive(num_vars, 0, &cnf, &mut result, &mut node_cache);
-
-        result
+        let result_pointer = build_recursive(num_vars, 0, &cnf, &mut result, &mut node_cache);
+        if result_pointer.is_zero() {
+            Bdd::mk_false(num_vars)
+        } else {
+            result
+        }
     }
 
     /// Construct a CNF representation of this BDD.

diff --git a/src/_impl_bdd/_impl_dnf.rs b/src/_impl_bdd/_impl_dnf.rs
@@ -10,7 +10,7 @@ impl Bdd {
     /// it definitely needs to be tested at some point.
     pub(crate) fn mk_dnf(num_vars: u16, dnf: &[BddPartialValuation]) -> Bdd {
         if dnf.is_empty() {
-            Bdd::mk_false(num_vars);
+            return Bdd::mk_false(num_vars);
         }
 
         // TODO:

diff --git a/src/_impl_bdd_variable_set.rs b/src/_impl_bdd_variable_set.rs
@@ -464,6 +464,35 @@ mod tests {
         assert_eq!(cnf_expected, universe.mk_cnf(formula));
         assert_eq!(dnf_expected, universe.mk_dnf(formula));
 
+        assert_eq!(universe.mk_false(), universe.mk_dnf(&[]));
+        assert_eq!(
+            universe.mk_true(),
+            universe.mk_dnf(&[BddPartialValuation::empty()])
+        );
+        assert_eq!(universe.mk_true(), universe.mk_cnf(&[]));
+        assert_eq!(
+            universe.mk_false(),
+            universe.mk_cnf(&[BddPartialValuation::empty()])
+        );
+
+        // x | !x = true
+        assert_eq!(
+            universe.mk_true(),
+            universe.mk_dnf(&[
+                BddPartialValuation::from_values(&[(variables[0], true)]),
+                BddPartialValuation::from_values(&[(variables[0], false)]),
+            ])
+        );
+
+        // x & !x = false
+        assert_eq!(
+            universe.mk_false(),
+            universe.mk_cnf(&[
+                BddPartialValuation::from_values(&[(variables[0], true)]),
+                BddPartialValuation::from_values(&[(variables[0], false)]),
+            ])
+        );
+
         // Test the backwards conversion by converting each formula to the inverse normal form.
         let cnf_as_dnf = universe.mk_cnf(formula).to_dnf();
         let dnf_as_cnf = universe.mk_dnf(formula).to_cnf();