From dd235be4d2a316b7cfbec8f06a918cefe7cea592 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 6 Mar 2019 12:46:11 +1400 Subject: [PATCH] add randomness when generating model based sign lemma Signed-off-by: Lev Nachmanson --- src/util/lp/nla_solver.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 2ea006615..17d4464bd 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -947,14 +947,20 @@ struct solver::imp { init_abs_val_table(); std::unordered_map key_mons = create_relevant_abs_keys(); - for (unsigned i = 0; i < m_monomials.size(); i++) { + unsigned i = random() % m_monomials.size(); + unsigned ii = i; + do { unsigned_vector key = get_abs_key(m_monomials[i]); auto it = key_mons.find(key); - if (it == key_mons.end() || it->second == i) - continue; - if (basic_sign_lemma_on_two_mons_model_based(m_monomials[it->second], m_monomials[i])) + if ( + !(it == key_mons.end() || it->second == i) + && + basic_sign_lemma_on_two_mons_model_based(m_monomials[it->second], m_monomials[i])) return true; - } + i++; + if (i == m_monomials.size()) + i = 0; + } while (i != ii); return false; }