From b649cd93cb259d357754737c26a7a57b298fa191 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 May 2018 07:40:37 -0700 Subject: [PATCH] change pool solver to enable external control of pool allocation Signed-off-by: Nikolaj Bjorner --- src/solver/solver_pool.cpp | 44 ++++++++++++++++++-------------------- src/solver/solver_pool.h | 21 +++++++++++++----- src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/solver_pool.cpp | 34 +++++++++++++++++++++++++++++ 5 files changed, 73 insertions(+), 28 deletions(-) create mode 100644 src/test/solver_pool.cpp diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 6d08b95af..132a2bec4 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,7 +33,6 @@ 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): @@ -240,10 +239,8 @@ public: } }; -solver_pool::solver_pool(solver* base_solver, unsigned num_solvers_per_pool): - m_base_solver(base_solver), - m_num_solvers_per_pool(num_solvers_per_pool), - m_num_solvers_in_last_pool(0) +solver_pool::solver_pool(solver* base_solver): + m_base_solver(base_solver) {} @@ -261,10 +258,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("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.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("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); @@ -285,24 +282,25 @@ void solver_pool::reset_statistics() { } solver* solver_pool::mk_solver() { - ref base_solver; ast_manager& m = m_base_solver->get_manager(); - if (m_solvers.empty() || m_num_solvers_in_last_pool == m_num_solvers_per_pool) { - base_solver = m_base_solver->translate(m, m_base_solver->get_params()); - m_num_solvers_in_last_pool = 0; - } - else { - base_solver = dynamic_cast(m_solvers.back())->base_solver(); - } - m_num_solvers_in_last_pool++; - std::stringstream name; - name << "vsolver#" << m_solvers.size(); - app_ref pred(m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()), m); + 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(); + 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); + m_solvers.push_back(solver); + return solver; +} + void solver_pool::reset_solver(solver* s) { pool_solver* ps = dynamic_cast(s); SASSERT(ps); diff --git a/src/solver/solver_pool.h b/src/solver/solver_pool.h index d676ca54d..a1f650eb0 100644 --- a/src/solver/solver_pool.h +++ b/src/solver/solver_pool.h @@ -18,11 +18,20 @@ 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). + + --*/ #ifndef SOLVER_POOL_H_ #define SOLVER_POOL_H_ #include "solver/solver.h" +#include "solver/solver_na2as.h" #include "util/stopwatch.h" class pool_solver; @@ -39,11 +48,9 @@ class solver_pool { void reset() { memset(this, 0, sizeof(*this)); } }; - ref m_base_solver; - unsigned m_num_solvers_per_pool; - unsigned m_num_solvers_in_last_pool; + ref m_base_solver; sref_vector m_solvers; - stats m_stats; + stats m_stats; stopwatch m_check_watch; stopwatch m_check_sat_watch; @@ -55,13 +62,17 @@ class solver_pool { ptr_vector get_base_solvers() const; public: - solver_pool(solver* base_solver, unsigned num_solvers_per_pool); + solver_pool(solver* base_solver); 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/CMakeLists.txt b/src/test/CMakeLists.txt index b487fe9ba..da4194a2c 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -102,6 +102,7 @@ add_executable(test-z3 small_object_allocator.cpp smt2print_parse.cpp smt_context.cpp + solver_pool.cpp sorting_network.cpp stack.cpp string_buffer.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 64f754667..c1f169a3a 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -248,6 +248,7 @@ int main(int argc, char ** argv) { TST_ARGV(sat_local_search); TST_ARGV(cnf_backbones); TST(bdd); + TST(solver_pool); //TST_ARGV(hs); } diff --git a/src/test/solver_pool.cpp b/src/test/solver_pool.cpp new file mode 100644 index 000000000..a0b6832c2 --- /dev/null +++ b/src/test/solver_pool.cpp @@ -0,0 +1,34 @@ +#include "ast/reg_decl_plugins.h" +#include "solver/solver_pool.h" +#include "smt/smt_solver.h" + +void tst_solver_pool() { + ast_manager m; + 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); + s1->assert_expr(fml); + fml = m.mk_and(a,b); + s2->assert_expr(fml); + expr_ref_vector asms(m); + asms.push_back(m.mk_not(a)); + std::cout << s1->check_sat(asms) << "\n"; + std::cout << s2->check_sat(asms) << "\n"; + std::cout << s3->check_sat(asms) << "\n"; +}