From 5e19a52772b83cf335993d64137e858dad2dc143 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 25 Dec 2019 17:50:59 -0800
Subject: [PATCH] merge changes from Z3Prover

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/dd/dd_pdd.cpp           |  1 -
 src/math/dd/dd_pdd.h             |  2 ++
 src/math/grobner/pdd_grobner.cpp |  1 +
 src/math/grobner/pdd_solver.h    |  1 +
 src/math/lp/nla_core.cpp         |  1 +
 src/test/pdd.cpp                 | 41 ++++++++++++++++++++++++++++++--
 6 files changed, 44 insertions(+), 3 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 012791eb5..13451f270 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -723,7 +723,6 @@ namespace dd {
         bool do_gc = m_free_nodes.empty();
         if (do_gc && !m_disable_gc) {
             gc();
-            SASSERT(n.m_hi == 0 || (!m_free_nodes.contains(n.m_hi) && !m_free_nodes.contains(n.m_lo)));            
             e = m_node_table.insert_if_not_there2(n);
             e->get_data().m_refcount = 0;      
         }
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 1168952d4..6b09dfbf4 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -378,6 +378,8 @@ namespace dd {
     inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
     inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
     inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
+    inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
+    inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
 
     inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
     inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index c661ee4ef..992c7e784 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -698,6 +698,7 @@ namespace dd {
                 }
             }
             if (eq) {
+
                 pop_equation(eq);
                 m_watch[eq->poly().var()].erase(eq);
                 return eq;
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index 262e82329..3301aa246 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -130,6 +130,7 @@ public:
 private:
     bool step();
     equation* pick_next();
+    equation* pick_linear();
     bool canceled();
     bool done();
     void superpose(equation const& eq1, equation const& eq2);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 4b5ca5c06..fa257c704 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
 #include "math/lp/nex.h"
+#include "math/grobner/pdd_grobner.h"
 namespace nla {
 
 core::core(lp::lar_solver& s, reslimit & lim) :
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index 0efb4cae8..9cf0f5d46 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -82,7 +82,7 @@ static void test3() {
         e = e * e;
     }
     e = e * b;
-    std::cout << e << "\n";
+    //    std::cout << e << "\n";
 }
 
 static void test_reset() {
@@ -103,7 +103,44 @@ static void test_reset() {
         c = m.mk_var(2);
         d = m.mk_var(3);
         std::cout << (a + b)*(c + d) << "\n";
-    }
+}
+
+static void test5() {
+    std::cout << "\ntest5\n";
+    pdd_manager m(2);
+    pdd a = m.mk_var(0);
+    pdd b = m.mk_var(1);
+
+    pdd e = (a - b) * ( a + b);
+    pdd f = a * a  - b * b;
+    SASSERT(e == f);
+
+    e = (a - b)* (a - b);
+    f = a * a - 2 * a * b + b * b;
+    SASSERT(e == f);
+    e = a - 3;
+    e = e * e;
+    f = a * a - 6 * a + 9;
+    SASSERT(e == f);        
+    e = 2 * a - 3;
+    e = e * e;
+    f = 4 * a * a - 12 * a + 9;
+    SASSERT(e == f);        
+}
+
+static void test6() {
+    std::cout << "\ntest6\n";
+    pdd_manager m(5);
+    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 e = a * b * b * d + 2*a*b*c + (b*c*d) + (b*c) + (c*d) + 3;
+    pdd f = a * d * c + a + d;
+    pdd l = m.zero();
+    VERIFY(m.try_spoly(e, f, l));
+    std::cout << "superpose\n" << e << "\nand\n" << f << "\nresult\n" << l << "\n"; 
+}
 
     void test_iterator() {
         std::cout << "test iterator\n";