add incremental propagate for nla to retain some propagation lemmas

src/math/lp/monomial_bounds.cpp

@@ -199,13 +199,15 @@ namespace nla {
         }
     }
 
-    bool monomial_bounds::propagate_linear_monomials() {        
+    bool monomial_bounds::propagate_changed_bounds() {        
         bool propagated = false;
         for (lpvar v : c().m_monics_with_changed_bounds) {
             if (!c().is_monic_var(v))
                 continue;
             monic& m = c().emon(v);
-            if (propagate_linear_monomial(m))
+            if (propagate_changed_bound(m))
+                propagated = true;
+            if (tighten_lp(m))
                 propagated = true;
             if (c().lra.get_status() == lp::lp_status::INFEASIBLE)
                 break;
@@ -223,7 +225,7 @@ namespace nla {
         return true;
     }
 
-    bool monomial_bounds::propagate_linear_monomial(monic & m) {
+    bool monomial_bounds::propagate_changed_bound(monic & m) {
         if (m.is_propagated())
             return false;
         lpvar w, fixed_to_zero;
@@ -642,7 +644,6 @@ namespace nla {
      */
     void monomial_bounds::propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d) {
         SASSERT(cmp != llc::EQ && cmp != llc::NE);
-        IF_VERBOSE(1, verbose_stream() << "propagate_lp_bound: v=" << v << " cmp=" << cmp << " q=" << q << "\n";);
         if (!c().var_is_int(v))
             c().lra.update_column_type_and_bound(v, cmp, q, d);
         else if (q.is_int()) {
@@ -673,9 +674,6 @@ namespace nla {
         for (auto &m : c().emons()) 
             if (tighten_lp(m))
                 new_bound = true;
-        if (propagate_linear_monomials())
-            new_bound = true;
-        IF_VERBOSE(1, verbose_stream() << "tighten_lp_bounds: new_bound=" << new_bound << "\n";);
         return new_bound;
     }
 

src/math/lp/monomial_bounds.h

@@ -48,13 +48,13 @@ namespace nla {
         // linear-monomial equality propagation:
         // when all but one variable of a monomial are fixed, the monomial is
         // linear and its value/equality can be propagated into the LP solver.
-        bool propagate_linear_monomial(monic & m);
-        bool propagate_linear_monomials();
+        bool propagate_changed_bound(monic & m);
         bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero);
         rational fixed_var_product(monic const& m, lpvar w);
     public:
         monomial_bounds(core* core);
         void generate_lemmas();
         bool tighten_lp_bounds();
+        bool propagate_changed_bounds();
     }; 
 }

src/math/lp/nla_core.cpp

@@ -1525,12 +1525,26 @@ void core::set_use_nra_model(bool m) {
 
     
 bool core::propagate() {
-    clear();   
     bool propagated = m_monomial_bounds.tighten_lp_bounds();
+    if (m_monomial_bounds.propagate_changed_bounds())
+        propagated = true;
     m_monics_with_changed_bounds.reset();
+    if (propagated)
+        m_check_feasible = true;
     return propagated;
 }
 
+bool core::incremental_propagate() {
+    bool propagated = false;
+    clear();
+    if (m_monomial_bounds.propagate_changed_bounds())
+        propagated = true;
+    m_monics_with_changed_bounds.reset();
+    if (propagated)
+        m_check_feasible = true;
+    return propagated;    
+}
+
 /**
    \brief Tighten the bounds of variables occurring in nonlinear monomials by
    maximizing/minimizing them over the LP tableau (analogous to theory_arith's

src/math/lp/nla_core.h

@@ -410,6 +410,7 @@ public:
     bool  no_lemmas_hold() const;
 
     bool propagate();
+    bool incremental_propagate();
 
     void simplify();
     

src/math/lp/nla_solver.cpp

@@ -57,6 +57,10 @@ namespace nla {
     bool solver::propagate() {
         return m_core->propagate();
     }
+
+    bool solver::incremental_propagate() {
+        return m_core->incremental_propagate();
+    }
     
     void solver::push(){
         m_core->push();

src/math/lp/nla_solver.h

@@ -40,6 +40,7 @@ namespace nla {
         bool need_check();
         lbool check(unsigned level);
         bool propagate();
+        bool incremental_propagate();
         void simplify() { m_core->simplify(); }
         lbool check_power(lpvar r, lpvar x, lpvar y);
         bool is_monic_var(lpvar) const;

src/smt/theory_lra.cpp

@@ -2319,7 +2319,7 @@ public:
             get_infeasibility_explanation_and_set_conflict();
             break;
         case l_true:
-            propagate_nla();
+            incremental_propagate_nla();         
             propagate_bounds_with_lp_solver();
             break;
         case l_undef:
@@ -2332,7 +2332,17 @@ public:
     bool propagate_nla() {
         bool propagated = false;
         if (m_nla) {
-            propagated = m_nla->propagate() || propagated;
+            propagated = m_nla->propagate();
+            add_lemmas();
+            lp().collect_more_rows_for_lp_propagation();
+        }
+        return propagated;
+    }
+
+    bool incremental_propagate_nla() {
+        bool propagated = false;
+        if (m_nla) {
+            propagated = m_nla->incremental_propagate();
             add_lemmas();
             lp().collect_more_rows_for_lp_propagation();
         }