From 7386b7d68ddda9a29753367bc8fd60ffe784a83e Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 5 Sep 2019 15:17:30 -0700
Subject: [PATCH] start porting grobner basis functionality

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_arith_nl.h | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 2e0890a8f..c38b1b416 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -2233,7 +2233,7 @@ void theory_arith<Ext>::update_statistics(grobner & gb) {
 }
 
 template<typename Ext>
-void theory_arith<Ext>::set_gb_exhausted(bool r) {
+void theory_arith<Ext>::set_gb_exhausted() {
     IF_VERBOSE(3, verbose_stream() << "Grobner basis computation interrupted. Increase threshold using NL_ARITH_GB_THRESHOLD=<limit>\n";);
     get_context().push_trail(value_trail<context, bool>(m_nl_gb_exhausted));
     m_nl_gb_exhausted = true;
@@ -2305,6 +2305,19 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::scan_for_linear(ptr_vec
     return result;
 }
 
+
+template<typename Ext>
+bool theory_arith<Ext>::compute_basis_loop(grobner & gb) {
+    while (gb.get_num_new_equations() < m_params.m_nl_arith_gb_threshold) {
+        if (get_context().get_cancel_flag()) {
+            return false;
+        }
+        if (gb.compute_basis_step())
+            return true;
+    }
+    return false;
+}
+
 /**
    \brief Compute Grobner basis, return true if a conflict or new fixed variables were detected.
 */
@@ -2321,17 +2334,11 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
 
     while (true) {
         TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
-        bool r = false;
         gb.compute_basis_init();
-        while (!r && gb.get_num_new_equations() < m_params.m_nl_arith_gb_threshold) {
-            if (get_context().get_cancel_flag()) {
-                return GB_FAIL;
-            }
-            r = gb.compute_basis_step();
-        }
+        bool r = compute_basis_loop(gb);
         update_statistics(gb);
         if (!r && !warn) {
-            set_gb_exhausted(r);
+            set_gb_exhausted();
             warn = true;
         }
         if (get_context().get_cancel_flag()) {