fix pdd_stack for gc on reduce, add unit test for linear_simplify

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/grobner/pdd_grobner.cpp

@@ -143,7 +143,10 @@ namespace dd {
     }
 
     bool grobner::basic_step() {
-        equation* e = pick_next();
+        return basic_step(pick_next());
+    }
+
+    bool grobner::basic_step(equation* e) {
         if (!e) return false;
         scoped_detach sd(*this, e);
         equation& eq = *e;
@@ -164,13 +167,89 @@ namespace dd {
                 eq = curr;
             }
         }
-        if (eq) pop_equation(eq->idx(), m_to_simplify);
+        if (eq) pop_equation(eq, m_to_simplify);
         return eq;
     }
 
+    grobner::equation* grobner::pick_linear() {
+        equation* eq = nullptr;
+        for (auto* curr : m_to_simplify) {
+            if (!eq || curr->poly().is_linear() && is_simpler(*curr, *eq)) {
+                eq = curr;
+            }
+        }
+        if (eq) pop_equation(eq, m_to_simplify);
+        return eq;
+    }
+
+    void grobner::simplify_linear() {
+        try {
+            while (simplify_linear_step()) {
+                DEBUG_CODE(invariant(););
+            }
+        }
+        catch (pdd_manager::mem_out) {
+            // done reduce
+        }
+    }
+
+    struct grobner::compare_top_var {
+        bool operator()(equation* a, equation* b) const {
+            return a->poly().var() < b->poly().var();
+        }
+    };
+
+    bool grobner::simplify_linear_step() {
+        equation_vector linear;
+        for (equation* e : m_to_simplify) {
+            if (e->poly().is_linear()) {
+                linear.push_back(e);
+            }
+        }
+        if (linear.empty()) return false;
+        std::cout << "linear eqs: " << linear.size() << "\n";
+        vector<equation_vector> use_list;
+        for (equation * e : m_to_simplify) {
+            add_to_use(e, use_list);
+        }
+        for (equation * e : m_processed) {
+            add_to_use(e, use_list);
+        }
+        compare_top_var ctv;
+        std::stable_sort(linear.begin(), linear.end(), ctv);
+        for (equation* src : linear) {
+            equation_vector const& uses = use_list[src->poly().var()];
+            bool changed_leading_term;
+            for (equation* dst : uses) {
+                if (src == dst || !simplify_source_target(*src, *dst, changed_leading_term)) {
+                    continue;                    
+                }
+                if (dst->is_processed() && changed_leading_term) {
+                    dst->set_processed(false);
+                    pop_equation(dst, m_processed);
+                    push_equation(src, m_to_simplify);
+                }
+            }            
+        } 
+        for (equation* src : linear) {
+            pop_equation(src, m_to_simplify);
+            push_equation(src, m_processed);
+            src->set_processed(true);
+        }
+        return true;
+    }
+
+    void grobner::add_to_use(equation* e, vector<equation_vector>& use_list) {
+        unsigned_vector const& fv = m.free_vars(e->poly());
+        for (unsigned v : fv) {
+            use_list.reserve(v + 1);
+            use_list[v].push_back(e);
+        }
+    }
+
     void grobner::superpose(equation const & eq) {
         for (equation* target : m_processed) {
-            retire(target);             
+            superpose(eq, *target);
         }
     }
 
@@ -343,7 +422,7 @@ namespace dd {
                 }
             }
             if (eq) {
-                pop_equation(eq->idx(), m_to_simplify);
+                pop_equation(eq, m_to_simplify);
                 m_watch[eq->poly().var()].erase(eq);
                 return eq;
             }
@@ -390,11 +469,12 @@ namespace dd {
     }
 
     void grobner::del_equation(equation& eq) {
-        pop_equation(eq.idx(), eq.is_processed() ? m_processed : m_to_simplify);
+        pop_equation(eq, eq.is_processed() ? m_processed : m_to_simplify);
         retire(&eq);
     }
 
-    void grobner::pop_equation(unsigned idx, equation_vector& v) {
+    void grobner::pop_equation(equation& eq, equation_vector& v) {
+        unsigned idx = eq.idx();
         if (idx != v.size() - 1) {
             equation* eq2 = v.back();
             eq2->set_index(idx);

src/math/grobner/pdd_grobner.h

@@ -99,6 +99,7 @@ public:
     void add(pdd const& p) { add(p, nullptr); }
     void add(pdd const& p, u_dependency * dep);
 
+    void simplify_linear();
     void saturate();
 
     equation_vector const& equations();
@@ -111,7 +112,9 @@ public:
 private:
     bool step();
     bool basic_step();
+    bool basic_step(equation* e);
     equation* pick_next();
+    equation* pick_linear();
     bool canceled();
     bool done();
     void superpose(equation const& eq1, equation const& eq2);
@@ -128,7 +131,6 @@ private:
     bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
     bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit;  }
 
-
     // tuned implementation
     vector<equation_vector> m_watch;           // watch list mapping variables to vector of equations where they occur (generally a subset)
     unsigned                m_levelp1;         // index into level+1
@@ -142,11 +144,16 @@ private:
     void add_to_watch(equation& eq);
 
     void del_equation(equation& eq);    
-    void retire(equation* eq) {
-        dealloc(eq);
-    }
-    void pop_equation(unsigned idx, equation_vector& v);
+    void retire(equation* eq) { dealloc(eq); }
+    void pop_equation(equation& eq, equation_vector& v);
+    void pop_equation(equation* eq, equation_vector& v) { pop_equation(*eq, v); }
     void push_equation(equation& eq, equation_vector& v);
+    void push_equation(equation* eq, equation_vector& v) { push_equation(*eq, v); }
+
+    struct compare_top_var;
+    bool simplify_linear_step();
+    void add_to_use(equation* e, vector<equation_vector>& use_list);
+
 
     void invariant() const;
     struct scoped_detach {