runs a simple test

src/math/lp/bound_analyzer_on_row.h

@@ -26,6 +26,8 @@ Revision History:
 #include "math/lp/test_bound_analyzer.h"
 
 namespace lp {
+  
+ 
 template <typename C, typename B> // C plays a role of a container, B - lp_bound_propagator
 class bound_analyzer_on_row {
     const C&                           m_row;
@@ -301,8 +303,12 @@ private:
     //     */
     // }
 
-    void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
-        m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_index, strict);
+    
+    void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
+        lar_solver* lar = & this->m_bp.lp();
+        unsigned row_index = this->m_row_index;
+        auto explain = [lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index]() { return explain_bound_on_var_on_coeff(lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); };
+        m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain );
     }
     
     void advance_u(unsigned j) {
@@ -335,6 +341,27 @@ private:
             break;
         }
     }   
+    static u_dependency* explain_bound_on_var_on_coeff(lar_solver* lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
+        int bound_sign = (is_lower_bound ? 1 : -1);
+        int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
+
+        if (tv::is_term(bound_j))
+            bound_j = lar->map_term_index_to_column_index(bound_j);
+        u_dependency* ret = nullptr;
+        for (auto const& r : lar->get_row(row_index)) {
+            unsigned j = r.var();
+            if (j == bound_j)
+                continue;
+            mpq const& a = r.coeff();
+            int a_sign = is_pos(a) ? 1 : -1;
+            int sign = j_sign * a_sign;
+            u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j);
+            ret = lar->join_deps(ret, witness);
+        }
+        return ret;
+    }
 };
+   
+
 }
 

src/math/lp/implied_bound.h

@@ -21,37 +21,34 @@ Revision History:
 #include "math/lp/lp_settings.h"
 #include "math/lp/lar_constraints.h"
 namespace lp {
-struct implied_bound {
+class implied_bound {
+    public:
     mpq m_bound;
     unsigned m_j; // the column for which the bound has been found
     bool m_is_lower_bound;
-    bool m_coeff_before_j_is_pos;
-    unsigned m_row_or_term_index;
-    bool m_strict;
+	bool m_strict;
+    private:
+    std::function<u_dependency*(void)> m_explain_bound = nullptr;
+    public:
+    u_dependency* explain() const { return m_explain_bound(); }
+    void set_explain(std::function<u_dependency*(void)> f) { m_explain_bound = f; }
     lconstraint_kind kind() const {
         lconstraint_kind k = m_is_lower_bound? GE : LE;
         if (m_strict)
             k = static_cast<lconstraint_kind>(k / 2);
         return k;
     }
-    bool operator==(const implied_bound & o) const {
-        return m_j == o.m_j && m_is_lower_bound == o.m_is_lower_bound && m_bound == o.m_bound &&
-            m_coeff_before_j_is_pos == o.m_coeff_before_j_is_pos &&
-            m_row_or_term_index == o.m_row_or_term_index && m_strict == o.m_strict;
-    }
     implied_bound(){}
     implied_bound(const mpq & a,
                   unsigned j,
-                  bool lower_bound,
-                  bool coeff_before_j_is_pos,
-                  unsigned row_or_term_index,
-                  bool strict):
+                  bool is_lower_bound,
+				  bool is_strict,
+                  std::function<u_dependency*(void)> get_dep):
         m_bound(a),
         m_j(j),
-        m_is_lower_bound(lower_bound),
-        m_coeff_before_j_is_pos(coeff_before_j_is_pos),
-        m_row_or_term_index(row_or_term_index),
-        m_strict(strict) {
+        m_is_lower_bound(is_lower_bound),
+        m_strict(is_strict),
+        m_explain_bound(get_dep) {
     }
 };
 }

src/math/lp/lar_solver.h

@@ -311,26 +311,34 @@ class lar_solver : public column_namer {
 
     template <typename T>
     void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
-        unsigned i = ib.m_row_or_term_index;
-        int bound_sign = (ib.m_is_lower_bound ? 1 : -1);
-        int j_sign = (ib.m_coeff_before_j_is_pos ? 1 : -1) * bound_sign;
-        unsigned bound_j = ib.m_j;
-        if (tv::is_term(bound_j))
-            bound_j = m_var_register.external_to_local(bound_j);
+        u_dependency* dep = ib.explain();
+        for (auto ci : flatten(dep))
+            bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients
+        /*
+        if (ib.m_is_monic) {
+            NOT_IMPLEMENTED_YET();
+        } else {
+            unsigned i = ib.m_row_or_term_index;
+            int bound_sign = (ib.m_is_lower_bound ? 1 : -1);
+            int j_sign = (ib.m_coeff_before_j_is_pos ? 1 : -1) * bound_sign;
+            unsigned bound_j = ib.m_j;
+            if (tv::is_term(bound_j))
+                bound_j = m_var_register.external_to_local(bound_j);
 
-        for (auto const& r : get_row(i)) {
-            unsigned j = r.var();
-            if (j == bound_j)
-                continue;
-            mpq const& a = r.coeff();
-            int a_sign = is_pos(a) ? 1 : -1;
-            int sign = j_sign * a_sign;
-            const ul_pair& ul = m_columns_to_ul_pairs[j];
-            auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
-            lp_assert(witness);
-            for (auto ci : flatten(witness))
-                bp.consume(a, ci);
-        }
+            for (auto const& r : get_row(i)) {
+                unsigned j = r.var();
+                if (j == bound_j)
+                    continue;
+                mpq const& a = r.coeff();
+                int a_sign = is_pos(a) ? 1 : -1;
+                int sign = j_sign * a_sign;
+                const ul_pair& ul = m_columns_to_ul_pairs[j];
+                auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
+                lp_assert(witness);
+                for (auto ci : flatten(witness))
+                    bp.consume(a, ci);
+            }
+            }*/
     }
 
     void set_value_for_nbasic_column(unsigned j, const impq& new_val);
@@ -564,6 +572,16 @@ class lar_solver : public column_namer {
         const ul_pair& ul = m_columns_to_ul_pairs[j];
         return m_dependencies.mk_join(ul.lower_bound_witness(), ul.upper_bound_witness());
     }
+    template <typename T>
+    u_dependency* get_bound_constraint_witnesses_for_columns(const T& collection) {
+        u_dependency* dep = nullptr;
+        for (auto j : collection) {
+            u_dependency* d = get_bound_constraint_witnesses_for_column(j);
+            dep = m_dependencies.mk_join(dep, d);
+        }
+        return dep;
+    }
+    u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); }
     inline constraint_set const& constraints() const { return m_constraints; }
     void push();
     void pop();

