From b06beed6f7e4a8b973313025c85bd4ac373fae5b Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Tue, 23 Jan 2024 18:10:10 +0100
Subject: [PATCH] Fix a minor bug with handling of constants in `mk_cnf` and
 `mk_dnf`.

---
 src/_impl_bdd/_impl_cnf.rs    | 11 +++++++----
 src/_impl_bdd/_impl_dnf.rs    |  2 +-
 src/_impl_bdd_variable_set.rs | 29 +++++++++++++++++++++++++++++
 3 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/src/_impl_bdd/_impl_cnf.rs b/src/_impl_bdd/_impl_cnf.rs
index cb35ef0..1978bdc 100644
--- 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
index 4e627b7..69fc9e2 100644
--- 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
index ecd6628..7bae8c1 100644
--- 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();