From 8744d987a3dbd9db8f7bf634922b1688a867d46a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 28 Oct 2019 11:50:51 -0700
Subject: [PATCH] port Grobner: address memory issues

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

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 575f1634c..735b53feb 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -184,15 +184,11 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
 }
 
 void nla_grobner::del_equation(equation * eq) {
-    NOT_IMPLEMENTED_YET();
-    /*
     m_to_superpose.erase(eq);
     m_to_simplify.erase(eq);
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
     m_equations_to_delete[eq->m_bidx] = 0;
-    del_monomials(eq->m_exp);
     dealloc(eq);
-    */
 }
 
 nla_grobner::equation* nla_grobner::pick_next() {
@@ -526,7 +522,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
     if (!find_b_c(ab, ac, b, c)) {
         return;
     }
-    equation* eq = new equation(); // to do - need no remove !!!!!!!!!!!!!!!!!!!
+    equation* eq = alloc(equation);
     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);
 }
@@ -764,7 +760,7 @@ void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
     TRACE("grobner", tout << "e = " << *e << "\n";);
     if (e == nullptr)
         return;
-    equation * eq = new equation();
+    equation * eq = alloc(equation);
     init_equation(eq, e, dep);
     insert_to_simplify(eq);
 }
@@ -779,6 +775,10 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
 }
 
+nla_grobner::~nla_grobner() {
+    del_equations(0);
+}
+
 std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* dep) const {
     svector<lp::constraint_index> expl;
     m_dep_manager.linearize(dep, expl);   
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index e2b1661f8..4c8a42d85 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -97,6 +97,7 @@ class nla_grobner : common {
 public:
     nla_grobner(core *core);
     void grobner_lemmas();
+    ~nla_grobner();
 private:
     bool scan_for_linear(ptr_vector<equation>& eqs);
     void find_nl_cluster();