From 6a45c5d17ce5b450a473902b7bdaa202b416aac6 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 30 May 2020 11:42:27 +0100
Subject: [PATCH] fix build with prehistorical compilers because of
 pip/manylinux

---
 src/math/simplex/bit_matrix.cpp |  1 +
 src/util/heap.h                 |  7 ++-----
 src/util/vector.h               | 29 ++++++++++++-----------------
 3 files changed, 15 insertions(+), 22 deletions(-)

diff --git a/src/math/simplex/bit_matrix.cpp b/src/math/simplex/bit_matrix.cpp
index 8c9280b30..fa4b481b5 100644
--- a/src/math/simplex/bit_matrix.cpp
+++ b/src/math/simplex/bit_matrix.cpp
@@ -15,6 +15,7 @@ Notes:
 
 #include "math/simplex/bit_matrix.h"
 #include "util/stopwatch.h"
+#include <cstring>
 
 
 bit_matrix::col_iterator bit_matrix::row::begin() const { 
diff --git a/src/util/heap.h b/src/util/heap.h
index 182932fd0..4651012aa 100644
--- a/src/util/heap.h
+++ b/src/util/heap.h
@@ -16,11 +16,11 @@ Author:
 Revision History:
 
 --*/
-#ifndef HEAP_H_
-#define HEAP_H_
+#pragma once
 
 #include "util/vector.h"
 #include "util/debug.h"
+#include <cstring>
 
 template<typename LT>
 class heap : private LT {
@@ -290,6 +290,3 @@ public:
 
   
 };
-
-#endif /* HEAP_H_ */
-
diff --git a/src/util/vector.h b/src/util/vector.h
index b1929ed0c..9de2b2a86 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -23,14 +23,13 @@ Revision History:
 
 
 --*/
-#ifndef VECTOR_H_
-#define VECTOR_H_
+#pragma once
 
 #include "util/debug.h"
-#include<algorithm>
-#include<type_traits>
-#include<memory.h>
-#include<functional>
+#include <algorithm>
+#include <functional>
+#include <memory>
+#include <type_traits>
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
@@ -79,7 +78,11 @@ class vector {
                 throw default_exception("Overflow encountered when expanding vector");
             }
             SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
+#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
+            if (__has_trivial_copy(T)) {
+#else
             if (std::is_trivially_copyable<T>::value) {
+#endif
                 mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
                 m_data = reinterpret_cast<T *>(mem + 2);
             } else {
@@ -106,14 +109,8 @@ class vector {
         mem++;
         *mem = size; 
         mem++;
-        m_data             = reinterpret_cast<T *>(mem);
-        const_iterator it  = source.begin();
-        iterator it2       = begin();
-        SASSERT(it2 == m_data);
-        const_iterator e   = source.end();
-        for (; it != e; ++it, ++it2) {
-            new (it2) T(*it); 
-        }
+        m_data = reinterpret_cast<T *>(mem);
+        std::uninitialized_copy(source.begin(), source.end(), begin());
     }
 
     void destroy() {
@@ -445,7 +442,7 @@ public:
         ++pos;
         iterator e    = end();
         for(; pos != e; ++pos, ++prev) {
-            *prev = *pos;
+            *prev = std::move(*pos);
         }
         reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
     }
@@ -651,5 +648,3 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
 
 template<typename Hash>
 struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
-
-#endif /* VECTOR_H_ */