From 49821e7c91fe6931c938edf629300ee87891bef2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 16 May 2018 08:58:37 -0700 Subject: [PATCH] Revised solver_pool --- src/solver/solver.h | 4 ++ src/solver/solver_pool.cpp | 134 +++++++++++++++++++++++-------------- src/solver/solver_pool.h | 22 ++---- src/test/solver_pool.cpp | 27 +++++--- 4 files changed, 110 insertions(+), 77 deletions(-) diff --git a/src/solver/solver.h b/src/solver/solver.h index 2c056ff90..bb330636f 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -229,4 +229,8 @@ protected: typedef ref solver_ref; +inline std::ostream& operator<<(std::ostream& out, solver const& s) { + return s.display(out); +} + #endif diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 132a2bec4..3cf39a64c 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -17,10 +17,10 @@ Notes: --*/ +#include "solver/solver_pool.h" +#include "solver/solver_na2as.h" #include "ast/proofs/proof_utils.h" #include "ast/ast_util.h" -#include "solver/solver_pool.h" - class pool_solver : public solver_na2as { solver_pool& m_pool; @@ -33,6 +33,7 @@ class pool_solver : public solver_na2as { bool m_pushed; bool m_in_delayed_scope; unsigned m_dump_counter; + bool is_virtual() const { return !m.is_true(m_pred); } public: pool_solver(solver* b, solver_pool& pool, app_ref& pred): @@ -66,6 +67,8 @@ public: void updt_params(params_ref const& p) override { solver::updt_params(p); m_base->updt_params(p); } void collect_param_descrs(param_descrs & r) override { m_base->collect_param_descrs(r); } void collect_statistics(statistics & st) const override { m_base->collect_statistics(st); } + unsigned get_num_assertions() const override { return m_base->get_num_assertions(); } + expr * get_assertion(unsigned idx) const override { return m_base->get_assertion(idx); } void get_unsat_core(ptr_vector & r) override { m_base->get_unsat_core(r); @@ -81,6 +84,7 @@ public: return is_virtual() ? sz - 1 : sz; } + proof * get_proof() override { scoped_watch _t_(m_pool.m_proof_watch); if (!m_proof.get()) { @@ -126,33 +130,7 @@ public: set_status(res); if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) { - std::stringstream file_name; - file_name << "virt_solver"; - if (is_virtual()) { file_name << "_" << m_pred->get_decl()->get_name(); } - file_name << "_" << (m_dump_counter++) << ".smt2"; - - std::ofstream out(file_name.str().c_str()); - if (!out) { verbose_stream() << "could not open file " << file_name.str() << " for output\n"; } - - out << "(set-info :status "; - switch (res) { - case l_true: out << "sat"; break; - case l_false: out << "unsat"; break; - case l_undef: out << "unknown"; break; - } - out << ")\n"; - m_base->display(out, num_assumptions, assumptions); - out << "(check-sat"; - for (unsigned i = 0; i < num_assumptions; ++i) { - out << " " << mk_pp(assumptions[i], m); - } - out << ")"; - out << "(exit)\n"; - ::statistics st; - m_base->collect_statistics(st); - st.update("time", sw.get_seconds()); - st.display_smt2(out); - out.close(); + dump_benchmark(num_assumptions, assumptions, res, sw); } return res; } @@ -171,21 +149,21 @@ public: m_in_delayed_scope = true; } else { - SASSERT(m_pushed); SASSERT(!m_in_delayed_scope); m_base->push(); } } void pop_core(unsigned n) override { - SASSERT(!m_pushed || get_scope_level() > 0); + unsigned lvl = get_scope_level(); + SASSERT(!m_pushed || lvl > 0); if (m_pushed) { SASSERT(!m_in_delayed_scope); m_base->pop(n); - m_pushed = get_scope_level() - n > 0; + m_pushed = lvl - n > 0; } else { - m_in_delayed_scope = get_scope_level() - n > 0; + m_in_delayed_scope = lvl - n > 0; } } @@ -237,11 +215,58 @@ public: m_assertions.reset(); m_pool.refresh(m_base.get()); } + +private: + + void dump_benchmark(unsigned num_assumptions, expr * const * assumptions, lbool res, stopwatch& sw) { + std::string file_name = mk_file_name(); + std::ofstream out(file_name); + if (!out) { + IF_VERBOSE(0, verbose_stream() << "could not open file " << file_name << " for output\n"); + return; + } + + out << "(set-info :status " << lbool2status(res) << ")\n"; + m_base->display(out, num_assumptions, assumptions); + out << "(check-sat"; + for (unsigned i = 0; i < num_assumptions; ++i) { + out << " " << mk_pp(assumptions[i], m); + } + out << ")"; + out << "(exit)\n"; + ::statistics st; + m_base->collect_statistics(st); + st.update("time", sw.get_seconds()); + st.display_smt2(out); + out.close(); + } + + char const* lbool2status(lbool r) const { + switch (r) { + case l_true: return "sat"; + case l_false: return "unsat"; + case l_undef: return "unknown"; + } + return "?"; + } + + std::string mk_file_name() { + std::stringstream file_name; + file_name << "virt_solver"; + if (is_virtual()) file_name << "_" << m_pred->get_decl()->get_name(); + file_name << "_" << (m_dump_counter++) << ".smt2"; + return file_name.str(); + } + }; -solver_pool::solver_pool(solver* base_solver): - m_base_solver(base_solver) -{} +solver_pool::solver_pool(solver* base_solver, unsigned num_pools): + m_base_solver(base_solver), + m_num_pools(num_pools), + m_current_pool(0) +{ + SASSERT(num_pools > 0); +} ptr_vector solver_pool::get_base_solvers() const { @@ -258,10 +283,10 @@ ptr_vector solver_pool::get_base_solvers() const { void solver_pool::collect_statistics(statistics &st) const { ptr_vector solvers = get_base_solvers(); for (solver* s : solvers) s->collect_statistics(st); - st.update("pool_solver.time.total", m_check_watch.get_seconds()); - st.update("pool_solver.time.total.sat", m_check_sat_watch.get_seconds()); - st.update("pool_solver.time.total.undef", m_check_undef_watch.get_seconds()); - st.update("pool_solver.time.proof", m_proof_watch.get_seconds()); + st.update("time.pool_solver.smt.total", m_check_watch.get_seconds()); + st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds()); + st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds()); + st.update("time.pool_solver.proof", m_proof_watch.get_seconds()); st.update("pool_solver.checks", m_stats.m_num_checks); st.update("pool_solver.checks.sat", m_stats.m_num_sat_checks); st.update("pool_solver.checks.undef", m_stats.m_num_undef_checks); @@ -281,24 +306,29 @@ void solver_pool::reset_statistics() { m_proof_watch.reset(); } +/** + \brief Create a fresh solver instance. + The first num_pools solvers are independent and + use a fresh instance of the base solver. + Subsequent solvers reuse the first num_polls base solvers, rotating + among the first num_pools. +*/ solver* solver_pool::mk_solver() { + ref base_solver; ast_manager& m = m_base_solver->get_manager(); - ref base_solver = m_base_solver->translate(m, m_base_solver->get_params()); - app_ref pred(m.mk_true(), m); - pool_solver* solver = alloc(pool_solver, base_solver.get(), *this, pred); - m_solvers.push_back(solver); - return solver; -} - -solver* solver_pool::clone_solver(solver* psolver) { - ast_manager& m = m_base_solver->get_manager(); - solver* base_solver = dynamic_cast(psolver)->base_solver(); + if (m_solvers.size() < m_num_pools) { + base_solver = m_base_solver->translate(m, m_base_solver->get_params()); + } + else { + solver* s = m_solvers[(m_current_pool++) % m_num_pools]; + base_solver = dynamic_cast(s)->base_solver(); + } std::stringstream name; name << "vsolver#" << m_solvers.size(); app_ref pred(m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()), m); - pool_solver* solver = alloc(pool_solver, base_solver, *this, pred); + pool_solver* solver = alloc(pool_solver, base_solver.get(), *this, pred); m_solvers.push_back(solver); - return solver; + return solver; } void solver_pool::reset_solver(solver* s) { diff --git a/src/solver/solver_pool.h b/src/solver/solver_pool.h index a1f650eb0..f279dfd4b 100644 --- a/src/solver/solver_pool.h +++ b/src/solver/solver_pool.h @@ -16,22 +16,16 @@ Author: Notes: - This is a revision of spacer_virtual_solver by Arie Gurfinkel - - -it is not quite the same + there are good reasons to do that management at a higher level. -not the same == in spacer, there is an upper bound on the number of base solvers (i.e., number of pools). -Then the pools are distributed between different predicate transformers. I can't just switch to solver_pool, -since this, in most configuration, will result in either few solvers (which is bad for most of my benchmarks), -or one solver per predicate transformer (which is bad for a few benchmarks with many predicates). - + This is a revision of spacer_virtual_solver + consolidated with spacer_smt_context_manager + by Arie Gurfinkel + Use this module as a replacement for spacer_smt_context_manager. --*/ #ifndef SOLVER_POOL_H_ #define SOLVER_POOL_H_ #include "solver/solver.h" -#include "solver/solver_na2as.h" #include "util/stopwatch.h" class pool_solver; @@ -49,6 +43,8 @@ class solver_pool { }; ref m_base_solver; + unsigned m_num_pools; + unsigned m_current_pool; sref_vector m_solvers; stats m_stats; @@ -62,17 +58,13 @@ class solver_pool { ptr_vector get_base_solvers() const; public: - solver_pool(solver* base_solver); + solver_pool(solver* base_solver, unsigned num_pools); void collect_statistics(statistics &st) const; void reset_statistics(); - // create a fresh pool solver solver* mk_solver(); - // clone an existing pool solver - solver* clone_solver(solver* pool_solver); - void reset_solver(solver* s); }; diff --git a/src/test/solver_pool.cpp b/src/test/solver_pool.cpp index a0b6832c2..4a2e533bf 100644 --- a/src/test/solver_pool.cpp +++ b/src/test/solver_pool.cpp @@ -7,28 +7,35 @@ void tst_solver_pool() { reg_decl_plugins(m); params_ref p; ref base = mk_smt_solver(m, p, symbol::null); - solver_pool pool(base.get()); - ref s1 = pool.mk_solver(); - ref s2 = pool.clone_solver(s1.get()); - ref s3 = pool.clone_solver(s1.get()); - - ref s4 = pool.mk_solver(); - ref s5 = pool.clone_solver(s4.get()); - ref s6 = pool.clone_solver(s4.get()); - expr_ref a(m.mk_const(symbol("a"), m.mk_bool_sort()), m); expr_ref b(m.mk_const(symbol("b"), m.mk_bool_sort()), m); expr_ref c(m.mk_const(symbol("c"), m.mk_bool_sort()), m); expr_ref d(m.mk_const(symbol("d"), m.mk_bool_sort()), m); expr_ref fml(m); fml = m.mk_or(a, b); + base->assert_expr(fml); + + solver_pool pool(base.get(), 3); + + // base solver is cloned so any assertions + // added to base after mk_solver() are ignored. + ref s1 = pool.mk_solver(); + ref s2 = pool.mk_solver(); + ref s3 = pool.mk_solver(); + ref s4 = pool.mk_solver(); + + fml = m.mk_and(b, c); s1->assert_expr(fml); - fml = m.mk_and(a,b); + fml = m.mk_and(a, b); s2->assert_expr(fml); expr_ref_vector asms(m); asms.push_back(m.mk_not(a)); + std::cout << base->check_sat(asms) << "\n"; std::cout << s1->check_sat(asms) << "\n"; std::cout << s2->check_sat(asms) << "\n"; std::cout << s3->check_sat(asms) << "\n"; + std::cout << *s1; + std::cout << *s2; + std::cout << *base; }