Change partial ordering underlying array to vector

Kernel/PartialOrdering.cpp

@@ -147,29 +147,6 @@ string pocompToInfix(PoComp c) {
   ASSERTION_VIOLATION;
 }
 
-PartialOrdering::PartialOrdering()
-  : _size(0), _array(nullptr) {}
-
-PartialOrdering::PartialOrdering(const PartialOrdering& other)
-  : _size(other._size), _array(nullptr)
-{
-  size_t arrSize = ((_size - 1) * _size / 2);
-  if (arrSize) {
-    void* mem = ALLOC_KNOWN(arrSize*sizeof(PoComp), "Kernel::PartialOrdering");
-    _array = array_new<PoComp>(mem, arrSize);
-    memcpy(_array,other._array,arrSize*sizeof(PoComp));
-  }
-}
-
-PartialOrdering::~PartialOrdering()
-{
-  size_t arrSize = ((_size - 1) * _size / 2);
-  if (arrSize) {
-    array_delete(_array, arrSize);
-    DEALLOC_KNOWN(_array, arrSize*sizeof(PoComp), "Kernel::PartialOrdering");
-  }
-}
-
 PoComp PartialOrdering::get(size_t x, size_t y) const
 {
   ASS_L(x,_size);
@@ -239,31 +216,14 @@ const PartialOrdering* PartialOrdering::extend(const PartialOrdering* po)
 
 void PartialOrdering::extend()
 {
-  // extend array
-  size_t prevSize = ((_size - 1) * _size / 2);
-  auto prevArray = _array;
   _size++;
-  if (_size>1) {
-    size_t newSize = prevSize + _size;
-    void* mem = ALLOC_KNOWN(newSize*sizeof(PoComp), "Kernel::PartialOrdering");
-    _array = array_new<PoComp>(mem, newSize);
-    std::memset(_array, 0, newSize*sizeof(PoComp));
-    static_assert(static_cast<unsigned>(PoComp::UNKNOWN) == 0);
-    if (prevArray) {
-      memcpy(_array,prevArray,prevSize*sizeof(PoComp));
-    }
-  }
-  // remove previous array
-  if (prevSize) {
-    array_delete(prevArray, prevSize);
-    DEALLOC_KNOWN(prevArray, prevSize*sizeof(PoComp), "Kernel::PartialOrdering");
-  }
+  _array.insert(_array.end(),_size,PoComp::UNKNOWN);
 }
 
 bool PartialOrdering::setRel(size_t x, size_t y, PoComp v, bool& changed)
 {
   size_t idx = y*(y-1)/2 + x;
-  ASS_L(idx,((_size - 1) * _size / 2));
+  ASS_L(idx,_array.size());
   PoComp new_v;
   if (!checkCompatibility(_array[idx], v, new_v)) {
     changed = false;
@@ -286,7 +246,7 @@ bool PartialOrdering::setRelSafe(size_t x, size_t y, PoComp v, bool& changed)
 PoComp PartialOrdering::getUnsafe(size_t x, size_t y) const
 {
   size_t idx = y*(y-1)/2 + x;
-  ASS_L(idx,((_size - 1) * _size / 2));
+  ASS_L(idx,_array.size());
   return _array[idx];
 }
 

Kernel/PartialOrdering.hpp

@@ -15,6 +15,7 @@
 #define __PartialOrdering__
 
 #include <string>
+#include <vector>
 
 namespace Kernel {
 
@@ -72,9 +73,9 @@ class PartialOrdering
   friend std::ostream& operator<<(std::ostream& str, const PartialOrdering& po);
 
 private:
-  PartialOrdering();
-  ~PartialOrdering();
-  PartialOrdering(const PartialOrdering& other);
+  PartialOrdering() = default;
+  ~PartialOrdering() = default;
+  PartialOrdering(const PartialOrdering&) = default;
   PartialOrdering& operator=(const PartialOrdering&) = delete;
 
   void extend();
@@ -88,8 +89,8 @@ class PartialOrdering
   bool setInferredHelperInc(size_t x, size_t y, PoComp wkn);
   bool setInferredHelperEq(size_t x, size_t y);
 
-  size_t _size;
-  PoComp* _array;
+  size_t _size = 0;
+  std::vector<PoComp> _array;
 };
 
 };