From f30a2c13be7384eda00ecc3e336bcf9a21f0fa8f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 28 Sep 2023 17:24:34 -0700 Subject: [PATCH] propagate only one non-fixed monomial intrernally lar_solver --- src/math/lp/monomial_bounds.cpp | 20 +++++++++ src/math/lp/monomial_bounds.h | 4 +- src/math/lp/nla_core.cpp | 80 +-------------------------------- src/math/lp/nla_core.h | 1 - 4 files changed, 23 insertions(+), 82 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 7d2dc5ce6..981677ab0 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/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& vars, lpvar non_fixed, const rational& k) { + vector> 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& 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), diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index 15477e19a..76524012f 100644 --- a/src/math/lp/monomial_bounds.h +++ b/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& 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& vars, lpvar non_fixed, const rational& k); }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 97c9c82d9..f574f20ad 100644 --- a/src/math/lp/nla_core.cpp +++ b/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& 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& 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); } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d5feac8a2..ef7863817 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -435,7 +435,6 @@ public: bool is_linear(const svector& 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& vars, lpvar non_fixed, const rational& k); void propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k); void propagate_monic_with_all_fixed(lpvar monic_var, const svector& vars, const rational& k); void add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function explain_dep);