From e96f69e76ce9728f8155569311b9360ddf667cd6 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 28 Sep 2023 11:42:08 +0200
Subject: [PATCH] Fix pdd_iterator for non-zero constant polynomials

---
 src/math/dd/dd_pdd.cpp |  3 +++
 src/math/dd/dd_pdd.h   |  2 +-
 src/test/pdd.cpp       | 48 +++++++++++++++++++++++++++++++++++++-----
 3 files changed, 47 insertions(+), 6 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 7a7f2521e..6f51e2f30 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1969,6 +1969,9 @@ namespace dd {
             n = m.hi(n);
         }
         m_mono.coeff = m.val(n);
+        // if m_pdd is constant and non-zero, the iterator should return a single monomial
+        if (m_nodes.empty() && !m_mono.coeff.is_zero())
+            m_nodes.push_back(std::make_pair(false, n));
     }
 
     pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 193fc3e3a..03a41e695 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -570,7 +570,7 @@ namespace dd {
         pdd_iterator& operator++() { next(); return *this; }
         pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; }
         bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; }
-        bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
+        bool operator!=(pdd_iterator const& other) const { return !operator==(other); }
     };
 
     class pdd_linear_iterator {
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index 0c9b0f85c..740ae4f2b 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -153,12 +153,49 @@ public:
         pdd b = m.mk_var(1);
         pdd c = m.mk_var(2);
         pdd d = m.mk_var(3);
-        pdd p = (a + b)*(c + 3*d) + 2;
-        std::cout << p << "\n";
-        for (auto const& m : p) {
-            std::cout << m << "\n";
-        }
+
+        auto const check = [](unsigned const expected_num_monomials, pdd const& p) {
+            unsigned count = 0;
+            std::cout << p << "\n";
+            for (auto const& m : p) {
+                std::cout << "  " << m << "\n";
+                ++count;
+            }
+            VERIFY_EQ(expected_num_monomials, count);
+        };
+
+        check(9, (a + b + 2)*(c + 3*d + 5) + 2);
+        check(5, (a + b)*(c + 3*d) + 2);
+        check(1, a);
+        check(2, a + 5);
+        check(1, m.mk_val(5));
+        check(0, m.mk_val(0));
     }
+
+    static void linear_iterator() {
+        std::cout << "test linear iterator\n";
+        pdd_manager m(4);
+        pdd a = m.mk_var(0);
+        pdd b = m.mk_var(1);
+        pdd c = m.mk_var(2);
+        pdd d = m.mk_var(3);
+        pdd p = (a + b + 2)*(c + 3*d + 5) + 2;
+        std::cout << p << "\n";
+        for (auto const& m : p.linear_monomials())
+            std::cout << "  " << m << "\n";
+        std::cout << a << "\n";
+        for (auto const& m : a.linear_monomials())
+            std::cout << "  " << m << "\n";
+        pdd one = m.mk_val(5);
+        std::cout << one << "\n";
+        for (auto const& m : one.linear_monomials())
+            std::cout << "  " << m << "\n";
+        pdd zero = m.mk_val(0);
+        std::cout << zero << "\n";
+        for (auto const& m : zero.linear_monomials())
+            std::cout << "  " << m << "\n";
+    }
+
     static void order() {
         std::cout << "order\n";
         pdd_manager m(4);
@@ -693,6 +730,7 @@ void tst_pdd() {
     dd::test::canonize();
     dd::test::reset();
     dd::test::iterator();
+    dd::test::linear_iterator();
     dd::test::order();
     dd::test::order_lm();
     dd::test::mod4_operations();