use cone of influence reduction before calling nlsat.

src/math/lp/nla_core.cpp

@@ -1549,7 +1549,6 @@ lbool core::check() {
     lbool ret = l_undef;
     bool run_grobner = need_run_grobner();
     bool run_horner = need_run_horner();
-    bool run_bounded_nlsat = should_run_bounded_nlsat();
     bool run_bounds = params().arith_nl_branching();
 
     auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; };
@@ -1572,7 +1571,7 @@ lbool core::check() {
             return l_false;
     }
 
-    if (no_effect() && run_bounded_nlsat)
+    if (no_effect() && should_run_bounded_nlsat())
         ret = bounded_nlsat();
 
     if (no_effect()) 
@@ -1582,8 +1581,7 @@ lbool core::check() {
         m_basics.basic_lemma(false);
 
     if (no_effect()) 
-        m_divisions.check();
-
+        m_divisions.check();    
 
     if (no_effect() && ret == l_undef) {
         std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
@@ -1610,7 +1608,6 @@ lbool core::check() {
         ret = l_false;
 
     lp_settings().stats().m_nla_lemmas += m_lemmas.size();
-
 
     TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
     IF_VERBOSE(5, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
@@ -1623,7 +1620,7 @@ bool core::should_run_bounded_nlsat() {
         return false;
     if (m_nlsat_delay > 0) 
         --m_nlsat_delay;
-    return m_nlsat_delay < 5;
+    return m_nlsat_delay < 2;
 }
 
 lbool core::bounded_nlsat() {

src/math/lp/nla_grobner.cpp

@@ -50,10 +50,10 @@ namespace nla {
             return;
         }
 
-
         lp_settings().stats().m_grobner_calls++;
         find_nl_cluster();        
-        configure();
+        if (!configure())
+            return;
         m_solver.saturate();
 
         if (m_delay_base > 0)
@@ -89,15 +89,14 @@ namespace nla {
 
         IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
         IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
+    }
 
-
-#if 0
-        // diagnostics: did we miss something
-        vector<dd::pdd> eqs;
-        for (auto eq : m_solver.equations())
-            eqs.push_back(eq->poly());
-        c().m_nra.check(eqs);
-#endif
+    dd::solver::equation_vector const& grobner::core_equations(bool all_eqs) {
+        flet<bool> _add_all(m_add_all_eqs, all_eqs);
+        find_nl_cluster();        
+        if (!configure()) 
+            throw dd::pdd_manager::mem_out();
+        return m_solver.equations();
     }
 
     bool grobner::is_conflicting() {
@@ -220,7 +219,7 @@ namespace nla {
         return true;
     }
 
-    void grobner::explain(const dd::solver::equation& eq, lp::explanation& exp) {
+    void grobner::explain(dd::solver::equation const& eq, lp::explanation& exp) {
         u_dependency_manager dm;
         vector<unsigned, false> lv;
         dm.linearize(eq.dep(), lv);
@@ -235,7 +234,7 @@ namespace nla {
         lemma &= exp;
     }
 
-    void grobner::configure() {
+    bool grobner::configure() {
         m_solver.reset();
         try {
             set_level2var();
@@ -253,12 +252,12 @@ namespace nla {
                     add_fixed_monic(j);
             }
         }
-        catch (...) {
+        catch (dd::pdd_manager::mem_out) {
             IF_VERBOSE(2, verbose_stream() << "pdd throw\n");
-            return;
+            return false;
         }
         TRACE("grobner", m_solver.display(tout));
-    
+
 #if 0
         IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
         dd::pdd_eval eval(m_pdd_manager);
@@ -282,6 +281,8 @@ namespace nla {
         m_solver.set(cfg);
         m_solver.adjust_cfg();
         m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
+
+        return true;
     }
 
     std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) {
@@ -389,8 +390,8 @@ namespace nla {
         for (auto const& m : c().emons()) 
             m_mon2var[m.vars()] = m.var();
         for (auto eq : m_solver.equations()) 
-            if (propagate_linear_equations(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
-                return true;
+            if (propagate_linear_equations(*eq))
+                ++changed;
         return changed > 0;
     }
 
@@ -430,7 +431,7 @@ namespace nla {
         lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
         term_index = c().lra.map_term_index_to_column_index(term_index);
         c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, offset, e.dep());
-        c().m_check_feasible = true;
+        c().m_check_feasible = true; 
         return true;
     }
 
@@ -455,11 +456,16 @@ namespace nla {
                 continue;
             m_rows.insert(row);
             unsigned k = lra.get_base_column_in_row(row);
-            if (lra.column_is_free(k) && k != j)
+            // grobner bassis does not know about integer constraints
+            if (lra.column_is_free(k) && !m_add_all_eqs && k != j)
+                continue;
+            // a free column over the reals can be assigned
+            if (lra.column_is_free(k) && k != j && !lra.var_is_int(k)) 
                 continue;
             CTRACE("grobner", matrix.m_rows[row].size() > c().params().arith_nl_grobner_row_length_limit(),
-                   tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); 
-            if (matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit())
+                   tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";);
+            // limits overhead of grobner equations, unless this is for extracting a complete COI of the non-satisfied subset.
+            if (!m_add_all_eqs && matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit())
                 continue;
             for (auto& rc : matrix.m_rows[row]) 
                 add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
@@ -585,7 +591,6 @@ namespace nla {
         add_eq(sum, dep);
     }
 
-
     void grobner::find_nl_cluster() {        
         prepare_rows_and_active_vars();
         svector<lpvar> q;

src/math/lp/nla_grobner.h

@@ -26,6 +26,7 @@ namespace nla {
         unsigned                 m_quota = 0;
         unsigned                 m_delay_base = 0;
         unsigned                 m_delay = 0;
+        bool                     m_add_all_eqs = false;
         std::unordered_map<unsigned_vector, lpvar, hash_svector> m_mon2var;
 
         lp::lp_settings& lp_settings();
@@ -58,7 +59,7 @@ namespace nla {
         bool equation_is_true(dd::solver::equation const& eq);
 
         // setup
-        void configure();
+        bool configure();
         void set_level2var();
         void find_nl_cluster();
         void prepare_rows_and_active_vars();
@@ -76,5 +77,6 @@ namespace nla {
     public:
         grobner(core *core);        
         void operator()();
+        dd::solver::equation_vector const& core_equations(bool all_eqs);
     }; 
 }