also remove vstringstream, vvector, vmap, vset, and friends

CASC/PortfolioMode.hpp

@@ -22,8 +22,6 @@
 #include "Lib/ScopedPtr.hpp"
 #include "Lib/Stack.hpp"
 
-#include "Lib/VString.hpp"
-
 #include "Kernel/Problem.hpp"
 
 #include "Shell/Property.hpp"

CMakeLists.txt

@@ -189,8 +189,6 @@ set(VAMPIRE_LIB_SOURCES
     Lib/TriangularArray.hpp
     Lib/Vector.hpp
     Lib/VirtualIterator.hpp
-    Lib/VString.hpp
-    Lib/STL.hpp
     )
 source_group(lib_source_files FILES ${VAMPIRE_LIB_SOURCES})
 

DP/SimpleCongruenceClosure.cpp

@@ -37,7 +37,7 @@ const unsigned SimpleCongruenceClosure::NO_SIG_SYMBOL = 0xFFFFFFFF;
 
 vstring SimpleCongruenceClosure::CEq::toString() const
 {
-  vostringstream res;
+  std::ostringstream res;
   res << c1<<"="<<c2<<" implied by ";
   if(foOrigin) {
     if(foPremise) {
@@ -55,7 +55,7 @@ vstring SimpleCongruenceClosure::CEq::toString() const
 
 vstring SimpleCongruenceClosure::CEq::toString(SimpleCongruenceClosure& parent) const
 {
-  vostringstream res;
+  std::ostringstream res;
   res << c1<<"="<<c2<<" implied by ";
   if(foOrigin) {
     if(foPremise) {

FMB/FiniteModel.cpp

@@ -139,7 +139,7 @@ bool FiniteModel::isPartial()
 
 vstring FiniteModel::toString()
 {
-  vostringstream modelStm;
+  std::ostringstream modelStm;
 
   bool printIntroduced = false;
 

FMB/FiniteModelMultiSorted.cpp

@@ -181,7 +181,7 @@ bool FiniteModelMultiSorted::isPartial()
 
 vstring FiniteModelMultiSorted::toString()
 {
-  vostringstream modelStm;
+  std::ostringstream modelStm;
 
   bool printIntroduced = false;
 

FMB/FunctionRelationshipInference.cpp

@@ -17,7 +17,6 @@
 #include "Lib/DHSet.hpp"
 #include "Lib/Stack.hpp"
 #include "Lib/Environment.hpp"
-#include "Lib/VString.hpp"
 #include "Lib/Timer.hpp"
 #include "Lib/IntUnionFind.hpp"
 

Forwards.hpp

@@ -17,13 +17,14 @@
 
 #include <memory>
 
-#include "Lib/VString.hpp"
-
 namespace Lib
 {
 struct EmptyStruct {};
 typedef void (*VoidFunc)();
 
+// historical alias to std::string: do not use in new code
+using vstring = std::string;
+
 template<typename T> class VirtualIterator;
 
 template<typename T> class ScopedPtr;

Indexing/CodeTree.hpp

@@ -297,7 +297,7 @@ class CodeTree
      */
     CodeOp landingOp;
     Kind kind;
-    vvector<CodeOp*> targets;
+    std::vector<CodeOp*> targets;
 
   protected:
     SearchStruct(Kind kind, size_t length);
@@ -319,7 +319,7 @@ class CodeTree
      */
     template<bool doInsert> CodeOp*& targetOp(const T& val);
 
-    vvector<T> values;
+    std::vector<T> values;
   };
 
   using FnSearchStruct = SearchStructImpl<SearchStruct::FN_STRUCT>;

Indexing/RequestedIndex.hpp

@@ -14,7 +14,6 @@
 #include "Indexing/Index.hpp"
 #include "Indexing/IndexManager.hpp"
 #include "Lib/Allocator.hpp"
-#include "Lib/STL.hpp"
 
 namespace Indexing {
 

Inferences/BackwardSubsumptionDemodulation.cpp

@@ -115,7 +115,7 @@ void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRe
   Literal* lmLit1 = best2.first.lit();
   Literal* lmLit2 = best2.second.lit();
 
-  static vvector<BwSimplificationRecord> simplificationsStorage;
+  static std::vector<BwSimplificationRecord> simplificationsStorage;
   ASS_EQ(simplificationsStorage.size(), 0);
 
   if (!lmLit1->isEquality() || !lmLit1->isPositive()) {
@@ -134,7 +134,7 @@ void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRe
 }  // perform
 
 
-void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, vvector<BwSimplificationRecord>& simplifications)
+void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, std::vector<BwSimplificationRecord>& simplifications)
 {
   //   sideCl
   // vvvvvvvvvv
@@ -258,9 +258,9 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera
 
 /// Handles the matching part.
 /// Returns true iff the main premise has been simplified.
-bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* mainCl, vvector<BwSimplificationRecord>& simplifications)
+bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector<BwSimplificationRecord>& simplifications)
 {
-    static vvector<LiteralList*> alts;
+    static std::vector<LiteralList*> alts;
 
     alts.clear();
     alts.resize(sideCl->length(), LiteralList::empty());
@@ -383,15 +383,15 @@ bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* m
   }
 
   // isMatched[i] is true iff (*mainCl)[i] is matched by some literal in sideCl (other than eqLit)
-  static vvector<bool> isMatched;
+  static std::vector<bool> isMatched;
   matcher.getMatchedAltsBitmap(isMatched);
 
   static OverlayBinder binder;
   binder.clear();
   matcher.getBindings(binder.base());
 
   // NOTE: for explanation see comments in ForwardSubsumptionDemodulation::perform
-  static vvector<TermList> lhsVector;
+  static std::vector<TermList> lhsVector;
   lhsVector.clear();
   {
     TermList t0 = *eqLit->nthArgument(0);

Inferences/BackwardSubsumptionDemodulation.hpp

@@ -62,8 +62,8 @@ class BackwardSubsumptionDemodulation
     bool _preorderedOnly;
     bool _allowIncompleteness;
 
-    void performWithQueryLit(Clause* premise, Literal* candidateQueryLit, vvector<BwSimplificationRecord>& simplifications);
-    bool simplifyCandidate(Clause* sideCl, Clause* mainCl, vvector<BwSimplificationRecord>& simplifications);
+    void performWithQueryLit(Clause* premise, Literal* candidateQueryLit, std::vector<BwSimplificationRecord>& simplifications);
+    bool simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector<BwSimplificationRecord>& simplifications);
     bool rewriteCandidate(Clause* sideCl, Clause* mainCl, MLMatcherSD const& matcher, Clause*& replacement);
 };
 

Inferences/ForwardSubsumptionDemodulation.cpp

@@ -27,7 +27,6 @@
 #include "Kernel/SubstHelper.hpp"
 #include "Kernel/Term.hpp"
 #include "Lib/ScopeGuard.hpp"
-#include "Lib/STL.hpp"
 #include "Saturation/SaturationAlgorithm.hpp"
 #include "Shell/TPTPPrinter.hpp"
 #include <array>
@@ -150,7 +149,7 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C
       /**
        * Step 2: choose a positive equality in mcl to use for demodulation and try to instantiate the rest to some subset of cl
        */
-      static vvector<LiteralList*> alts;
+      static std::vector<LiteralList*> alts;
       alts.clear();
       alts.reserve(mcl->length());
       ASS_EQ(alts.size(), 0);
@@ -262,7 +261,7 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C
         }
 
         // isMatched[i] is true iff (*cl)[i] is matched my some literal in mcl (without eqLit)
-        static vvector<bool> isMatched;
+        static std::vector<bool> isMatched;
         matcher.getMatchedAltsBitmap(isMatched);
 
         static OverlayBinder binder;
@@ -291,7 +290,7 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C
         // 1. No LHS (if INCOMPARABLE and no side contains all variables of the other side)
         // 2. One LHS (oriented, or INCOMPARABLE with exactly one variable-free side)
         // 3. Two LHSs (INCOMPARABLE and same variables)
-        static vvector<TermList> lhsVector;
+        static std::vector<TermList> lhsVector;
         lhsVector.clear();
         {
           TermList t0 = *eqLit->nthArgument(0);

Inferences/Induction.cpp

@@ -13,6 +13,7 @@
  */
 
 #include <utility>
+#include <set>
 
 #include "Debug/Output.hpp"
 #include "Forwards.hpp"
@@ -70,7 +71,7 @@ Term* ActiveOccurrenceIterator::next()
   return t;
 }
 
-Term* getPlaceholderForTerm(const vvector<Term*>& ts, unsigned i)
+Term* getPlaceholderForTerm(const std::vector<Term*>& ts, unsigned i)
 {
   static DHMap<pair<TermList,unsigned>,Term*> placeholders;
   TermList srt = SortHelper::getResultSort(ts[i]);
@@ -132,13 +133,13 @@ Formula* InductionContext::getFormula(TermReplacement& tr, bool opposite) const
   return JunctionFormula::generalJunction(opposite ? Connective::OR : Connective::AND, argLists);
 }
 
-Formula* InductionContext::getFormula(const vvector<TermList>& r, bool opposite, Substitution* subst) const
+Formula* InductionContext::getFormula(const std::vector<TermList>& r, bool opposite, Substitution* subst) const
 {
   ASS_EQ(_indTerms.size(), r.size());
 
   // Assuming this object is the result of a ContextReplacement (or similar iterator)
   // we can replace the ith placeholder with the ith term in r.
-  vmap<Term*,TermList> replacementMap;
+  std::map<Term*,TermList> replacementMap;
   for (unsigned i = 0; i < _indTerms.size(); i++) {
     auto ph = getPlaceholderForTerm(_indTerms,i);
     replacementMap.insert(make_pair(ph,r[i]));
@@ -151,14 +152,14 @@ Formula* InductionContext::getFormula(const vvector<TermList>& r, bool opposite,
   return getFormula(tr, opposite);
 }
 
-Formula* InductionContext::getFormulaWithSquashedSkolems(const vvector<TermList>& r, bool opposite,
+Formula* InductionContext::getFormulaWithSquashedSkolems(const std::vector<TermList>& r, bool opposite,
   unsigned& var, VList** varList, Substitution* subst) const
 {
   const bool strengthenHyp = env.options->inductionStrengthenHypothesis();
   if (!strengthenHyp) {
     return getFormula(r, opposite, subst);
   }
-  vmap<Term*,TermList> replacementMap;
+  std::map<Term*,TermList> replacementMap;
   for (unsigned i = 0; i < _indTerms.size(); i++) {
     auto ph = getPlaceholderForTerm(_indTerms,i);
     replacementMap.insert(make_pair(ph,r[i]));
@@ -189,9 +190,9 @@ Formula* InductionContext::getFormulaWithSquashedSkolems(const vvector<TermList>
   return res;
 }
 
-vmap<Term*,TermList> getContextReplacementMap(const InductionContext& context, bool inverse = false)
+std::map<Term*,TermList> getContextReplacementMap(const InductionContext& context, bool inverse = false)
 {
-  vmap<Term*,TermList> m;
+  std::map<Term*,TermList> m;
   for (unsigned i = 0; i < context._indTerms.size(); i++) {
     auto ph = getPlaceholderForTerm(context._indTerms,i);
     m.insert(make_pair(inverse ? ph : context._indTerms[i], inverse ? context._indTerms[i] : ph));
@@ -495,7 +496,7 @@ struct InductionContextFn
 {
   InductionContextFn(Clause* premise, Literal* lit) : _premise(premise), _lit(lit) {}
 
-  VirtualIterator<InductionContext> operator()(pair<vvector<Term*>, VirtualIterator<QueryRes<ResultSubstitutionSP, TermLiteralClause>>> arg) {
+  VirtualIterator<InductionContext> operator()(pair<std::vector<Term*>, VirtualIterator<QueryRes<ResultSubstitutionSP, TermLiteralClause>>> arg) {
     auto indDepth = _premise->inference().inductionDepth();
     // heuristic 2
     if (indDepth) {
@@ -584,19 +585,19 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
 
   if (lit->ground()) {
       Set<Term*,SharedTermHash> int_terms;
-      vmap<vvector<Term*>,vset<pair<const InductionTemplate*,vvector<Term*>>>> ta_terms;
+      std::map<std::vector<Term*>,std::set<pair<const InductionTemplate*,std::vector<Term*>>>> ta_terms;
 
       auto templ = _fnDefHandler.getInductionTemplate(lit);
       if (templ) {
-        vvector<Term*> indTerms;
+        std::vector<Term*> indTerms;
         if (templ->matchesTerm(lit, indTerms)) {
-          vvector<Term*> typeArgs;
+          std::vector<Term*> typeArgs;
           for (unsigned i = 0; i < lit->numTypeArguments(); i++) {
             typeArgs.push_back(lit->nthArgument(i)->term());
           }
           auto it = ta_terms.find(indTerms);
           if (it == ta_terms.end()) {
-            it = ta_terms.insert(make_pair(indTerms,vset<pair<const InductionTemplate*,vvector<Term*>>>())).first;
+            it = ta_terms.insert(make_pair(indTerms,std::set<pair<const InductionTemplate*,std::vector<Term*>>>())).first;
           }
           it->second.insert(make_pair(templ,typeArgs));
         }
@@ -616,10 +617,10 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
         auto f = t->functor();
         if(InductionHelper::isInductionTermFunctor(f)){
           if(InductionHelper::isStructInductionOn() && InductionHelper::isStructInductionTerm(t)){
-            vvector<Term*> indTerms = { t };
+            std::vector<Term*> indTerms = { t };
             auto it = ta_terms.find(indTerms);
             if (it == ta_terms.end()) {
-              ta_terms.insert(make_pair(indTerms,vset<pair<const InductionTemplate*,vvector<Term*>>>()));
+              ta_terms.insert(make_pair(indTerms,std::set<pair<const InductionTemplate*,std::vector<Term*>>>()));
             }
           }
           if(InductionHelper::isIntInductionOneOn() && InductionHelper::isIntInductionTermListInLiteral(t, lit)){
@@ -628,15 +629,15 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
         }
         auto templ = _fnDefHandler.getInductionTemplate(t);
         if (templ) {
-          vvector<Term*> indTerms;
+          std::vector<Term*> indTerms;
           if (templ->matchesTerm(t, indTerms)) {
-            vvector<Term*> typeArgs;
+            std::vector<Term*> typeArgs;
             for (unsigned i = 0; i < t->numTypeArguments(); i++) {
               typeArgs.push_back(t->nthArgument(i)->term());
             }
             auto it = ta_terms.find(indTerms);
             if (it == ta_terms.end()) {
-              it = ta_terms.insert(make_pair(indTerms,vset<pair<const InductionTemplate*,vvector<Term*>>>())).first;
+              it = ta_terms.insert(make_pair(indTerms,std::set<pair<const InductionTemplate*,std::vector<Term*>>>())).first;
             }
             it->second.insert(make_pair(templ,typeArgs));
           }
@@ -696,13 +697,13 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
       }
     }
     // collect term queries for each induction term
-    auto sideLitsIt = VirtualIterator<pair<vvector<Term*>, VirtualIterator<QueryRes<ResultSubstitutionSP, TermLiteralClause>>>>::getEmpty();
+    auto sideLitsIt = VirtualIterator<pair<std::vector<Term*>, VirtualIterator<QueryRes<ResultSubstitutionSP, TermLiteralClause>>>>::getEmpty();
     if (_opt.nonUnitInduction()) {
       sideLitsIt = pvi(iterTraits(getSTLIterator(ta_terms.begin(), ta_terms.end()))
-        .map([](pair<vvector<Term*>,vset<pair<const InductionTemplate*,vvector<Term*>>>> kv){
+        .map([](pair<std::vector<Term*>,std::set<pair<const InductionTemplate*,std::vector<Term*>>>> kv){
           return kv.first;
         })
-        .map([this](vvector<Term*> ts) {
+        .map([this](std::vector<Term*> ts) {
           auto res = VirtualIterator<QueryRes<ResultSubstitutionSP, TermLiteralClause>>::getEmpty();
           for (const auto& t : ts) {
             res = pvi(concatIters(res, _structInductionTermIndex->getGeneralizations(t, false)));
@@ -731,7 +732,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
       });
     // collect contexts for single-literal induction with given clause
     auto indCtxSingle = iterTraits(getSTLIterator(ta_terms.begin(), ta_terms.end()))
-      .map([&lit,&premise](pair<vvector<Term*>,vset<pair<const InductionTemplate*,vvector<Term*>>>> arg) {
+      .map([&lit,&premise](pair<std::vector<Term*>,std::set<pair<const InductionTemplate*,std::vector<Term*>>>> arg) {
         return InductionContext(arg.first, lit, premise);
       })
       // generalize all contexts if needed
@@ -1527,11 +1528,11 @@ void InductionClauseIterator::performStructInductionThree(const InductionContext
   e->add(std::move(cls), std::move(subst));
 }
 
-void InductionClauseIterator::performRecursionInduction(const InductionContext& context, const InductionTemplate* templ, const vvector<Term*>& typeArgs, InductionFormulaIndex::Entry* e)
+void InductionClauseIterator::performRecursionInduction(const InductionContext& context, const InductionTemplate* templ, const std::vector<Term*>& typeArgs, InductionFormulaIndex::Entry* e)
 {
   unsigned var = 0;
   FormulaList* formulas = FormulaList::empty();
-  vvector<TermList> ts(context._indTerms.size(), TermList());
+  std::vector<TermList> ts(context._indTerms.size(), TermList());
   auto& indPos = templ->inductionPositions();
   auto header = templ->branches().begin()->_header;
   Substitution typeSubst;