From ba2b1ea9296b1cdf4106d652ec3aed9e04be0ef2 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 22 Oct 2019 17:36:47 -0700
Subject: [PATCH] port Grobner

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

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index f2e9a0ee9..711e5853d 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -488,7 +488,38 @@ void  nla_grobner::simplify_to_process(equation* eq) {
         del_equation(eq);
 
 }
+// let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0
+nex * nla_grobner::expr_superpose(nex* e1, nex* e2, nex_mul* ab, nex_mul* ac, nex_mul* b, nex_mul* c) {
+    TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";);    
+    nex_sum * r = m_nex_creator.mk_sum();
+    rational alpha = - ab->coeff();
+    TRACE("grobner", tout << "e2 *= " << alpha << "*(" <<  *b << ")\n";);
+    if (e2->is_sum()) {
+        nex_sum *e2s = to_sum(e2);
+        for (unsigned j = 1; j < e2s->size(); j++) {
+            r->add_child(m_nex_creator.mk_mul(alpha, (*e2s)[j], b));
+        }
+        TRACE("grobner", tout << "r = " << *r << "\n";);
+    } else {
+        NOT_IMPLEMENTED_YET();
+    }
 
+    rational beta = ac->coeff();
+    TRACE("grobner", tout << "e1 *= " << beta << "*(" <<  *c << ")\n";);
+    if (e1->is_sum()) {
+        nex_sum *e1s = to_sum(e1);
+        for (unsigned j = 1; j < e1s->size(); j++) {
+            r->add_child(m_nex_creator.mk_mul(beta, (*e1s)[j], c));
+        }
+        TRACE("grobner", tout << "r = " << *r << "\n";);        
+    } else {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    nex * ret = m_nex_creator.simplify(r);
+    TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\nsuperpose = " << *ret << "\n";);
+    return ret;
+}
 // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
 void nla_grobner::superpose(equation * eq1, equation * eq2) {
     TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
@@ -499,8 +530,9 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
     if (!find_b_c(ab, ac, b, c)) {
         return;
     }
-    NOT_IMPLEMENTED_YET();
-    //    insert_to_
+    equation* eq = new equation(); // to do - need no remove !!!!!!!!!!!!!!!!!!!
+    init_equation(eq, expr_superpose( eq1->exp(), eq2->exp(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep()));  
+    insert_to_simplify(eq);
 }
 
 bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) {
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 48219c220..bf8beb031 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -157,5 +157,6 @@ bool simplify_processed_with_eq(equation*);
     nex_mul * divide_ignore_coeffs(nex* ej, const nex_mul*);
     bool divide_ignore_coeffs_check_only(nex_mul* , const nex_mul*);
     nex_mul * divide_ignore_coeffs_perform(nex_mul* , const nex_mul*);
+    nex * expr_superpose(nex* e1, nex* e2, nex_mul* ab, nex_mul* ac, nex_mul* b, nex_mul* c);
 }; // end of grobner
 }