From 178e5b31e8fbc7073cefd4c85de8371721819442 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 21 Dec 2018 22:49:06 +0000 Subject: [PATCH] spread a few anonymous namespaces and remove some m_imp idioms --- .gitignore | 1 + src/qe/qe_lite.cpp | 8 +- src/qe/qe_lite.h | 5 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 64 +++++------- src/tactic/bv/bv_size_reduction_tactic.h | 5 +- src/tactic/bv/elim_small_bv_tactic.cpp | 108 ++++++++------------- src/tactic/bv/elim_small_bv_tactic.h | 5 +- 7 files changed, 71 insertions(+), 125 deletions(-) diff --git a/.gitignore b/.gitignore index b7e4a0186..e189a9569 100644 --- a/.gitignore +++ b/.gitignore @@ -43,6 +43,7 @@ bld_dbg/* bld_rel/* bld_dbg_x64/* bld_rel_x64/* +.vscode # Auto generated files. config.log config.status diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 3226f7554..4585c88c1 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2370,6 +2370,7 @@ void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_re (*m_impl)(index_set, index_of_bound, fmls); } +namespace { class qe_lite_tactic : public tactic { struct imp { @@ -2494,7 +2495,6 @@ public: (*m_imp)(in, result); } - void collect_statistics(statistics & st) const override { // m_imp->collect_statistics(st); } @@ -2503,14 +2503,14 @@ public: // m_imp->reset_statistics(); } - void cleanup() override { ast_manager & m = m_imp->m; - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + m_imp->~imp(); + m_imp = new (m_imp) imp(m, m_params); } }; +} tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) { return alloc(qe_lite_tactic, m, p); diff --git a/src/qe/qe_lite.h b/src/qe/qe_lite.h index 63ad8bedd..3251fa3f8 100644 --- a/src/qe/qe_lite.h +++ b/src/qe/qe_lite.h @@ -18,8 +18,7 @@ Revision History: --*/ -#ifndef QE_LITE_H_ -#define QE_LITE_H_ +#pragma once #include "ast/ast.h" #include "util/uint_set.h" @@ -67,5 +66,3 @@ tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref()) /* ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)") */ - -#endif diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 964102825..fd1d1499b 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -27,28 +27,8 @@ Notes: #include "tactic/generic_model_converter.h" #include "ast/ast_smt2_pp.h" +namespace { class bv_size_reduction_tactic : public tactic { - struct imp; - imp * m_imp; -public: - bv_size_reduction_tactic(ast_manager & m); - - tactic * translate(ast_manager & m) override { - return alloc(bv_size_reduction_tactic, m); - } - - ~bv_size_reduction_tactic() override; - - void operator()(goal_ref const & g, goal_ref_buffer & result) override; - - void cleanup() override; -}; - -tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(bv_size_reduction_tactic, m)); -} - -struct bv_size_reduction_tactic::imp { typedef rational numeral; typedef generic_model_converter bv_size_reduction_mc; @@ -63,12 +43,29 @@ struct bv_size_reduction_tactic::imp { scoped_ptr m_replacer; bool m_produce_models; - imp(ast_manager & _m): - m(_m), +public: + bv_size_reduction_tactic(ast_manager & m) : + m(m), m_util(m), m_replacer(mk_default_expr_replacer(m)) { } + tactic * translate(ast_manager & m) override { + return alloc(bv_size_reduction_tactic, m); + } + + void operator()(goal_ref const & g, goal_ref_buffer & result) override; + + void cleanup() override { + m_signed_lowers.reset(); + m_signed_uppers.reset(); + m_unsigned_lowers.reset(); + m_unsigned_uppers.reset(); + m_mc = nullptr; + m_fmc = nullptr; + m_replacer->reset(); + } + void update_signed_lower(app * v, numeral const & k) { // k <= v obj_map::obj_map_entry * entry = m_signed_lowers.insert_if_not_there2(v, k); @@ -178,7 +175,7 @@ struct bv_size_reduction_tactic::imp { throw tactic_exception(m.limit().get_cancel_msg()); } - void operator()(goal & g, model_converter_ref & mc) { + void run(goal & g, model_converter_ref & mc) { if (g.inconsistent()) return; TRACE("before_bv_size_reduction", g.display(tout);); @@ -373,14 +370,6 @@ struct bv_size_reduction_tactic::imp { }; -bv_size_reduction_tactic::bv_size_reduction_tactic(ast_manager & m) { - m_imp = alloc(imp, m); -} - -bv_size_reduction_tactic::~bv_size_reduction_tactic() { - dealloc(m_imp); -} - void bv_size_reduction_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { SASSERT(g->is_well_sorted()); @@ -388,17 +377,14 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g, fail_if_unsat_core_generation("bv-size-reduction", g); result.reset(); model_converter_ref mc; - m_imp->operator()(*(g.get()), mc); + run(*(g.get()), mc); g->inc_depth(); g->add(mc.get()); result.push_back(g.get()); SASSERT(g->is_well_sorted()); } - - -void bv_size_reduction_tactic::cleanup() { - ast_manager & m = m_imp->m; - m_imp->~imp(); - new (m_imp) imp(m); } +tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(bv_size_reduction_tactic, m)); +} diff --git a/src/tactic/bv/bv_size_reduction_tactic.h b/src/tactic/bv/bv_size_reduction_tactic.h index 4a24a1d78..1bb512f3f 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.h +++ b/src/tactic/bv/bv_size_reduction_tactic.h @@ -21,8 +21,7 @@ Author: Notes: --*/ -#ifndef BV_SIZE_REDUCTION_TACTIC_H_ -#define BV_SIZE_REDUCTION_TACTIC_H_ +#pragma once #include "util/params.h" class ast_manager; @@ -32,5 +31,3 @@ tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p = par /* ADD_TACTIC("reduce-bv-size", "try to reduce bit-vector sizes using inequalities.", "mk_bv_size_reduction_tactic(m, p)") */ - -#endif diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 0b5b98308..38b4638ee 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -28,6 +28,7 @@ Revision History: #include "tactic/bv/elim_small_bv_tactic.h" +namespace { class elim_small_bv_tactic : public tactic { struct rw_cfg : public default_rewriter_cfg { @@ -183,20 +184,6 @@ class elim_small_bv_tactic : public tactic { return true; } - bool pre_visit(expr * t) { - TRACE("elim_small_bv_pre", tout << "pre_visit: " << mk_ismt2_pp(t, m) << std::endl;); - if (is_quantifier(t)) { - quantifier * q = to_quantifier(t); - TRACE("elim_small_bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m) << std::endl;); - sort_ref_vector new_bindings(m); - for (unsigned i = 0; i < q->get_num_decls(); i++) - new_bindings.push_back(q->get_decl_sort(i)); - SASSERT(new_bindings.size() == q->get_num_decls()); - m_bindings.append(new_bindings); - } - return true; - } - void updt_params(params_ref const & p) { m_params = p; m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); @@ -214,69 +201,24 @@ class elim_small_bv_tactic : public tactic { } }; - struct imp { - ast_manager & m; - rw m_rw; + ast_manager & m; + rw m_rw; + params_ref m_params; - imp(ast_manager & _m, params_ref const & p) : - m(_m), - m_rw(m, p) { - } - - void updt_params(params_ref const & p) { - m_rw.cfg().updt_params(p); - } - - void operator()(goal_ref const & g, goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); - tactic_report report("elim-small-bv", *g); - bool produce_proofs = g->proofs_enabled(); - fail_if_proof_generation("elim-small-bv", g); - fail_if_unsat_core_generation("elim-small-bv", g); - m_rw.cfg().m_produce_models = g->models_enabled(); - - m_rw.m_cfg.m_goal = g.get(); - expr_ref new_curr(m); - proof_ref new_pr(m); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { - expr * curr = g->form(idx); - m_rw(curr, new_curr, new_pr); - if (produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - g->add(m_rw.m_cfg.m_mc.get()); - - report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated); - g->inc_depth(); - result.push_back(g.get()); - TRACE("elim-small-bv", g->display(tout);); - SASSERT(g->is_well_sorted()); - } - }; - - imp * m_imp; - params_ref m_params; public: elim_small_bv_tactic(ast_manager & m, params_ref const & p) : + m(m), + m_rw(m, p), m_params(p) { - m_imp = alloc(imp, m, p); } tactic * translate(ast_manager & m) override { return alloc(elim_small_bv_tactic, m, m_params); } - ~elim_small_bv_tactic() override { - dealloc(m_imp); - } - void updt_params(params_ref const & p) override { m_params = p; - m_imp->m_rw.cfg().updt_params(p); + m_rw.cfg().updt_params(p); } void collect_param_descrs(param_descrs & r) override { @@ -285,18 +227,44 @@ public: r.insert("max_bits", CPK_UINT, "(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated."); } - void operator()(goal_ref const & in, + void operator()(goal_ref const & g, goal_ref_buffer & result) override { - (*m_imp)(in, result); + SASSERT(g->is_well_sorted()); + tactic_report report("elim-small-bv", *g); + bool produce_proofs = g->proofs_enabled(); + fail_if_proof_generation("elim-small-bv", g); + fail_if_unsat_core_generation("elim-small-bv", g); + m_rw.cfg().m_produce_models = g->models_enabled(); + + m_rw.m_cfg.m_goal = g.get(); + expr_ref new_curr(m); + proof_ref new_pr(m); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + expr * curr = g->form(idx); + m_rw(curr, new_curr, new_pr); + if (produce_proofs) { + proof * pr = g->pr(idx); + new_pr = m.mk_modus_ponens(pr, new_pr); + } + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + g->add(m_rw.m_cfg.m_mc.get()); + + report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated); + g->inc_depth(); + result.push_back(g.get()); + TRACE("elim-small-bv", g->display(tout);); + SASSERT(g->is_well_sorted()); } void cleanup() override { - ast_manager & m = m_imp->m; - m_imp->~imp(); - m_imp = new (m_imp) imp(m, m_params); + m_rw.~rw(); + new (&m_rw) rw(m, m_params); } }; +} tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(elim_small_bv_tactic, m, p)); diff --git a/src/tactic/bv/elim_small_bv_tactic.h b/src/tactic/bv/elim_small_bv_tactic.h index 675ec3de7..e4a91f70f 100644 --- a/src/tactic/bv/elim_small_bv_tactic.h +++ b/src/tactic/bv/elim_small_bv_tactic.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef ELIM_SMALL_BV_H_ -#define ELIM_SMALL_BV_H_ +#pragma once #include "util/params.h" class ast_manager; @@ -28,5 +27,3 @@ tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p = params_ /* ADD_TACTIC("elim-small-bv", "eliminate small, quantified bit-vectors by expansion.", "mk_elim_small_bv_tactic(m, p)") */ - -#endif