From 861a0745c148ae5a775a7ea9f3de0ecd1828ddf6 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 6 Nov 2017 10:36:10 +0000
Subject: [PATCH] remove a few unneded mem allocations

---
 src/tactic/bv/bv_size_reduction_tactic.cpp  | 6 +++---
 src/tactic/bv/max_bv_sharing_tactic.cpp     | 7 ++++---
 src/tactic/core/propagate_values_tactic.cpp | 5 +++--
 src/tactic/core/simplify_tactic.cpp         | 6 +++---
 src/tactic/smtlogics/qfufbv_tactic.cpp      | 8 ++++----
 5 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index 9401f74c1..ec4c21fe8 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -399,8 +399,8 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
 
  
 void bv_size_reduction_tactic::cleanup() {
-    imp * d = alloc(imp, m_imp->m);
-    std::swap(d, m_imp);    
-    dealloc(d);
+    ast_manager & m = m_imp->m;
+    m_imp->~imp();
+    new (m_imp) imp(m);
 }
 
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index b0affeb4b..becaed276 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -307,9 +307,10 @@ public:
     }
     
     virtual void cleanup() {
-        imp * d = alloc(imp, m_imp->m(), m_params);
-        std::swap(d, m_imp);        
-        dealloc(d);
+        ast_manager & m = m_imp->m();
+        params_ref p = std::move(m_params);
+        m_imp->~imp();
+        new (m_imp) imp(m, p);
     }
 };
 
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 7baac0b99..607ecbd79 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -255,8 +255,9 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        dealloc(m_imp);
-        m_imp = alloc(imp, m, m_params);
+        params_ref p = std::move(m_params);
+        m_imp->~imp();
+        new (m_imp) imp(m, p);
     }
     
 };
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 9deff968e..de1fcc99c 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -111,9 +111,9 @@ void simplify_tactic::operator()(goal_ref const & in,
 
 void simplify_tactic::cleanup() {
     ast_manager & m = m_imp->m();
-    imp * d = alloc(imp, m, m_params);
-    std::swap(d, m_imp);    
-    dealloc(d);
+    params_ref p = std::move(m_params);
+    m_imp->~imp();
+    new (m_imp) imp(m, p);
 }
 
 unsigned simplify_tactic::get_num_steps() const {
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index e89da3631..df2791a8f 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -70,8 +70,8 @@ public:
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
         scoped_ptr<solver> uffree_solver = setup_sat();
-        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get());
-        const lbool o = imp->operator()();
+        lackr imp(m, m_p, m_st, flas, uffree_solver.get());
+        const lbool o = imp.operator()();
         flas.reset();
         // report result
         goal_ref resg(alloc(goal, *g, true));
@@ -79,8 +79,8 @@ public:
         if (o != l_undef) result.push_back(resg.get());
         // report model
         if (g->models_enabled() && (o == l_true)) {
-            model_ref abstr_model = imp->get_model();
-            mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model);
+            model_ref abstr_model = imp.get_model();
+            mc = mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model);
         }
     }