src/math/lp/lp_bound_propagator.h

@@ -40,6 +40,7 @@ class lp_bound_propagator {
         return x != UINT_MAX;
     }
 
+   
     void try_add_equation_with_internal_fixed_tables(unsigned r1) {
         unsigned v1, v2;
         if (!only_one_nfixed(r1, v1))
@@ -94,6 +95,115 @@ class lp_bound_propagator {
         m_ibounds.reset();
         m_column_types = &lp().get_column_types();
     }
+   
+    bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
+        zero_var = non_fixed = null_lpvar;
+        unsigned n_of_non_fixed = 0;
+        bool big_bound = false;
+        for (lpvar v : m) {
+            if (!this->column_is_fixed(v)) {
+                n_of_non_fixed++;
+                non_fixed = v;
+                continue;                
+            } 
+            const auto & b = get_lower_bound(v).x;
+            if (b.is_zero()) {
+                zero_var = v;
+                return true;
+            } 
+            if (b.is_big()) {
+                big_bound |= true;
+            }
+        }
+        return n_of_non_fixed <= 1 && !big_bound;
+    }
+
+    void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
+        add_lower_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);});
+        add_upper_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);});
+    }
+
+    void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function<u_dependency* ()> explain_dep) {
+       unsigned k;
+       if (!try_get_value(m_improved_lower_bounds, monic_var, k)) {
+            m_improved_lower_bounds[monic_var] = m_ibounds.size();
+            m_ibounds.push_back(implied_bound(v, monic_var, true, is_strict, explain_dep));
+       } else {
+            auto& found_bound = m_ibounds[k];
+            if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
+                found_bound = implied_bound(v, monic_var, true, is_strict, explain_dep);
+                TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
+            }
+       }
+    }
+
+    void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function <u_dependency* ()> explain_bound) {
+        unsigned k;
+        if (!try_get_value(m_improved_upper_bounds, monic_var, k)) {
+            m_improved_upper_bounds[monic_var] = m_ibounds.size();
+            m_ibounds.push_back(implied_bound(bound_val, monic_var, false, is_strict, explain_bound));
+       } else {
+            auto& found_bound = m_ibounds[k];
+            if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
+                found_bound = implied_bound(bound_val, monic_var, false, is_strict, explain_bound);
+                TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
+            }
+       }
+    }
+
+    void propagate_monic(lpvar monic_var, const svector<lpvar>& vars) {
+        lpvar non_fixed, zero_var;
+        if (!is_linear(vars, zero_var, non_fixed)) {
+            return;
+        }
+
+        if (zero_var != null_lpvar) {
+            add_bounds_for_zero_var(monic_var, zero_var);
+        } else {
+            if (non_fixed != null_lpvar && get_column_type(non_fixed) == column_type::free_column) return;
+            rational k = rational(1);
+            for (auto v : vars)
+                if (v != non_fixed) {
+                    k *= lp().get_column_value(v).x;
+                    if (k.is_big()) return;
+                }
+            u_dependency* dep;
+            lp::mpq bound_value;
+            bool is_strict;
+            if (non_fixed != null_lpvar) {
+                if (this->lp().has_lower_bound(non_fixed, dep, bound_value, is_strict)) {
+                    if (k.is_pos())
+                        add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() { return dep; });
+                    else
+                        add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;});
+                }
+                if (this->lp().has_upper_bound(non_fixed, dep, bound_value, is_strict)) {
+                    if (k.is_neg())
+                        add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;});
+                    else
+                        add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;});
+                }
+
+                if (this->lp().has_lower_bound(monic_var, dep, bound_value, is_strict)) {
+                    if (k.is_pos())
+                        add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+                    else
+                        add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+                }
+
+                if (this->lp().has_upper_bound(monic_var, dep, bound_value, is_strict)) {
+                    if (k.is_neg())
+                        add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+                    else
+                        add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+                }
+
+            } else {  // all variables are fixed
+                add_lower_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);});
+                add_upper_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);});                
+            }
+        }
+    }
 
     const lar_solver& lp() const { return m_imp.lp(); }
     lar_solver& lp() { return m_imp.lp(); }
