From 738165f0e766f723c6063a2bab10b3b1f5e33f2a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 28 Oct 2019 12:46:10 -0700
Subject: [PATCH] port Grobner: renaming and handle deps in simplifying

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_grobner.cpp | 9 +++++----
 src/math/lp/nla_grobner.h   | 6 +++---
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 735b53feb..66eff73d3 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -301,6 +301,7 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
         simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
     }
     target->exp() = m_nex_creator.simplify(targ_sum);
+    target->dep = m_dep_manager.mk_join(source->dep, target->dep);
     TRACE("grobner", tout << "target = "; display_equation(tout, *target););
     return true;
 }
@@ -428,7 +429,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
     }
 }
 
-bool nla_grobner::simplify_processed_with_eq(equation* eq) {
+bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
     ptr_buffer<equation> to_insert;
     ptr_buffer<equation> to_remove;
     ptr_buffer<equation> to_delete;
@@ -454,7 +455,7 @@ bool nla_grobner::simplify_processed_with_eq(equation* eq) {
     return !canceled();
 }
 
-void  nla_grobner::simplify_to_process(equation* eq) {
+void  nla_grobner::simplify_to_superpose(equation* eq) {
     ptr_buffer<equation> to_insert;
     ptr_buffer<equation> to_remove;
     ptr_buffer<equation> to_delete;
@@ -622,11 +623,11 @@ bool nla_grobner::compute_basis_step() {
         eq = new_eq;
     }
     if (canceled()) return false;
-    if (!simplify_processed_with_eq(eq)) return false;
+    if (!simplify_to_superpose_with_eq(eq)) return false;
     TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
     superpose(eq);
     insert_to_superpose(eq);
-    simplify_to_process(eq);
+    simplify_to_superpose(eq);
     TRACE("grobner", tout << "end of iteration:\n"; display(tout););
     return false;
 }
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 4c8a42d85..59010f72f 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -115,9 +115,9 @@ private:
     equation * simplify_source_target(equation * source, equation * target);
     equation* simplify_using_processed(equation*);
     bool simplify_target_monomials(equation * source, equation * target);
-    void process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove);
-bool simplify_processed_with_eq(equation*);
-    void simplify_to_process(equation*);
+    void process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove);    
+    bool simplify_to_superpose_with_eq(equation*);
+    void simplify_to_superpose(equation*);
     equation* pick_next();
     void set_gb_exhausted();
     bool canceled() const;