From 098e70a9e23fdd816184032941c93ee0b586aef2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 24 May 2018 15:31:31 -0700 Subject: [PATCH] spacer: switched to using solver_pool --- src/muz/spacer/spacer_context.cpp | 6 ++--- src/muz/spacer/spacer_manager.cpp | 17 +++++++----- src/muz/spacer/spacer_manager.h | 39 ++++++++++++++------------- src/muz/spacer/spacer_prop_solver.cpp | 4 +-- 4 files changed, 36 insertions(+), 30 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index acc7fb268..3c94e5521 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -642,7 +642,7 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), ctx(ctx), m_head(head, m), m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()), - m_reach_ctx (pm.mk_fresh3 ()), + m_reach_ctx (pm.mk_solver2()), m_pobs(*this), m_frames(*this), m_reach_facts(), m_rf_init_sz(0), @@ -2320,9 +2320,9 @@ void context::init_global_smt_params() { // fparams.m_pi_use_database = true; } - m_pm.updt_params(p); + m_pm.updt_params0(p); + m_pm.updt_params1(p); m_pm.updt_params2(p); - m_pm.updt_params3(p); } void context::init_lemma_generalizers() { diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index 04d3c09d4..a281cac81 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -30,6 +30,7 @@ Revision History: #include "model/model_smt2_pp.h" #include "tactic/model_converter.h" +#include "smt/smt_solver.h" namespace spacer { class collect_decls_proc { @@ -176,12 +177,16 @@ static std::vector state_suffixes() { } manager::manager(unsigned max_num_contexts, ast_manager& manager) : - m(manager), - m_mux(m, state_suffixes()), - m_contexts(m, max_num_contexts), - m_contexts2(m, max_num_contexts), - m_contexts3(m, max_num_contexts) -{} + m(manager), m_mux(m, state_suffixes()) { + + m_pool0_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null); + m_pool1_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null); + m_pool2_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null); + + m_pool0 = alloc(solver_pool, m_pool0_base.get(), max_num_contexts); + m_pool1 = alloc(solver_pool, m_pool1_base.get(), max_num_contexts); + m_pool2 = alloc(solver_pool, m_pool2_base.get(), max_num_contexts); +} void manager::add_new_state(func_decl * s) diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index 471090c30..f7d43ccb0 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -34,9 +34,9 @@ Revision History: #include "muz/spacer/spacer_util.h" #include "muz/spacer/spacer_sym_mux.h" #include "muz/spacer/spacer_farkas_learner.h" -#include "muz/spacer/spacer_smt_context_manager.h" #include "muz/base/dl_rule.h" - +#include "solver/solver.h" +#include "solver/solver_pool.h" namespace smt {class context;} namespace spacer { @@ -78,10 +78,13 @@ class manager { // manager of multiplexed names sym_mux m_mux; + ref m_pool0_base; + ref m_pool1_base; + ref m_pool2_base; // three solver pools for different queries - spacer::smt_context_manager m_contexts; - spacer::smt_context_manager m_contexts2; - spacer::smt_context_manager m_contexts3; + scoped_ptr m_pool0; + scoped_ptr m_pool1; + scoped_ptr m_pool2; unsigned n_index() const { return 0; } unsigned o_index(unsigned i) const { return i + 1; } @@ -154,27 +157,25 @@ public: // three different solvers with three different sets of parameters // different solvers are used for different types of queries in spacer - solver* mk_fresh() {return m_contexts.mk_fresh();} - void updt_params(const params_ref &p) {m_contexts.updt_params(p);} - - solver* mk_fresh2() {return m_contexts2.mk_fresh();} - void updt_params2(const params_ref &p) {m_contexts2.updt_params(p);} - - solver* mk_fresh3() {return m_contexts3.mk_fresh();} - void updt_params3(const params_ref &p) {m_contexts3.updt_params(p);} + solver* mk_solver0() {return m_pool0->mk_solver();} + void updt_params0(const params_ref &p) {m_pool0->updt_params(p);} + solver* mk_solver1() {return m_pool1->mk_solver();} + void updt_params1(const params_ref &p) {m_pool1->updt_params(p);} + solver* mk_solver2() {return m_pool2->mk_solver();} + void updt_params2(const params_ref &p) {m_pool2->updt_params(p);} void collect_statistics(statistics& st) const { - m_contexts.collect_statistics(st); - m_contexts2.collect_statistics(st); - m_contexts3.collect_statistics(st); + m_pool0->collect_statistics(st); + m_pool1->collect_statistics(st); + m_pool2->collect_statistics(st); } void reset_statistics() { - m_contexts.reset_statistics(); - m_contexts2.reset_statistics(); - m_contexts3.reset_statistics(); + m_pool0->reset_statistics(); + m_pool1->reset_statistics(); + m_pool2->reset_statistics(); } }; diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index a4ea79a25..6b29df074 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -55,8 +55,8 @@ prop_solver::prop_solver(spacer::manager& pm, m_use_push_bg(p.spacer_keep_proxy()) { - m_solvers[0] = pm.mk_fresh(); - m_solvers[1] = pm.mk_fresh2(); + m_solvers[0] = pm.mk_solver0(); + m_solvers[1] = pm.mk_solver1(); m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]), p.spacer_iuc(),