From 36db31e15406fc1c5ec5ad853cc345f65674601e Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 28 Oct 2019 11:21:52 -0700
Subject: [PATCH] port Grobner

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

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 0685f9a86..575f1634c 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -647,8 +647,17 @@ void nla_grobner::compute_basis_init(){
     
 }        
 
+bool nla_grobner::canceled() const {
+    return c().lp_settings().get_cancel_flag();
+}
+
+
+bool nla_grobner::done() const {
+    return m_num_of_equations >= c().m_nla_settings.grobner_eqs_threshold() || canceled();
+}
+
 bool nla_grobner::compute_basis_loop(){
-    while (m_num_of_equations < c().m_nla_settings.grobner_eqs_threshold()) {
+    while (!done()) {
         if (compute_basis_step())
             return true;
     }
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 1da44d141..e2b1661f8 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -119,7 +119,7 @@ bool simplify_processed_with_eq(equation*);
     void simplify_to_process(equation*);
     equation* pick_next();
     void set_gb_exhausted();
-    bool canceled() { return false; } // todo, implement
+    bool canceled() const;
     void superpose(equation * eq1, equation * eq2);
     void superpose(equation * eq);
     bool find_b_c(const nex *ab, const nex* ac, nex_mul*& b, nex_mul*& c);
@@ -160,5 +160,6 @@ bool simplify_processed_with_eq(equation*);
     nex_mul * divide_ignore_coeffs_perform(nex_mul* , const nex*);
     nex * expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c);
     void add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c);
+    bool done() const;
 }; // end of grobner
 }