From c6032949c84023f37de61e8403e83274995b95cd Mon Sep 17 00:00:00 2001 From: Saikat Chakraborty Date: Fri, 23 Aug 2024 18:13:08 +0000 Subject: [PATCH] Migrate `aig_manager` to use smart pointer. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit To decide whether `m_aig_manager` should be a `std::unique_ptr`, `std::shared_ptr`, or `std::weak_ptr`, let's analyze the ownership semantics and usage pattern of `m_aig_manager` in the `aig_tactic` class. Analysis of Ownership: 1. **Single Ownership**: - `m_aig_manager` is allocated within the `mk_aig_manager` struct's constructor, where it calls `alloc(aig_manager, ...)`, and deallocated within the `mk_aig_manager` destructor using `dealloc(m_owner.m_aig_manager);`. - `m_aig_manager` is not shared or referenced by any other part of the code outside of `aig_tactic` and `mk_aig_manager`. This suggests that `aig_manager` is owned exclusively by the `aig_tactic` class. 2. **Lifespan Management**: - `m_aig_manager` is created within `mk_aig_manager` and is automatically destroyed when `mk_aig_manager` goes out of scope (which happens after the tactic is applied). - This indicates that `m_aig_manager`'s lifespan is tightly coupled with the `aig_tactic` class or its method execution. 3. **No Sharing Needed**: - There is no indication that `m_aig_manager` needs to be shared across multiple owners or instances. Therefore, there’s no need for `std::shared_ptr`. - Since there’s no sharing, `std::weak_ptr` is also unnecessary. Conclusion: Given the analysis, **`std::unique_ptr`** is the most appropriate choice for managing `m_aig_manager`. It ensures that the memory is properly managed (automatically deleted when the pointer goes out of scope), and it enforces the exclusive ownership semantics that are currently implied by the code. --- src/tactic/aig/aig_tactic.cpp | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 8027e6484..fa673e92f 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -27,24 +27,21 @@ class aig_manager; class aig_tactic : public tactic { unsigned long long m_max_memory; bool m_aig_gate_encoding; - aig_manager * m_aig_manager; + std::unique_ptr m_aig_manager; struct mk_aig_manager { aig_tactic & m_owner; mk_aig_manager(aig_tactic & o, ast_manager & m):m_owner(o) { aig_manager * mng = alloc(aig_manager, m, o.m_max_memory, o.m_aig_gate_encoding); - m_owner.m_aig_manager = mng; + m_owner.m_aig_manager.reset(mng); } - ~mk_aig_manager() { - dealloc(m_owner.m_aig_manager); - m_owner.m_aig_manager = nullptr; - } + ~mk_aig_manager() {} }; public: - aig_tactic(params_ref const & p = params_ref()):m_aig_manager(nullptr) { + aig_tactic(params_ref const & p = params_ref()) { updt_params(p); }