From 15d0fd4b4236a66c2511048cdeae64e820d705c6 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 24 May 2018 15:35:46 -0700 Subject: [PATCH] spacer: removed virtual_solver This commit removes virtual_solver and smt_context_manager that have been migrated into solver_pool --- src/muz/spacer/CMakeLists.txt | 2 - src/muz/spacer/spacer_manager.h | 1 + src/muz/spacer/spacer_prop_solver.h | 1 - src/muz/spacer/spacer_smt_context_manager.cpp | 88 ----- src/muz/spacer/spacer_smt_context_manager.h | 69 ---- src/muz/spacer/spacer_virtual_solver.cpp | 333 ------------------ src/muz/spacer/spacer_virtual_solver.h | 150 -------- 7 files changed, 1 insertion(+), 643 deletions(-) delete mode 100644 src/muz/spacer/spacer_smt_context_manager.cpp delete mode 100644 src/muz/spacer/spacer_smt_context_manager.h delete mode 100644 src/muz/spacer/spacer_virtual_solver.cpp delete mode 100644 src/muz/spacer/spacer_virtual_solver.h diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index a7bc74b88..68464a40d 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -8,11 +8,9 @@ z3_add_component(spacer spacer_generalizers.cpp spacer_manager.cpp spacer_prop_solver.cpp - spacer_smt_context_manager.cpp spacer_sym_mux.cpp spacer_util.cpp spacer_iuc_solver.cpp - spacer_virtual_solver.cpp spacer_legacy_mbp.cpp spacer_proof_utils.cpp spacer_unsat_core_learner.cpp diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index f7d43ccb0..4c3d861cb 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -13,6 +13,7 @@ Abstract: Author: Krystof Hoder (t-khoder) 2011-8-25. + Arie Gurfinkel Revision History: diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 27b2fd51d..e87732e94 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -30,7 +30,6 @@ Revision History: #include "util/util.h" #include "util/vector.h" #include "muz/spacer/spacer_manager.h" -#include "muz/spacer/spacer_smt_context_manager.h" #include "muz/spacer/spacer_iuc_solver.h" struct fixedpoint_params; diff --git a/src/muz/spacer/spacer_smt_context_manager.cpp b/src/muz/spacer/spacer_smt_context_manager.cpp deleted file mode 100644 index 78f01b6e5..000000000 --- a/src/muz/spacer/spacer_smt_context_manager.cpp +++ /dev/null @@ -1,88 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - spacer_smt_context_manager.cpp - -Abstract: - - Manager of smt contexts - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-26. - Arie Gurfinkel -Revision History: - ---*/ - - -#include "ast/ast_pp.h" -#include "ast/ast_pp_util.h" -#include "ast/ast_smt_pp.h" - -#include "smt/smt_context.h" -#include "smt/params/smt_params.h" -#include "smt/smt_solver.h" - -#include "muz/spacer/spacer_util.h" -#include "muz/spacer/spacer_smt_context_manager.h" -namespace spacer { - -smt_context_manager::smt_context_manager(ast_manager &m, - unsigned max_num_contexts, - const params_ref &p) : - m(m), - m_params(p), - m_max_num_contexts(max_num_contexts), - m_num_contexts(0) { m_stats.reset();} - - -smt_context_manager::~smt_context_manager() -{ - std::for_each(m_solvers.begin(), m_solvers.end(), - delete_proc()); - m_solvers.reset(); - m_base_solvers.reset(); -} - -void smt_context_manager::updt_params(params_ref const &p) { - m_params.append(p); - for (auto *s : m_base_solvers) {s->updt_params(m_params);} -} - -virtual_solver* smt_context_manager::mk_fresh() -{ - ++m_num_contexts; - virtual_solver_factory *solver_factory = nullptr; - - if (m_max_num_contexts == 0 || m_solvers.size() < m_max_num_contexts) { - m_base_solvers.push_back(mk_smt_solver(m, m_params, symbol::null)); - m_solvers.push_back(alloc(spacer::virtual_solver_factory, - *m_base_solvers.back())); - solver_factory = m_solvers.back(); - } - else { - solver_factory = m_solvers[(m_num_contexts - 1) % m_max_num_contexts]; - } - - return solver_factory->mk_solver(); -} - -void smt_context_manager::collect_statistics(statistics& st) const -{ - for (unsigned i = 0; i < m_solvers.size(); ++i) { - m_solvers[i]->collect_statistics(st); - } -} - -void smt_context_manager::reset_statistics() -{ - for (unsigned i = 0; i < m_solvers.size(); ++i) { - m_solvers[i]->reset_statistics(); - } -} - - -}; diff --git a/src/muz/spacer/spacer_smt_context_manager.h b/src/muz/spacer/spacer_smt_context_manager.h deleted file mode 100644 index a62aba6cd..000000000 --- a/src/muz/spacer/spacer_smt_context_manager.h +++ /dev/null @@ -1,69 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - spacer_smt_context_manager.h - -Abstract: - - Manager of smt contexts - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-26. - Arie Gurfinkel -Revision History: - ---*/ - -#ifndef _SPACER_SMT_CONTEXT_MANAGER_H_ -#define _SPACER_SMT_CONTEXT_MANAGER_H_ - -#include "util/stopwatch.h" - -#include "smt/smt_kernel.h" -#include "muz/base/dl_util.h" -#include "muz/spacer/spacer_virtual_solver.h" - -namespace spacer { - -class smt_context_manager { - - struct stats { - unsigned m_num_smt_checks; - unsigned m_num_sat_smt_checks; - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - ast_manager& m; - params_ref m_params; - unsigned m_max_num_contexts; - sref_vector m_base_solvers; - ptr_vector m_solvers; - unsigned m_num_contexts; - - - stats m_stats; - stopwatch m_check_watch; - stopwatch m_check_sat_watch; - -public: - smt_context_manager(ast_manager& m, unsigned max_num_contexts = 1, - const params_ref &p = params_ref::get_empty()); - - ~smt_context_manager(); - virtual_solver* mk_fresh(); - - void collect_statistics(statistics& st) const; - void reset_statistics(); - - void updt_params(params_ref const &p); - - -}; - -}; - -#endif diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp deleted file mode 100644 index a1a1a7eec..000000000 --- a/src/muz/spacer/spacer_virtual_solver.cpp +++ /dev/null @@ -1,333 +0,0 @@ -/** -Copyright (c) 2017 Arie Gurfinkel - -Module Name: - - spacer_virtual_solver.cpp - -Abstract: - - multi-solver view of a single solver - -Author: - - Arie Gurfinkel - -Notes: - ---*/ - -#include "muz/spacer/spacer_virtual_solver.h" -#include "ast/ast_util.h" -#include "ast/ast_pp_util.h" -#include "muz/spacer/spacer_util.h" -#include "ast/rewriter/bool_rewriter.h" - -#include "ast/proofs/proof_checker.h" -#include "ast/proofs/proof_utils.h" - -#include "ast/scoped_proof.h" - -#include "smt/smt_kernel.h" - -namespace spacer { -virtual_solver::virtual_solver(virtual_solver_factory &factory, app* pred) : - solver_na2as(factory.get_manager()), - m_factory(factory), - m(factory.get_manager()), - m_context(factory.get_base_solver()), - m_pred(pred, m), - m_virtual(!m.is_true(pred)), - m_assertions(m), - m_head(0), - m_flat(m), - m_pushed(false), - m_in_delay_scope(false), - m_dump_benchmarks(false /*factory.fparams().m_dump_benchmarks*/), - m_dump_counter(0), - m_proof(m) -{ - // -- insert m_pred->true background assumption this will not - // -- change m_context, but will add m_pred to - // -- the private field solver_na2as::m_assumptions - if (m_virtual) - { solver_na2as::assert_expr_core2(m.mk_true(), m_pred); } -} - -virtual_solver::~virtual_solver() -{ - SASSERT(!m_pushed || get_scope_level() > 0); - if (m_pushed) { pop(get_scope_level()); } - - if (m_virtual) { - m_pred = m.mk_not(m_pred); - m_context.assert_expr(m_pred); - } -} - -namespace { - - -// TBD: move to ast/proofs/elim_aux_assertions - - -} - -proof *virtual_solver::get_proof() -{ - scoped_watch _t_(m_factory.m_proof_watch); - - if (!m_proof.get()) { - elim_aux_assertions pc(m_pred); - m_proof = m_context.get_proof(); - pc(m, m_proof.get(), m_proof); - } - return m_proof.get(); -} - -bool virtual_solver::is_aux_predicate(expr *p) -{return is_app(p) && to_app(p) == m_pred.get();} - -lbool virtual_solver::check_sat_core(unsigned num_assumptions, - expr *const * assumptions) -{ - SASSERT(!m_pushed || get_scope_level() > 0); - m_proof.reset(); - scoped_watch _t_(m_factory.m_check_watch); - m_factory.m_stats.m_num_smt_checks++; - - stopwatch sw; - sw.start(); - internalize_assertions(); - if (false) { - std::stringstream file_name; - file_name << "virt_solver"; - if (m_virtual) { file_name << "_" << m_pred->get_decl()->get_name(); } - file_name << "_" << (m_dump_counter++) << ".smt2"; - - verbose_stream() << "Dumping SMT2 benchmark: " << file_name.str() << "\n"; - - std::ofstream out(file_name.str().c_str()); - - to_smt2_benchmark(out, m_context, num_assumptions, assumptions, - "virt_solver"); - - out << "(exit)\n"; - out.close(); - } - lbool res = m_context.check_sat(num_assumptions, assumptions); - sw.stop(); - if (res == l_true) { - m_factory.m_check_sat_watch.add(sw); - m_factory.m_stats.m_num_sat_smt_checks++; - } else if (res == l_undef) { - m_factory.m_check_undef_watch.add(sw); - m_factory.m_stats.m_num_undef_smt_checks++; - } - set_status(res); - - if (false /*m_dump_benchmarks && - sw.get_seconds() >= m_factory.fparams().m_dump_min_time*/) { - std::stringstream file_name; - file_name << "virt_solver"; - if (m_virtual) { file_name << "_" << m_pred->get_decl()->get_name(); } - file_name << "_" << (m_dump_counter++) << ".smt2"; - - std::ofstream out(file_name.str().c_str()); - - - out << "(set-info :status "; - if (res == l_true) { out << "sat"; } - else if (res == l_false) { out << "unsat"; } - else { out << "unknown"; } - out << ")\n"; - - to_smt2_benchmark(out, m_context, num_assumptions, assumptions, - "virt_solver"); - - out << "(exit)\n"; - ::statistics st; - m_context.collect_statistics(st); - st.update("time", sw.get_seconds()); - st.display_smt2(out); - - - if (false /* m_factory.fparams().m_dump_recheck */) { - scoped_no_proof _no_proof_(m); - smt_params p; - stopwatch sw2; - smt::kernel kernel(m, p); - for (unsigned i = 0, sz = m_context.get_num_assertions(); i < sz; ++i) - { kernel.assert_expr(m_context.get_assertion(i)); } - sw2.start(); - kernel.check(num_assumptions, assumptions); - sw2.stop(); - verbose_stream() << file_name.str() << " :orig " - << sw.get_seconds() << " :new " << sw2.get_seconds(); - - out << ";; :orig " << sw.get_seconds() - << " :new " << sw2.get_seconds() << "\n" - << ";; :new is time to solve with fresh smt::kernel\n"; - } - - out.close(); - } - - - return res; -} - -void virtual_solver::push_core() -{ - SASSERT(!m_pushed || get_scope_level() > 0); - if (m_in_delay_scope) { - // second push - internalize_assertions(); - m_context.push(); - m_pushed = true; - m_in_delay_scope = false; - } - - if (!m_pushed) { m_in_delay_scope = true; } - else { - SASSERT(m_pushed); - SASSERT(!m_in_delay_scope); - m_context.push(); - } -} -void virtual_solver::pop_core(unsigned n) { - SASSERT(!m_pushed || get_scope_level() > 0); - if (m_pushed) { - SASSERT(!m_in_delay_scope); - m_context.pop(n); - m_pushed = get_scope_level() - n > 0; - } - else { - m_in_delay_scope = get_scope_level() - n > 0; - } -} - -void virtual_solver::get_unsat_core(ptr_vector &r) -{ - ptr_vector core; - m_context.get_unsat_core(core); - - for (unsigned i = 0, sz = core.size(); i < sz; ++i) { - if (is_aux_predicate(core.get(i))) { continue; } - r.push_back(core.get(i)); - } -} - -void virtual_solver::assert_expr_core(expr *e) -{ - SASSERT(!m_pushed || get_scope_level() > 0); - if (m.is_true(e)) { return; } - if (m_in_delay_scope) { - internalize_assertions(); - m_context.push(); - m_pushed = true; - m_in_delay_scope = false; - } - - if (m_pushed) - { m_context.assert_expr(e); } - else { - m_flat.push_back(e); - flatten_and(m_flat); - m_assertions.append(m_flat); - m_flat.reset(); - } -} -void virtual_solver::internalize_assertions() -{ - SASSERT(!m_pushed || m_head == m_assertions.size()); - for (unsigned sz = m_assertions.size(); m_head < sz; ++m_head) { - expr_ref f(m); - f = m.mk_implies(m_pred, (m_assertions.get(m_head))); - m_context.assert_expr(f); - } -} - -void virtual_solver::get_labels(svector &r) -{m_context.get_labels(r);} - -solver* virtual_solver::translate(ast_manager& m, params_ref const& p) -{ - UNREACHABLE(); - return nullptr; -} -void virtual_solver::updt_params(params_ref const &p) {m_context.updt_params(p);} -void virtual_solver::reset_params(params_ref const &p) {m_context.reset_params(p);} -const params_ref &virtual_solver::get_params() const {return m_context.get_params();} -void virtual_solver::push_params(){m_context.push_params();} -void virtual_solver::pop_params(){m_context.pop_params();} -void virtual_solver::collect_param_descrs(param_descrs &r) { m_context.collect_param_descrs(r); } -void virtual_solver::set_produce_models(bool f) { m_context.set_produce_models(f); } - -void virtual_solver::to_smt2_benchmark(std::ostream &out, - solver &context, - unsigned num_assumptions, - expr * const * assumptions, - char const * name, - symbol const &logic, - char const * status, - char const * attributes) -{ - ast_pp_util pp(m); - expr_ref_vector asserts(m); - - context.get_assertions(asserts); - pp.collect(asserts); - pp.collect(num_assumptions, assumptions); - pp.display_decls(out); - pp.display_asserts(out, asserts); - out << "(check-sat "; - for (unsigned i = 0; i < num_assumptions; ++i) - { out << mk_pp(assumptions[i], m) << " "; } - out << ")\n"; -} - - -virtual_solver_factory::virtual_solver_factory(solver &base) : - m(base.get_manager()), m_context(base) {m_stats.reset();} - -virtual_solver* virtual_solver_factory::mk_solver() -{ - std::stringstream name; - name << "vsolver#" << m_solvers.size(); - app_ref pred(m); - pred = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()); - SASSERT(m_context.get_scope_level() == 0); - m_solvers.push_back(alloc(virtual_solver, *this, pred)); - return m_solvers.back(); -} - -void virtual_solver_factory::collect_statistics(statistics &st) const -{ - m_context.collect_statistics(st); - st.update("time.virtual_solver.smt.total", m_check_watch.get_seconds()); - st.update("time.virtual_solver.smt.total.sat", m_check_sat_watch.get_seconds()); - st.update("time.virtual_solver.smt.total.undef", m_check_undef_watch.get_seconds()); - st.update("time.virtual_solver.proof", m_proof_watch.get_seconds()); - st.update("virtual_solver.checks", m_stats.m_num_smt_checks); - st.update("virtual_solver.checks.sat", m_stats.m_num_sat_smt_checks); - st.update("virtual_solver.checks.undef", m_stats.m_num_undef_smt_checks); -} -void virtual_solver_factory::reset_statistics() -{ - m_stats.reset(); - m_check_sat_watch.reset(); - m_check_undef_watch.reset(); - m_check_watch.reset(); - m_proof_watch.reset(); -} - -virtual_solver_factory::~virtual_solver_factory() -{ - for (unsigned i = 0, e = m_solvers.size(); i < e; ++i) - { dealloc(m_solvers[i]); } -} - - - -} diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h deleted file mode 100644 index e5db5e396..000000000 --- a/src/muz/spacer/spacer_virtual_solver.h +++ /dev/null @@ -1,150 +0,0 @@ -/** -Copyright (c) 2017 Arie Gurfinkel - -Module Name: - - spacer_virtual_solver.h - -Abstract: - - multi-solver view of a single solver - -Author: - - Arie Gurfinkel - -Notes: - ---*/ -#ifndef SPACER_VIRTUAL_SOLVER_H_ -#define SPACER_VIRTUAL_SOLVER_H_ -#include"ast/ast.h" -#include"util/params.h" -#include"solver/solver_na2as.h" -#include"smt/params/smt_params.h" -#include"util/stopwatch.h" -namespace spacer { -class virtual_solver_factory; - -class virtual_solver : public solver_na2as { - friend class virtual_solver_factory; - -private: - virtual_solver_factory &m_factory; - ast_manager &m; - solver &m_context; - app_ref m_pred; - - bool m_virtual; - expr_ref_vector m_assertions; - unsigned m_head; - // temporary to flatten conjunction - expr_ref_vector m_flat; - - bool m_pushed; - bool m_in_delay_scope; - bool m_dump_benchmarks; - unsigned m_dump_counter; - - proof_ref m_proof; - - virtual_solver(virtual_solver_factory &factory, app* pred); - - bool is_aux_predicate(expr *p); - void internalize_assertions(); - void to_smt2_benchmark(std::ostream &out, - solver &context, - unsigned num_assumptions, - expr * const * assumptions, - char const * name = "benchmarks", - symbol const &logic = symbol::null, - char const * status = "unknown", - char const * attributes = ""); - -public: - ~virtual_solver() override; - unsigned get_num_assumptions() const override - { - unsigned sz = solver_na2as::get_num_assumptions(); - return m_virtual ? sz - 1 : sz; - } - expr* get_assumption(unsigned idx) const override - { - if(m_virtual) { idx++; } - return solver_na2as::get_assumption(idx); - } - - - void get_unsat_core(ptr_vector &r) override; - void assert_expr_core(expr *e) override; - void collect_statistics(statistics &st) const override {m_context.collect_statistics(st);} - void get_model_core(model_ref &m) override {m_context.get_model(m);} - proof* get_proof() override; - std::string reason_unknown() const override - {return m_context.reason_unknown();} - void set_reason_unknown(char const *msg) override - {m_context.set_reason_unknown(msg);} - ast_manager& get_manager() const override {return m;} - void get_labels(svector &r) override; - void set_produce_models(bool f) override; - smt_params &fparams(); - expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } - void set_progress_callback(progress_callback *callback) override {UNREACHABLE();} - - solver *translate(ast_manager &m, params_ref const &p) override; - - void updt_params(params_ref const &p) override; - void reset_params(params_ref const& p) override; - params_ref const& get_params() const override; - void collect_param_descrs(param_descrs &r) override; - void push_params() override; - void pop_params() override; - - -protected: - lbool check_sat_core(unsigned num_assumptions, expr *const * assumptions) override; - void push_core() override; - void pop_core(unsigned n) override; -}; - -/// multi-solver abstraction on top of a single solver -class virtual_solver_factory { - friend class virtual_solver; -private: - ast_manager &m; - solver &m_context; - /// solvers managed by this factory - ptr_vector m_solvers; - - struct stats { - unsigned m_num_smt_checks; - unsigned m_num_sat_smt_checks; - unsigned m_num_undef_smt_checks; - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - stats m_stats; - stopwatch m_check_watch; - stopwatch m_check_sat_watch; - stopwatch m_check_undef_watch; - stopwatch m_proof_watch; - - - solver &get_base_solver() {return m_context;} - ast_manager &get_manager() {return m;} - -public: - virtual_solver_factory(solver &base); - virtual ~virtual_solver_factory(); - virtual_solver* mk_solver(); - void collect_statistics(statistics &st) const; - void reset_statistics(); - void updt_params(params_ref const &p) {m_context.updt_params(p);} - void collect_param_descrs(param_descrs &r) {m_context.collect_param_descrs(r);} -}; - -} - - -#endif