From caa929f01f4ba66f5fcacd4e83c5fe7c7bfe363f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 22 Sep 2023 14:27:26 -0700 Subject: [PATCH] do not use lemmase in monomial propagation --- src/math/lp/nla_core.cpp | 88 ++++++++++++++++++++++++++++++-------- src/math/lp/nla_core.h | 2 +- src/math/lp/nla_solver.cpp | 4 +- src/math/lp/nla_solver.h | 2 +- src/smt/theory_lra.cpp | 5 +-- 5 files changed, 75 insertions(+), 26 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 514b2ad61..916b80f6c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1920,22 +1920,76 @@ bool core::lower_bound_is_available(unsigned j) const void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k) { lp::impq bound_value; - new_lemma lemma(*this, "propagate monic with non fixed"); - // using += to not assert thath the inequality does not hold - lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0); - lp::explanation exp; - for (auto v : m_emons[monic_var].vars()) { - if (v == non_fixed) continue; - u_dependency* dep = lra.get_column_lower_bound_witness(v); - for (auto ci : lra.flatten(dep)) { - exp.push_back(ci); - } - dep = lra.get_column_upper_bound_witness(v); - for (auto ci : lra.flatten(dep)) { - exp.push_back(ci); - } + 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); } - lemma &= exp; } void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector& vars, const rational& k) @@ -1981,14 +2035,12 @@ void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector& } } - void core::init_bound_propagation(vector & 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 diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 456709771..54c7e1df1 100644 --- a/src/math/lp/nla_core.h +++ b/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&); + void init_bound_propagation(); }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 08c1e1e62..3475a3509 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -100,8 +100,8 @@ namespace nla { m_core->check_bounded_divisions(lemmas); } - void solver::init_bound_propagation(vector& lemmas) { - m_core->init_bound_propagation(lemmas); + void solver::init_bound_propagation() { + m_core->init_bound_propagation(); } } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index fa206ea40..a4de90320 100644 --- a/src/math/lp/nla_solver.h +++ b/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&); + void init_bound_propagation(); }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ea1dcd9b9..ef7ab7091 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2199,14 +2199,11 @@ 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); } m_nla->reset_monics_with_changed_bounds(); - for (const auto & l:m_nla_lemma_vector) { - false_case_of_check_nla(l); - } } void propagate_bounds_with_nlp() {