mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

spacer: switched to using solver_pool

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-24 15:31:31 -07:00
parent 180d38378a
commit 098e70a9e2
4 changed files with 36 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/spacer/spacer_context.cpp
View file

@ -642,7 +642,7 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
pm(pm), m(pm.get_manager()), pm(pm), m(pm.get_manager()),
ctx(ctx), m_head(head, m), ctx(ctx), m_head(head, m),
m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()), 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_pobs(*this),
m_frames(*this), m_frames(*this),
m_reach_facts(), m_rf_init_sz(0), m_reach_facts(), m_rf_init_sz(0),
@ -2320,9 +2320,9 @@ void context::init_global_smt_params() {
// fparams.m_pi_use_database = true; // 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_params2(p);
m_pm.updt_params3(p);
} }
void context::init_lemma_generalizers() void context::init_lemma_generalizers()
{ {

17
src/muz/spacer/spacer_manager.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "tactic/model_converter.h" #include "tactic/model_converter.h"
#include "smt/smt_solver.h"
namespace spacer { namespace spacer {
class collect_decls_proc { class collect_decls_proc {
@ -176,12 +177,16 @@ static std::vector<std::string> state_suffixes() {
} }
manager::manager(unsigned max_num_contexts, ast_manager& manager) : manager::manager(unsigned max_num_contexts, ast_manager& manager) :
m(manager), m(manager), m_mux(m, state_suffixes()) {
m_mux(m, state_suffixes()),
m_contexts(m, max_num_contexts), m_pool0_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
m_contexts2(m, max_num_contexts), m_pool1_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
m_contexts3(m, max_num_contexts) 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) void manager::add_new_state(func_decl * s)

39
src/muz/spacer/spacer_manager.h
View file

@ -34,9 +34,9 @@ Revision History:
#include "muz/spacer/spacer_util.h" #include "muz/spacer/spacer_util.h"
#include "muz/spacer/spacer_sym_mux.h" #include "muz/spacer/spacer_sym_mux.h"
#include "muz/spacer/spacer_farkas_learner.h" #include "muz/spacer/spacer_farkas_learner.h"
#include "muz/spacer/spacer_smt_context_manager.h"
#include "muz/base/dl_rule.h" #include "muz/base/dl_rule.h"
#include "solver/solver.h"
#include "solver/solver_pool.h"
namespace smt {class context;} namespace smt {class context;}
namespace spacer { namespace spacer {
@ -78,10 +78,13 @@ class manager {
// manager of multiplexed names // manager of multiplexed names
sym_mux m_mux; sym_mux m_mux;
ref<solver> m_pool0_base;
ref<solver> m_pool1_base;
ref<solver> m_pool2_base;
// three solver pools for different queries // three solver pools for different queries
spacer::smt_context_manager m_contexts; scoped_ptr<solver_pool> m_pool0;
spacer::smt_context_manager m_contexts2; scoped_ptr<solver_pool> m_pool1;
spacer::smt_context_manager m_contexts3; scoped_ptr<solver_pool> m_pool2;
unsigned n_index() const { return 0; } unsigned n_index() const { return 0; }
unsigned o_index(unsigned i) const { return i + 1; } unsigned o_index(unsigned i) const { return i + 1; }
@ -154,27 +157,25 @@ public:
// three different solvers with three different sets of parameters // three different solvers with three different sets of parameters
// different solvers are used for different types of queries in spacer // different solvers are used for different types of queries in spacer
solver* mk_fresh() {return m_contexts.mk_fresh();} solver* mk_solver0() {return m_pool0->mk_solver();}
void updt_params(const params_ref &p) {m_contexts.updt_params(p);} void updt_params0(const params_ref &p) {m_pool0->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_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 { void collect_statistics(statistics& st) const {
m_contexts.collect_statistics(st); m_pool0->collect_statistics(st);
m_contexts2.collect_statistics(st); m_pool1->collect_statistics(st);
m_contexts3.collect_statistics(st); m_pool2->collect_statistics(st);
} }
void reset_statistics() { void reset_statistics() {
m_contexts.reset_statistics(); m_pool0->reset_statistics();
m_contexts2.reset_statistics(); m_pool1->reset_statistics();
m_contexts3.reset_statistics(); m_pool2->reset_statistics();
} }
}; };

4
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -55,8 +55,8 @@ prop_solver::prop_solver(spacer::manager& pm,
m_use_push_bg(p.spacer_keep_proxy()) m_use_push_bg(p.spacer_keep_proxy())
{ {
m_solvers[0] = pm.mk_fresh(); m_solvers[0] = pm.mk_solver0();
m_solvers[1] = pm.mk_fresh2(); m_solvers[1] = pm.mk_solver1();
m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]), m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]),
p.spacer_iuc(), p.spacer_iuc(),