From 44d2f6da6c3bc0ddf37abeda4d486ad1618d7ad7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Mar 2020 01:12:04 -0700 Subject: [PATCH] fix #3261 Signed-off-by: Nikolaj Bjorner --- src/math/lp/emonics.cpp | 246 +++++++++++++++++++++------- src/math/lp/emonics.h | 35 ++-- src/math/lp/monic.h | 32 ++-- src/math/lp/nla_basics_lemmas.cpp | 2 +- src/math/lp/nla_core.cpp | 11 +- src/math/lp/nla_core.h | 2 +- src/math/lp/nla_monotone_lemmas.cpp | 2 +- src/math/lp/nra_solver.cpp | 2 +- 8 files changed, 232 insertions(+), 100 deletions(-) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index 450e98c98..8b5e28c8b 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -15,9 +15,9 @@ Revision History: - to replace rooted_mons.h and rooted_mon, rooted_mon_tabled + replaced rooted_mons.h and rooted_mon, rooted_mon_tabled - --*/ +--*/ #include "math/lp/emonics.h" #include "math/lp/nla_defs.h" @@ -30,42 +30,60 @@ void emonics::inc_visited() const { ++m_visited; if (m_visited == 0) { for (auto& svt : m_monics) { - svt.visited() = 0; + svt.set_visited(0); } ++m_visited; } } void emonics::push() { + TRACE("nla_solver_mons", display(tout << "push\n");); + SASSERT(invariant()); m_u_f_stack.push_scope(); m_lim.push_back(m_monics.size()); m_region.push_scope(); m_ve.push(); SASSERT(monics_are_canonized()); - SASSERT(consistent()); + SASSERT(invariant()); } +// +// this assumes that all calls to m_ve.merge are after emonics::add within +// the same scope. Suppose that m_ve.merge is used before an emonics:add in the same scope +// then the unmerge on the variable applies to the monic during pop, which it shouldn't. +// To fix this, the undo-stack for m_ve and monics addition have to be coordinated +// this could be achieved in some ways, such as pushing a scope on m_ve whenever a monic is added. +// Before fixing this it is worth adding a unit test to exercise this scenario. +// The scenario is difficult to trigger from the normal solving context because emonics::add +// is triggered by internalization, which typically happens before search (except for quantifier instantiation). +// void emonics::pop(unsigned n) { - m_ve.pop(n); - unsigned old_sz = m_lim[m_lim.size() - n]; - for (unsigned i = m_monics.size(); i-- > old_sz; ) { - monic & m = m_monics[i]; - remove_cg_mon(m); - m_var2index[m.var()] = UINT_MAX; - lpvar last_var = UINT_MAX; - for (lpvar v : m.vars()) { - if (v != last_var) { - remove_cell(m_use_lists[v]); - last_var = v; + TRACE("nla_solver_mons", tout << "pop: " << n << "\n";); + SASSERT(invariant()); + for (unsigned j = 0; j < n; ++j) { + m_ve.pop(1); + unsigned old_sz = m_lim[m_lim.size() - 1]; + for (unsigned i = m_monics.size(); i-- > old_sz; ) { + monic & m = m_monics[i]; + TRACE("nla_solver_mons", display(tout << m << "\n");); + remove_cg_mon(m); + m_var2index[m.var()] = UINT_MAX; + lpvar last_var = UINT_MAX; + for (lpvar v : m.vars()) { + if (v != last_var) { + TRACE("nla_solver_mons", tout << "remove cell " << v << ": " << i << " " << m_use_lists[v].m_head->m_index << "\n";); + remove_cell(m_use_lists[v]); + last_var = v; + } } } + m_monics.shrink(old_sz); + m_region.pop_scope(1); + m_lim.pop_back(); + m_u_f_stack.pop_scope(1); + SASSERT(invariant()); + SASSERT(monics_are_canonized()); } - m_monics.shrink(old_sz); - m_region.pop_scope(n); - m_lim.shrink(m_lim.size() - n); - SASSERT(consistent()); - SASSERT(monics_are_canonized()); - m_u_f_stack.pop_scope(n); } void emonics::remove_cell(head_tail& v) { @@ -118,6 +136,11 @@ void emonics::unmerge_cells(head_tail& root, head_tail& other) { cell*& root_tail = root.m_tail; cell* other_head = other.m_head; cell* other_tail = other.m_tail; + + TRACE("nla_solver_mons", + display(tout << "other: ", other_head) << "\n"; + display(tout << "root: ", root_head) << "\n"; ); + if (other_head == nullptr) { // no-op } @@ -130,6 +153,9 @@ void emonics::unmerge_cells(head_tail& root, head_tail& other) { root_tail->m_next = root_head; other_tail->m_next = other_head; } + TRACE("nla_solver_mons", + display(tout << "other: ", other_head) << "\n"; + display(tout << "root: ", root_head) << "\n"; ); } emonics::cell* emonics::head(lpvar v) const { @@ -151,6 +177,8 @@ monic const* emonics::find_canonical(svector const& vars) const { } void emonics::remove_cg(lpvar v) { + TRACE("nla_solver_mons", tout << "remove: " << v << "\n";); + TRACE("nla_solver_mons", display(tout);); cell* c = m_use_lists[v].m_head; if (c == nullptr) { return; @@ -172,7 +200,7 @@ void emonics::remove_cg(lpvar v) { void emonics::remove_cg_mon(const monic& m) { lpvar u = m.var(), w; // equivalence class of u: - if (m_cg_table.find(u, w)) { + if (m_cg_table.find(u, w) && u == w) { TRACE("nla_solver_mons", tout << "erase << " << m << "\n";); m_cg_table.erase(u); } @@ -204,6 +232,7 @@ void emonics::insert_cg(lpvar v) { } } while (c != first); + TRACE("nla_solver_mons", display(tout << "insert: " << v << "\n");); } bool emonics::elists_are_consistent(std::unordered_map, hash_svector>& lists) const { @@ -237,7 +266,9 @@ bool emonics::elists_are_consistent(std::unordered_mapsecond) { tout << (*this)[j] << "\n"; } - }); + } + display(tout); + ); SASSERT(c == it->second); } return true; @@ -247,6 +278,7 @@ bool emonics::elists_are_consistent(std::unordered_map " << r1 << "\n";); if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged + TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";); unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); rehash_cg(r1.var()); } @@ -398,7 +444,9 @@ std::ostream& emonics::display(const core& cr, std::ostream& out) const { for (auto const& m : m_monics) { out << "m" << (idx++) << ": " << pp_mon_with_vars(cr, m) << "\n"; } - return display_use(out); + display_use(out); + //display_uf(out); + return out; } std::ostream& emonics::display(std::ostream& out) const { @@ -407,26 +455,112 @@ std::ostream& emonics::display(std::ostream& out) const { for (auto const& m : m_monics) { out << "m" << (idx++) << ": " << m << "\n"; } - return display_use(out); + display_use(out); + //display_uf(out); + return out; } - std::ostream& emonics::display_use(std::ostream& out) const { - out << "use lists\n"; - unsigned idx = 0; - for (auto const& ht : m_use_lists) { - cell* c = ht.m_head; - if (c) { - out << idx << ": "; - do { - out << "m" << c->m_index << " "; - c = c->m_next; - } - while (c != ht.m_head); - out << "\n"; - } - ++idx; +std::ostream& emonics::display_use(std::ostream& out) const { + out << "use lists\n"; + unsigned v = 0; + for (auto const& ht : m_use_lists) { + cell* c = ht.m_head; + if (c) { + out << v << ": "; + do { + out << "m" << c->m_index << " "; + c = c->m_next; + } + while (c != ht.m_head); + out << "\n"; + } + ++v; } - return out; - } + return out; +} + +std::ostream& emonics::display_uf(std::ostream& out) const { + m_u_f.display(out << "uf\n"); + m_ve.display(out << "ve\n"); + return out; +} + +std::ostream& emonics::display(std::ostream& out, cell* c) const { + cell* c0 = c; + if (c) { + do { + out << c->m_index << " "; + c = c->m_next; + } + while (c != c0); + } + return out; +} + + +bool emonics::invariant() const { + // the varible index contains exactly the active monomials + unsigned mons = 0; + for (lpvar v = 0; v < m_var2index.size(); v++) { + if (is_monic_var(v)) { + mons++; + } + } + if (m_monics.size() != mons) + return false; + + // check that every monomial in the + // use list of v contains v. + unsigned v = 0; + for (auto const& ht : m_use_lists) { + cell* c = ht.m_head; + if (c) { + auto v1 = m_ve.find(v); + do { + auto const& m = m_monics[c->m_index]; + bool found = false; + for (lp::var_index w : m.vars()) { + auto w1 = m_ve.find(w); + found |= v1 == w1; + } + CTRACE("nla_solver_mons", !found, tout << v << ": " << m << "\n";); + SASSERT(found); + c = c->m_next; + } + while (c != ht.m_head); + } + v++; + } + + // all monomials are in congruence table. + // the variables of each monomial contain the monomial in their use-list + std::function find_index = [&,this](lpvar v, unsigned idx) { + cell* c = m_use_lists[v].m_head; + cell* c0 = c; + bool found = false; + do { + found |= c->m_index == idx; + c = c->m_next; + } + while (c != c0 && !found); + CTRACE("nla_solver_mons", !found, tout << "m" << idx << " not found in use list for v" << v << "\n";); + return found; + }; + unsigned idx = 0; + for (auto const& m : m_monics) { + SASSERT(m_cg_table.contains(m.var())); + for (auto v : m.vars()) { + if (!find_index(v, idx)) + return false; + } + // same with rooted variables + for (auto v : m.rvars()) { + if (!find_index(v, idx)) + return false; + } + idx++; + } + return true; +} } diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index 4931c90e6..5b12f24b2 100644 --- a/src/math/lp/emonics.h +++ b/src/math/lp/emonics.h @@ -82,16 +82,17 @@ class emonics { union_find m_u_f; trail_stack m_u_f_stack; - mutable svector m_find_key; // the key used when looking for a monic with the specific variables + mutable svector m_find_key; // the key used when looking for a monic with the specific variables var_eqs& m_ve; - mutable vector m_monics; // set of monics - mutable unsigned_vector m_var2index; // var_mIndex -> mIndex - unsigned_vector m_lim; // backtracking point - mutable unsigned m_visited; // timestamp of visited monics during pf_iterator - region m_region; // region for allocating linked lists - mutable svector m_use_lists; // use list of monics where variables occur. - hash_canonical m_cg_hash; - eq_canonical m_cg_eq; + mutable vector m_monics; // set of monics + mutable unsigned_vector m_var2index; // var_mIndex -> mIndex + unsigned_vector m_lim; // backtracking point + mutable unsigned m_visited; // timestamp of visited monics during pf_iterator + region m_region; // region for allocating linked lists + mutable svector m_use_lists; // use list of monics where variables occur. + hash_canonical m_cg_hash; + eq_canonical m_cg_eq; + unsigned_vector m_vs; // temporary buffer of canonized variables hashtable m_cg_table; // congruence (canonical) table. @@ -112,6 +113,8 @@ class emonics { void set_visited(monic& m) const; bool is_visited(monic const& m) const; std::ostream& display_use(std::ostream& out) const; + std::ostream& display_uf(std::ostream& out) const; + std::ostream& display(std::ostream& out, cell* c) const; public: unsigned number_of_monics() const { return m_monics.size(); } /** @@ -237,8 +240,8 @@ public: class products_of { emonics const& m; - monic * mon; - lpvar m_var; + monic * mon; + lpvar m_var; public: products_of(emonics const& m, monic & mon): m(m), mon(&mon), m_var(UINT_MAX) {} products_of(emonics const& m, lpvar v): m(m), mon(nullptr), m_var(v) {} @@ -328,15 +331,7 @@ public: bool elists_are_consistent(std::unordered_map, hash_svector> &lists) const; - bool consistent() const { - unsigned mons = 0; - for (lpvar v = 0; v < m_var2index.size(); v++) { - if (is_monic_var(v)) { - mons ++; - } - } - return m_monics.size() == mons; - } + bool invariant() const; }; // end of emonics diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h index b600a71c9..9eba04d5b 100644 --- a/src/math/lp/monic.h +++ b/src/math/lp/monic.h @@ -17,22 +17,24 @@ namespace nla { class mon_eq { // fields + bool m_sign; lp::var_index m_v; svector m_vs; public: // constructors - mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs): - m_v(v), m_vs(sz, vs) { + mon_eq(bool sign, lp::var_index v, unsigned sz, lp::var_index const* vs): + m_sign(sign), m_v(v), m_vs(sz, vs) { std::sort(m_vs.begin(), m_vs.end()); } - mon_eq(lp::var_index v, const svector &vs): - m_v(v), m_vs(vs) { + mon_eq(bool sign, lp::var_index v, const svector &vs): + m_sign(sign), m_v(v), m_vs(vs) { std::sort(m_vs.begin(), m_vs.end()); } - mon_eq() {} + mon_eq():m_sign(false), m_v(UINT_MAX) {} unsigned var() const { return m_v; } unsigned size() const { return m_vs.size(); } + bool sign() const { return m_sign; } const svector& vars() const { return m_vs; } svector& vars() { return m_vs; } bool empty() const { return m_vs.empty(); } @@ -41,30 +43,30 @@ public: // support the congruence class monic: public mon_eq { // fields - svector m_rvars; - bool m_rsign; + svector m_rvars; + bool m_rsign; mutable unsigned m_visited; public: // constructors - monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monic(v, svector(sz, vs), idx) { + monic(bool sign, lpvar v, unsigned sz, lpvar const* vs, unsigned idx): + monic(sign, v, svector(sz, vs), idx) { } - monic(lpvar v, const svector &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_visited(0) { + monic(bool sign, lpvar v, const svector &vs, unsigned idx): + mon_eq(sign, v, vs), m_rsign(false), m_visited(0) { std::sort(vars().begin(), vars().end()); } unsigned visited() const { return m_visited; } - unsigned& visited() { return m_visited; } + void set_visited(unsigned v) { m_visited = v; } svector const& rvars() const { return m_rvars; } bool rsign() const { return m_rsign; } - void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); } + void reset_rfields() { m_rsign = sign(); m_rvars.reset(); SASSERT(m_rvars.size() == 0); } void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); } - void sort_rvars() { - std::sort(m_rvars.begin(), m_rvars.end()); - } + void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } }; inline std::ostream& operator<<(std::ostream& out, monic const& m) { - return out << m.var() << " := " << m.vars() << " r ( " << sign_to_rat(m.rsign()) << " * " << m.rvars() << ")"; + return out << m.var() << " := " << (m.sign()?"- ":"") << m.vars() << " r ( " << (m.rsign()?"- ":"") << m.rvars() << ")"; } diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 15176190e..270d65a00 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -36,7 +36,7 @@ bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) { } void basics::generate_zero_lemmas(const monic& m) { - SASSERT(!val(m).is_zero() && c().product_value(m.vars()).is_zero()); + SASSERT(!val(m).is_zero() && c().product_value(m).is_zero()); int sign = nla::rat_sign(val(m)); unsigned_vector fixed_zeros; lpvar zero_j = find_best_zero(m, fixed_zeros); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index c8d3cb7d1..8089be8ee 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -152,9 +152,9 @@ void core::pop(unsigned n) { SASSERT(elists_are_consistent(false)); } -rational core::product_value(const unsigned_vector & m) const { - rational r(1); - for (auto j : m) { +rational core::product_value(const monic& m) const { + rational r(m.sign() ? -1 : 1); + for (auto j : m.vars()) { r *= m_lar_solver.get_column_value_rational(j); } return r; @@ -163,7 +163,7 @@ rational core::product_value(const unsigned_vector & m) const { // return true iff the monic value is equal to the product of the values of the factors bool core::check_monic(const monic& m) const { SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); - bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); + bool ret = product_value(m) == m_lar_solver.get_column_value_rational(m.var()); CTRACE("nla_solver_check_monic", !ret, print_monic(m, tout) << '\n';); return ret; } @@ -955,9 +955,10 @@ void core::clear() { } void core::init_search() { + TRACE("nla_solver_mons", tout << "init\n";); clear(); init_vars_equivalence(); - SASSERT(m_emons.consistent()); + SASSERT(m_emons.invariant()); SASSERT(elists_are_consistent(false)); } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 669f646e1..74d8404e0 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -183,7 +183,7 @@ public: void pop(unsigned n); rational mon_value_by_vars(unsigned i) const; - rational product_value(const unsigned_vector & m) const; + rational product_value(const monic & m) const; // return true iff the monic value is equal to the product of the values of the factors bool check_monic(const monic& m) const; diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 2346af54c..978ca51df 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -81,7 +81,7 @@ void monotone::monotonicity_lemma(monic const& m) { SASSERT(!check_monic(m)); if (c().mon_has_zero(m.vars())) return; - const rational prod_val = abs(c().product_value(m.vars())); + const rational prod_val = abs(c().product_value(m)); const rational m_val = abs(val(m)); if (m_val < prod_val) monotonicity_lemma_lt(m, prod_val); diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index e79c9b643..57e383297 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -38,7 +38,7 @@ typedef nla::variable_map_type variable_map_type; } void add(lp::var_index v, unsigned sz, lp::var_index const* vs) { - m_monics.push_back(mon_eq(v, sz, vs)); + m_monics.push_back(mon_eq(false, v, sz, vs)); } void push() {