From ad412d4f08f63e61778f940fef7afdb0f54c7f51 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Mar 2014 14:58:59 +0000 Subject: [PATCH] bvsls refactoring Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_engine.cpp | 21 ++++++++++++--------- src/tactic/sls/sls_engine.h | 2 ++ 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 10aaf6601..e7ee2abbd 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -1069,6 +1069,16 @@ bailout: } #endif +void sls_engine::init_tracker() { +#if _WEIGHT_DIST_ == 4 + m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); +#endif +#if _WEIGHT_TOGGLE_ + m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_); +#endif + m_tracker.initialize(m_assertions); +} + void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { if (g->inconsistent()) { mc = 0; @@ -1078,8 +1088,7 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { m_produce_models = g->models_enabled(); for (unsigned i = 0; i < g->size(); i++) - assert_expr(g->form(i)); - + assert_expr(g->form(i)); verbose_stream() << "_BFS_ " << _BFS_ << std::endl; verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl; @@ -1118,13 +1127,7 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; -#if _WEIGHT_DIST_ == 4 - m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); -#endif -#if _WEIGHT_TOGGLE_ - m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_); -#endif - m_tracker.initialize(m_assertions); + init_tracker(); lbool res = l_undef; m_restart_limit = _RESTART_LIMIT_; diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 96041d09e..c56d6ec40 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -109,6 +109,8 @@ public: void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted); void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); + void init_tracker(void); + lbool search(void); void operator()(goal_ref const & g, model_converter_ref & mc);