From f1d46b58a41b6d742ef72b7afb142c34e794ceed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 11 Dec 2021 17:38:09 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_pdd.cpp       | 46 ++++++++++++++++++++++--------------
 src/math/dd/dd_pdd.h         |  2 ++
 src/math/polysat/explain.cpp | 14 +++++------
 src/math/polysat/solver.cpp  |  2 +-
 src/test/polysat.cpp         |  2 +-
 5 files changed, 39 insertions(+), 27 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 0fb848953..cb438b815 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -946,40 +946,50 @@ namespace dd {
     * result := reduce(v, q*b2*v^{l-m}, b) + reduce(v, a2, b)
     */
     pdd pdd_manager::reduce(unsigned v, pdd const& a, pdd const& b) {
-        unsigned const l = a.degree(v);
         unsigned const m = b.degree(v);
         // no reduction
-        if (l < m || m == 0)
+        if (m == 0)
             return a;
                     
-        pdd a1 = zero();
-        pdd a2 = zero();
         pdd b1 = zero();
         pdd b2 = zero();
+        b.factor(v, m, b1, b2);
+
+        // TODO - generalize this case to when leading coefficient is not a value
+        if (m_semantics == mod2N_e && b1.is_val() && b1.val().is_odd() && !b1.is_one()) {
+            rational b_inv;
+            VERIFY(b1.val().mult_inverse(m_power_of_2, b_inv));
+            b1 = 1;
+            b2 *= b_inv;
+        }
+
+        return reduce(v, a, m, b1, b2);
+    }
+
+    pdd pdd_manager::reduce(unsigned v, pdd const& a, unsigned m, pdd const& b1, pdd const& b2) {
+        SASSERT(m > 0);
+        unsigned const l = a.degree(v);
+        if (l < m)
+            return a;
+
+        pdd a1 = zero();
+        pdd a2 = zero();
         pdd q = zero();
         pdd r = zero();
         a.factor(v, l, a1, a2);
-        b.factor(v, m, b1, b2);
-        std::cout << "factor v*" << a1 << " ++ " << a2 << "\n";
-        std::cout << "factor v*" << b1 << " ++ " << b2 << "\n";
 
         quot_rem(a1, b1, q, r);
-        std::cout << "quot " << q << " rem " << r << "\n";
         if (r.is_zero()) {
             SASSERT(q * b1 == a1);
-            a1 = -q * pow(mk_var(v), l - m) * b2;
+            a1 = -q * b2;
             if (l > m)
-                a1 = reduce(v, a1, b);
+                a1 = reduce(v, a1 * pow(mk_var(v), l - m), m, b1, b2);
         }
-        else if (m_semantics == mod2N_e && r.is_val() && r.val().is_odd() && q.is_zero()) {
-            
-        }
-        else 
-            a1 = a1 * pow(mk_var(v), l);        
-        a2 = a2.reduce(v, b);
+        else
+            a1 = a1 * pow(mk_var(v), l);
+        a2 = reduce(v, a2, m, b1, b2);
 
-        pdd result = a1 + a2;
-        return result;
+        return a1 + a2;
     }
 
     /**
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 1c8f31ce7..ca8b73fd3 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -280,6 +280,8 @@ namespace dd {
         void factor(pdd const& p, unsigned v, unsigned degree, pdd& lc, pdd& rest);
         bool factor(pdd const& p, unsigned v, unsigned degree, pdd& lc);
 
+        pdd reduce(unsigned v, pdd const& a, unsigned m, pdd const& b1, pdd const& b2);
+
         bool var_is_leaf(PDD p, unsigned v);
 
         bool is_reachable(PDD p);
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index a792a74ee..65ae48a3f 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -147,10 +147,6 @@ namespace polysat {
             if (c.is_eq())
                 continue;
             LOG("try-reduce: " << c << " " << c.is_currently_false(s));
-#if 0
-            if (!c.is_currently_false(s))
-                continue;
-#endif
             if (!c->is_ule())
                 continue;
             auto lhs = c->to_ule().lhs();
@@ -166,9 +162,13 @@ namespace polysat {
             LOG("try-reduce is false " << c2.is_currently_false(s));
             if (!c2.is_currently_false(s))
                 continue;
-            SASSERT(c2.is_currently_false(s));
-            if (!c2->has_bvar() || l_undef == c2.bvalue(s))
-                core.keep(c2);  // adds propagation of c to the search stack
+            if (!c2->has_bvar() || l_undef == c2.bvalue(s)) {
+                vector<signed_constraint> premises;
+                premises.push_back(c);
+                premises.push_back(eq);
+                core.insert(c2, premises);
+            }
+            //    core.keep(c2);  // adds propagation of c to the search stack
             core.reset();
             LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
             if (c2.bvalue(s) == l_false) {
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 330f989eb..8a87e654c 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -782,7 +782,7 @@ namespace polysat {
         LOG("Lemma: " << lemma);
         for (sat::literal lit : lemma) {
             LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
-            SASSERT(m_bvars.value(lit) != l_true);
+            // SASSERT(m_bvars.value(lit) != l_true);
         }
         SASSERT(!lemma.empty());
         m_constraints.store(&lemma, *this);
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 42f7e2c96..ed4feb4a9 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -946,7 +946,7 @@ namespace polysat {
 
     static void test_quot_rem(unsigned bw = 32) {
         scoped_solver s(__func__);
-        s.set_max_conflicts(2);
+        s.set_max_conflicts(5);
         auto a = s.var(s.add_var(bw));
         auto quot = s.var(s.add_var(bw));
         auto rem = s.var(s.add_var(bw));