change pool solver to enable external control of pool allocation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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> solver_pool::get_base_solvers() const {
 void solver_pool::collect_statistics(statistics &st) const {
     ptr_vector<solver> 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<solver> 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<pool_solver*>(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<solver> 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<pool_solver*>(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<pool_solver*>(s);
     SASSERT(ps);

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<solver>        m_base_solver;
-    unsigned           m_num_solvers_per_pool;
-    unsigned           m_num_solvers_in_last_pool;
+    ref<solver>         m_base_solver;
     sref_vector<solver> 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<solver> 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);
 };
 

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

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);
 }
 

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<solver> base = mk_smt_solver(m, p, symbol::null);
+    solver_pool pool(base.get());
+
+    ref<solver> s1 = pool.mk_solver();
+    ref<solver> s2 = pool.clone_solver(s1.get());
+    ref<solver> s3 = pool.clone_solver(s1.get());
+
+    ref<solver> s4 = pool.mk_solver();
+    ref<solver> s5 = pool.clone_solver(s4.get());
+    ref<solver> 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";
+}