allow for propagations the trigger make-feasible check

src/math/lp/nla_core.cpp

@@ -819,6 +819,7 @@ void core::clear() {
     m_fixed_equalities.clear();
     m_equalities.clear();
     m_conflicts = 0;
+    m_check_feasible = false;
 }
 
 void core::init_search() {
@@ -1192,11 +1193,7 @@ void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
 }
 
 bool core::conflict_found() const {
-    for (const auto & l : m_lemmas) {
-        if (l.is_conflict())
-            return true;
-    }
-    return false;
+    return any_of(m_lemmas, [&](const auto& l) { return l.is_conflict(); });
 }
 
 bool core::done() const {
@@ -1555,7 +1552,7 @@ lbool core::check() {
     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(); };
+    auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; };
 
     if (no_effect())
         m_monomial_bounds.propagate();
@@ -1573,6 +1570,7 @@ lbool core::check() {
               {1, check2},
               {1, check3} };
         check_weighted(3, checks);
+
         if (!m_lemmas.empty() || !m_literals.empty())
             return l_false;
     }
@@ -1610,7 +1608,7 @@ lbool core::check() {
         lp_settings().stats().m_nra_calls++;
     }
 
-    if (ret == l_undef && !m_lemmas.empty() && m_reslim.inc()) 
+    if (ret == l_undef && !no_effect() && m_reslim.inc()) 
         ret = l_false;
 
     lp_settings().stats().m_nla_lemmas += m_lemmas.size();

src/math/lp/nla_core.h

@@ -87,6 +87,7 @@ class core {
     intervals                m_intervals; 
     monomial_bounds          m_monomial_bounds;
     unsigned                 m_conflicts;
+    bool                     m_check_feasible = false;
     horner                   m_horner;
     grobner                  m_grobner;
     emonics                  m_emons;
@@ -424,6 +425,7 @@ class core {
     vector<nla::ineq> const& literals() const { return m_literals; }
     vector<equality> const& equalities() const { return m_equalities; }
     vector<fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
+    bool check_feasible() const { return m_check_feasible; }
 
     void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
     void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }

src/math/lp/nla_grobner.cpp

@@ -401,9 +401,7 @@ namespace nla {
         auto q = e.poly();
 
 
-#if 0
-        // TODO: instead add a row to lra solver, make sure that make_feasible
-        // gets invoked (for example, bail out of final check).
+#if 1
         vector<std::pair<lp::mpq, unsigned>> coeffs;        
         while (!q.is_val()) {
             coeffs.push_back({lc*q.hi().val(), q.var()});
@@ -413,7 +411,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, -lc*q.val(), e.dep());
-
+        c().m_check_feasible = true;
 #else
         
         new_lemma lemma(m_core,"nla-linear");

src/math/lp/nla_solver.h

@@ -51,5 +51,6 @@ namespace nla {
         vector<nla::ineq> const& literals() const;
         vector<nla::fixed_equality> const& fixed_equalities() const;
         vector<nla::equality> const& equalities() const;
+        bool check_feasible() const { return m_core->check_feasible(); }
     };
 }

src/smt/theory_lra.cpp

@@ -2162,15 +2162,6 @@ class theory_lra::imp {
         }
     }
 
-    void add_equalities() {
-        if (!propagate_eqs()) 
-            return;
-        for (auto const& [v,k,e] : m_nla->fixed_equalities())
-            add_equality(v, k, e);
-        for (auto const& [i,j,e] : m_nla->equalities())
-            add_eq(i,j,e,false);
-    }
-
     void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
         TRACE("arith", tout << "equality " << j << " " << k << "\n");
         theory_var v;
@@ -2188,11 +2179,23 @@ class theory_lra::imp {
     }
 
     void add_lemmas() {
+        if (m_nla->check_feasible()) {
+            auto is_sat = make_feasible();
+            if (l_false == is_sat) {
+                get_infeasibility_explanation_and_set_conflict();
+                return;
+            }
+        }
         for (const nla::ineq& i : m_nla->literals())
             assume_literal(i); 
         for (const nla::lemma & l : m_nla->lemmas()) 
             false_case_of_check_nla(l);
-        add_equalities();
+        if (!propagate_eqs())
+            return;
+        for (auto const& [v, k, e] : m_nla->fixed_equalities())
+            add_equality(v, k, e);
+        for (auto const& [i, j, e] : m_nla->equalities())
+            add_eq(i, j, e, false);
     }
 
     bool should_propagate() const {