@@ -123,7 +233,7 @@ class lp_bound_propagator {
         return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero();
     }
 
-    void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
+    void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* ()> explain_bound) {
         j = m_imp.lp().column_to_reported_index(j);
 
         lconstraint_kind kind = is_low ? GE : LE;
@@ -137,25 +247,29 @@ class lp_bound_propagator {
             if (try_get_value(m_improved_lower_bounds, j, k)) {
                 auto& found_bound = m_ibounds[k];
                 if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
-                    found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
-                    TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
+                    found_bound.m_bound = v;
+                    found_bound.m_strict = strict;
+                    found_bound.set_explain(explain_bound);
+                    TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
                 }
             } else {
                 m_improved_lower_bounds[j] = m_ibounds.size();
-                m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
-                TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
+                m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound));
+                TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
             }
         } else {  // the upper bound case
             if (try_get_value(m_improved_upper_bounds, j, k)) {
                 auto& found_bound = m_ibounds[k];
                 if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
-                    found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
-                    TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
+                    found_bound.m_bound = v;
+                    found_bound.m_strict = strict;
+                    found_bound.set_explain(explain_bound);
+                    TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
                 }
             } else {
                 m_improved_upper_bounds[j] = m_ibounds.size();
-                m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
-                TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
+                m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound));
+                TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
             }
         }
     }

src/math/lp/monomial_bounds.cpp

