From 8cdf754990f23d416516913fbbcbaf858d7d6628 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 30 Apr 2019 10:25:05 -0700 Subject: [PATCH] debug emons Signed-off-by: Lev Nachmanson --- src/smt/smt_context_pp.cpp | 1 + src/util/lp/emonomials.cpp | 656 +++++++++++++++--------------- src/util/lp/emonomials.h | 9 +- src/util/lp/monomial.h | 2 +- src/util/lp/nla_basics_lemmas.cpp | 12 +- src/util/lp/nla_core.cpp | 7 +- src/util/lp/var_eqs.cpp | 2 + 7 files changed, 360 insertions(+), 329 deletions(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 02ad786dd..1dbe3be67 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -493,6 +493,7 @@ namespace smt { TRACE("lemma", tout << strm.str() << "\n";); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); out.close(); + if (m_lemma_id==6998) exit(0); return m_lemma_id; } diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index 78c1f8909..512172702 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -3,19 +3,19 @@ Module Name: - emonomials.cpp + emonomials.cpp Abstract: - table that associate monomials to congruence class representatives modulo a union find structure. + table that associate monomials to congruence class representatives modulo a union find structure. Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) Revision History: - to replace rooted_mons.h and rooted_mon, rooted_mon_tabled + to replace rooted_mons.h and rooted_mon, rooted_mon_tabled --*/ @@ -26,342 +26,360 @@ namespace nla { - void emonomials::inc_visited() const { +void emonomials::inc_visited() const { + ++m_visited; + if (m_visited == 0) { + for (auto& svt : m_monomials) { + svt.visited() = 0; + } ++m_visited; - if (m_visited == 0) { - for (auto& svt : m_monomials) { - svt.visited() = 0; - } - ++m_visited; - } } +} - void emonomials::push() { - m_lim.push_back(m_monomials.size()); - m_region.push_scope(); - m_ve.push(); - } +void emonomials::push() { + m_lim.push_back(m_monomials.size()); + m_region.push_scope(); + m_ve.push(); + SASSERT(monomials_are_canonized()); +} - void emonomials::pop(unsigned n) { - m_ve.pop(n); - unsigned old_sz = m_lim[m_lim.size() - n]; - for (unsigned i = m_monomials.size(); i-- > old_sz; ) { - monomial & m = m_monomials[i]; - remove_cg(i, 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], i); - last_var = v; - } - } - } - m_monomials.shrink(old_sz); - m_monomials.shrink(old_sz); - m_region.pop_scope(n); - m_lim.shrink(m_lim.size() - n); - } - - void emonomials::remove_cell(head_tail& v, unsigned mIndex) { - cell*& cur_head = v.m_head; - cell*& cur_tail = v.m_tail; - cell* old_head = cur_head->m_next; - if (old_head == cur_head) { - cur_head = nullptr; - cur_tail = nullptr; - } - else { - cur_head = old_head; - cur_tail->m_next = old_head; - } - } - - void emonomials::insert_cell(head_tail& v, unsigned mIndex) { - cell*& cur_head = v.m_head; - cell*& cur_tail = v.m_tail; - cell* new_head = new (m_region) cell(mIndex, cur_head); - cur_head = new_head; - if (!cur_tail) cur_tail = new_head; - cur_tail->m_next = new_head; - } - - void emonomials::merge_cells(head_tail& root, head_tail& other) { - if (&root == &other) return; - cell*& root_head = root.m_head; - cell*& root_tail = root.m_tail; - cell* other_head = other.m_head; - cell* other_tail = other.m_tail; - if (root_head == nullptr) { - root_head = other_head; - root_tail = other_tail; - } - else if (other_head) { - // other_head -> other_tail -> root_head --> root_tail -> other_head. - root_tail->m_next = other_head; - other_tail->m_next = root_head; - root_head = other_head; - } - else { - // other_head = other_tail = nullptr - } - } - - void emonomials::unmerge_cells(head_tail& root, head_tail& other) { - if (&root == &other) return; - cell*& root_head = root.m_head; - cell*& root_tail = root.m_tail; - cell* other_head = other.m_head; - cell* other_tail = other.m_tail; - if (other_head == nullptr) { - // no-op - } - else if (root_tail == other_tail) { - root_head = nullptr; - root_tail = nullptr; - } - else { - root_head = other_tail->m_next; - root_tail->m_next = root_head; - other_tail->m_next = other_head; - } - } - - emonomials::cell* emonomials::head(lpvar v) const { - v = m_ve.find(v).var(); - m_use_lists.reserve(v + 1); - return m_use_lists[v].m_head; - } - - monomial const* emonomials::find_canonical(svector const& vars) const { - SASSERT(m_ve.is_root(vars)); - m_find_key = vars; - std::sort(m_find_key.begin(), m_find_key.end()); - monomial const* result = nullptr; - lpvar w; - if (m_cg_table.find(UINT_MAX, w)) { - result = &m_monomials[m_var2index[w]]; - } - return result; - } - - - void emonomials::remove_cg(lpvar v) { - cell* c = m_use_lists[v].m_head; - if (c == nullptr) { - return; - } - cell* first = c; - inc_visited(); - do { - unsigned idx = c->m_index; - c = c->m_next; - monomial & m = m_monomials[idx]; - if (!is_visited(m)) { - set_visited(m); - remove_cg(idx, m); - } - } - while (c != first); - } - - void emonomials::remove_cg(unsigned idx, monomial& m) { - monomial& sv = m_monomials[idx]; - unsigned next = sv.next(); - unsigned prev = sv.prev(); - - lpvar u = m.var(), w; - // equivalence class of u: - if (m_cg_table.find(u, w) && w == u) { - m_cg_table.erase(u); - // insert other representative: - if (prev != idx) { - m_cg_table.insert(m_monomials[prev].var()); - } - } - if (prev != idx) { - m_monomials[next].prev() = prev; - m_monomials[prev].next() = next; - sv.next() = idx; - sv.prev() = idx; - } - } - - /** - \brief insert canonized monomials using v into a congruence table. - Prior to insertion, the monomials are canonized according to the current - variable equivalences. The canonized monomials (monomial) are considered - in the same equivalence class if they have the same set of representative - variables. Their signs may differ. - */ - void emonomials::insert_cg(lpvar v) { - cell* c = m_use_lists[v].m_head; - if (c == nullptr) { - return; - } - - cell* first = c; - inc_visited(); - do { - unsigned idx = c->m_index; - c = c->m_next; - monomial & m = m_monomials[idx]; - if (!is_visited(m)) { - set_visited(m); - insert_cg(idx, m); - } - } - while (c != first); - } - - void emonomials::insert_cg(unsigned idx, monomial & m) { - do_canonize(m); - lpvar v = m.var(), w; - if (m_cg_table.find(v, w)) { - SASSERT(w != v); - unsigned idxr = m_var2index[w]; - unsigned idxl = m_monomials[idxr].prev(); - m_monomials[idx].next() = idxr; - m_monomials[idx].prev() = idxl; - m_monomials[idxr].prev() = idx; - m_monomials[idxl].next() = idx; - } - else { - m_cg_table.insert(v); - SASSERT(m_monomials[idx].next() == idx); - SASSERT(m_monomials[idx].prev() == idx); - } - } - - void emonomials::set_visited(monomial& m) const { - m_monomials[m_var2index[m.var()]].visited() = m_visited; - } - - bool emonomials::is_visited(monomial const& m) const { - return m_visited == m_monomials[m_var2index[m.var()]].visited(); - } - - /** - \brief insert a new monomial. - - Assume that the variables are canonical, that is, not equal in current - context to another variable. The monomial is inserted into a congruence - class of equal up-to var_eqs monomials. - */ - void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) { - unsigned idx = m_monomials.size(); - m_monomials.push_back(monomial(v, sz, vs, idx)); +void emonomials::pop(unsigned n) { + m_ve.pop(n); + unsigned old_sz = m_lim[m_lim.size() - n]; + for (unsigned i = m_monomials.size(); i-- > old_sz; ) { + monomial & m = m_monomials[i]; + remove_cg(i, m); + m_var2index[m.var()] = UINT_MAX; lpvar last_var = UINT_MAX; - for (unsigned i = 0; i < sz; ++i) { - lpvar w = vs[i]; - SASSERT(m_ve.is_root(w)); - if (w != last_var) { - m_use_lists.reserve(w + 1); - insert_cell(m_use_lists[w], idx); - last_var = w; - } - } - SASSERT(m_ve.is_root(v)); - m_var2index.setx(v, idx, UINT_MAX); - insert_cg(idx, m_monomials[idx]); - } - - void emonomials::do_canonize(monomial & m) const { - m.reset_rfields(); for (lpvar v : m.vars()) { - m.push_rvar(m_ve.find(v)); - } - m.sort_rvars(); - } - - bool emonomials::canonize_divides(monomial& m, monomial & n) const { - if (m.size() > n.size()) return false; - unsigned ms = m.size(), ns = n.size(); - unsigned i = 0, j = 0; - while (true) { - if (i == ms) { - return true; - } - else if (j == ns) { - return false; - } - else if (m.rvars()[i] == n.rvars()[j]) { - ++i; ++j; - } - else if (m.rvars()[i] < n.rvars()[j]) { - return false; - } - else { - ++j; + if (v != last_var) { + remove_cell(m_use_lists[v], i); + last_var = v; } } } + m_monomials.shrink(old_sz); + m_monomials.shrink(old_sz); + m_region.pop_scope(n); + m_lim.shrink(m_lim.size() - n); + SASSERT(monomials_are_canonized()); +} -// yes, assume that monomials are non-empty. - emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end): - m_em(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) { - fast_forward(); +void emonomials::remove_cell(head_tail& v, unsigned mIndex) { + cell*& cur_head = v.m_head; + cell*& cur_tail = v.m_tail; + cell* old_head = cur_head->m_next; + if (old_head == cur_head) { + cur_head = nullptr; + cur_tail = nullptr; } - - emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end): - m_em(m), m_mon(nullptr), m_it(iterator(m, m.head(v), at_end)), m_end(iterator(m, m.head(v), true)) { - fast_forward(); + else { + cur_head = old_head; + cur_tail->m_next = old_head; } +} - void emonomials::pf_iterator::fast_forward() { - for (; m_it != m_end; ++m_it) { - if (m_mon && m_mon->var() != (*m_it).var() && m_em.canonize_divides(*m_mon, *m_it) && !m_em.is_visited(*m_it)) { - m_em.set_visited(*m_it); - break; - } - if (!m_mon && !m_em.is_visited(*m_it)) { - m_em.set_visited(*m_it); - break; - } - } +void emonomials::insert_cell(head_tail& v, unsigned mIndex) { + cell*& cur_head = v.m_head; + cell*& cur_tail = v.m_tail; + cell* new_head = new (m_region) cell(mIndex, cur_head); + cur_head = new_head; + if (!cur_tail) cur_tail = new_head; + cur_tail->m_next = new_head; +} + +void emonomials::merge_cells(head_tail& root, head_tail& other) { + if (&root == &other) return; + cell*& root_head = root.m_head; + cell*& root_tail = root.m_tail; + cell* other_head = other.m_head; + cell* other_tail = other.m_tail; + if (root_head == nullptr) { + root_head = other_head; + root_tail = other_tail; } + else if (other_head) { + // other_head -> other_tail -> root_head --> root_tail -> other_head. + root_tail->m_next = other_head; + other_tail->m_next = root_head; + root_head = other_head; + } + else { + // other_head = other_tail = nullptr + } +} - void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { +void emonomials::unmerge_cells(head_tail& root, head_tail& other) { + if (&root == &other) return; + cell*& root_head = root.m_head; + cell*& root_tail = root.m_tail; + cell* other_head = other.m_head; + cell* other_tail = other.m_tail; + if (other_head == nullptr) { // no-op } + else if (root_tail == other_tail) { + root_head = nullptr; + root_tail = nullptr; + } + else { + root_head = other_tail->m_next; + root_tail->m_next = root_head; + other_tail->m_next = other_head; + } +} - void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { - if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) { - m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); - rehash_cg(r1.var()); - merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); - } +emonomials::cell* emonomials::head(lpvar v) const { + v = m_ve.find(v).var(); + m_use_lists.reserve(v + 1); + return m_use_lists[v].m_head; +} + +monomial const* emonomials::find_canonical(svector const& vars) const { + SASSERT(m_ve.is_root(vars)); + m_find_key = vars; + std::sort(m_find_key.begin(), m_find_key.end()); + monomial const* result = nullptr; + lpvar w; + if (m_cg_table.find(UINT_MAX, w)) { + result = &m_monomials[m_var2index[w]]; + } + return result; +} + + +void emonomials::remove_cg(lpvar v) { + cell* c = m_use_lists[v].m_head; + if (c == nullptr) { + return; + } + cell* first = c; + inc_visited(); + do { + unsigned idx = c->m_index; + c = c->m_next; + monomial & m = m_monomials[idx]; + if (!is_visited(m)) { + set_visited(m); + remove_cg(idx, m); + } + } + while (c != first); +} + +void emonomials::remove_cg(unsigned idx, monomial& m) { + monomial& sv = m_monomials[idx]; + unsigned next = sv.next(); + unsigned prev = sv.prev(); + + lpvar u = m.var(), w; + // equivalence class of u: + if (m_cg_table.find(u, w) && w == u) { + m_cg_table.erase(u); + // insert other representative: + if (prev != idx) { + m_cg_table.insert(m_monomials[prev].var()); + } + } + if (prev != idx) { + m_monomials[next].prev() = prev; + m_monomials[prev].next() = next; + sv.next() = idx; + sv.prev() = idx; + } +} + +/** + \brief insert canonized monomials using v into a congruence table. + Prior to insertion, the monomials are canonized according to the current + variable equivalences. The canonized monomials (monomial) are considered + in the same equivalence class if they have the same set of representative + variables. Their signs may differ. +*/ +void emonomials::insert_cg(lpvar v) { + cell* c = m_use_lists[v].m_head; + if (c == nullptr) { + return; } - void emonomials::unmerge_eh(signed_var r2, signed_var r1) { - if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) { - unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); - rehash_cg(r1.var()); - } + cell* first = c; + inc_visited(); + do { + unsigned idx = c->m_index; + c = c->m_next; + monomial & m = m_monomials[idx]; + if (!is_visited(m)) { + set_visited(m); + insert_cg(idx, m); + } } + while (c != first); +} + +void emonomials::insert_cg(unsigned idx, monomial & m) { + do_canonize(m); + lpvar v = m.var(), w; + if (m_cg_table.find(v, w)) { + SASSERT(w != v); + unsigned idxr = m_var2index[w]; + unsigned idxl = m_monomials[idxr].prev(); + m_monomials[idx].next() = idxr; + m_monomials[idx].prev() = idxl; + m_monomials[idxr].prev() = idx; + m_monomials[idxl].next() = idx; + } + else { + m_cg_table.insert(v); + SASSERT(m_monomials[idx].next() == idx); + SASSERT(m_monomials[idx].prev() == idx); + } +} + +void emonomials::set_visited(monomial& m) const { + m_monomials[m_var2index[m.var()]].visited() = m_visited; +} + +bool emonomials::is_visited(monomial const& m) const { + return m_visited == m_monomials[m_var2index[m.var()]].visited(); +} + +/** + \brief insert a new monomial. + + Assume that the variables are canonical, that is, not equal in current + context to another variable. The monomial is inserted into a congruence + class of equal up-to var_eqs monomials. +*/ +void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) { + unsigned idx = m_monomials.size(); + m_monomials.push_back(monomial(v, sz, vs, idx)); + lpvar last_var = UINT_MAX; + for (unsigned i = 0; i < sz; ++i) { + lpvar w = vs[i]; + SASSERT(m_ve.is_root(w)); + if (w != last_var) { + m_use_lists.reserve(w + 1); + insert_cell(m_use_lists[w], idx); + last_var = w; + } + } + SASSERT(m_ve.is_root(v)); + m_var2index.setx(v, idx, UINT_MAX); + insert_cg(idx, m_monomials[idx]); +} + +void emonomials::do_canonize(monomial & m) const { + m.reset_rfields(); + for (lpvar v : m.vars()) { + m.push_rvar(m_ve.find(v)); + } + m.sort_rvars(); +} + +bool emonomials::is_canonized(const monomial & m) const { + monomial mm(m); + do_canonize(mm); + return mm.rvars() == m.rvars(); +} + +bool emonomials:: monomials_are_canonized() const { + for (auto & m: m_monomials) { + if (! is_canonized(m)) { + return false; + } + } + return true; +} + + +bool emonomials::canonize_divides(monomial& m, monomial & n) const { + if (m.size() > n.size()) return false; + unsigned ms = m.size(), ns = n.size(); + unsigned i = 0, j = 0; + while (true) { + if (i == ms) { + return true; + } + else if (j == ns) { + return false; + } + else if (m.rvars()[i] == n.rvars()[j]) { + ++i; ++j; + } + else if (m.rvars()[i] < n.rvars()[j]) { + return false; + } + else { + ++j; + } + } +} + +// yes, assume that monomials are non-empty. +emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end): + m_em(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) { + fast_forward(); +} + +emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end): + m_em(m), m_mon(nullptr), m_it(iterator(m, m.head(v), at_end)), m_end(iterator(m, m.head(v), true)) { + fast_forward(); +} + +void emonomials::pf_iterator::fast_forward() { + for (; m_it != m_end; ++m_it) { + if (m_mon && m_mon->var() != (*m_it).var() && m_em.canonize_divides(*m_mon, *m_it) && !m_em.is_visited(*m_it)) { + m_em.set_visited(*m_it); + break; + } + if (!m_mon && !m_em.is_visited(*m_it)) { + m_em.set_visited(*m_it); + break; + } + } +} + +void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { + // no-op +} + +void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { + if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) { + m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); + rehash_cg(r1.var()); + merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); + } +} + +void emonomials::unmerge_eh(signed_var r2, signed_var r1) { + if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) { + unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); + rehash_cg(r1.var()); + } +} std::ostream& emonomials::display(const core& cr, std::ostream& out) const { - out << "monomials\n"; - unsigned idx = 0; - for (auto const& m : m_monomials) { - out << (idx++) << ": " << pp_mon(cr, m) << "\n"; - } - out << "use lists\n"; - idx = 0; - for (auto const& ht : m_use_lists) { - cell* c = ht.m_head; - if (c) { - out << "v" << idx << ": "; - do { - out << c->m_index << " "; - c = c->m_next; - } - while (c != ht.m_head); - out << "\n"; - } - ++idx; - } - return out; - } + out << "monomials\n"; + unsigned idx = 0; + for (auto const& m : m_monomials) { + out << (idx++) << ": " << pp_rmon(cr, m) << "\n"; + } + out << "use lists\n"; + idx = 0; + for (auto const& ht : m_use_lists) { + cell* c = ht.m_head; + if (c) { + out << "v" << idx << ": "; + do { + out << c->m_index << " "; + c = c->m_next; + } + while (c != ht.m_head); + out << "\n"; + } + ++idx; + } + return out; +} } diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 64528e1b5..b37c2ee51 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -100,7 +100,6 @@ class emonomials : public var_eqs_merge_handler { void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); } void do_canonize(monomial& m) const; - cell* head(lpvar v) const; void set_visited(monomial& m) const; bool is_visited(monomial const& m) const; @@ -141,7 +140,9 @@ public: */ monomial const& operator[](lpvar v) const { return m_monomials[m_var2index[v]]; } monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; } - + bool is_canonized(const monomial&) const; + bool monomials_are_canonized() const; + /** \brief obtain the representative canonized monomial */ @@ -204,7 +205,9 @@ public: public: pf_iterator(emonomials const& m, monomial& mon, bool at_end); pf_iterator(emonomials const& m, lpvar v, bool at_end); - monomial & operator*() { return *m_it; } + monomial & operator*() { + return *m_it; + } pf_iterator& operator++() { ++m_it; fast_forward(); return *this; } pf_iterator operator++(int) { pf_iterator tmp = *this; ++*this; return tmp; } bool operator==(pf_iterator const& other) const { return m_it == other.m_it; } diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h index 206028fb3..e0ebce7f5 100644 --- a/src/util/lp/monomial.h +++ b/src/util/lp/monomial.h @@ -63,7 +63,7 @@ public: svector const& rvars() const { return m_rvars; } bool sign() const { return m_rsign; } rational rsign() const { return rational(m_rsign ? -1 : 1); } - void reset_rfields() { m_rsign = false; m_rvars.reset(); } + void reset_rfields() { m_rsign = false; 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()); diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp index 3adde59f9..bb1df83cf 100644 --- a/src/util/lp/nla_basics_lemmas.cpp +++ b/src/util/lp/nla_basics_lemmas.cpp @@ -121,11 +121,13 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set & exp if (!try_insert(v, explored)) { return false; } - const monomial& m_v = c().m_emons[v]; - TRACE("nla_solver_details", tout << "mon = " << pp_mon(c(), m_v);); + TRACE("nla_solver", tout << "m_v = " << pp_rmon(c(), m_v);); + SASSERT(c().m_emons.is_canonized(m_v)); for (auto const& m : c().m_emons.enum_sign_equiv_monomials(v)) { + TRACE("nla_solver_details", tout << "m = " << pp_rmon(c(), m);); + SASSERT(m.rvars() == m_v.rvars()); if (m_v.var() != m.var() && basic_sign_lemma_on_two_monomials(m_v, m) && done()) return true; } @@ -154,12 +156,14 @@ bool basics::basic_sign_lemma(bool derived) { void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) { add_empty_lemma(); TRACE("nla_solver", - tout << "m = "; c().print_monomial_with_vars(m, tout); - tout << "n = "; c().print_monomial_with_vars(n, tout); + tout << "m = " << pp_rmon(_(), m); + tout << "n = " << pp_rmon(_(), n); ); c().mk_ineq(m.var(), -sign, n.var(), llc::EQ); explain(m); + TRACE("nla_solver", tout << "m exp = "; _().print_explanation(_().current_expl(), tout);); explain(n); + TRACE("nla_solver", tout << "n exp = "; _().print_explanation(_().current_expl(), tout);); TRACE("nla_solver", c().print_lemma(tout);); } // try to find a variable j such that val(j) = 0 diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index 0a587dcd3..25cebd2d9 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -112,7 +112,9 @@ void core::push() { void core::pop(unsigned n) { TRACE("nla_solver", tout << "n = " << n << "\n";); - m_emons.pop(n); + TRACE("nla_solver", tout << "before pop mons = " << pp_emons(*this, m_emons) << "\n";); + m_emons.pop(n); + TRACE("nla_solver", tout << "after pop mons = " << pp_emons(*this, m_emons) << "\n";); } rational core::product_value(const unsigned_vector & m) const { @@ -718,7 +720,8 @@ std::ostream & core::print_var(lpvar j, std::ostream & out) const { out << " = " << val(j);; } - m_lar_solver.print_column_info(j, out) <<";"; + m_lar_solver.print_column_info(j, out); + out << "root=" << m_evars.find(j) << "\n"; return out; } diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp index 7fc711d25..5a71b1595 100644 --- a/src/util/lp/var_eqs.cpp +++ b/src/util/lp/var_eqs.cpp @@ -120,6 +120,8 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons } void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const { + static int ddd=0; + TRACE("nla_solver", tout << ++ddd << "\n";); SASSERT(find(v1) == find(v2)); if (v1 == v2) { return;