spread a few anonymous namespaces and remove some m_imp idioms

VeriFIT · Dec 21, 2018 · 178e5b3 · 178e5b3
1 parent 52f960a
commit 178e5b3
Show file tree

Hide file tree

Showing 7 changed files with 71 additions and 125 deletions.
diff --git 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
@@ -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 @@ class qe_lite_tactic : public tactic {
         (*m_imp)(in, result);
     }
 
-
     void collect_statistics(statistics & st) const override {
         // m_imp->collect_statistics(st);
     }
@@ -2503,14 +2503,14 @@ class qe_lite_tactic : public tactic {
         // 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
@@ -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
@@ -27,28 +27,8 @@ Module Name:
 #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<expr_replacer> 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<app, numeral>::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,32 +370,21 @@ 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());
     fail_if_proof_generation("bv-size-reduction", 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
@@ -21,8 +21,7 @@ Module Name:
 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
@@ -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;
-
-        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());
-        }
-    };
+    ast_manager & m;
+    rw            m_rw;
+    params_ref    m_params;
 
-    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 @@ class elim_small_bv_tactic : public tactic {
         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
@@ -16,8 +16,7 @@ Module Name:
 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