From 5d5d4a22642d3dba829e86d18447e03523364774 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 17 Jun 2019 20:47:33 -0700 Subject: [PATCH] randomize m_to_refine() init Signed-off-by: Lev Nachmanson --- src/math/lp/emonomials.h | 1 + src/math/lp/nla_core.cpp | 5 ++++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/math/lp/emonomials.h b/src/math/lp/emonomials.h index 5b0979946..a97b7d92a 100644 --- a/src/math/lp/emonomials.h +++ b/src/math/lp/emonomials.h @@ -95,6 +95,7 @@ class emonomials { hashtable m_cg_table; // congruence (canonical) table. + unsigned number_of_monomials() const { return m_monomials.size(); } void inc_visited() const; void remove_cell(head_tail& v, unsigned mIndex); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 561935a83..856a84f03 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -965,9 +965,12 @@ void core::init_search() { void core::init_to_refine() { TRACE("nla_solver", tout << "emons:" << pp_emons(*this, m_emons);); m_to_refine.clear(); - for (auto const & m : m_emons) + unsigned r = random(), sz = m_emons.number_of_monomials(); + for (unsigned k = 0; k < sz; k++) { + auto const & m = m_emons[(k + r)% sz]; if (!check_monomial(m)) m_to_refine.push_back(m.var()); + } TRACE("nla_solver", tout << m_to_refine.size() << " mons to refine:\n";