From 291d3186a2e89b388630e67b1db61f3582e8f3ae Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Mon, 17 Jun 2024 15:27:51 +0100 Subject: [PATCH] also remove vstringstream, vvector, vmap, vset, and friends --- CASC/PortfolioMode.hpp | 2 - CMakeLists.txt | 2 - DP/SimpleCongruenceClosure.cpp | 4 +- FMB/FiniteModel.cpp | 2 +- FMB/FiniteModelMultiSorted.cpp | 2 +- FMB/FunctionRelationshipInference.cpp | 1 - Forwards.hpp | 5 +- Indexing/CodeTree.hpp | 4 +- Indexing/RequestedIndex.hpp | 1 - .../BackwardSubsumptionDemodulation.cpp | 12 ++-- .../BackwardSubsumptionDemodulation.hpp | 4 +- Inferences/ForwardSubsumptionDemodulation.cpp | 7 +-- Inferences/Induction.cpp | 47 ++++++++------- Inferences/Induction.hpp | 37 ++++++------ Inferences/SubsumptionDemodulationHelper.cpp | 8 +-- Inferences/SubsumptionDemodulationHelper.hpp | 12 ++-- Kernel/Inference.hpp | 2 - Kernel/InferenceStore.cpp | 6 +- Kernel/InferenceStore.hpp | 1 - Kernel/KBO.cpp | 6 +- Kernel/KBOComparator.cpp | 2 +- Kernel/LPOComparator.cpp | 4 +- Kernel/MLMatcher.cpp | 12 ++-- Kernel/MLMatcher.hpp | 7 +-- Kernel/MLMatcherSD.cpp | 12 ++-- Kernel/MLMatcherSD.hpp | 5 +- Kernel/OperatorType.hpp | 1 - Kernel/Renaming.hpp | 4 -- Kernel/RobSubstitution.hpp | 1 - Kernel/Signature.hpp | 1 - Kernel/Substitution.cpp | 2 +- Kernel/Substitution.hpp | 1 - Kernel/Unit.hpp | 1 - Lib/Allocator.cpp | 2 + Lib/Backtrackable.hpp | 1 - Lib/Exception.cpp | 1 - Lib/Exception.hpp | 7 ++- Lib/Hash.hpp | 1 - Lib/Int.hpp | 3 +- Lib/IntNameTable.cpp | 1 - Lib/IntNameTable.hpp | 2 - Lib/Map.hpp | 1 - Lib/STL.hpp | 60 ------------------- Lib/ScopeGuard.hpp | 1 - Lib/SharedSet.hpp | 3 +- Lib/StringUtils.hpp | 1 - Lib/Timer.hpp | 3 +- Lib/VString.hpp | 33 ---------- Lib/Vector.hpp | 1 - Parse/SMTLIB2.cpp | 3 +- SAT/SATClause.hpp | 1 - SAT/SATLiteral.hpp | 1 - SAT/Z3Interfacing.cpp | 4 +- .../PredicateSplitPassiveClauseContainer.cpp | 12 ++-- .../PredicateSplitPassiveClauseContainer.hpp | 23 ++++--- Saturation/SaturationAlgorithm.cpp | 11 ++-- Saturation/Splitter.cpp | 2 +- Shell/AnswerExtractor.cpp | 4 +- Shell/AnswerExtractor.hpp | 4 +- Shell/CommandLine.cpp | 1 - Shell/FunctionDefinitionHandler.cpp | 38 ++++++------ Shell/FunctionDefinitionHandler.hpp | 21 ++++--- Shell/LaTeX.hpp | 1 - Shell/LispParser.hpp | 1 - Shell/Options.cpp | 31 +++++----- Shell/Options.hpp | 18 +++--- Shell/Property.hpp | 1 - Shell/TPTPPrinter.cpp | 2 +- Shell/TermAlgebra.hpp | 1 - Shell/Token.cpp | 1 + Shell/Token.hpp | 2 - Shell/UIHelper.cpp | 3 +- Shell/VarManager.hpp | 2 - Test/SyntaxSugar.hpp | 2 +- Test/UnitTesting.hpp | 3 - UnitTests/tCoproduct.cpp | 2 +- UnitTests/tFunctionDefinitionHandler.cpp | 2 +- UnitTests/tInduction.cpp | 4 +- UnitTests/tOptionConstraints.cpp | 1 - vampire.cpp | 1 - 80 files changed, 206 insertions(+), 336 deletions(-) delete mode 100644 Lib/STL.hpp delete mode 100644 Lib/VString.hpp diff --git a/CASC/PortfolioMode.hpp b/CASC/PortfolioMode.hpp index f7b4f82092..cc93c376f8 100644 --- a/CASC/PortfolioMode.hpp +++ b/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" diff --git a/CMakeLists.txt b/CMakeLists.txt index a68a93686a..efc2929cab 100644 --- a/CMakeLists.txt +++ b/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}) diff --git a/DP/SimpleCongruenceClosure.cpp b/DP/SimpleCongruenceClosure.cpp index ed269c2fa2..20da28c214 100644 --- a/DP/SimpleCongruenceClosure.cpp +++ b/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<<"="< -#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 class VirtualIterator; template class ScopedPtr; diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index f9afa4233c..160021f941 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -297,7 +297,7 @@ class CodeTree */ CodeOp landingOp; Kind kind; - vvector targets; + std::vector targets; protected: SearchStruct(Kind kind, size_t length); @@ -319,7 +319,7 @@ class CodeTree */ template CodeOp*& targetOp(const T& val); - vvector values; + std::vector values; }; using FnSearchStruct = SearchStructImpl; diff --git a/Indexing/RequestedIndex.hpp b/Indexing/RequestedIndex.hpp index 569a8589f4..48b3a85e3c 100644 --- a/Indexing/RequestedIndex.hpp +++ b/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 { diff --git a/Inferences/BackwardSubsumptionDemodulation.cpp b/Inferences/BackwardSubsumptionDemodulation.cpp index f17e71dcfd..94b9063790 100644 --- a/Inferences/BackwardSubsumptionDemodulation.cpp +++ b/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 simplificationsStorage; + static std::vector 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& simplifications) +void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, std::vector& 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& simplifications) +bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector& simplifications) { - static vvector alts; + static std::vector alts; alts.clear(); alts.resize(sideCl->length(), LiteralList::empty()); @@ -383,7 +383,7 @@ 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 isMatched; + static std::vector isMatched; matcher.getMatchedAltsBitmap(isMatched); static OverlayBinder binder; @@ -391,7 +391,7 @@ bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* m matcher.getBindings(binder.base()); // NOTE: for explanation see comments in ForwardSubsumptionDemodulation::perform - static vvector lhsVector; + static std::vector lhsVector; lhsVector.clear(); { TermList t0 = *eqLit->nthArgument(0); diff --git a/Inferences/BackwardSubsumptionDemodulation.hpp b/Inferences/BackwardSubsumptionDemodulation.hpp index e722bba040..a4cca326b6 100644 --- a/Inferences/BackwardSubsumptionDemodulation.hpp +++ b/Inferences/BackwardSubsumptionDemodulation.hpp @@ -62,8 +62,8 @@ class BackwardSubsumptionDemodulation bool _preorderedOnly; bool _allowIncompleteness; - void performWithQueryLit(Clause* premise, Literal* candidateQueryLit, vvector& simplifications); - bool simplifyCandidate(Clause* sideCl, Clause* mainCl, vvector& simplifications); + void performWithQueryLit(Clause* premise, Literal* candidateQueryLit, std::vector& simplifications); + bool simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector& simplifications); bool rewriteCandidate(Clause* sideCl, Clause* mainCl, MLMatcherSD const& matcher, Clause*& replacement); }; diff --git a/Inferences/ForwardSubsumptionDemodulation.cpp b/Inferences/ForwardSubsumptionDemodulation.cpp index 195a1f4796..68996e5817 100644 --- a/Inferences/ForwardSubsumptionDemodulation.cpp +++ b/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 @@ -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 alts; + static std::vector 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 isMatched; + static std::vector 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 lhsVector; + static std::vector lhsVector; lhsVector.clear(); { TermList t0 = *eqLit->nthArgument(0); diff --git a/Inferences/Induction.cpp b/Inferences/Induction.cpp index 5a34b5ba14..a0eee1cf25 100644 --- a/Inferences/Induction.cpp +++ b/Inferences/Induction.cpp @@ -13,6 +13,7 @@ */ #include +#include #include "Debug/Output.hpp" #include "Forwards.hpp" @@ -70,7 +71,7 @@ Term* ActiveOccurrenceIterator::next() return t; } -Term* getPlaceholderForTerm(const vvector& ts, unsigned i) +Term* getPlaceholderForTerm(const std::vector& ts, unsigned i) { static DHMap,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& r, bool opposite, Substitution* subst) const +Formula* InductionContext::getFormula(const std::vector& 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 replacementMap; + std::map 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& r, bool opposite, return getFormula(tr, opposite); } -Formula* InductionContext::getFormulaWithSquashedSkolems(const vvector& r, bool opposite, +Formula* InductionContext::getFormulaWithSquashedSkolems(const std::vector& r, bool opposite, unsigned& var, VList** varList, Substitution* subst) const { const bool strengthenHyp = env.options->inductionStrengthenHypothesis(); if (!strengthenHyp) { return getFormula(r, opposite, subst); } - vmap replacementMap; + std::map 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 return res; } -vmap getContextReplacementMap(const InductionContext& context, bool inverse = false) +std::map getContextReplacementMap(const InductionContext& context, bool inverse = false) { - vmap m; + std::map 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 operator()(pair, VirtualIterator>> arg) { + VirtualIterator operator()(pair, VirtualIterator>> 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 int_terms; - vmap,vset>>> ta_terms; + std::map,std::set>>> ta_terms; auto templ = _fnDefHandler.getInductionTemplate(lit); if (templ) { - vvector indTerms; + std::vector indTerms; if (templ->matchesTerm(lit, indTerms)) { - vvector typeArgs; + std::vector 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>>())).first; + it = ta_terms.insert(make_pair(indTerms,std::set>>())).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 indTerms = { t }; + std::vector indTerms = { t }; auto it = ta_terms.find(indTerms); if (it == ta_terms.end()) { - ta_terms.insert(make_pair(indTerms,vset>>())); + ta_terms.insert(make_pair(indTerms,std::set>>())); } } 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 indTerms; + std::vector indTerms; if (templ->matchesTerm(t, indTerms)) { - vvector typeArgs; + std::vector 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>>())).first; + it = ta_terms.insert(make_pair(indTerms,std::set>>())).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, VirtualIterator>>>::getEmpty(); + auto sideLitsIt = VirtualIterator, VirtualIterator>>>::getEmpty(); if (_opt.nonUnitInduction()) { sideLitsIt = pvi(iterTraits(getSTLIterator(ta_terms.begin(), ta_terms.end())) - .map([](pair,vset>>> kv){ + .map([](pair,std::set>>> kv){ return kv.first; }) - .map([this](vvector ts) { + .map([this](std::vector ts) { auto res = VirtualIterator>::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,vset>>> arg) { + .map([&lit,&premise](pair,std::set>>> 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& typeArgs, InductionFormulaIndex::Entry* e) +void InductionClauseIterator::performRecursionInduction(const InductionContext& context, const InductionTemplate* templ, const std::vector& typeArgs, InductionFormulaIndex::Entry* e) { unsigned var = 0; FormulaList* formulas = FormulaList::empty(); - vvector ts(context._indTerms.size(), TermList()); + std::vector ts(context._indTerms.size(), TermList()); auto& indPos = templ->inductionPositions(); auto header = templ->branches().begin()->_header; Substitution typeSubst; diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index ea8a0bd691..d698b84cb9 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -18,6 +18,7 @@ #include #include +#include #include "Forwards.hpp" @@ -96,7 +97,7 @@ struct StlClauseHash { * formulas can be easily detected. We allow multiple induction terms, * so we have to index the placeholders as well with @b i. */ -Term* getPlaceholderForTerm(const vvector& ts, unsigned i); +Term* getPlaceholderForTerm(const std::vector& ts, unsigned i); /** * Term transformer class that replaces @@ -104,10 +105,10 @@ Term* getPlaceholderForTerm(const vvector& ts, unsigned i); */ class TermReplacement : public TermTransformer { public: - TermReplacement(const vmap& m) : _m(m) {} + TermReplacement(const std::map& m) : _m(m) {} TermList transformSubterm(TermList trm) override; protected: - vmap _m; + std::map _m; }; /** @@ -116,7 +117,7 @@ class TermReplacement : public TermTransformer { */ class SkolemSquashingTermReplacement : public TermReplacement { public: - SkolemSquashingTermReplacement(const vmap& m, unsigned& var) + SkolemSquashingTermReplacement(const std::map& m, unsigned& var) : TermReplacement(m), _v(var) {} TermList transformSubterm(TermList trm) override; DHMap _tv; // maps terms to their variable replacement @@ -131,11 +132,11 @@ class SkolemSquashingTermReplacement : public TermReplacement { * which are inducted upon. */ struct InductionContext { - explicit InductionContext(vvector&& ts) + explicit InductionContext(std::vector&& ts) : _indTerms(ts) {} - explicit InductionContext(const vvector& ts) + explicit InductionContext(const std::vector& ts) : _indTerms(ts) {} - InductionContext(const vvector& ts, Literal* l, Clause* cl) + InductionContext(const std::vector& ts, Literal* l, Clause* cl) : InductionContext(ts) { insert(cl, l); @@ -150,12 +151,12 @@ struct InductionContext { // These two functions should be only called on objects where // all induction term occurrences actually inducted upon are // replaced with placeholders (e.g. with ContextReplacement). - Formula* getFormula(const vvector& r, bool opposite, Substitution* subst = nullptr) const; - Formula* getFormulaWithSquashedSkolems(const vvector& r, bool opposite, unsigned& var, + Formula* getFormula(const std::vector& r, bool opposite, Substitution* subst = nullptr) const; + Formula* getFormulaWithSquashedSkolems(const std::vector& r, bool opposite, unsigned& var, VList** varList = nullptr, Substitution* subst = nullptr) const; vstring toString() const { - vstringstream str; + std::stringstream str; for (const auto& indt : _indTerms) { str << *indt << std::endl; } @@ -168,7 +169,7 @@ struct InductionContext { return str.str(); } - vvector _indTerms; + std::vector _indTerms; // One could induct on all literals of a clause, but if a literal // doesn't contain the induction term, it just introduces a couple // of tautologies and duplicate literals (a hypothesis clause will @@ -176,7 +177,7 @@ struct InductionContext { // we only store the literals we actually induct on. An alternative // would be storing indices but then we need to pass around the // clause as well. - vunordered_map _cls; + std::unordered_map _cls; private: /** * Creates a formula which corresponds to the conjunction of disjunction @@ -223,8 +224,8 @@ class ActiveOccurrenceContextReplacement private: FunctionDefinitionHandler& _fnDefHandler; - vvector _iteration; - vvector _matchCount; + std::vector _iteration; + std::vector _matchCount; bool _hasNonActive; }; @@ -248,10 +249,10 @@ class ContextSubsetReplacement bool shouldSkipIteration() const; void stepIteration(); // _iteration serves as a map of occurrences to replace - vvector _iteration; - vvector _maxIterations; + std::vector _iteration; + std::vector _maxIterations; // Counts how many occurrences were already encountered in one transformation - vvector _matchCount; + std::vector _matchCount; const unsigned _maxOccurrences = 1 << 20; const unsigned _maxSubsetSize; bool _ready; @@ -335,7 +336,7 @@ class InductionClauseIterator void performStructInductionOne(const InductionContext& context, InductionFormulaIndex::Entry* e); void performStructInductionTwo(const InductionContext& context, InductionFormulaIndex::Entry* e); void performStructInductionThree(const InductionContext& context, InductionFormulaIndex::Entry* e); - void performRecursionInduction(const InductionContext& context, const InductionTemplate* templ, const vvector& typeArgs, InductionFormulaIndex::Entry* e); + void performRecursionInduction(const InductionContext& context, const InductionTemplate* templ, const std::vector& typeArgs, InductionFormulaIndex::Entry* e); /** * Whether an induction formula is applicable (or has already been generated) diff --git a/Inferences/SubsumptionDemodulationHelper.cpp b/Inferences/SubsumptionDemodulationHelper.cpp index 89bd62fb18..cfe6612ef6 100644 --- a/Inferences/SubsumptionDemodulationHelper.cpp +++ b/Inferences/SubsumptionDemodulationHelper.cpp @@ -171,12 +171,12 @@ SDHelper::ClauseComparisonResult SDHelper::clauseCompare(Literal* const lits1[], ASS(env.options->literalComparisonMode() != Options::LiteralComparisonMode::REVERSE); // Copy given literals so we can sort them - vvector c1(lits1, lits1+n1); - vvector c2(lits2, lits2+n2); + std::vector c1(lits1, lits1+n1); + std::vector c2(lits2, lits2+n2); // These will contain literals from c1/c2 with equal occurrences removed - vvector v1; - vvector v2; + std::vector v1; + std::vector v2; // The equality tests below only make sense for shared literals std::for_each(c1.begin(), c1.end(), [](Literal* lit) { ASS(lit->shared()); }); diff --git a/Inferences/SubsumptionDemodulationHelper.hpp b/Inferences/SubsumptionDemodulationHelper.hpp index 7a0e644948..e425bbdc34 100644 --- a/Inferences/SubsumptionDemodulationHelper.hpp +++ b/Inferences/SubsumptionDemodulationHelper.hpp @@ -11,13 +11,13 @@ #ifndef SUBSUMPTIONDEMODULATIONHELPER_HPP #define SUBSUMPTIONDEMODULATIONHELPER_HPP +#include + #include "Indexing/LiteralMiniIndex.hpp" #include "Kernel/Clause.hpp" #include "Kernel/Ordering.hpp" #include "Kernel/SubstHelper.hpp" #include "Kernel/Term.hpp" -#include "Lib/STL.hpp" - // Set to true to output FSD inferences on stdout @@ -62,7 +62,7 @@ class OverlayBinder public: using Var = unsigned int; - using BindingsMap = vunordered_map; + using BindingsMap = std::unordered_map; OverlayBinder() : m_base(16) @@ -262,7 +262,7 @@ class SDClauseMatches private: Clause* m_base; - vvector m_alts; + std::vector m_alts; unsigned m_basePosEqs; unsigned m_baseLitsWithoutAlts; unsigned m_basePosEqsWithoutAlts; @@ -290,7 +290,7 @@ class SDHelper template static ClauseComparisonResult substClauseCompare(Clause* mcl, Applicator const& applicator, Clause* cl, Ordering const& ordering) { - vvector mclS(mcl->literals(), mcl->literals() + mcl->length()); + std::vector mclS(mcl->literals(), mcl->literals() + mcl->length()); ASS_EQ(mcl->length(), mclS.size()); for (auto it = mclS.begin(); it != mclS.end(); ++it) { *it = applicator.applyTo(*it); @@ -342,7 +342,7 @@ class SDHelper template bool termContainsAllVariablesOfOtherUnderSubst(TermList term, TermList other, Applicator const& applicator) { - static vunordered_set vars(16); + static std::unordered_set vars(16); vars.clear(); static VariableIterator vit; diff --git a/Kernel/Inference.hpp b/Kernel/Inference.hpp index 17441b4a98..bdab1c2af6 100644 --- a/Kernel/Inference.hpp +++ b/Kernel/Inference.hpp @@ -20,12 +20,10 @@ #include #include "Lib/Allocator.hpp" -#include "Lib/VString.hpp" #include "Forwards.hpp" #include #include -#include using namespace Lib; diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 07d32050fe..176565d9dd 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -638,7 +638,7 @@ struct InferenceStore::TPTPProofPrinter /** It is an iterator over SymbolId */ template vstring getNewSymbols(vstring origin, It symIt) { - vostringstream symsStr; + std::ostringstream symsStr; while(symIt.hasNext()) { SymbolId sym = symIt.next(); if (sym.first == SymbolType::FUNC ) { @@ -831,7 +831,7 @@ struct InferenceStore::TPTPProofPrinter List::destroy(nameVars); SymbolId nameSymbol = SymbolId(SymbolType::PRED,nameLit->functor()); - vostringstream originStm; + std::ostringstream originStm; originStm << "introduced(" << tptpRuleName(rule) << ",[" << getNewSymbols("naming",getSingletonIterator(nameSymbol)) << "])"; @@ -856,7 +856,7 @@ struct InferenceStore::TPTPProofPrinter out< KBO::weightsFromFile(const Options& opts) const for (vstring ln; getline(file, ln);) { unsigned dflt; vstring special_name; - bool err = !(vstringstream(ln) >> special_name >> dflt); + bool err = !(std::stringstream(ln) >> special_name >> dflt); if (!err && special_name == SPECIAL_WEIGHT_IDENT_DEFAULT_WEIGHT) { return dflt; } @@ -564,7 +564,7 @@ KboWeightMap KBO::weightsFromFile(const Options& opts) const /** tries to parse line of the form ` ` */ auto tryParseSpecialLine = [](const vstring& ln, unsigned& introducedWeight, KboSpecialWeights& specialWeights) -> bool { - vstringstream lnstr(ln); + std::stringstream lnstr(ln); vstring name; unsigned weight; @@ -582,7 +582,7 @@ KboWeightMap KBO::weightsFromFile(const Options& opts) const /** tries to parse line of the form ` ` */ auto tryParseNormalLine = [&](const vstring& ln) -> bool { - vstringstream lnstr(ln); + std::stringstream lnstr(ln); vstring name; unsigned arity; diff --git a/Kernel/KBOComparator.cpp b/Kernel/KBOComparator.cpp index 12c87e3bf5..60a0a00da6 100644 --- a/Kernel/KBOComparator.cpp +++ b/Kernel/KBOComparator.cpp @@ -272,7 +272,7 @@ void KBOComparator::countSymbols(const KBO& kbo, DHMap& vars, int& vstring KBOComparator::toString() const { - vstringstream str; + std::stringstream str; unsigned cnt = 1; for (unsigned i = 0; i < _instructions.size();) { diff --git a/Kernel/LPOComparator.cpp b/Kernel/LPOComparator.cpp index 5cde4bbde0..a56dcd4cd4 100644 --- a/Kernel/LPOComparator.cpp +++ b/Kernel/LPOComparator.cpp @@ -79,7 +79,7 @@ ostream& operator<<(ostream& out, const Instruction& n) vstring LPOComparator::toString() const { - vstringstream str; + std::stringstream str; switch (_res) { case BranchTag::T_EQUAL: str << "equal" << endl; @@ -148,7 +148,7 @@ void deleteDuplicates(Stack& st) { unsigned removedCnt = 0; Map lastPos; - vvector removedAfter(st.size(),0); + std::vector removedAfter(st.size(),0); // First pass, remember the last position of // any duplicate instruction, and update every diff --git a/Kernel/MLMatcher.cpp b/Kernel/MLMatcher.cpp index 878f3d53f2..2cb88c1581 100644 --- a/Kernel/MLMatcher.cpp +++ b/Kernel/MLMatcher.cpp @@ -365,9 +365,9 @@ class MLMatcher::Impl final void init(Literal** baseLits, unsigned baseLen, Clause* instance, LiteralList const* const* alts, Literal* resolvedLit, bool multiset); bool nextMatch(); - void getMatchedAltsBitmap(vvector& outMatchedBitmap) const; + void getMatchedAltsBitmap(std::vector& outMatchedBitmap) const; - void getBindings(vunordered_map& outBindings) const; + void getBindings(std::unordered_map& outBindings) const; // Disallow copy and move because the internal implementation still uses pointers to the underlying storage and it seems hard to untangle that. Impl(Impl const&) = delete; @@ -636,7 +636,7 @@ bool MLMatcher::Impl::nextMatch() } -void MLMatcher::Impl::getMatchedAltsBitmap(vvector& outMatchedBitmap) const +void MLMatcher::Impl::getMatchedAltsBitmap(std::vector& outMatchedBitmap) const { MatchingData const* const md = &s_matchingData; @@ -657,7 +657,7 @@ void MLMatcher::Impl::getMatchedAltsBitmap(vvector& outMatchedBitmap) cons } -void MLMatcher::Impl::getBindings(vunordered_map& outBindings) const +void MLMatcher::Impl::getBindings(std::unordered_map& outBindings) const { MatchingData const* const md = &s_matchingData; @@ -707,13 +707,13 @@ bool MLMatcher::nextMatch() return m_impl->nextMatch(); } -void MLMatcher::getMatchedAltsBitmap(vvector& outMatchedBitmap) const +void MLMatcher::getMatchedAltsBitmap(std::vector& outMatchedBitmap) const { ASS(m_impl); m_impl->getMatchedAltsBitmap(outMatchedBitmap); } -void MLMatcher::getBindings(vunordered_map& outBindings) const +void MLMatcher::getBindings(std::unordered_map& outBindings) const { ASS(m_impl); m_impl->getBindings(outBindings); diff --git a/Kernel/MLMatcher.hpp b/Kernel/MLMatcher.hpp index 60c53bc2ec..fe37c2c75a 100644 --- a/Kernel/MLMatcher.hpp +++ b/Kernel/MLMatcher.hpp @@ -16,9 +16,8 @@ #ifndef __MLMatcher__ #define __MLMatcher__ -#include "Clause.hpp" #include "Forwards.hpp" -#include "Lib/STL.hpp" +#include "Clause.hpp" namespace Kernel { @@ -99,13 +98,13 @@ class MLMatcher * * The given vector will be cleared before operating on it. */ - void getMatchedAltsBitmap(vvector& outMatchedBitmap) const; + void getMatchedAltsBitmap(std::vector& outMatchedBitmap) const; /** * Returns the variable bindings due to the current match. * May only be called in a matched state (i.e., after nextMatch() has returned true). */ - void getBindings(vunordered_map& outBindings) const; + void getBindings(std::unordered_map& outBindings) const; // Disallow copy because the internal implementation still uses pointers to the underlying storage and it seems hard to untangle that. MLMatcher(MLMatcher const&) = delete; diff --git a/Kernel/MLMatcherSD.cpp b/Kernel/MLMatcherSD.cpp index d71500b205..0ae30a48e1 100644 --- a/Kernel/MLMatcherSD.cpp +++ b/Kernel/MLMatcherSD.cpp @@ -711,9 +711,9 @@ class MLMatcherSD::Impl final Literal* getEqualityForDemodulation() const; - void getMatchedAltsBitmap(vvector& outMatchedBitmap) const; + void getMatchedAltsBitmap(std::vector& outMatchedBitmap) const; - void getBindings(vunordered_map& outBindings) const; + void getBindings(std::unordered_map& outBindings) const; // Disallow copy and move because the internal implementation still uses pointers to the underlying storage and it seems hard to untangle that. Impl(Impl const&) = delete; @@ -1093,7 +1093,7 @@ Literal* MLMatcherSD::Impl::getEqualityForDemodulation() const } } -void MLMatcherSD::Impl::getMatchedAltsBitmap(vvector& outMatchedBitmap) const +void MLMatcherSD::Impl::getMatchedAltsBitmap(std::vector& outMatchedBitmap) const { MatchingData const* const md = &s_matchingData; @@ -1111,7 +1111,7 @@ void MLMatcherSD::Impl::getMatchedAltsBitmap(vvector& outMatchedBitmap) co } -void MLMatcherSD::Impl::getBindings(vunordered_map& outBindings) const +void MLMatcherSD::Impl::getBindings(std::unordered_map& outBindings) const { MatchingData const* const md = &s_matchingData; @@ -1169,13 +1169,13 @@ Literal* MLMatcherSD::getEqualityForDemodulation() const return m_impl->getEqualityForDemodulation(); } -void MLMatcherSD::getMatchedAltsBitmap(vvector& outMatchedBitmap) const +void MLMatcherSD::getMatchedAltsBitmap(std::vector& outMatchedBitmap) const { ASS(m_impl); m_impl->getMatchedAltsBitmap(outMatchedBitmap); } -void MLMatcherSD::getBindings(vunordered_map& outBindings) const +void MLMatcherSD::getBindings(std::unordered_map& outBindings) const { ASS(m_impl); m_impl->getBindings(outBindings); diff --git a/Kernel/MLMatcherSD.hpp b/Kernel/MLMatcherSD.hpp index 6214b1b50a..44857f8718 100644 --- a/Kernel/MLMatcherSD.hpp +++ b/Kernel/MLMatcherSD.hpp @@ -13,7 +13,6 @@ #include "Clause.hpp" #include "Forwards.hpp" -#include "Lib/STL.hpp" namespace Kernel { @@ -89,13 +88,13 @@ class MLMatcherSD final * * The given vector will be cleared before operating on it. */ - void getMatchedAltsBitmap(vvector& outMatchedBitmap) const; + void getMatchedAltsBitmap(std::vector& outMatchedBitmap) const; /** * Returns the variable bindings due to the current match. * May only be called in a matched state (i.e., after nextMatch() has returned true). */ - void getBindings(vunordered_map& outBindings) const; + void getBindings(std::unordered_map& outBindings) const; // Disallow copy because the internal implementation still uses pointers to the underlying storage and it seems hard to untangle that. MLMatcherSD(MLMatcherSD const&) = delete; diff --git a/Kernel/OperatorType.hpp b/Kernel/OperatorType.hpp index 543678d884..c42e47d929 100644 --- a/Kernel/OperatorType.hpp +++ b/Kernel/OperatorType.hpp @@ -25,7 +25,6 @@ #include "Lib/Stack.hpp" #include "Lib/Vector.hpp" #include "Lib/Allocator.hpp" -#include "Lib/VString.hpp" #include "Term.hpp" diff --git a/Kernel/Renaming.hpp b/Kernel/Renaming.hpp index 381d51b0e8..95b7fb3d7c 100644 --- a/Kernel/Renaming.hpp +++ b/Kernel/Renaming.hpp @@ -16,10 +16,6 @@ #ifndef __Renaming__ #define __Renaming__ -#if VDEBUG -#include "Lib/VString.hpp" -#endif - #include "Lib/DHMap.hpp" #include "Lib/VirtualIterator.hpp" #include "Lib/Metaiterators.hpp" diff --git a/Kernel/RobSubstitution.hpp b/Kernel/RobSubstitution.hpp index d1bdd8d346..4a8cfad34d 100644 --- a/Kernel/RobSubstitution.hpp +++ b/Kernel/RobSubstitution.hpp @@ -32,7 +32,6 @@ #if VDEBUG #include -#include "Lib/VString.hpp" #endif diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 497665ed5e..57d6b5f624 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -28,7 +28,6 @@ #include "Lib/Map.hpp" #include "Lib/List.hpp" #include "Lib/DHMap.hpp" -#include "Lib/VString.hpp" #include "Lib/Environment.hpp" #include "Lib/SmartPtr.hpp" diff --git a/Kernel/Substitution.cpp b/Kernel/Substitution.cpp index f2038626bf..7721f55848 100644 --- a/Kernel/Substitution.cpp +++ b/Kernel/Substitution.cpp @@ -98,7 +98,7 @@ bool Substitution::findBinding(int var, TermList& res) const #if VDEBUG vstring Substitution::toString() const { - vstringstream out; + std::stringstream out; out << *this; return out.str(); } // Substitution::toString() diff --git a/Kernel/Substitution.hpp b/Kernel/Substitution.hpp index ad05df9523..77488171d8 100644 --- a/Kernel/Substitution.hpp +++ b/Kernel/Substitution.hpp @@ -21,7 +21,6 @@ #include "Lib/DHMap.hpp" #include "Lib/Environment.hpp" -#include "Lib/VString.hpp" #include "Lib/Allocator.hpp" diff --git a/Kernel/Unit.hpp b/Kernel/Unit.hpp index 7fb1412ab5..8c76139a4d 100644 --- a/Kernel/Unit.hpp +++ b/Kernel/Unit.hpp @@ -20,7 +20,6 @@ #include "Forwards.hpp" #include "Lib/List.hpp" -#include "Lib/VString.hpp" #include "Kernel/Inference.hpp" namespace Kernel { diff --git a/Lib/Allocator.cpp b/Lib/Allocator.cpp index 8275c7f090..ef8af07a87 100644 --- a/Lib/Allocator.cpp +++ b/Lib/Allocator.cpp @@ -19,6 +19,8 @@ #include "Allocator.hpp" #include "Lib/Timer.hpp" +#include + #ifndef INDIVIDUAL_ALLOCATIONS Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR; #endif diff --git a/Lib/Backtrackable.hpp b/Lib/Backtrackable.hpp index 5761f02680..7e1393a383 100644 --- a/Lib/Backtrackable.hpp +++ b/Lib/Backtrackable.hpp @@ -17,7 +17,6 @@ #include "List.hpp" #include "Int.hpp" -#include "VString.hpp" #include "Lib/Stack.hpp" namespace Lib diff --git a/Lib/Exception.cpp b/Lib/Exception.cpp index 311e5588fe..ac3fe1fa7e 100644 --- a/Lib/Exception.cpp +++ b/Lib/Exception.cpp @@ -18,7 +18,6 @@ #include "Int.hpp" #include "Exception.hpp" -#include "VString.hpp" namespace Lib { diff --git a/Lib/Exception.hpp b/Lib/Exception.hpp index 0ff144fbcb..bec45aa252 100644 --- a/Lib/Exception.hpp +++ b/Lib/Exception.hpp @@ -16,9 +16,10 @@ #ifndef __Exception__ #define __Exception__ -#include +#include "Forwards.hpp" -#include "VString.hpp" +#include +#include namespace Lib { @@ -54,7 +55,7 @@ class Exception : public ThrowableBase { template vstring toString(Msg... msg){ - vstringstream out; + std::stringstream out; OutputAll::apply(out, msg...); return out.str(); } diff --git a/Lib/Hash.hpp b/Lib/Hash.hpp index 947e038990..1ec13e0451 100644 --- a/Lib/Hash.hpp +++ b/Lib/Hash.hpp @@ -20,7 +20,6 @@ #include #include "Forwards.hpp" -#include "VString.hpp" #include "Kernel/Unit.hpp" #include "Lib/Option.hpp" diff --git a/Lib/Int.hpp b/Lib/Int.hpp index fff08b9407..0a2a1d41e5 100644 --- a/Lib/Int.hpp +++ b/Lib/Int.hpp @@ -18,9 +18,10 @@ #ifndef __INT__ #define __INT__ +#include "Forwards.hpp" + #include "Comparison.hpp" #include "Portability.hpp" -#include "VString.hpp" #include #include diff --git a/Lib/IntNameTable.cpp b/Lib/IntNameTable.cpp index 90a9716cf9..37f0bf7f57 100644 --- a/Lib/IntNameTable.cpp +++ b/Lib/IntNameTable.cpp @@ -16,7 +16,6 @@ #include "IntNameTable.hpp" #include "Hash.hpp" #include "Exception.hpp" -#include "VString.hpp" namespace Lib { diff --git a/Lib/IntNameTable.hpp b/Lib/IntNameTable.hpp index 30e1d5c7e2..e5f81a7c41 100644 --- a/Lib/IntNameTable.hpp +++ b/Lib/IntNameTable.hpp @@ -23,8 +23,6 @@ #include "Array.hpp" #include "Map.hpp" -#include "VString.hpp" - namespace Lib { diff --git a/Lib/Map.hpp b/Lib/Map.hpp index a9161b9ba1..38cd681c8f 100644 --- a/Lib/Map.hpp +++ b/Lib/Map.hpp @@ -20,7 +20,6 @@ #include "Debug/Assertion.hpp" #include "Allocator.hpp" -#include "VString.hpp" #include "Hash.hpp" #include "Exception.hpp" #include "Option.hpp" diff --git a/Lib/STL.hpp b/Lib/STL.hpp deleted file mode 100644 index 0ea4c5a033..0000000000 --- a/Lib/STL.hpp +++ /dev/null @@ -1,60 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ - -#ifndef STL_HPP -#define STL_HPP - -#include -#include -#include -#include -#include -#include -#include -#include -#include - -namespace Lib { - - -template< typename Key - , typename T - , typename Compare = std::less - > -using vmap = std::map; - - -template< typename Key - , typename Compare = std::less - > -using vset = std::set; - - -template< typename Key - , typename T - , typename Hash = std::hash - , typename KeyEqual = std::equal_to - > -using vunordered_map = std::unordered_map; - - -template< typename Key - , typename Hash = std::hash - , typename KeyEqual = std::equal_to - > -using vunordered_set = std::unordered_set; - - -template< typename T > -using vvector = std::vector; - -} // namespace Lib - -#endif /* !STL_HPP */ diff --git a/Lib/ScopeGuard.hpp b/Lib/ScopeGuard.hpp index 44f8eb4c50..7e620377c8 100644 --- a/Lib/ScopeGuard.hpp +++ b/Lib/ScopeGuard.hpp @@ -11,7 +11,6 @@ #ifndef SCOPEGUARD_HPP #define SCOPEGUARD_HPP -#include "Lib/STL.hpp" #include #include diff --git a/Lib/SharedSet.hpp b/Lib/SharedSet.hpp index 9d7687e347..f778d4b1d1 100644 --- a/Lib/SharedSet.hpp +++ b/Lib/SharedSet.hpp @@ -24,7 +24,6 @@ #include "Set.hpp" #include "Sort.hpp" #include "Stack.hpp" -#include "VString.hpp" namespace Lib { @@ -303,7 +302,7 @@ class SharedSet { vstring toString() const { - vostringstream res; + std::ostringstream res; res<<(*this); return res.str(); } diff --git a/Lib/StringUtils.hpp b/Lib/StringUtils.hpp index 93f0752287..03ae279ec8 100644 --- a/Lib/StringUtils.hpp +++ b/Lib/StringUtils.hpp @@ -15,7 +15,6 @@ #ifndef __StringUtils__ #define __StringUtils__ -#include "VString.hpp" #include "DHMap.hpp" #include diff --git a/Lib/Timer.hpp b/Lib/Timer.hpp index d4c6f8d527..2ea5a70006 100644 --- a/Lib/Timer.hpp +++ b/Lib/Timer.hpp @@ -19,9 +19,10 @@ #include #include +#include "Forwards.hpp" + #include "Debug/Assertion.hpp" #include "Allocator.hpp" -#include "VString.hpp" #define VAMPIRE_PERF_EXISTS 0 #ifdef __linux__ diff --git a/Lib/VString.hpp b/Lib/VString.hpp deleted file mode 100644 index 121d52c21c..0000000000 --- a/Lib/VString.hpp +++ /dev/null @@ -1,33 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file VString.hpp - * Vampire string is basic_string equipped with STLAllocator, - * so that it's allocated via vampire's Allocator. - * - * @since 5/8/2014 Prague. - * @author Martin Suda - */ - - -#ifndef __VString__ -#define __VString__ - -#include -#include - -namespace Lib { -typedef std::string vstring; -typedef std::stringstream vstringstream; -typedef std::istringstream vistringstream; -typedef std::ostringstream vostringstream; -} - -#endif // __VString__ diff --git a/Lib/Vector.hpp b/Lib/Vector.hpp index 5135417d24..b2f3b841f4 100644 --- a/Lib/Vector.hpp +++ b/Lib/Vector.hpp @@ -22,7 +22,6 @@ #include "Debug/Assertion.hpp" #include "Allocator.hpp" -#include "VString.hpp" namespace Indexing { class CodeTree; diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index 4f4493820b..cff5baf32a 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -14,6 +14,7 @@ #include #include +#include #include "Lib/Environment.hpp" #include "Lib/NameArray.hpp" @@ -1747,7 +1748,7 @@ void SMTLIB2::parseMatchEnd(LExpr *exp) LOG2("CASE matched ", matchedTerm.toString()); - vmap ctorFunctors; + std::map ctorFunctors; TermAlgebra *ta = env.signature->getTermAlgebraOfSort(matchedTermSort); if (ta == nullptr) { USER_ERROR_EXPR("Match term '" + matchedTerm.toString() + "' is not of a term algebra type in expression '" + exp->toString() + "'"); diff --git a/SAT/SATClause.hpp b/SAT/SATClause.hpp index 34f6595712..7ffe51f61d 100644 --- a/SAT/SATClause.hpp +++ b/SAT/SATClause.hpp @@ -22,7 +22,6 @@ #include "Lib/Metaiterators.hpp" #include "Lib/Reflection.hpp" -#include "Lib/VString.hpp" #include "SATLiteral.hpp" diff --git a/SAT/SATLiteral.hpp b/SAT/SATLiteral.hpp index b03651aec7..c131331710 100644 --- a/SAT/SATLiteral.hpp +++ b/SAT/SATLiteral.hpp @@ -20,7 +20,6 @@ #include "Shell/Options.hpp" #include "Debug/Assertion.hpp" -#include "Lib/VString.hpp" #include "Kernel/Clause.hpp" namespace SAT { diff --git a/SAT/Z3Interfacing.cpp b/SAT/Z3Interfacing.cpp index d668ee01d9..f7670af73a 100644 --- a/SAT/Z3Interfacing.cpp +++ b/SAT/Z3Interfacing.cpp @@ -521,7 +521,7 @@ z3::sort Z3Interfacing::getz3sort(SortId s) template vstring to_vstring(A const& a) { - vstringstream out; + std::stringstream out; out << a; return out.str(); } @@ -713,7 +713,7 @@ void Z3Interfacing::createTermAlgebra(TermList sort) outputln(" ) ("); auto quote = [&](auto x){ - vstringstream s; + std::stringstream s; s << x; auto str = s.str(); if (str[0] == '\'') { diff --git a/Saturation/PredicateSplitPassiveClauseContainer.cpp b/Saturation/PredicateSplitPassiveClauseContainer.cpp index c661e44ac4..9b3a080a8a 100644 --- a/Saturation/PredicateSplitPassiveClauseContainer.cpp +++ b/Saturation/PredicateSplitPassiveClauseContainer.cpp @@ -33,8 +33,8 @@ int computeLCM(int a, int b) { } PredicateSplitPassiveClauseContainer::PredicateSplitPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name, - Lib::vvector> queues, - Lib::vvector cutoffs, Lib::vvector ratios, bool layeredArrangement) + std::vector> queues, + std::vector cutoffs, std::vector ratios, bool layeredArrangement) : PassiveClauseContainer(isOutermost, opt, name), _queues(std::move(queues)), _cutoffs(cutoffs), _layeredArrangement(layeredArrangement) { _randomize = opt.randomAWR(); @@ -462,7 +462,7 @@ bool PredicateSplitPassiveClauseContainer::childrenPotentiallyFulfilLimits(Claus return false; } -TheoryMultiSplitPassiveClauseContainer::TheoryMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues) : +TheoryMultiSplitPassiveClauseContainer::TheoryMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues) : PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), opt.theorySplitQueueCutoffs(), opt.theorySplitQueueRatios(), opt.theorySplitQueueLayeredArrangement()) {} float TheoryMultiSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const @@ -480,7 +480,7 @@ float TheoryMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigned, return inf.th_ancestors * expectedRatioDenominator - inf.all_ancestors; } -AvatarMultiSplitPassiveClauseContainer::AvatarMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues) : +AvatarMultiSplitPassiveClauseContainer::AvatarMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues) : PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), opt.avatarSplitQueueCutoffs(), opt.avatarSplitQueueRatios(), opt.avatarSplitQueueLayeredArrangement()) {} float AvatarMultiSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const @@ -496,7 +496,7 @@ float AvatarMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigned, return (inf.splits() == nullptr) ? 0 : inf.splits()->size(); } -SineLevelMultiSplitPassiveClauseContainer::SineLevelMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues) : +SineLevelMultiSplitPassiveClauseContainer::SineLevelMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues) : PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), opt.sineLevelSplitQueueCutoffs(), opt.sineLevelSplitQueueRatios(), opt.sineLevelSplitQueueLayeredArrangement()) {} float SineLevelMultiSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const @@ -511,7 +511,7 @@ float SineLevelMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigne return inf.getSineLevel(); } -PositiveLiteralMultiSplitPassiveClauseContainer::PositiveLiteralMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues) : +PositiveLiteralMultiSplitPassiveClauseContainer::PositiveLiteralMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues) : PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), opt.positiveLiteralSplitQueueCutoffs(), opt.positiveLiteralSplitQueueRatios(), opt.positiveLiteralSplitQueueLayeredArrangement()) {} float PositiveLiteralMultiSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const diff --git a/Saturation/PredicateSplitPassiveClauseContainer.hpp b/Saturation/PredicateSplitPassiveClauseContainer.hpp index 5d761d1641..4ee5dc114f 100644 --- a/Saturation/PredicateSplitPassiveClauseContainer.hpp +++ b/Saturation/PredicateSplitPassiveClauseContainer.hpp @@ -16,14 +16,13 @@ #include "Lib/Allocator.hpp" #include "ClauseContainer.hpp" #include "AWPassiveClauseContainer.hpp" -#include "Lib/STL.hpp" namespace Saturation { class PredicateSplitPassiveClauseContainer : public PassiveClauseContainer { public: - PredicateSplitPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name, Lib::vvector> queues, Lib::vvector cutoffs, Lib::vvector ratios, bool layeredArrangement); + PredicateSplitPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name, std::vector> queues, std::vector cutoffs, std::vector ratios, bool layeredArrangement); virtual ~PredicateSplitPassiveClauseContainer(); void add(Clause* cl) override; @@ -34,13 +33,13 @@ class PredicateSplitPassiveClauseContainer private: bool _randomize; - Lib::vvector _ratios; + std::vector _ratios; unsigned _ratioSum; - Lib::vvector> _queues; - Lib::vvector _cutoffs; - Lib::vvector _invertedRatios; - Lib::vvector _balances; + std::vector> _queues; + std::vector _cutoffs; + std::vector _invertedRatios; + std::vector _balances; bool _layeredArrangement; // if set to true, queues are arranged as multi-split-queues. if false, queues use a tammet-style arrangement. unsigned bestQueue(float featureValue) const; @@ -64,7 +63,7 @@ class PredicateSplitPassiveClauseContainer void onLimitsUpdated() override; private: - Lib::vvector _simulationBalances; + std::vector _simulationBalances; /* * LRS specific methods and fields for usage of limits @@ -90,7 +89,7 @@ class PredicateSplitPassiveClauseContainer class TheoryMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClauseContainer { public: - TheoryMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues); + TheoryMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues); private: float evaluateFeature(Clause* cl) const override; @@ -100,7 +99,7 @@ class TheoryMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClaus class AvatarMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClauseContainer { public: - AvatarMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues); + AvatarMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues); private: float evaluateFeature(Clause* cl) const override; @@ -110,7 +109,7 @@ class AvatarMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClaus class SineLevelMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClauseContainer { public: - SineLevelMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues); + SineLevelMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues); private: float evaluateFeature(Clause* cl) const override; @@ -120,7 +119,7 @@ class SineLevelMultiSplitPassiveClauseContainer : public PredicateSplitPassiveCl class PositiveLiteralMultiSplitPassiveClauseContainer : public PredicateSplitPassiveClauseContainer { public: - PositiveLiteralMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues); + PositiveLiteralMultiSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, std::vector> queues); private: float evaluateFeature(Clause* cl) const override; diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 2517d920da..a7c2d5b2a6 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -22,7 +22,6 @@ #include "Lib/Timer.hpp" #include "Lib/VirtualIterator.hpp" #include "Lib/System.hpp" -#include "Lib/STL.hpp" #include "Indexing/LiteralIndexingStructure.hpp" @@ -140,7 +139,7 @@ std::unique_ptr makeLevel1(bool isOutermost, const Optio { if (opt.useTheorySplitQueues()) { - Lib::vvector> queues; + std::vector> queues; auto cutoffs = opt.theorySplitQueueCutoffs(); for (unsigned i = 0; i < cutoffs.size(); i++) { @@ -159,7 +158,7 @@ std::unique_ptr makeLevel2(bool isOutermost, const Optio { if (opt.useAvatarSplitQueues()) { - Lib::vvector> queues; + std::vector> queues; auto cutoffs = opt.avatarSplitQueueCutoffs(); for (unsigned i = 0; i < cutoffs.size(); i++) { @@ -178,7 +177,7 @@ std::unique_ptr makeLevel3(bool isOutermost, const Optio { if (opt.useSineLevelSplitQueues()) { - Lib::vvector> queues; + std::vector> queues; auto cutoffs = opt.sineLevelSplitQueueCutoffs(); for (unsigned i = 0; i < cutoffs.size(); i++) { @@ -197,8 +196,8 @@ std::unique_ptr makeLevel4(bool isOutermost, const Optio { if (opt.usePositiveLiteralSplitQueues()) { - Lib::vvector> queues; - Lib::vvector cutoffs = opt.positiveLiteralSplitQueueCutoffs(); + std::vector> queues; + std::vector cutoffs = opt.positiveLiteralSplitQueueCutoffs(); for (unsigned i = 0; i < cutoffs.size(); i++) { auto queueName = name + "PLSQ" + Int::toString(cutoffs[i]) + ":"; diff --git a/Saturation/Splitter.cpp b/Saturation/Splitter.cpp index 72b37dfef7..916248b467 100644 --- a/Saturation/Splitter.cpp +++ b/Saturation/Splitter.cpp @@ -992,7 +992,7 @@ bool Splitter::handleNonSplittable(Clause* cl) */ vstring Splitter::splitsToString(SplitSet* splits) { - vostringstream res; + std::ostringstream res; auto it = splits->iter(); while(it.hasNext()) { diff --git a/Shell/AnswerExtractor.cpp b/Shell/AnswerExtractor.cpp index 40bcb2a82d..8b0a610dc9 100644 --- a/Shell/AnswerExtractor.cpp +++ b/Shell/AnswerExtractor.cpp @@ -12,6 +12,8 @@ * Implements class AnswerExtractor. */ +#include + #include "Lib/DArray.hpp" #include "Lib/Environment.hpp" #include "Lib/Stack.hpp" @@ -752,7 +754,7 @@ TermList SynthesisManager::ConjectureSkolemReplacement::transformTermList(TermLi } } else { Substitution s; - vset done; + std::set done; Kernel::VariableWithSortIterator vit(tl.term()); while (vit.hasNext()) { pair p = vit.next(); diff --git a/Shell/AnswerExtractor.hpp b/Shell/AnswerExtractor.hpp index fcd615f555..a94dc425ef 100644 --- a/Shell/AnswerExtractor.hpp +++ b/Shell/AnswerExtractor.hpp @@ -17,6 +17,8 @@ #include "Forwards.hpp" +#include + #include "Lib/DHMap.hpp" #include "Kernel/Formula.hpp" @@ -114,7 +116,7 @@ class SynthesisManager : public AnswerLiteralManager protected: TermList transformSubterm(TermList trm) override; private: - vmap _skolemToVar; + std::map _skolemToVar; // Map from functions to predicates they represent in answer literal conditions DHMap _condFnToPred; }; diff --git a/Shell/CommandLine.cpp b/Shell/CommandLine.cpp index 297cc46091..e145ff0776 100644 --- a/Shell/CommandLine.cpp +++ b/Shell/CommandLine.cpp @@ -19,7 +19,6 @@ #include "Debug/Assertion.hpp" -#include "Lib/VString.hpp" #include "Lib/Environment.hpp" #include "Lib/Exception.hpp" #include "SAT/Z3Interfacing.hpp" diff --git a/Shell/FunctionDefinitionHandler.cpp b/Shell/FunctionDefinitionHandler.cpp index de880a2309..7451bcd7c8 100644 --- a/Shell/FunctionDefinitionHandler.cpp +++ b/Shell/FunctionDefinitionHandler.cpp @@ -8,6 +8,8 @@ * and in the source directory */ +#include + #include "FunctionDefinitionHandler.hpp" #include "Inferences/InductionHelper.hpp" @@ -170,7 +172,7 @@ void FunctionDefinitionHandler::addFunctionBranch(Term* header, TermList body) _templates.getValuePtr(make_pair(fn,SymbolType::FUNC), templ, InductionTemplate(header)); // handle for induction - vvector recursiveCalls; + std::vector recursiveCalls; if (body.isTerm()) { NonVariableNonTypeIterator it(body.term(), true); while (it.hasNext()) { @@ -190,7 +192,7 @@ void FunctionDefinitionHandler::addPredicateBranch(Literal* header, const Litera _templates.getValuePtr(make_pair(fn,SymbolType::PRED), templ, InductionTemplate(header)); // handle for induction - vvector recursiveCalls; + std::vector recursiveCalls; ASS(static_cast(header)->isPositive()); for(const auto& lit : conditions) { if (!lit->isEquality() && fn == lit->functor()) { @@ -212,11 +214,11 @@ bool InductionTemplate::finalize() void InductionTemplate::checkWellDefinedness() { - vvector cases; + std::vector cases; for (auto& b : _branches) { cases.push_back(b._header); } - vvector> missingCases; + std::vector> missingCases; InductionPreprocessor::checkWellDefinedness(cases, missingCases); if (!missingCases.empty()) { @@ -235,7 +237,7 @@ void InductionTemplate::checkWellDefinedness() } else { t = Term::create(_functor, _arity, args.begin()); } - addBranch(vvector(), Renaming::normalize(t)); + addBranch(std::vector(), Renaming::normalize(t)); } if (env.options->showInduction()) { cout << ". New template is " << toString() << endl; @@ -243,7 +245,7 @@ void InductionTemplate::checkWellDefinedness() } } -bool InductionTemplate::matchesTerm(Term* t, vvector& inductionTerms) const +bool InductionTemplate::matchesTerm(Term* t, std::vector& inductionTerms) const { ASS(t->ground()); inductionTerms.clear(); @@ -313,7 +315,7 @@ bool InductionTemplate::checkUsefulness() const bool InductionTemplate::checkWellFoundedness() { - vvector> relatedTerms; + std::vector> relatedTerms; for (auto& b : _branches) { for (auto& r : b._recursiveCalls) { relatedTerms.push_back(make_pair(b._header, r)); @@ -335,7 +337,7 @@ InductionTemplate::InductionTemplate(const Term* t) : env.signature->getFunction(_functor)->fnType()), _branches(), _indPos(_arity, false) {} -void InductionTemplate::addBranch(vvector&& recursiveCalls, Term* header) +void InductionTemplate::addBranch(std::vector&& recursiveCalls, Term* header) { ASS(header->arity() == _arity && header->isLiteral() == _isLit && header->functor() == _functor); Branch branch(std::move(recursiveCalls), std::move(header)); @@ -353,7 +355,7 @@ void InductionTemplate::addBranch(vvector&& recursiveCalls, Term* header) vstring InductionTemplate::toString() const { - vstringstream str; + std::stringstream str; str << "Branches: "; unsigned n = 0; for (const auto& b : _branches) { @@ -392,8 +394,8 @@ vstring InductionTemplate::toString() const * Try to find a lexicographic order between the arguments * by exhaustively trying all combinations. */ -bool checkWellFoundednessHelper(const vvector>& relatedTerms, - const vset& indices, const vset& positions) +bool checkWellFoundednessHelper(const std::vector>& relatedTerms, + const std::set& indices, const std::set& positions) { if (indices.empty()) { return true; @@ -402,7 +404,7 @@ bool checkWellFoundednessHelper(const vvector>& relatedTerms, return false; } for (const auto& p : positions) { - vset newInd; + std::set newInd; bool canOrder = true; for (const auto& i : indices) { auto arg1 = *relatedTerms[i].first->nthArgument(p); @@ -425,7 +427,7 @@ bool checkWellFoundednessHelper(const vvector>& relatedTerms, return false; } -bool InductionPreprocessor::checkWellFoundedness(const vvector>& relatedTerms) +bool InductionPreprocessor::checkWellFoundedness(const std::vector>& relatedTerms) { if (relatedTerms.empty()) { return true; @@ -440,13 +442,13 @@ bool InductionPreprocessor::checkWellFoundedness(const vvector } else { type = env.signature->getPredicate(fn)->predType(); } - vset positions; + std::set positions; for (unsigned i = 0; i < arity; i++) { if (env.signature->isTermAlgebraSort(type->arg(i))) { positions.insert(i); } } - vset indices; + std::set indices; for (unsigned i = 0; i < relatedTerms.size(); i++) { indices.insert(i); } @@ -457,7 +459,7 @@ bool InductionPreprocessor::checkWellFoundedness(const vvector * Check well-definedness for term algebra arguments and * in the process generate all missing cases. */ -bool InductionPreprocessor::checkWellDefinedness(const vvector& cases, vvector>& missingCases) +bool InductionPreprocessor::checkWellDefinedness(const std::vector& cases, std::vector>& missingCases) { if (cases.empty()) { return false; @@ -500,13 +502,13 @@ bool InductionPreprocessor::checkWellDefinedness(const vvector& cases, vv for (const auto& availableTerms : availableTermsLists) { bool valid = true; - vvector> argTuples(1); + std::vector> argTuples(1); for (const auto& v : availableTerms) { if (v.isEmpty()) { valid = false; break; } - vvector> temp; + std::vector> temp; for (const auto& e : v) { for (auto a : argTuples) { a.push_back(e); diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp index e07f5b6e3d..9a4208fee1 100644 --- a/Shell/FunctionDefinitionHandler.hpp +++ b/Shell/FunctionDefinitionHandler.hpp @@ -19,7 +19,6 @@ #include "Indexing/CodeTreeInterfaces.hpp" #include "Kernel/TermTransformer.hpp" #include "TermAlgebra.hpp" -#include "Lib/STL.hpp" namespace Shell { @@ -37,10 +36,10 @@ struct InductionTemplate { InductionTemplate() = default; InductionTemplate(const Term* t); - void addBranch(vvector&& recursiveCalls, Term* header); + void addBranch(std::vector&& recursiveCalls, Term* header); bool finalize(); - const vvector& inductionPositions() const { return _indPos; } - bool matchesTerm(Term* t, vvector& inductionTerms) const; + const std::vector& inductionPositions() const { return _indPos; } + bool matchesTerm(Term* t, std::vector& inductionTerms) const; /** * Stores the template for a recursive case @@ -50,16 +49,16 @@ struct InductionTemplate { * (if not present it is a base case) */ struct Branch { - Branch(vvector&& recursiveCalls, Term*&& header) + Branch(std::vector&& recursiveCalls, Term*&& header) : _recursiveCalls(recursiveCalls), _header(header) {} bool contains(const Branch& other) const; - vvector _recursiveCalls; + std::vector _recursiveCalls; Term* _header; }; - const vvector& branches() const { return _branches; } + const std::vector& branches() const { return _branches; } vstring toString() const; @@ -73,8 +72,8 @@ struct InductionTemplate { bool checkWellFoundedness(); void checkWellDefinedness(); - vvector _branches; - vvector _indPos; + std::vector _branches; + std::vector _indPos; }; class FunctionDefinitionHandler @@ -120,8 +119,8 @@ class FunctionDefinitionHandler * the marked recursive function definitions from the parser. */ struct InductionPreprocessor { - static bool checkWellFoundedness(const vvector>& relatedTerms); - static bool checkWellDefinedness(const vvector& cases, vvector>& missingCases); + static bool checkWellFoundedness(const std::vector>& relatedTerms); + static bool checkWellDefinedness(const std::vector& cases, std::vector>& missingCases); }; } // Shell diff --git a/Shell/LaTeX.hpp b/Shell/LaTeX.hpp index 2fc7063270..4e3ad53521 100644 --- a/Shell/LaTeX.hpp +++ b/Shell/LaTeX.hpp @@ -22,7 +22,6 @@ #include "Lib/DHMap.hpp" #include "Lib/Stack.hpp" -#include "Lib/VString.hpp" #include "Kernel/Connective.hpp" #include "Kernel/InferenceStore.hpp" diff --git a/Shell/LispParser.hpp b/Shell/LispParser.hpp index 66d577287d..e0f8a41eb1 100644 --- a/Shell/LispParser.hpp +++ b/Shell/LispParser.hpp @@ -24,7 +24,6 @@ #include "Lib/List.hpp" #include "Lib/Portability.hpp" #include "Lib/Stack.hpp" -#include "Lib/VString.hpp" namespace Shell { diff --git a/Shell/Options.cpp b/Shell/Options.cpp index cc8bd8385b..25db946990 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -39,7 +39,6 @@ #include "Debug/Assertion.hpp" -#include "Lib/VString.hpp" #include "Lib/StringUtils.hpp" #include "Lib/Environment.hpp" #include "Lib/Timer.hpp" @@ -2558,7 +2557,7 @@ void Options::output (ostream& str) const } } else{ - vstringstream vs; + std::stringstream vs; option->output(vs,lineWrapInShowOptions()); str << vs.str(); } @@ -3327,7 +3326,7 @@ void Options::setForcedOptionValues() */ vstring Options::generateEncodedOptions() const { - vostringstream res; + std::ostringstream res; //saturation algorithm vstring sat; switch(_saturationAlgorithm.actualValue){ @@ -3592,10 +3591,10 @@ bool Options::checkProblemOptionConstraints(Property* prop, bool before_preproce } template -Lib::vvector parseCommaSeparatedList(vstring const& str) +std::vector parseCommaSeparatedList(vstring const& str) { - vstringstream stream(str); - Lib::vvector parsed; + std::stringstream stream(str); + std::vector parsed; vstring cur; while (std::getline(stream, cur, ',')) { parsed.push_back(StringUtils::parse(cur)); @@ -3603,7 +3602,7 @@ Lib::vvector parseCommaSeparatedList(vstring const& str) return parsed; } -Lib::vvector Options::theorySplitQueueRatios() const +std::vector Options::theorySplitQueueRatios() const { auto inputRatios = parseCommaSeparatedList(_theorySplitQueueRatios.actualValue); @@ -3620,10 +3619,10 @@ Lib::vvector Options::theorySplitQueueRatios() const return inputRatios; } -Lib::vvector Options::theorySplitQueueCutoffs() const +std::vector Options::theorySplitQueueCutoffs() const { // initialize cutoffs - Lib::vvector cutoffs; + std::vector cutoffs; /* if (_theorySplitQueueCutoffs.isDefault()) { @@ -3654,9 +3653,9 @@ Lib::vvector Options::theorySplitQueueCutoffs() const return cutoffs; } -Lib::vvector Options::avatarSplitQueueRatios() const +std::vector Options::avatarSplitQueueRatios() const { - Lib::vvector inputRatios = parseCommaSeparatedList(_avatarSplitQueueRatios.actualValue); + std::vector inputRatios = parseCommaSeparatedList(_avatarSplitQueueRatios.actualValue); // sanity checks if (inputRatios.size() < 2) { @@ -3671,7 +3670,7 @@ Lib::vvector Options::avatarSplitQueueRatios() const return inputRatios; } -Lib::vvector Options::avatarSplitQueueCutoffs() const +std::vector Options::avatarSplitQueueCutoffs() const { // initialize cutoffs and add float-max as last value auto cutoffs = parseCommaSeparatedList(_avatarSplitQueueCutoffs.actualValue); @@ -3691,7 +3690,7 @@ Lib::vvector Options::avatarSplitQueueCutoffs() const return cutoffs; } -Lib::vvector Options::sineLevelSplitQueueRatios() const +std::vector Options::sineLevelSplitQueueRatios() const { auto inputRatios = parseCommaSeparatedList(_sineLevelSplitQueueRatios.actualValue); @@ -3708,7 +3707,7 @@ Lib::vvector Options::sineLevelSplitQueueRatios() const return inputRatios; } -Lib::vvector Options::sineLevelSplitQueueCutoffs() const +std::vector Options::sineLevelSplitQueueCutoffs() const { // initialize cutoffs and add float-max as last value auto cutoffs = parseCommaSeparatedList(_sineLevelSplitQueueCutoffs.actualValue); @@ -3728,7 +3727,7 @@ Lib::vvector Options::sineLevelSplitQueueCutoffs() const return cutoffs; } -Lib::vvector Options::positiveLiteralSplitQueueRatios() const +std::vector Options::positiveLiteralSplitQueueRatios() const { auto inputRatios = parseCommaSeparatedList(_positiveLiteralSplitQueueRatios.actualValue); @@ -3745,7 +3744,7 @@ Lib::vvector Options::positiveLiteralSplitQueueRatios() const return inputRatios; } -Lib::vvector Options::positiveLiteralSplitQueueCutoffs() const +std::vector Options::positiveLiteralSplitQueueCutoffs() const { // initialize cutoffs and add float-max as last value auto cutoffs = parseCommaSeparatedList(_positiveLiteralSplitQueueCutoffs.actualValue); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index cbea511f14..491d66da8a 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -44,7 +44,6 @@ #include "Debug/Assertion.hpp" -#include "Lib/VString.hpp" #include "Lib/VirtualIterator.hpp" #include "Lib/DHMap.hpp" #include "Lib/DArray.hpp" @@ -52,7 +51,6 @@ #include "Lib/Int.hpp" #include "Lib/Allocator.hpp" #include "Lib/Comparison.hpp" -#include "Lib/STL.hpp" #include "Lib/Timer.hpp" #include "Property.hpp" @@ -2136,21 +2134,21 @@ bool _hard; void setAgeRatio(int v){ _ageWeightRatio.actualValue = v; } int weightRatio() const { return _ageWeightRatio.otherValue; } bool useTheorySplitQueues() const { return _useTheorySplitQueues.actualValue; } - Lib::vvector theorySplitQueueRatios() const; - Lib::vvector theorySplitQueueCutoffs() const; + std::vector theorySplitQueueRatios() const; + std::vector theorySplitQueueCutoffs() const; int theorySplitQueueExpectedRatioDenom() const { return _theorySplitQueueExpectedRatioDenom.actualValue; } bool theorySplitQueueLayeredArrangement() const { return _theorySplitQueueLayeredArrangement.actualValue; } bool useAvatarSplitQueues() const { return _useAvatarSplitQueues.actualValue; } - Lib::vvector avatarSplitQueueRatios() const; - Lib::vvector avatarSplitQueueCutoffs() const; + std::vector avatarSplitQueueRatios() const; + std::vector avatarSplitQueueCutoffs() const; bool avatarSplitQueueLayeredArrangement() const { return _avatarSplitQueueLayeredArrangement.actualValue; } bool useSineLevelSplitQueues() const { return _useSineLevelSplitQueues.actualValue; } - Lib::vvector sineLevelSplitQueueRatios() const; - Lib::vvector sineLevelSplitQueueCutoffs() const; + std::vector sineLevelSplitQueueRatios() const; + std::vector sineLevelSplitQueueCutoffs() const; bool sineLevelSplitQueueLayeredArrangement() const { return _sineLevelSplitQueueLayeredArrangement.actualValue; } bool usePositiveLiteralSplitQueues() const { return _usePositiveLiteralSplitQueues.actualValue; } - Lib::vvector positiveLiteralSplitQueueRatios() const; - Lib::vvector positiveLiteralSplitQueueCutoffs() const; + std::vector positiveLiteralSplitQueueRatios() const; + std::vector positiveLiteralSplitQueueCutoffs() const; bool positiveLiteralSplitQueueLayeredArrangement() const { return _positiveLiteralSplitQueueLayeredArrangement.actualValue; } void setWeightRatio(int v){ _ageWeightRatio.otherValue = v; } AgeWeightRatioShape ageWeightRatioShape() const { return _ageWeightRatioShape.actualValue; } diff --git a/Shell/Property.hpp b/Shell/Property.hpp index bb717fa712..c2626be032 100644 --- a/Shell/Property.hpp +++ b/Shell/Property.hpp @@ -25,7 +25,6 @@ #include "Lib/DHSet.hpp" #include "Kernel/Unit.hpp" #include "Kernel/Theory.hpp" -#include "Lib/VString.hpp" #include "SMTLIBLogic.hpp" namespace Kernel { diff --git a/Shell/TPTPPrinter.cpp b/Shell/TPTPPrinter.cpp index aaef410510..694f108fbe 100644 --- a/Shell/TPTPPrinter.cpp +++ b/Shell/TPTPPrinter.cpp @@ -83,7 +83,7 @@ void TPTPPrinter::printWithRole(vstring name, vstring role, Unit* u, bool includ */ vstring TPTPPrinter::getBodyStr(Unit* u, bool includeSplitLevels) { - vostringstream res; + std::ostringstream res; typedef DHMap SortMap; static SortMap varSorts; diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index 0efecbe214..6ce419522e 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -15,7 +15,6 @@ #include "Lib/Allocator.hpp" #include "Lib/List.hpp" #include "Lib/Array.hpp" -#include "Lib/VString.hpp" #include "Kernel/OperatorType.hpp" #include "Lib/Metaiterators.hpp" #include "Lib/Set.hpp" diff --git a/Shell/Token.cpp b/Shell/Token.cpp index f161476458..2b91891c63 100644 --- a/Shell/Token.cpp +++ b/Shell/Token.cpp @@ -14,6 +14,7 @@ * @since 25/07/2004 Torrevieja */ +#include "Forwards.hpp" #include "Debug/Assertion.hpp" #include "Token.hpp" diff --git a/Shell/Token.hpp b/Shell/Token.hpp index 3a55c2bc34..76426ac95f 100644 --- a/Shell/Token.hpp +++ b/Shell/Token.hpp @@ -17,8 +17,6 @@ #ifndef __Token__ #define __Token__ -#include "Lib/VString.hpp" - namespace Shell { /** diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index 8e858e2c55..eed9d54612 100644 --- a/Shell/UIHelper.cpp +++ b/Shell/UIHelper.cpp @@ -24,7 +24,6 @@ #include "Lib/Environment.hpp" #include "Debug/TimeProfiling.hpp" -#include "Lib/VString.hpp" #include "Lib/Timer.hpp" #include "Lib/Allocator.hpp" #include "Lib/ScopedLet.hpp" @@ -251,7 +250,7 @@ void UIHelper::parseSingleLine(const vstring& lineToParse, Options::InputSyntax ScopedLet localAssing(env.statistics->phase,Statistics::PARSING); - vistringstream stream(lineToParse); + std::istringstream stream(lineToParse); try { switch (inputSyntax) { case Options::InputSyntax::TPTP: diff --git a/Shell/VarManager.hpp b/Shell/VarManager.hpp index c54ab64b98..510ff5f526 100644 --- a/Shell/VarManager.hpp +++ b/Shell/VarManager.hpp @@ -15,8 +15,6 @@ #ifndef __VarManager__ #define __VarManager__ -#include "Lib/VString.hpp" - #include "Forwards.hpp" namespace Shell { diff --git a/Test/SyntaxSugar.hpp b/Test/SyntaxSugar.hpp index 455e46031b..32d1b95910 100644 --- a/Test/SyntaxSugar.hpp +++ b/Test/SyntaxSugar.hpp @@ -722,7 +722,7 @@ inline void createTermAlgebra(SortSugar sort, std::initializer_list f ->markTermAlgebraCons(); auto dtor = [&](unsigned i) { - vstringstream name; + std::stringstream name; name << f << "@" << i; auto d = FuncSugar(name.str(), { f.result() }, f.arg(i)); env.signature->getFunction(d.functor()) diff --git a/Test/UnitTesting.hpp b/Test/UnitTesting.hpp index 00d44ef338..b317457305 100644 --- a/Test/UnitTesting.hpp +++ b/Test/UnitTesting.hpp @@ -21,9 +21,6 @@ #include "Forwards.hpp" #include "Lib/Stack.hpp" -#include "Lib/VString.hpp" - - namespace Test { diff --git a/UnitTests/tCoproduct.cpp b/UnitTests/tCoproduct.cpp index f34f472316..9c4397e268 100644 --- a/UnitTests/tCoproduct.cpp +++ b/UnitTests/tCoproduct.cpp @@ -96,7 +96,7 @@ TEST_FUN(examples__match_02) { auto x = Coproduct(1); vstring str = x.apply([](auto const& c) { - vstringstream out; + std::stringstream out; out << c; return out.str(); }); diff --git a/UnitTests/tFunctionDefinitionHandler.cpp b/UnitTests/tFunctionDefinitionHandler.cpp index 9e2d328076..98ef291f48 100644 --- a/UnitTests/tFunctionDefinitionHandler.cpp +++ b/UnitTests/tFunctionDefinitionHandler.cpp @@ -56,7 +56,7 @@ inline void addFunctionDefs(FunctionDefinitionHandler& handler, std::initializer handler.initAndPreprocessLate(prb,opts); } -inline void checkTemplateBranches(FunctionDefinitionHandler& handler, TermSugar t, const vvector>>& expected) { +inline void checkTemplateBranches(FunctionDefinitionHandler& handler, TermSugar t, const std::vector>>& expected) { auto templ = handler.getInductionTemplate(t.sugaredExpr().term()); ASS(templ); auto actual = templ->branches(); diff --git a/UnitTests/tInduction.cpp b/UnitTests/tInduction.cpp index cd65a85785..1eb53a3fa8 100644 --- a/UnitTests/tInduction.cpp +++ b/UnitTests/tInduction.cpp @@ -9,6 +9,8 @@ */ +#include + #include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Test/TestUtils.hpp" @@ -183,7 +185,7 @@ class GenerationTesterInduction } Kernel::RobSubstitution _subst; - unordered_set _varsMatched; + std::unordered_set _varsMatched; BacktrackData _btd; class MatchedVarBacktrackObject : public BacktrackObject { diff --git a/UnitTests/tOptionConstraints.cpp b/UnitTests/tOptionConstraints.cpp index 6db3e7e048..0d2748ad2e 100644 --- a/UnitTests/tOptionConstraints.cpp +++ b/UnitTests/tOptionConstraints.cpp @@ -8,7 +8,6 @@ * and in the source directory */ -#include "Lib/VString.hpp" #include "Shell/Options.hpp" #include "Test/UnitTesting.hpp" diff --git a/vampire.cpp b/vampire.cpp index 75198e6562..ad14bbe4ca 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -24,7 +24,6 @@ #include "Lib/Environment.hpp" #include "Lib/Random.hpp" #include "Lib/Timer.hpp" -#include "Lib/VString.hpp" #include "Lib/List.hpp" #include "Lib/System.hpp" #include "Lib/Metaiterators.hpp"