indentation

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

src/math/lp/nla_core.cpp

@@ -1913,26 +1913,81 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
         }
     }
 
-    void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
+void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
-        lp::impq bound_value;
+{
-        new_lemma lemma(*this, "propagate monic with non fixed");
+    lp::impq bound_value;
-        // using += to not assert thath the inequality does not hold
+    bool is_strict;
-        lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
+    auto& lps = lra;
-        lp::explanation exp;
+
-        for (auto v : m_emons[monic_var].vars()) {
+    if (lower_bound_is_available(non_fixed)) {
-            if (v == non_fixed) continue;
+        bound_value = lra.column_lower_bound(non_fixed);
-            u_dependency* dep = lra.get_column_lower_bound_witness(v);
+        is_strict = !bound_value.y.is_zero();
-            for (auto ci : lra.flatten(dep)) {
+        auto lambda = [vars, non_fixed, &lps]() {
-                exp.push_back(ci);
+            u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
-            }
+            for (auto v : vars)
-            dep = lra.get_column_upper_bound_witness(v);
+                if (v != non_fixed)
-            for (auto ci : lra.flatten(dep)) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-                exp.push_back(ci);
+            return dep;
-            }
+        };
-        }
+        if (k.is_pos())
-        lemma &= exp;
+            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        else
+            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
     }
 
+    if (upper_bound_is_available(non_fixed)) {
+        bound_value = lra.column_upper_bound(non_fixed);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
+            for (auto v : vars)
+                if (v != non_fixed)
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+            return dep;
+        };
+        if (k.is_neg())
+            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        else
+            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+    }
+
+    if (lower_bound_is_available(monic_var)) {
+        auto lambda = [vars, monic_var, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
+            for (auto v : vars) {
+                if (v != non_fixed) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                }
+            }
+            return dep;
+        };
+        bound_value = lra.column_lower_bound(monic_var);
+        is_strict = !bound_value.y.is_zero();
+        if (k.is_pos())
+            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        else
+            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+    }
+
+    if (upper_bound_is_available(monic_var)) {
+        bound_value = lra.column_upper_bound(monic_var);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, monic_var, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
+            for (auto v : vars) {
+                if (v != non_fixed) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                }
+            }
+            return dep;
+        };
+        if (k.is_neg())
+            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        else
+            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+    }
+}
+
     void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
     {
         auto* lps = &lra;
@@ -1976,14 +2031,12 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
         }
     }
 
-    void core::init_bound_propagation(vector<lemma> & l_vec)
+    void core::init_bound_propagation()
     {
         m_implied_bounds.clear();
         m_improved_lower_bounds.reset();
         m_improved_upper_bounds.reset();
         m_column_types = &lra.get_column_types();
-        m_lemma_vec = &l_vec;
-        m_lemma_vec->clear();
     }
 
 }  // namespace nla

src/math/lp/nla_core.h

@@ -451,7 +451,7 @@ private:
     void save_tableau();
     bool integrality_holds();
     void calculate_implied_bounds_for_monic(lp::lpvar v);
-    void init_bound_propagation(vector<lemma>&);    
+    void init_bound_propagation();    
 };  // end of core
 
 struct pp_mon {

src/math/lp/nla_solver.cpp

@@ -100,8 +100,8 @@ namespace nla {
         m_core->check_bounded_divisions(lemmas);
     }
 
-    void solver::init_bound_propagation(vector<lemma>& lemmas) {
+    void solver::init_bound_propagation() {
-        m_core->init_bound_propagation(lemmas);
+        m_core->init_bound_propagation();
     }
 
 }

src/math/lp/nla_solver.h

@@ -49,6 +49,6 @@ namespace nla {
         nlsat::anum const& am_value(lp::var_index v) const;
         void collect_statistics(::statistics & st);
         void calculate_implied_bounds_for_monic(lp::lpvar v);
-        void init_bound_propagation(vector<lemma>&);
+        void init_bound_propagation();
     };
 }

src/smt/theory_lra.cpp

@@ -2205,7 +2205,7 @@ public:
     }
     
     void propagate_bounds_for_touched_monomials() {
-        m_nla->init_bound_propagation(m_nla_lemma_vector);
+        m_nla->init_bound_propagation();
         for (unsigned v : m_nla->monics_with_changed_bounds()) 
             m_nla->calculate_implied_bounds_for_monic(v);
         
@@ -3891,7 +3891,6 @@ public:
                 IF_VERBOSE(1, verbose_stream() << enode_pp(n, ctx()) << " evaluates to " << r2 << " but arith solver has " << r1 << "\n"); 
         }
     }
-
 };
     
 theory_lra::theory_lra(context& ctx):