From 61da9a8aeb35bde4c668b688182925a30225f38b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 8 Jan 2020 11:38:30 -0800
Subject: [PATCH] test the new order on pdd

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/dd/dd_pdd.h |  2 +-
 src/test/pdd.cpp     | 78 +++++++++++++++++++++++++++++++++++++-------
 2 files changed, 67 insertions(+), 13 deletions(-)

diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 1168952d4..1b168ba74 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -14,7 +14,7 @@ Abstract:
 
     Non-leaf nodes are of the form x*hi + lo
     where 
-    - maxdegree(x, lo) = 0, 
+    - maxdegree(x, lo) = 0, meaning x does not appear in lo
 
     Leaf nodes are of the form (0*idx + 0), where idx is an index into m_values.
 
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index 53abf991e..d9c9e4774 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -127,19 +127,72 @@ static void test5() {
 }
 
 
-    void test_iterator() {
-        std::cout << "test 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)*(c + 3*d) + 2;
-        std::cout << p << "\n";
-        for (auto const& m : p) {
-            std::cout << m << "\n";
-        }
+void test_iterator() {
+    std::cout << "test 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)*(c + 3*d) + 2;
+    std::cout << p << "\n";
+    for (auto const& m : p) {
+        std::cout << m << "\n";
     }
+}
+
+void order() {
+    std::cout << "order\n";
+    pdd_manager m(4);
+    unsigned va = 0;
+    unsigned vb = 1;
+    unsigned vc = 2;
+    unsigned vd = 3;
+    pdd a = m.mk_var(va);
+    pdd b = m.mk_var(vb);
+    pdd c = m.mk_var(vc);
+    pdd d = m.mk_var(vd);
+    pdd p = a + b;
+    std::cout << p << "\n";
+    unsigned i = 0;
+    for (auto const& m : p) {
+        std::cout << m << "\n";        
+        SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
+        SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
+        i++;
+        //        SASSERT(i != 1 || m == a);
+    }
+    pdd ccbbaa = c*c*b*b*a*a;
+    pdd ccbbba = c*c*b*b*b*a;
+    p = ccbbaa + ccbbba;
+
+    i = 0;
+    std::cout << "p = " <<  p << "\n";
+    for (auto const& m : p) {
+        std::cout << m << "\n";
+        SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
+        SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
+        i++;
+        //        SASSERT(i != 1 || m == a);
+    }
+    pdd dcbba = c*c*b*b*a*a;
+    pdd dd = d * d;
+    p = dcbba + ccbbba + d;
+    std::cout << "p = " <<  p << "\n";
+    std::cout << "more complex\n";
+    i = 0;
+    for (auto const& m : p) {
+        std::cout << m << "\n";
+        SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[0] == vc)); // the first one has to be ccbbba
+        SASSERT(i != 1 ||( m.vars.size() == 5 && m.vars[0] == vd)); // the second one has to be dcbba
+        SASSERT(i != 2 ||( m.vars.size() == 2 && m.vars[1] == vd)); // the second one has to be dd
+        
+        i++;
+        //        SASSERT(i != 1 || m == a);
+    }
+    
+    
+}
 
 }
 
@@ -150,4 +203,5 @@ void tst_pdd() {
     dd::test5();
     dd::test_reset();
     dd::test_iterator();
+    dd::order();
 }