From d3bd55d0cfb2cfccf55a57d9c0c4532406a0874c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 15 May 2019 15:34:57 -0700 Subject: [PATCH] remove m_mons_to_rehash, fix a bug in emonomials::after_merge_eh(), generate order and tangent lemmas on any monomial Signed-off-by: Lev Nachmanson --- src/util/lp/emonomials.cpp | 7 +------ src/util/lp/emonomials.h | 3 --- src/util/lp/nla_core.cpp | 3 +-- src/util/lp/nla_order_lemmas.cpp | 5 ++--- src/util/lp/nla_order_lemmas.h | 2 +- 5 files changed, 5 insertions(+), 15 deletions(-) diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index 659d9f141..80ac9a54f 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -64,12 +64,7 @@ void emonomials::pop(unsigned n) { m_region.pop_scope(n); m_lim.shrink(m_lim.size() - n); SASSERT(monomials_are_canonized()); - m_mons_to_rehash.clear(); m_u_f_stack.pop_scope(n); - for (unsigned j : m_mons_to_rehash) { - remove_cg_mon(m_monomials[j]); - insert_cg_mon(m_monomials[j]); - } } void emonomials::remove_cell(head_tail& v, unsigned mIndex) { @@ -384,8 +379,8 @@ void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, sig if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); TRACE("nla_solver", tout << "rehasing " << r1.var() << "\n";); - rehash_cg(r1.var()); merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); + rehash_cg(r1.var()); } } diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 23611da45..dd0325282 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -82,7 +82,6 @@ class emonomials { union_find m_u_f; trail_stack m_u_f_stack; - std::unordered_set m_mons_to_rehash; mutable svector m_find_key; // the key used when looking for a monomial with the specific variables var_eqs& m_ve; mutable vector m_monomials; // set of monomials @@ -133,8 +132,6 @@ public: void unmerge_eh(unsigned i, unsigned j) { TRACE("nla_solver", tout << "unmerged " << i << " and " << j << "\n";); - m_mons_to_rehash.insert(i); - m_mons_to_rehash.insert(j); } void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index 7f659660d..a1bf8958b 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -1599,13 +1599,12 @@ bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf) return false; } -// finds a canonical monomial with its binary factorization +// finds a monomial to refine with its binary factorization bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){ m = nullptr; unsigned r = random(), sz = m_to_refine.size(); for (unsigned k = 0; k < sz; k++) { lpvar i = m_to_refine[(k + r) % sz]; - if (!is_canonical_monomial(i)) continue; m = &m_emons[i]; SASSERT (!check_monomial(*m)); if (m->size() == 2) { diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp index ee624725b..87becb05c 100644 --- a/src/util/lp/nla_order_lemmas.cpp +++ b/src/util/lp/nla_order_lemmas.cpp @@ -38,8 +38,7 @@ void order::order_lemma() { unsigned sz = to_ref.size(); for (unsigned i = 0; i < sz && !done(); ++i) { lpvar j = to_ref[(i + r) % sz]; - if (c().is_canonical_monomial(j)) - order_lemma_on_canonical_monomial(c().emons()[j]); + order_lemma_on_monomial(c().emons()[j]); } } @@ -47,7 +46,7 @@ void order::order_lemma() { // a > b && c > 0 => ac > bc // Consider here some binary factorizations of m=ac and // try create order lemmas with either factor playing the role of c. -void order::order_lemma_on_canonical_monomial(const monomial& m) { +void order::order_lemma_on_monomial(const monomial& m) { TRACE("nla_solver_details", tout << "m = " << pp_mon(c(), m);); diff --git a/src/util/lp/nla_order_lemmas.h b/src/util/lp/nla_order_lemmas.h index ea7f7501e..ea6328aee 100644 --- a/src/util/lp/nla_order_lemmas.h +++ b/src/util/lp/nla_order_lemmas.h @@ -67,7 +67,7 @@ private: void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d); void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign); void order_lemma_on_binomial(const monomial& ac); - void order_lemma_on_canonical_monomial(const monomial& rm); + void order_lemma_on_monomial(const monomial& rm); // |c_sign| = 1, and c*c_sign > 0 // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign void generate_ol(const monomial& ac,