add limit checks in Grobner. Issue #599

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

src/math/grobner/grobner.cpp

@@ -670,7 +670,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
             simplify(target);
         }
     }
-    while (simplified);
+    while (simplified && !m_manager.canceled());
     TRACE("grobner", tout << "result: "; display_equation(tout, *target););
     return result ? target : 0;
 }
@@ -697,7 +697,10 @@ grobner::equation * grobner::simplify_using_processed(equation * eq) {
                 simplified = true;
                 eq         = new_eq;
             }
-        }
+            if (m_manager.canceled()) {
+                return 0;
+            }
+        }        
     }
     while (simplified);
     TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq););
@@ -749,13 +752,13 @@ grobner::equation * grobner::pick_next() {
 /**
    \brief Use the given equation to simplify processed terms.
 */
-void grobner::simplify_processed(equation * eq) {
+bool grobner::simplify_processed(equation * eq) {
     ptr_buffer<equation> to_insert;
     ptr_buffer<equation> to_remove;
     ptr_buffer<equation> to_delete;
     equation_set::iterator it  = m_processed.begin();
     equation_set::iterator end = m_processed.end();
-    for (; it != end; ++it) {
+    for (; it != end && !m_manager.canceled(); ++it) {
         equation * curr        = *it;
         m_changed_leading_term = false;
         // if the leading term is simplified, then the equation has to be moved to m_to_process
@@ -795,6 +798,7 @@ void grobner::simplify_processed(equation * eq) {
     end1 = to_delete.end();
     for (; it1 != end1; ++it1)
         del_equation(*it1);
+    return !m_manager.canceled();
 }
 
 /**
@@ -944,7 +948,8 @@ bool grobner::compute_basis_step() {
         m_equations_to_unfreeze.push_back(eq);
         eq = new_eq;
     }
-    simplify_processed(eq);
+    if (m_manager.canceled()) return false;
+    if (!simplify_processed(eq)) return false;
     superpose(eq);
     m_processed.insert(eq);
     simplify_to_process(eq);
@@ -954,7 +959,7 @@ bool grobner::compute_basis_step() {
 
 bool grobner::compute_basis(unsigned threshold) {
     compute_basis_init();
-    while (m_num_new_equations < threshold) {
+    while (m_num_new_equations < threshold && !m_manager.canceled()) {
         if (compute_basis_step()) return true;
     }
     return false;

src/math/grobner/grobner.h

@@ -175,7 +175,7 @@ protected:
 
     equation * pick_next();
 
-    void simplify_processed(equation * eq);
+    bool simplify_processed(equation * eq);
 
     void simplify_to_process(equation * eq);
 

src/model/model_evaluator.cpp

@@ -114,7 +114,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
         family_id fid = f->get_family_id();
-        if (num == 0 && (fid == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {
+        bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f);
+        if (num == 0 && (fid == null_family_id || is_uninterp)) {
             expr * val = m_model.get_const_interp(f);
             if (val != 0) {
                 result = val;

src/qe/qsat.cpp

@@ -620,7 +620,7 @@ namespace qe {
         }
 
         kernel& get_kernel(unsigned j) {        
-            if (is_exists(j)) {
+            if (m_kernel_ex || is_exists(j)) {
                 return m_ex; 
             }
             else {
@@ -1073,7 +1073,7 @@ namespace qe {
             m_mode(mode),
             m_avars(m),
             m_free_vars(m),
-            m_kernel(m)
+            m_kernel_ex(false)
         {
             reset();
         }
@@ -1240,9 +1240,10 @@ namespace qe {
         }
 
 
-        kernel          m_kernel;
+        bool         m_kernel_ex;
 
         lbool max_min(expr_ref_vector const& fmls, svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
+            m_kernel_ex = true;
             // Assume this is the only call to check.
             expr_ref_vector defs(m);
             app_ref_vector free_vars(m), vars1(m);
@@ -1250,8 +1251,8 @@ namespace qe {
             m_pred_abs.get_free_vars(fml, free_vars);
             m_pred_abs.abstract_atoms(fml, defs);
             fml = m_pred_abs.mk_abstract(fml);
-            m_kernel.assert_expr(mk_and(defs));
+            get_kernel(0).k().assert_expr(mk_and(defs));
-            m_kernel.assert_expr(fml);
+            get_kernel(0).k().assert_expr(fml);
             obj_hashtable<app> var_set;
             for (unsigned i = 0; i < vars.size(); ++i) {
                 var_set.insert(vars[i]);
@@ -1278,8 +1279,6 @@ namespace qe {
             m_vars.push_back(vars1);
             
             return max_min();
-            
-            // return l_undef;
         }
 
         lbool max_min() {
@@ -1288,15 +1287,39 @@ namespace qe {
                 check_cancel();
                 expr_ref_vector asms(m_asms);
                 m_pred_abs.get_assumptions(m_model.get(), asms);
+                //
+                // TBD: add bound to asms.
+                // 
                 smt::kernel& k = get_kernel(m_level).k();
                 lbool res = k.check(asms);
                 switch (res) {
                 case l_true:
+                    k.get_model(m_model);
+                    SASSERT(validate_model(asms));
+                    TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
+                    // 
+                    // TBD: compute new bound on objective.
+                    // 
+                    push();
                     break;
                 case l_false:
+                    switch (m_level) {
+                    case 0: return l_false;
+                    case 1:
+                        // TBD
+                        break;
+                    default:
+                        if (m_model.get()) {
+                            project(asms); 
+                        }
+                        else {
+                            pop(1);
+                        }
+                        break; 
+                    }
                     break;
                 case l_undef:
-                    break;
+                    return res;
                 }
             }
             return l_undef;