From c2b353ba7225b92a9165e77103f997d74a41ec52 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 26 Mar 2021 12:20:51 -0700
Subject: [PATCH] adding factorization

---
 src/math/dd/dd_pdd.cpp | 82 +++++++++++++++++++++++++++++++++++++++++-
 src/math/dd/dd_pdd.h   |  5 +++
 2 files changed, 86 insertions(+), 1 deletion(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 7fe80b214..2422f3fd1 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -30,6 +30,8 @@ namespace dd {
         m_dmark_level = 0;
         m_disable_gc = false;
         m_is_new_node = false;
+        if (s == mod2N_e && power_of_2 == 1)
+            s = mod2_e;
         m_semantics = s;
         m_mod2N = rational::power_of_two(power_of_2);
         m_power_of_2 = power_of_2;
@@ -685,12 +687,61 @@ namespace dd {
         return p;
     }
 
+    /**
+     * factor p into lc*v^degree + rest
+     * such that degree(rest, v) < degree
+     * Initial implementation is very naive
+     * - memoize intermediary results
+     */
+    void pdd_manager::factor(pdd const& p, unsigned v, unsigned degree, pdd& lc, pdd& rest) {
+        unsigned level_v = m_var2level[v];
+        if (degree == 0) {
+            lc = p;
+            rest = zero();
+        }
+        else if (level(p.root) < level_v) {
+            lc = zero();
+            rest = p;
+        }
+        else if (level(p.root) > level_v) {
+            pdd lc1 = zero(), rest1 = zero();
+            pdd vv = mk_var(p.var());
+            factor(p.hi(), v, degree, lc,  rest);
+            factor(p.lo(), v, degree, lc1, rest1);
+            lc   += lc1;
+            rest += rest1;
+            lc   *= vv;
+            rest *= vv;
+        }
+        else {
+            unsigned d = 0;
+            pdd r = p;
+            while (d < degree && !r.is_val() && level(r.root) == level_v) {
+                d++;
+                r = r.hi();
+            }
+            if (d == degree) {
+                lc = r;
+                r = p;
+                rest = zero();
+                pdd pow = one();
+                for (unsigned i = 0; i < degree; r = r.hi(), pow *= mk_var(v), ++i) 
+                    rest += pow * r.lo();
+            }
+            else {
+                lc = zero();
+                rest = p;
+            }
+        }
+    }
+
+
     bool pdd_manager::is_linear(pdd const& p) { 
         return is_linear(p.root); 
     }
 
     /*
-      Determine whether p is a binary polynomials 
+      Determine whether p is a binary polynomial 
       of the form v1, x*v1 + v2, or x*v1 + y*v2 + v3
       where v1, v2 are values.      
      */
@@ -952,6 +1003,35 @@ namespace dd {
         return m_degree[p];
     }
 
+    unsigned pdd_manager::degree(PDD p, unsigned v) {
+        init_mark();
+        unsigned level_v = level(v);
+        unsigned max_d = 0, d = 0;
+        m_todo.push_back(p);
+        while (!m_todo.empty()) {
+            PDD r = m_todo.back();
+            if (is_marked(r)) 
+                m_todo.pop_back();
+            else if (is_val(r))
+                m_todo.pop_back();
+            else if (level(r) < level_v)
+                m_todo.pop_back();
+            else if (level(r) == level_v) {
+                d = 1;
+                while (!is_val(hi(r)) && level(hi(r)) == level_v) {
+                    ++d;
+                    r = hi(r);
+                }
+                max_d = std::max(d, max_d);
+                m_todo.pop_back();
+            }
+            else 
+                m_todo.push_back(lo(r)).push_back(hi(r));                
+        }
+        return max_d;
+    }
+
+
 
     double pdd_manager::tree_size(pdd const& p) {
         init_mark();
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index a8e65c0bf..28d273966 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -225,6 +225,9 @@ namespace dd {
         bool is_dmarked(unsigned i) const { return m_dmark[i] == m_dmark_level; }
         unsigned degree(pdd const& p) const;
         unsigned degree(PDD p) const;
+        unsigned degree(PDD p, unsigned v);
+
+        void factor(pdd const& p, unsigned v, unsigned degree, pdd& lc, pdd& rest);
 
         bool var_is_leaf(PDD p, unsigned v);
 
@@ -358,6 +361,7 @@ namespace dd {
         pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); }
         pdd reduce(pdd const& other) const { return m.reduce(*this, other); }
         bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }
+        void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) { m.factor(*this, v, degree, lc, rest); }
 
         pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
@@ -371,6 +375,7 @@ namespace dd {
         unsigned dag_size() const { return m.dag_size(*this); }
         double tree_size() const { return m.tree_size(*this); }
         unsigned degree() const { return m.degree(*this); }
+        unsigned degree(unsigned v) const { return m.degree(root, v); }
         unsigned_vector const& free_vars() const { return m.free_vars(*this); }