From b9f74db14c186d56025deb62225ecc22bfa8dd0d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 26 Dec 2019 17:24:31 -0800 Subject: [PATCH] hook up pdd_grobner Signed-off-by: Lev Nachmanson --- src/math/dd/pdd_interval.h | 2 +- src/math/interval/dep_intervals.h | 7 ++-- src/math/lp/nla_core.cpp | 70 +++++++++++++++++++++++++++++-- src/math/lp/nla_core.h | 6 ++- src/math/lp/nla_grobner.h | 2 +- src/math/lp/nla_intervals.h | 1 + 6 files changed, 79 insertions(+), 9 deletions(-) diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index fcae2e5da..9645c7314 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -43,7 +43,7 @@ public: m_dep_intervals.set_interval_for_scalar(k, p.val()); return k; } - bool deps = (wd == w_dep::with_deps); + bool deps = wd == w_dep::with_deps; interval a = m_var2interval(p.var(), deps); interval hi = get_interval(p.hi()); interval la = get_interval(p.lo()); diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index fd82b4dc7..34bcad9e8 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -255,12 +255,13 @@ public: inline bool separated_from_zero(const interval& i) const { return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i); } + // if the separation happens then call f() template - bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*& dep, std::function f) { + bool check_interval_for_conflict_on_zero(const interval& i, u_dependency* dep, std::function f) { return check_interval_for_conflict_on_zero_lower(i, dep, f) || check_interval_for_conflict_on_zero_upper(i, dep, f); } template - bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*& dep, std::function f) { + bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency* dep, std::function f) { if (!separated_from_zero_on_lower(i)) { return false; } @@ -272,7 +273,7 @@ public: return true; } template - bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*& dep, std::function f) { + bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency* dep, std::function f) { if (!separated_from_zero_on_upper(i)) return false; TRACE("dep_intervals", display(tout, i);); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 90be43350..f15af30c0 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -21,6 +21,7 @@ Revision History: #include "math/lp/factorization_factory_imp.h" #include "math/lp/nex.h" #include "math/grobner/pdd_grobner.h" +#include "math/dd/pdd_interval.h" namespace nla { core::core(lp::lar_solver& s, reslimit & lim) : @@ -33,7 +34,7 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_intervals(this, lim), m_horner(this, &m_intervals), m_nex_grobner(this, &m_intervals), - m_pdd_manager(0), + m_pdd_manager(s.number_of_vars()), m_pdd_grobner(lim, m_pdd_manager), m_emons(m_evars), m_reslim(lim) @@ -1410,8 +1411,15 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const out); } +void core::create_vars_used_in_mrows() { + for (unsigned i : m_rows) { + add_row_vars_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]); + } +} + void core::run_pdd_grobner() { m_pdd_manager.resize(m_lar_solver.number_of_vars()); + create_vars_used_in_mrows(); for (unsigned i : m_rows) { add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]); } @@ -1422,7 +1430,24 @@ void core::run_pdd_grobner() { } void core::check_pdd_eq(const dd::grobner::equation* e) { - NOT_IMPLEMENTED_YET(); + dd::pdd_interval eval(m_pdd_manager, m_reslim); + eval.var2interval() = + [this](lpvar j, bool deps) { + intervals::interval a; + if (deps) m_intervals.set_var_interval(j, a); + else m_intervals.set_var_interval(j, a); + return a; + }; + auto i = eval.get_interval(e->poly()); + dep_intervals di(m_reslim); + if (!di.separated_from_zero(i)) + return; + auto i_wd = eval.get_interval(e->poly()); + std::function f = [this](const lp::explanation& e) { + add_empty_lemma(); + current_expl().add(e); + }; + di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f); } void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector & q) { @@ -1454,8 +1479,47 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector> & row) { + for (const auto &p : row) { + lpvar j = p.var(); + if (!is_monic_var(j)) { + m_pdd_manager.mk_var(j); + } else { + const monic& m = emons()[j]; + for (lpvar k : m.vars()) { + m_pdd_manager.mk_var(k); + } + } + } +} + +dd::pdd core::pdd_expr(const rational& c, lpvar j) { + if (!is_monic_var(j)) + return c * m_pdd_manager.mk_var(j); + + // j is a monic var + dd::pdd r = m_pdd_manager.mk_val(c); + const monic& m = emons()[j]; + for (lpvar k : m.vars()) { + r *= m_pdd_manager.mk_var(k); + } + return r; +} + void core::add_row_to_pdd_grobner(const vector> & row) { - NOT_IMPLEMENTED_YET(); + u_dependency *dep = nullptr; + dd::pdd sum = m_pdd_manager.mk_val(rational(0)); + for (const auto &p : row) { + dd::pdd e = pdd_expr(p.coeff(), p.var()); + sum += e; + unsigned lc, uc; + m_lar_solver.get_bound_constraint_witnesses_for_column(p.var(), lc, uc); + if (lc != null_lpvar) + dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc)); + if (uc != null_lpvar) + dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc)); + } + m_pdd_grobner.add(sum, dep); } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index bfb26742b..d8a21b203 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -50,6 +50,7 @@ typedef lp::lconstraint_kind llc; typedef lp::constraint_index lpci; typedef lp::explanation expl_set; typedef lp::var_index lpvar; +const lpvar null_lpvar = UINT_MAX; inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); } inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); } @@ -122,7 +123,7 @@ public: m_active_var_set.resize(m_lar_solver.number_of_vars()); } - reslimit & reslim() { return m_reslim; } + reslimit& reslim() { return m_reslim; } emonics& emons() { return m_emons; } const emonics& emons() const { return m_emons; } // constructor @@ -401,6 +402,9 @@ public: var_weight get_var_weight(lpvar) const; void add_row_to_pdd_grobner(const vector> & row); void check_pdd_eq(const dd::grobner::equation*); + void create_vars_used_in_mrows(); + void add_row_vars_to_pdd_grobner(const vector> & row); + dd::pdd pdd_expr(const rational& c, lpvar j); }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index e319ae941..a9d1d8a2a 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -119,7 +119,7 @@ private: equation_set m_to_superpose; equation_set m_to_simplify; region m_alloc; - mutable u_dependency_manager m_dep_manager; + mutable u_dependency_manager m_dep_manager; nex_lt m_lt; bool m_changed_leading_term; params m_params; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 5141924e0..8d57d1f21 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -46,6 +46,7 @@ public: m_dep_intervals(lim), m_core(c) {} + dep_intervals& get_dep_intervals() { return m_dep_intervals; } u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_intervals.mk_join(a, b); } u_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_intervals.mk_leaf(ci); }