From e382742a29f06e818bf361e2829abe18d118d710 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Mar 2014 15:26:52 +0000 Subject: [PATCH] bvsls refactoring Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_engine.cpp | 44 +++++++++++++++++++---------------- src/tactic/sls/sls_engine.h | 1 + 2 files changed, 25 insertions(+), 20 deletions(-) diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index e7ee2abbd..2b359608a 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -1125,8 +1125,31 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl; verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl; verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; - verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; + verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; + lbool res = operator()(); + + if (res == l_true) { + report_tactic_progress("Number of flips:", m_stats.m_moves); + for (unsigned i = 0; i < g->size(); i++) + if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) + { + verbose_stream() << "Terminated before all assertions were SAT!" << std::endl; + NOT_IMPLEMENTED_YET(); + } + + if (m_produce_models) { + model_ref mdl = m_tracker.get_model(); + mc = model2model_converter(mdl.get()); + TRACE("sls_model", mc->display(tout);); + } + g->reset(); + } + else + mc = 0; +} + +lbool sls_engine::operator()() { init_tracker(); lbool res = l_undef; @@ -1149,25 +1172,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts); verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; - - if (res == l_true) { - report_tactic_progress("Number of flips:", m_stats.m_moves); - for (unsigned i = 0; i < g->size(); i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - { - verbose_stream() << "Terminated before all assertions were SAT!" << std::endl; - NOT_IMPLEMENTED_YET(); - } - - if (m_produce_models) { - model_ref mdl = m_tracker.get_model(); - mc = model2model_converter(mdl.get()); - TRACE("sls_model", mc->display(tout);); - } - g->reset(); - } - else - mc = 0; } unsigned sls_engine::check_restart(unsigned curr_value) diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index c56d6ec40..c6e3af155 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -113,6 +113,7 @@ public: lbool search(void); + lbool operator()(); void operator()(goal_ref const & g, model_converter_ref & mc); protected: