propagate only one non-fixed monomial intrernally

lar_solver

src/math/lp/monomial_bounds.cpp

@@ -12,6 +12,26 @@
 #include "math/lp/nla_intervals.h"
 
 namespace nla {
+    // here non_fixed is the only non-fixed variable in the monomial, 
+    // vars is the vector of the monomial variables, 
+    // k is the product of all fixed variables in vars 
+    void monomial_bounds::propagate_nonfixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
+        vector<std::pair<lp::mpq, unsigned>> coeffs;        
+        coeffs.push_back(std::make_pair(-k, non_fixed));
+        coeffs.push_back(std::make_pair(rational::one(), monic_var));
+        lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
+        auto* dep = explain_fixed(vars, non_fixed);
+        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, mpq(0), dep);
+    }
+
+    u_dependency* monomial_bounds::explain_fixed(const svector<lpvar>& vars, lpvar non_fixed) {
+        u_dependency* dep = nullptr;
+        for (auto v : vars)
+            if (v != non_fixed)
+                dep = c().lra.join_deps(dep, c().lra.get_bound_constraint_witnesses_for_column(v));
+        return dep;
+    }
 
     monomial_bounds::monomial_bounds(core* c):
         common(c), 

src/math/lp/monomial_bounds.h

@@ -17,7 +17,7 @@ namespace nla {
     class monomial_bounds : common {
         dep_intervals& dep;
 
-
+        u_dependency* explain_fixed(const svector<lpvar>& vars, lpvar non_fixed);
         void var2interval(lpvar v, scoped_dep_interval& i);
         bool is_too_big(mpq const& q) const;
         bool propagate_value(dep_interval& range, lpvar v);
@@ -35,6 +35,6 @@ namespace nla {
     public:
         monomial_bounds(core* core);
         void propagate();
-        
+        void propagate_nonfixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);    
     }; 
 }

src/math/lp/nla_core.cpp

@@ -1912,84 +1912,6 @@ 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) {
-        if (params().arith_nl_use_lemmas_in_unit_prop()) {
-            propagate_monic_non_fixed_with_lemma(monic_var, vars, non_fixed, k);
-            return;
-        }
-        lp::impq bound_value;
-        bool is_strict;
-        auto& lps = lra;
-        
-        if (lower_bound_is_available(non_fixed)) {
-            bound_value = lra.column_lower_bound(non_fixed);
-            is_strict = !bound_value.y.is_zero();
-            auto lambda = [vars, non_fixed, &lps]() {
-                u_dependency* dep = lps.get_column_lower_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_pos())
-                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;
         auto lambda = [vars, lps]() { return lps->get_bound_constraint_witnesses_for_columns(vars); };
@@ -2049,7 +1971,7 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
                 }
 
             if (non_fixed != null_lpvar)
-                propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
+                m_monomial_bounds.propagate_nonfixed(monic_var, vars, non_fixed, k);
             else  // all variables are fixed
                 propagate_monic_with_all_fixed(monic_var, vars, k);
         }

src/math/lp/nla_core.h

@@ -435,7 +435,6 @@ public:
 
     bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed);
     void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var);
-    void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);
     void propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);
     void propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k);
     void add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);