From 2c1d68e163aa3a25646fbe3463548fe384600258 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 9 Oct 2019 10:33:47 -0700
Subject: [PATCH] work on Grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/grobner/grobner.cpp | 84 ++++++++++++++++++++----------------
 src/math/grobner/grobner.h   |  1 +
 src/math/lp/var_eqs.h        |  4 --
 3 files changed, 47 insertions(+), 42 deletions(-)

diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 59060b624..ffbc198d5 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -581,6 +581,45 @@ grobner::equation * grobner::copy_equation(equation const * eq) {
     return r;
 }
 
+bool grobner::simplify_for_loop(equation const * source, equation * target, bool & result, unsigned& j ) {
+    bool simplified          = false;
+    unsigned i          = 0;
+    j = 0;
+    unsigned sz         = target->m_monomials.size();
+    monomial const * LT = source->get_monomial(0); 
+    ptr_vector<monomial> & new_monomials = m_tmp_monomials;
+    new_monomials.reset();
+    ptr_vector<expr>  & rest = m_tmp_vars1;
+    
+    for (; i < sz; i++) {
+        monomial * curr = target->m_monomials[i];
+        rest.reset();
+        if (is_subset(LT, curr, rest)) {
+            if (i == 0)
+                m_changed_leading_term = true;
+            if (!result) {
+                // first time that source is being applied.
+                target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
+            }
+            simplified     = true;
+            result         = true;
+            rational coeff = curr->m_coeff;
+            coeff         /= LT->m_coeff;
+            coeff.neg();
+            if (!rest.empty())
+                target->m_lc = false;
+            mul_append(1, source, coeff, rest, new_monomials);
+            del_monomial(curr);
+            target->m_monomials[i] = 0;
+        }
+        else {
+            target->m_monomials[j] = curr;
+            j++;
+        }
+    }
+    return simplified;
+}
+
 /**
    \brief Simplify the target equation using the source as a rewrite rule.
    Return 0 if target was not simplified.
@@ -593,49 +632,18 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
         return nullptr;
     m_stats.m_simplify++;
     bool result = false;
-    bool simplified;
+    
     do {
-        simplified          = false;
-        unsigned i          = 0;
-        unsigned j          = 0;
-        unsigned sz         = target->m_monomials.size();
-        monomial const * LT = source->get_monomial(0); 
-        ptr_vector<monomial> & new_monomials = m_tmp_monomials;
-        new_monomials.reset();
-        ptr_vector<expr>  & rest = m_tmp_vars1;
-        for (; i < sz; i++) {
-            monomial * curr = target->m_monomials[i];
-            rest.reset();
-            if (is_subset(LT, curr, rest)) {
-                if (i == 0)
-                    m_changed_leading_term = true;
-                if (!result) {
-                    // first time that source is being applied.
-                    target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
-                }
-                simplified     = true;
-                result         = true;
-                rational coeff = curr->m_coeff;
-                coeff         /= LT->m_coeff;
-                coeff.neg();
-                if (!rest.empty())
-                    target->m_lc = false;
-                mul_append(1, source, coeff, rest, new_monomials);
-                del_monomial(curr);
-                target->m_monomials[i] = 0;
-            }
-            else {
-                target->m_monomials[j] = curr;
-                j++;
-            }
-        }
-        if (simplified) {
+        unsigned j;
+        if( simplify_for_loop(source, target, result, j)) {
             target->m_monomials.shrink(j);
-            target->m_monomials.append(new_monomials.size(), new_monomials.c_ptr());
+            target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
             simplify(target);
+        } else {
+            break;
         }
     }
-    while (simplified && !m_manager.canceled());
+    while (!m_manager.canceled());
     TRACE("grobner", tout << "result: "; display_equation(tout, *target););
     return result ? target : nullptr;
 }
diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h
index c8668cf20..a16ef17f7 100644
--- a/src/math/grobner/grobner.h
+++ b/src/math/grobner/grobner.h
@@ -166,6 +166,7 @@ protected:
     equation * copy_equation(equation const * eq);
 
     equation * simplify(equation const * source, equation * target);
+    bool simplify_for_loop(equation const * source, equation * target, bool&, unsigned &);
 
     equation * simplify_using_processed(equation * eq);
 
diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h
index 58f5e3f09..66a629465 100644
--- a/src/math/lp/var_eqs.h
+++ b/src/math/lp/var_eqs.h
@@ -344,8 +344,4 @@ public:
         }
     }
 };  // end of var_eqs
-
-// template <typename T>
-// std::ostream& operator<<(var_eqs<T> const& ve, std::ostream& out) { return ve.display(out); }
-
 }