From 000796c25cbc06ef008c4701305a3b1bea3bdf4b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 14 Aug 2017 20:12:00 +0100 Subject: [PATCH] micro-optimization in tactics' cleanup(): avoid dealloc+alloc traffic --- src/tactic/bv/elim_small_bv_tactic.cpp | 5 ++--- src/tactic/core/elim_term_ite_tactic.cpp | 5 ++--- src/tactic/core/reduce_args_tactic.cpp | 7 +++---- 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index d24ae4f49..c40927179 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -307,9 +307,8 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); + m_imp->~imp(); + m_imp = new (m_imp) imp(m, m_params); } }; diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 91f1d9020..79526a101 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -171,9 +171,8 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); + m_imp->~imp(); + m_imp = new (m_imp) imp(m, m_params); } }; diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index a4b9825cc..476c21232 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -502,9 +502,8 @@ void reduce_args_tactic::operator()(goal_ref const & g, } void reduce_args_tactic::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m); - std::swap(d, m_imp); - dealloc(d); + ast_manager & m = m_imp->m(); + m_imp->~imp(); + m_imp = new (m_imp) imp(m); }