From b30004107572257e37ebacd536a9255cc2e1d932 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Apr 2014 16:52:57 -0700 Subject: [PATCH] resetting SLS engine between calls, moved statistics collection to engine Signed-off-by: Nikolaj Bjorner --- src/opt/opt_sls_solver.h | 30 ++++++++++++++++++++++-------- src/opt/weighted_maxsat.cpp | 2 +- src/tactic/sls/sls_engine.cpp | 14 ++++++++++++++ src/tactic/sls/sls_engine.h | 4 +++- src/tactic/sls/sls_tactic.cpp | 13 +------------ 5 files changed, 41 insertions(+), 22 deletions(-) diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h index 0873b4f01..542728cc4 100644 --- a/src/opt/opt_sls_solver.h +++ b/src/opt/opt_sls_solver.h @@ -28,16 +28,17 @@ namespace opt { class sls_solver : public solver_na2as { ast_manager& m; ref m_solver; - bvsls_opt_engine m_sls; + scoped_ptr m_sls; pb::card_pb_rewriter m_pb2bv; model_ref m_model; expr_ref m_objective; + params_ref m_params; public: sls_solver(ast_manager & m, solver* s, expr* to_maximize, params_ref const& p): solver_na2as(m), m(m), m_solver(s), - m_sls(m, p), + m_sls(0), m_pb2bv(m), m_objective(to_maximize, m) { @@ -46,13 +47,14 @@ namespace opt { virtual void updt_params(params_ref & p) { m_solver->updt_params(p); + m_params.copy(p); } virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); - // TBD: m_sls.get_stats(); + // TBD: m_sls->get_stats(); } virtual void assert_expr(expr * t) { m_solver->assert_expr(t); @@ -74,7 +76,13 @@ namespace opt { } virtual void set_cancel(bool f) { m_solver->set_cancel(f); - m_sls.set_cancel(f); + m_pb2bv.set_cancel(f); + #pragma omp critical (this) + { + if (m_sls) { + m_sls->set_cancel(f); + } + } } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); @@ -87,7 +95,7 @@ namespace opt { } virtual void display(std::ostream & out) const { m_solver->display(out); - // m_sls.display(out); + // if (m_sls) m_sls->display(out); } protected: @@ -97,10 +105,16 @@ namespace opt { lbool r = m_solver->check_sat(num_assumptions, assumptions); if (r == l_true) { m_solver->get_model(m_model); + #pragma omp critical (this) + { + m_sls = alloc(bvsls_opt_engine, m, m_params); + } assertions2sls(); - opt_result or = m_sls.optimize(m_objective, m_model, true); + opt_result or = m_sls->optimize(m_objective, m_model, true); SASSERT(or.is_sat == l_true || or.is_sat == l_undef); - m_sls.get_model(m_model); + if (or.is_sat == l_true) { + m_sls->get_model(m_model); + } } return r; } @@ -127,7 +141,7 @@ namespace opt { SASSERT(result.size() == 1); goal* r = result[0]; for (unsigned i = 0; i < r->size(); ++i) { - m_sls.assert_expr(r->form(i)); + m_sls->assert_expr(r->form(i)); } } diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 42a037b7d..ea3515ec7 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -75,7 +75,7 @@ namespace opt { virtual void collect_statistics(statistics& st) const { } virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } virtual void updt_params(params_ref& p) { - m_params = p; + m_params.copy(p); s().updt_params(p); opt_params _p(p); m_enable_sat = _p.enable_sat(); diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index dc4451bb5..7c85f3bd6 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -68,6 +68,20 @@ void sls_engine::updt_params(params_ref const & _p) { m_plateau_limit = p.plateau_limit(); } +void sls_engine::collect_statistics(statistics& st) const { + double seconds = m_stats.m_stopwatch.get_current_seconds(); + st.update("sls restarts", m_stats.m_restarts); + st.update("sls full evals", m_stats.m_full_evals); + st.update("sls incr evals", m_stats.m_incr_evals); + st.update("sls incr evals/sec", m_stats.m_incr_evals / seconds); + st.update("sls FLIP moves", m_stats.m_flips); + st.update("sls INC moves", m_stats.m_incs); + st.update("sls DEC moves", m_stats.m_decs); + st.update("sls INV moves", m_stats.m_invs); + st.update("sls moves", m_stats.m_moves); + st.update("sls moves/sec", m_stats.m_moves / seconds); +} + void sls_engine::checkpoint() { if (m_cancel) throw tactic_exception(TACTIC_CANCELED_MSG); diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index c6e3af155..9a5e905b3 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -27,6 +27,7 @@ Notes: #include"sls_compilation_settings.h" #include"sls_tracker.h" #include"sls_evaluator.h" +#include"statistics.h" class sls_engine { public: @@ -96,7 +97,8 @@ public: void assert_expr(expr * e) { m_assertions.push_back(e); } - stats const & get_stats(void) { return m_stats; } + // stats const & get_stats(void) { return m_stats; } + void collect_statistics(statistics & st) const; void reset_statistics(void) { m_stats.reset(); } bool full_eval(model & mdl); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index a9b110224..464a0925c 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -93,18 +93,7 @@ public: } virtual void collect_statistics(statistics & st) const { - sls_engine::stats const & stats = m_engine->get_stats(); - double seconds = stats.m_stopwatch.get_current_seconds(); - st.update("sls restarts", stats.m_restarts); - st.update("sls full evals", stats.m_full_evals); - st.update("sls incr evals", stats.m_incr_evals); - st.update("sls incr evals/sec", stats.m_incr_evals / seconds); - st.update("sls FLIP moves", stats.m_flips); - st.update("sls INC moves", stats.m_incs); - st.update("sls DEC moves", stats.m_decs); - st.update("sls INV moves", stats.m_invs); - st.update("sls moves", stats.m_moves); - st.update("sls moves/sec", stats.m_moves / seconds); + m_engine->collect_statistics(st); } virtual void reset_statistics() {