Allow in-place construction of `CDList` items (#6409)

This commit adds CDList::emplace_back(), which allows users to create
elements in CDList in-place (as opposed to copying the items using
CDList::push_back(). This allows CDList to be used with
std::unique_ptrs, which do not allow copying. Using
CDList::emplace_back() could also be more efficient in certain cases.

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 2bb66eaf25921b7fafe4a5e725be960377c50d57..281901c1c0d90e6fd4f3b376f28ddf7385acb314 100644 (file)
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -22,6 +22,7 @@
 
 #include <cstring>
 #include <iterator>
+#include <memory>
 #include <string>
 
 #include "base/check.h"
@@ -114,12 +115,23 @@ protected:
   }
   CDList& operator=(const CDList& l) = delete;
 
-private:
+ private:
   /**
-   * Reallocate the array with more space.
-   * Throws bad_alloc if memory allocation fails.
+   * Reallocate the array with more space. Throws bad_alloc if memory
+   * allocation fails. Does not perform any action if there is still unused
+   * allocated space.
    */
   void grow() {
+    Debug("cdlist") << "grow " << this << " " << getContext()->getLevel()
+                    << ": grow? " << d_size << " " << d_sizeAlloc << std::endl;
+    if (d_size != d_sizeAlloc)
+    {
+      // If there is still unused allocated space
+      return;
+    }
+    Debug("cdlist") << "grow " << this << " " << getContext()->getLevel()
+                    << ": grow!" << std::endl;
+
     if(d_list == NULL) {
       // Allocate an initial list if one does not yet exist
       d_sizeAlloc = INITIAL_SIZE;
@@ -217,9 +229,7 @@ protected:
     }
   }
 
-
-public:
-
+ public:
   /**
    * Main constructor: d_list starts as NULL, size is 0
    */
@@ -265,7 +275,11 @@ public:
   }
 
   /**
-   * Add an item to the end of the list.
+   * Add an item to the end of the list. This method uses the copy constructor
+   * of T, so the type has to support it. As a result, this method cannot be
+   * used with types that do not have a copy constructor such as
+   * std::unique_ptr. Use CDList::emplace_back() instead of CDList::push_back()
+   * to avoid this issue.
    */
   void push_back(const T& data) {
     Debug("cdlist") << "push_back " << this
@@ -273,17 +287,7 @@ public:
                     << ": make-current, "
                     << "d_list == " << d_list << std::endl;
     makeCurrent();
-
-    Debug("cdlist") << "push_back " << this
-                    << " " << getContext()->getLevel()
-                    << ": grow? " << d_size
-                    << " " << d_sizeAlloc << std::endl;
-    if(d_size == d_sizeAlloc) {
-      Debug("cdlist") << "push_back " << this
-                      << " " << getContext()->getLevel()
-                      << ": grow!" << std::endl;
-      grow();
-    }
+    grow();
     Assert(d_size < d_sizeAlloc);
 
     Debug("cdlist") << "push_back " << this
@@ -301,6 +305,34 @@ public:
                     << ": size now " << d_size << std::endl;
   }
 
+  /**
+   * Construct an item to the end of the list. This method constructs the item
+   * in-place (similar to std::vector::emplace_back()), so it can be used for
+   * types that do not have a copy constructor such as std::unique_ptr.
+   */
+  template <typename... Args>
+  void emplace_back(Args&&... args)
+  {
+    Debug("cdlist") << "emplace_back " << this << " "
+                    << getContext()->getLevel() << ": make-current, "
+                    << "d_list == " << d_list << std::endl;
+    makeCurrent();
+    grow();
+    Assert(d_size < d_sizeAlloc);
+
+    Debug("cdlist") << "emplace_back " << this << " "
+                    << getContext()->getLevel() << ": construct! at " << d_list
+                    << "[" << d_size << "] == " << &d_list[d_size] << std::endl;
+    std::allocator_traits<AllocatorT>::construct(
+        d_allocator, &d_list[d_size], std::forward<Args>(args)...);
+    Debug("cdlist") << "emplace_back " << this << " "
+                    << getContext()->getLevel() << ": done..." << std::endl;
+    ++d_size;
+    Debug("cdlist") << "emplace_back " << this << " "
+                    << getContext()->getLevel() << ": size now " << d_size
+                    << std::endl;
+  }
+
   /**
    * Access to the ith item in the list.
    */

diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp
index 57c25a2b3d2231cbb7ef9d244578c3da76d9443f..a8d9f952b1fe0169a184b534094ea4450a4b0d6c 100644 (file)
--- a/test/unit/context/cdlist_black.cpp
+++ b/test/unit/context/cdlist_black.cpp
@@ -161,5 +161,41 @@ TEST_F(TestContextBlackCDList, pop_below_level_created)
   d_context->popto(0);
   list.push_back(42);
 }
+
+TEST_F(TestContextBlackCDList, emplace_back)
+{
+  int32_t n = 10;
+  int32_t start = 42;
+  CDList<std::unique_ptr<int32_t>> list(d_context.get());
+
+  for (int32_t i = 0; i < n; i++)
+  {
+    list.emplace_back(new int32_t(start + i));
+  }
+  for (int32_t i = 0; i < n; i++)
+  {
+    ASSERT_EQ(*list[i], start + i);
+  }
+  ASSERT_EQ(list.size(), n);
+
+  d_context->push();
+  for (int32_t i = 0; i < n; i++)
+  {
+    list.emplace_back(new int32_t(start + n + i));
+  }
+  for (int32_t i = 0; i < n * 2; i++)
+  {
+    ASSERT_EQ(*list[i], start + i);
+  }
+  ASSERT_EQ(list.size(), n * 2);
+  d_context->pop();
+
+  for (int32_t i = 0; i < n; i++)
+  {
+    ASSERT_EQ(*list[i], start + i);
+  }
+  ASSERT_EQ(list.size(), n);
+}
+
 }  // namespace test
 }  // namespace cvc5