initial removal of STLAllocator<T>

CMakeLists.txt

@@ -183,7 +183,6 @@ set(VAMPIRE_LIB_SOURCES
     Lib/SmartPtr.hpp
     Lib/Sort.hpp
     Lib/Stack.hpp
-    Lib/STLAllocator.hpp
     Lib/StringUtils.hpp
     Lib/System.hpp
     Lib/Timer.hpp

Forwards.hpp

@@ -15,6 +15,8 @@
 #ifndef __Forwards__
 #define __Forwards__
 
+#include <memory>
+
 #include "Lib/VString.hpp"
 
 namespace Lib

Inferences/ForwardSubsumptionDemodulation.cpp

@@ -28,7 +28,6 @@
 #include "Kernel/Term.hpp"
 #include "Lib/ScopeGuard.hpp"
 #include "Lib/STL.hpp"
-#include "Lib/STLAllocator.hpp"
 #include "Saturation/SaturationAlgorithm.hpp"
 #include "Shell/TPTPPrinter.hpp"
 #include <array>

Kernel/Inference.hpp

@@ -24,6 +24,8 @@
 #include "Forwards.hpp"
 
 #include <type_traits>
+#include <limits>
+#include <memory>
 
 using namespace Lib;
 

Kernel/Polynomial.hpp

@@ -28,7 +28,6 @@
  * MonomFactor     ::= PolyNf int                   // the term of the factor, and its power
  */
 
-#include "Lib/STLAllocator.hpp"
 #include "Kernel/NumTraits.hpp"
 #include <cassert>
 #include "Lib/Coproduct.hpp"

Kernel/PolynomialNormalizer/PredicateEvaluator.hpp

@@ -12,7 +12,6 @@ template<Theory::Interpretation inter>
 struct PredicateEvaluator;
 
 template<class C> using Poly = Polynom<NumTraits<C>>;
-#include "Lib/STLAllocator.hpp"
 #include "Lib/Option.hpp"
 
 using LitSimplResult = Inferences::SimplifyingGeneratingLiteralSimplification::Result;

Lib/Int.hpp

@@ -23,7 +23,7 @@
 #include "VString.hpp"
 
 #include <iostream>
-
+#include <limits>
 
 #ifdef _MSC_VER // VC++
 #  undef max

Lib/NameArray.cpp

@@ -17,6 +17,8 @@
 
 #include <cstring>
 
+#include "Debug/Assertion.hpp"
+
 #include "Exception.hpp"
 #include "NameArray.hpp"
 

Lib/STL.hpp

@@ -20,7 +20,6 @@
 #include <unordered_set>
 #include <utility>
 #include <vector>
-#include "Lib/STLAllocator.hpp"
 
 namespace Lib {
 
@@ -29,32 +28,32 @@ template< typename Key
         , typename T
         , typename Compare = std::less<Key>
         >
-using vmap = std::map<Key, T, Compare, STLAllocator<std::pair<const Key, T>>>;
+using vmap = std::map<Key, T, Compare>;
 
 
 template< typename Key
         , typename Compare = std::less<Key>
         >
-using vset = std::set<Key, Compare, STLAllocator<Key>>;
+using vset = std::set<Key, Compare>;
 
 
 template< typename Key
         , typename T
         , typename Hash = std::hash<Key>
         , typename KeyEqual = std::equal_to<Key>
         >
-using vunordered_map = std::unordered_map<Key, T, Hash, KeyEqual, STLAllocator<std::pair<const Key, T>>>;
+using vunordered_map = std::unordered_map<Key, T, Hash, KeyEqual>;
 
 
 template< typename Key
         , typename Hash = std::hash<Key>
         , typename KeyEqual = std::equal_to<Key>
         >
-using vunordered_set = std::unordered_set<Key, Hash, KeyEqual, STLAllocator<Key>>;
+using vunordered_set = std::unordered_set<Key, Hash, KeyEqual>;
 
 
 template< typename T >
-using vvector = std::vector<T, STLAllocator<T>>;
+using vvector = std::vector<T>;
 
 }  // namespace Lib
 

Lib/ScopedPtr.hpp

@@ -18,6 +18,7 @@
 #include "Forwards.hpp"
 
 #include "Debug/Assertion.hpp"
+#include "Lib/Allocator.hpp"
 
 namespace Lib
 {

Lib/VString.hpp

@@ -23,54 +23,11 @@
 #include <string>
 #include <sstream>
 
-#include "STLAllocator.hpp"
-
 namespace Lib {
-
-// ostringstream which uses (returns) a vstring
-typedef std::basic_ostringstream<char,std::char_traits<char>,STLAllocator<char> > vostringstream_base;
-
-struct vostringstream : public vostringstream_base {
-  USE_ALLOCATOR(vostringstream);
-
-  // inherit parent's constructors (c++11)
-  using vostringstream_base::vostringstream_base;
-};
-
-// istringstream which uses (returns) a vstring
-typedef std::basic_istringstream<char,std::char_traits<char>,STLAllocator<char> > vistringstream_base;
-
-struct vistringstream : public vistringstream_base {
-  USE_ALLOCATOR(vistringstream);
-
-  // inherit parent's constructors (c++11)
-  using vistringstream_base::vistringstream_base;
-};
-
-// stringstream which uses (returns) a vstring 
-typedef std::basic_stringstream<char,std::char_traits<char>,STLAllocator<char> > vstringstream_base;
-
-struct vstringstream : public vstringstream_base {
-  USE_ALLOCATOR(vstringstream);
-
-  // inherit parent's constructors (c++11)
-  using vstringstream_base::vstringstream_base;
-};
-
-// vampire string, a STL string using vampire's Allocator
-typedef std::basic_string<char,std::char_traits<char>,STLAllocator<char> > vstring;
-
-/* 
- * Careful: doing the above inheritance trick with vstring might not be a good idea.
- * For one, basic_string does not have a virtual destructor so inheriting
- * from it is not a nice thing (although slicing problems shouldn't occur
- * if we just add the operator new functions and no data members ... )
- * For the other, it's not that simple to make it work anyway. For instance,
- * the globally available operators + for strings, would take vstring as argument
- * but still return only the parent, vstring_base. One would need to
- * redefine all of them and make an ugly explicit downcast.
- */
-
-} // namespace Lib
+typedef std::string vstring;
+typedef std::stringstream vstringstream;
+typedef std::istringstream vistringstream;
+typedef std::ostringstream vostringstream;
+}
 
 #endif // __VString__

Shell/NewCNF.hpp

@@ -20,7 +20,6 @@
 #include "Lib/List.hpp"
 #include "Lib/DArray.hpp"
 #include "Lib/Deque.hpp"
-#include "Lib/STLAllocator.hpp"
 #include "Lib/SmartPtr.hpp"
 #include "Lib/DHMap.hpp"
 #include "Lib/SharedSet.hpp"
@@ -177,7 +176,7 @@ class NewCNF
     }
 
     // Position of a gen literal in _genClauses
-    std::list<SmartPtr<GenClause>,STLAllocator<SmartPtr<GenClause>>>::iterator iter;
+    std::list<SmartPtr<GenClause>>::iterator iter;
 
     vstring toString() {
       vstring res = "GC("+Int::toString(size())+")";
@@ -210,7 +209,7 @@ class NewCNF
   bool mapSubstitution(List<GenLit>* gc, Substitution subst, bool onlyFormulaLevel, List<GenLit>* &output);
   Clause* toClause(SPGenClause gc);
 
-  typedef std::list<SPGenClause,STLAllocator<SPGenClause>> GenClauses;
+  typedef std::list<SPGenClause> GenClauses;
 
   /**
    * pushLiteral is responsible for tautology elimination. Whenever it sees two