@@ -261,6 +261,7 @@ namespace nla {
     void monomial_bounds::unit_propagate() {        
         for (lpvar v : c().m_monics_with_changed_bounds) 
             unit_propagate(c().emons()[v]);
+         c().m_monics_with_changed_bounds.clear();        
     }
 
     void monomial_bounds::unit_propagate(monic const& m) {
@@ -268,68 +269,61 @@ namespace nla {
         if (m_propagated[m.var()])
             return;
 
-        if (!is_linear(m))
+        lpvar non_fixed = null_lpvar, zero_var = null_lpvar; 
+        if (!is_linear(m, zero_var, non_fixed))
             return;
         
         c().trail().push(set_bitvector_trail(m_propagated, m.var()));
         
-        rational k = fixed_var_product(m);
         
-        new_lemma lemma(c(), "fixed-values");
-        if (k == 0) {
-            for (auto v : m) {
-                if (c().var_is_fixed(v) && c().val(v).is_zero()) {
-                    lemma.explain_fixed(v);
-                    break;
-                }
-            }
+        if (zero_var != null_lpvar) {
+            new_lemma lemma(c(), "fixed-values");
+            lemma.explain_fixed(zero_var);
             lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0);
         }
         else {
+            rational k =  rational(1);        
             for (auto v : m) 
-                if (c().var_is_fixed(v)) 
+                if (v != non_fixed) {
+                    k *= c().lra.get_column_value(v).x;
+                    if (k.is_big()) return;
+                }
+ 
+            new_lemma lemma(c(), "fixed-values");
+ 
+            for (auto v : m) 
+                if (v != non_fixed) 
                     lemma.explain_fixed(v);
             
-            lpvar w = non_fixed_var(m);
-            if (w != null_lpvar) {
+            if (non_fixed != null_lpvar) {
                 lp::lar_term term;
                 term.add_var(m.var());
-                term.add_monomial(-k, w);
+                term.add_monomial(-k, non_fixed);
                 lemma += ineq(term, lp::lconstraint_kind::EQ, 0);
             } else {
                 lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k);
             }
         }
-        
     }
-    
-    bool monomial_bounds::is_linear(monic const& m) {
-        unsigned non_fixed = 0;
+    // returns true iff  (all variables are fixed,
+    // or all but one variable are fixed) and the bounds are not big,
+    // or at least one variable is fixed to zero.
+    bool monomial_bounds::is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed) {
+        zero_var = non_fixed = null_lpvar;
+        unsigned n_of_non_fixed = 0;
+        bool big_bound = false;
         for (lpvar v : m) {
-            if (!c().var_is_fixed(v))
-                ++non_fixed;
-            else if (c().val(v).is_zero())
+            if (!c().var_is_fixed(v)) {
+                n_of_non_fixed++;
+                non_fixed = v;
+            } else if (c().var_is_fixed_to_zero(v)) {
+                zero_var = v;
                 return true;
+            } else if (c().fixed_var_has_big_bound(v)) {
+                big_bound |= true;
+            }
         }
-        return non_fixed <= 1;
+        return n_of_non_fixed <= 1 && !big_bound;
     }
-    
-    
-    rational monomial_bounds::fixed_var_product(monic const& m) {
-        rational r(1);
-        for (lpvar v : m) {
-            if (c().var_is_fixed(v))
-                r *= c().lra.get_column_value(v).x;
-        }
-        return r;
-    }
-    
-    lpvar monomial_bounds::non_fixed_var(monic const& m) {
-        for (lpvar v : m) 
-            if (!c().var_is_fixed(v))
-                return v;
-        return null_lpvar;
-    }
-
 }
 

src/math/lp/monomial_bounds.h

@@ -33,10 +33,8 @@ namespace nla {
         // monomial propagation
         bool_vector m_propagated;
         void unit_propagate(monic const& m);
-        bool is_linear(monic const& m);
-        rational fixed_var_product(monic const& m);
-        lpvar non_fixed_var(monic const& m);
-
+        bool is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed);
+        
     public:
         monomial_bounds(core* core);
         void propagate();

src/math/lp/nla_core.cpp

@@ -40,7 +40,6 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim) : m_evars(),
                                                                     m_nra(s, m_nra_lim, *this) {
     m_nlsat_delay = lp_settings().nlsat_delay();
     lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
-    m_monics_with_changed_bounds.clear();
     for (const auto& m : m_emons) {
         if (columns_with_changed_bounds.contains(m.var())) {
             m_monics_with_changed_bounds.push_back(m.var());
@@ -553,6 +552,13 @@ bool core::var_is_fixed_to_zero(lpvar j) const {
         lra.column_is_fixed(j) &&
         lra.get_lower_bound(j) == lp::zero_of_type<lp::impq>();
 }
+
+bool core::fixed_var_has_big_bound(lpvar j) const {
+    SASSERT(lra.column_is_fixed(j));
+    const auto& b = lra.get_lower_bound(j);
+    return  b.x.is_big() || b.y.is_big();
+}
+
 bool core::var_is_fixed_to_val(lpvar j, const rational& v) const {
     return 
         lra.column_is_fixed(j) &&

src/math/lp/nla_core.h

@@ -120,7 +120,8 @@ class core {
 public:    
     // constructor
     core(lp::lar_solver& s, params_ref const& p, reslimit&);
-
+    const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; }
+    void reset_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
     
@@ -310,6 +311,7 @@ public:
     bool sign_contradiction(const monic& m) const;
 
     bool var_is_fixed_to_zero(lpvar j) const;
+    bool fixed_var_has_big_bound(lpvar j) const;
     bool var_is_fixed_to_val(lpvar j, const rational& v) const;
 
     bool var_is_fixed(lpvar j) const;

src/math/lp/nla_solver.h

@@ -26,7 +26,8 @@ namespace nla {
 
         solver(lp::lar_solver& s, params_ref const& p, reslimit& limit);
         ~solver();
-
+        const auto& monics_with_changed_bounds() const { return m_core->monics_with_changed_bounds(); }
+        void reset_monics_with_changed_bounds() { m_core->reset_monics_with_changed_bounds(); } 
         void add_monic(lpvar v, unsigned sz, lpvar const* vs);
         void add_idivision(lpvar q, lpvar x, lpvar y);
         void add_rdivision(lpvar q, lpvar x, lpvar y);

src/sat/smt/arith_solver.cpp

@@ -253,7 +253,7 @@ namespace arith {
                 first = false;
                 reset_evidence();
                 m_explanation.clear();
-                lp().explain_implied_bound(be, m_bp);
+                be.explain();                
             }
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
             updt_unassigned_bounds(v, -1);

src/smt/theory_lra.cpp

@@ -2150,7 +2150,7 @@ public:
         case l_true:
             propagate_basic_bounds();
             propagate_bounds_with_lp_solver();
-            propagate_nla();
+            propagate_bounds_with_nlp();
             break;
         case l_undef:
             UNREACHABLE();
@@ -2185,33 +2185,55 @@ public:
         set_evidence(j, m_core, m_eqs);
         m_explanation.add_pair(j, v);
     }
-    
-    void propagate_bounds_with_lp_solver() {
-        if (!should_propagate()) 
-            return;
-
-        m_bp.init();
-        lp().propagate_bounds_for_touched_rows(m_bp);
-
-        if (!m.inc()) 
-            return;
 
+    void finish_bound_propagation() {
         if (is_infeasible()) {
             get_infeasibility_explanation_and_set_conflict();
             // verbose_stream() << "unsat\n";
-        }
-        else {
-            unsigned count = 0, prop = 0;
-            for (auto& ib : m_bp.ibounds()) {
+        } else {
+            for (auto &ib : m_bp.ibounds()) {
                 m.inc();
                 if (ctx().inconsistent())
                     break;
-                ++prop;
-                count += propagate_lp_solver_bound(ib);
+                propagate_lp_solver_bound(ib);
             }
         }
     }
 
+    void propagate_bounds_with_lp_solver() {
+        if (!should_propagate()) 
+            return;
+        m_bp.init();
+        lp().propagate_bounds_for_touched_rows(m_bp);
+
+        if (m.inc()) 
+            finish_bound_propagation();
+    }
+    
+    void calculate_implied_bounds_for_monic(lpvar monic_var, const svector<lpvar>& vars) {
+        m_bp.propagate_monic(monic_var, vars);
+    }
+    
+    void propagate_bounds_for_touched_monomials() {
+        for (unsigned v : m_nla->monics_with_changed_bounds()) {
+            calculate_implied_bounds_for_monic(v, m_nla->get_core().emons()[v].vars());
+        }
+        m_nla->reset_monics_with_changed_bounds();
+    }
+
+    void propagate_bounds_with_nlp() {
+        if (!m_nla)
+            return;
+        if (is_infeasible() || !should_propagate())
+            return;
+
+        m_bp.init();
+        propagate_bounds_for_touched_monomials();
+
+        if (m.inc())
+            finish_bound_propagation();
+    }
+
     bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
         theory_var v = lp().local_to_external(vi);
         if (v == null_theory_var)