mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

spacer: let pool_solver own the solver

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-24 16:25:55 -07:00
parent 15d0fd4b42
commit 14b9dd2cd7
2 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -179,13 +179,16 @@ static std::vector<std::string> state_suffixes() {
manager::manager(unsigned max_num_contexts, ast_manager& manager) :
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);
ref<solver> pool0_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
ref<solver> pool1_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
ref<solver> 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);
m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts);
m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts);
m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts);
}

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

@ -79,9 +79,6 @@ class manager {
// manager of multiplexed names
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
scoped_ptr<solver_pool> m_pool0;
scoped_ptr<solver_pool> m_pool1;