From 4a9b38e531e86f3b92435f064ae7bea678c8486d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 17:08:17 -0800 Subject: [PATCH] clean up nla_grobner --- src/math/lp/nla_grobner.cpp | 89 ++++--------------------------------- src/math/lp/nla_grobner.h | 6 --- 2 files changed, 9 insertions(+), 86 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index baf27a5bb..f9974b41c 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -59,21 +59,20 @@ namespace nla { if (m_delay_base > 0) --m_delay_base; - if (is_conflicting()) - return; - try { - if (propagate_bounds()) + + if (is_conflicting()) return; if (propagate_eqs()) return; - + if (propagate_factorization()) return; - + if (propagate_linear_equations()) return; + } catch (...) { @@ -111,17 +110,9 @@ namespace nla { return false; } - bool grobner::propagate_bounds() { - unsigned changed = 0; - for (auto eq : m_solver.equations()) - if (propagate_bounds(*eq) && ++changed >= m_solver.number_of_conflicts_to_report()) - return true; - return changed > 0; - } - bool grobner::propagate_eqs() { unsigned changed = 0; - for (auto eq : m_solver.equations()) + for (auto eq : m_solver.equations()) if (propagate_fixed(*eq) && ++changed >= m_solver.number_of_conflicts_to_report()) return true; return changed > 0; @@ -129,7 +120,7 @@ namespace nla { bool grobner::propagate_factorization() { unsigned changed = 0; - for (auto eq : m_solver.equations()) + for (auto eq : m_solver.equations()) if (propagate_factorization(*eq) && ++changed >= m_solver.number_of_conflicts_to_report()) return true; return changed > 0; @@ -165,19 +156,12 @@ namespace nla { rational d = lcm(denominator(a), denominator(b)); a *= d; b *= d; -#if 0 - c().lra.update_column_type_and_bound(v, lp::lconstraint_kind::EQ, b/a, eq.dep()); - lp::explanation exp; - explain(eq, exp); - c().add_fixed_equality(c().lra.column_to_reported_index(v), b/a, exp); -#else ineq new_eq(term(a, v), llc::EQ, b); if (c().ineq_holds(new_eq)) return false; new_lemma lemma(c(), "pdd-eq"); add_dependencies(lemma, eq); lemma |= new_eq; -#endif return true; } @@ -377,73 +361,18 @@ namespace nla { } } - bool grobner::propagate_bounds(const dd::solver::equation& e) { - return false; - // TODO - auto& di = c().m_intervals.get_dep_intervals(); - dd::pdd_interval eval(di); - eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) { - if (deps) c().m_intervals.set_var_interval(j, a); - else c().m_intervals.set_var_interval(j, a); - }; - scoped_dep_interval i(di), i_wd(di); - eval.get_interval(e.poly(), i); - return false; - } - bool grobner::propagate_linear_equations() { unsigned changed = 0; m_mon2var.clear(); for (auto const& m : c().emons()) m_mon2var[m.vars()] = m.var(); + for (auto eq : m_solver.equations()) if (propagate_linear_equations(*eq)) ++changed; -#if 0 - for (auto eq : m_solver.equations()) - if (check_missed_bound(*eq)) - return true; -#endif return changed > 0; } - - bool grobner::check_missed_bound(dd::solver::equation const& e) { - auto& di = c().m_intervals.get_dep_intervals(); - auto set_var_interval = [&](lpvar j, scoped_dep_interval& a) { - c().m_intervals.set_var_interval(j, a); - }; - scoped_dep_interval i(di), t(di), s(di), u(di); - di.set_value(i, rational::zero()); - - for (auto const& [coeff, vars] : e.poly()) { - if (vars.empty()) - di.add(coeff, i); - else { - di.set_value(t, coeff); - for (auto v : vars) { - set_var_interval(v, s); - di.mul(t, s, t); - } - if (m_mon2var.find(vars) != m_mon2var.end()) { - auto v = m_mon2var.find(vars)->second; - set_var_interval(v, u); - di.mul(coeff, u, u); - di.intersect(t, u, t); - } - di.add(i, t, i); - } - } - if (!di.separated_from_zero(i)) - return false; -// m_solver.display(verbose_stream() << "missed bound\n", e); -// exit(1); - std::function f = [this](const lp::explanation& e) { - new_lemma lemma(m_core, "pdd"); - lemma &= e; - }; - return di.check_interval_for_conflict_on_zero(i, e.dep(), f); - } - + bool grobner::propagate_linear_equations(dd::solver::equation const& e) { if (equation_is_true(e)) return false; diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index e70b5473d..be5f06136 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -35,20 +35,14 @@ namespace nla { bool is_conflicting(); bool is_conflicting(dd::solver::equation const& eq); - bool propagate_bounds(); - bool propagate_bounds(dd::solver::equation const& eq); - bool propagate_eqs(); bool propagate_fixed(dd::solver::equation const& eq); bool propagate_factorization(); bool propagate_factorization(dd::solver::equation const& eq); - bool propagate_linear_equations(); bool propagate_linear_equations(dd::solver::equation const& eq); - - bool check_missed_bound(dd::solver::equation const& eq); void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq); void explain(dd::solver::equation const& eq, lp::explanation& exp);