Make Groebner basis computation interruptable. Exponsed in issue #269

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/grobner/grobner.cpp

@@ -923,30 +923,39 @@ void grobner::superpose(equation * eq) {
     }
 }
 
-bool grobner::compute_basis(unsigned threshold) {
+void grobner::compute_basis_init() {
     m_stats.m_compute_basis++;
     m_num_new_equations = 0;
-    while (m_num_new_equations < threshold) {
-        equation * eq = pick_next();
-        if (!eq)
-            return true;
-        m_stats.m_num_processed++;
+}
+
+bool grobner::compute_basis_step() {
+    equation * eq = pick_next();
+    if (!eq)
+        return true;
+    m_stats.m_num_processed++;
 #ifdef PROFILE_GB
-        if (m_stats.m_num_processed % 100 == 0) {
-            verbose_stream() << "[grobner] " << m_processed.size() << " " << m_to_process.size() << "\n";
-        }
+    if (m_stats.m_num_processed % 100 == 0) {
+        verbose_stream() << "[grobner] " << m_processed.size() << " " << m_to_process.size() << "\n";
+    }
 #endif
-        equation * new_eq = simplify_using_processed(eq);
-        if (new_eq != 0 && eq != new_eq) {
-            // equation was updated using non destructive updates
-            m_equations_to_unfreeze.push_back(eq);
-            eq = new_eq;
-        }
-        simplify_processed(eq);
-        superpose(eq);
-        m_processed.insert(eq);
-        simplify_to_process(eq);
-        TRACE("grobner", tout << "end of iteration:\n"; display(tout););
+    equation * new_eq = simplify_using_processed(eq);
+    if (new_eq != 0 && eq != new_eq) {
+        // equation was updated using non destructive updates
+        m_equations_to_unfreeze.push_back(eq);
+        eq = new_eq;
+    }
+    simplify_processed(eq);
+    superpose(eq);
+    m_processed.insert(eq);
+    simplify_to_process(eq);
+    TRACE("grobner", tout << "end of iteration:\n"; display(tout););
+    return false;
+}
+
+bool grobner::compute_basis(unsigned threshold) {
+    compute_basis_init();
+    while (m_num_new_equations < threshold) {
+        if (compute_basis_step()) return true;
     }
     return false;
 }

src/math/grobner/grobner.h

@@ -251,6 +251,15 @@ public:
     */
     bool compute_basis(unsigned threshold);
 
+    /**
+       \brief Compute one step Grobner basis.
+       Return true if there is no new equation to take.
+    */
+    void compute_basis_init();
+    bool compute_basis_step();
+    unsigned get_num_new_equations() { return m_num_new_equations; }
+
+
     /**
        \brief Return true if an inconsistency was detected.
     */

src/smt/smt_model_checker.cpp

@@ -176,10 +176,11 @@ namespace smt {
             bindings.set(num_decls - i - 1, sk_value);
         }
         
-        TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance:\n";
+        TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
               for (unsigned i = 0; i < num_decls; i++) {
-                  tout << mk_ismt2_pp(bindings[i], m_manager) << "\n";
-              });
+                  tout << mk_ismt2_pp(bindings[i], m_manager) << " ";
+              }
+              tout << "\n";);
         
         for (unsigned i = 0; i < num_decls; i++) 
             m_new_instances_bindings.push_back(bindings[i]);

src/smt/smt_model_finder.cpp

@@ -149,7 +149,7 @@ namespace smt {
                     SASSERT(!contains_model_value(t));
                     unsigned gen = (*it).m_value;
                     expr * t_val = ev.eval(t, true);
-                    TRACE("model_finder", tout << mk_pp(t, m_manager) << "\n";);
+                    TRACE("model_finder", tout << mk_pp(t, m_manager) << " " << mk_pp(t_val, m_manager) << "\n";);
 
                     expr * old_t = 0;
                     if (m_inv.find(t_val, old_t)) {

src/smt/theory_arith_nl.h

@@ -2227,7 +2227,15 @@ namespace smt {
         
         while (true) {
             TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
-            bool r = gb.compute_basis(m_params.m_nl_arith_gb_threshold);
+            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()) {
+                    warn = true;
+                    break;
+                }
+                r = gb.compute_basis_step();
+            }
             m_stats.m_gb_simplify      += gb.m_stats.m_simplify;
             m_stats.m_gb_superpose     += gb.m_stats.m_superpose;
             m_stats.m_gb_num_processed += gb.m_stats.m_num_processed;