diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 01fe42dff..6a01d4ace 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -162,12 +162,12 @@ private: void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function explain_dep) { TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;); j = lp().column_to_reported_index(j); - auto *e = m_improved_lower_bounds.find_core(j); - if (!e) { + unsigned k; + if (!m_improved_lower_bounds.find(j, k)) { m_improved_lower_bounds.insert(j,static_cast(m_ibounds.size())); m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep)); } else { - auto& found_bound = m_ibounds[e->get_data().m_value]; + 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, j, true, is_strict, explain_dep); TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); @@ -177,12 +177,12 @@ private: void add_upper_bound_monic(lpvar j, const mpq& bound_val, bool is_strict, std::function explain_bound) { j = lp().column_to_reported_index(j); - auto *e = m_improved_upper_bounds.find_core(j); - if (!e) { + unsigned k; + if (!m_improved_upper_bounds.find(j, k)) { m_improved_upper_bounds.insert(j, static_cast(m_ibounds.size())); m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound)); } else { - auto& found_bound = m_ibounds[e->get_data().m_value]; + 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, j, false, is_strict, explain_bound); TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); @@ -336,9 +336,9 @@ private: if (!m_imp.bound_is_interesting(j, kind, v)) return; if (is_low) { - auto *e = m_improved_lower_bounds.find_core(j); - if (e) { - auto& found_bound = m_ibounds[e->get_data().m_value]; + unsigned k; + if (m_improved_lower_bounds.find(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.m_bound = v; found_bound.m_strict = strict; @@ -351,9 +351,9 @@ private: TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout);); } } else { // the upper bound case - auto *e = m_improved_upper_bounds.find_core(j); - if (e) { - auto& found_bound = m_ibounds[e->get_data().m_value]; + unsigned k; + if (m_improved_upper_bounds.find(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.m_bound = v; found_bound.m_strict = strict; @@ -591,12 +591,12 @@ private: lp_assert(y_sign == 1 || y_sign == -1); auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg; const auto& v = val(x); - auto * e = table.find_core(v); - if (!e) { + unsigned found_i;; + + if (!table.find(v, found_i)) { table.insert(v, i); } else { explanation ex; - unsigned found_i = e->get_data().m_value; unsigned base_of_found = lp().get_base_column_in_row(found_i); if (is_int(x) != is_int(base_of_found) || ival(x).y != ival(base_of_found).y) continue; diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index ad2b20c07..7d2dc5ce6 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -24,7 +24,6 @@ namespace nla { } } - bool monomial_bounds::is_too_big(mpq const& q) const { return rational(q).bitsize() > 256; } @@ -258,53 +257,6 @@ 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) { - m_propagated.reserve(m.var() + 1, false); - if (m_propagated[m.var()]) - return; - - 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())); - - - 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 (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); - - if (non_fixed != null_lpvar) { - lp::lar_term term; - term.add_var(m.var()); - term.add_monomial(-k, non_fixed); - lemma += ineq(term, lp::lconstraint_kind::EQ, 0); - } else { - lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k); - } - } - } // 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. diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index 15ab6b992..6253af744 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -20,7 +20,6 @@ namespace nla { void var2interval(lpvar v, scoped_dep_interval& i); bool is_too_big(mpq const& q) const; - bool propagate_down(monic const& m, lpvar u); bool propagate_value(dep_interval& range, lpvar v); bool propagate_value(dep_interval& range, lpvar v, unsigned power); void compute_product(unsigned start, monic const& m, scoped_dep_interval& i); @@ -32,12 +31,11 @@ namespace nla { // monomial propagation bool_vector m_propagated; - void unit_propagate(monic const& m); bool is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed); public: monomial_bounds(core* core); void propagate(); - void unit_propagate(); + }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 20003f947..63dd29d9b 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1836,17 +1836,6 @@ bool core::improve_bounds() { } return bounds_improved; } - -void core::propagate(vector& lemmas) { - // propagate linear monomials, those that have all, or all but one, variables fixed - lemmas.reset(); - m_lemma_vec = &lemmas; - - m_monomial_bounds.unit_propagate(); - -} - - } // end of nla diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index b7197ff2f..8be918f01 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -46,10 +46,6 @@ namespace nla { return m_core->check(lits, lemmas); } - void solver::propagate(vector& lemmas) { - m_core->propagate(lemmas); - } - void solver::push(){ m_core->push(); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1a022e087..fa73788e6 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2159,20 +2159,6 @@ public: return true; } - void propagate_nla() { - if (!m_nla) - return; - m_nla->propagate(m_nla_lemma_vector); - if (lp().get_status() == lp::lp_status::INFEASIBLE) { - TRACE("arith", tout << "propagation conflict\n";); - get_infeasibility_explanation_and_set_conflict(); - } - else { - for (nla::lemma const& l : m_nla_lemma_vector) - false_case_of_check_nla(l); - } - } - bool should_propagate() const { return bound_prop_mode::BP_NONE != propagation_mode(); }