inline pointless vstring typedef

CASC/PortfolioMode.cpp

@@ -298,31 +298,31 @@ void PortfolioMode::rescaleScheduleLimits(const Schedule& sOld, Schedule& sNew,
 {
   Schedule::BottomFirstIterator it(sOld);
   while(it.hasNext()){
-    vstring s = it.next();
+    std::string s = it.next();
 
     // rescale the instruction limit, if present
     size_t bidx = s.rfind(":i=");
-    if (bidx == vstring::npos) {
+    if (bidx == std::string::npos) {
       bidx = s.rfind("_i=");
     }
-    if (bidx != vstring::npos) {
+    if (bidx != std::string::npos) {
       bidx += 3; // advance past the "[:_]i=" bit
       size_t eidx = s.find_first_of(":_",bidx); // find the end of the number there
-      ASS_NEQ(eidx,vstring::npos);
-      vstring instrStr = s.substr(bidx,eidx-bidx);
+      ASS_NEQ(eidx,std::string::npos);
+      std::string instrStr = s.substr(bidx,eidx-bidx);
       unsigned instr;
       ALWAYS(Int::stringToUnsignedInt(instrStr,instr));
       instr *= limit_multiplier;
       s = s.substr(0,bidx) + Lib::Int::toString(instr) + s.substr(eidx);
     }
 
     // do the analogous with the time limit suffix
-    vstring ts = s.substr(s.find_last_of("_")+1,vstring::npos);
+    std::string ts = s.substr(s.find_last_of("_")+1,std::string::npos);
     unsigned time;
     ALWAYS(Lib::Int::stringToUnsignedInt(ts,time));
-    vstring prefix = s.substr(0,s.find_last_of("_"));
+    std::string prefix = s.substr(0,s.find_last_of("_"));
     // Add a copy with increased time limit ...
-    vstring new_time_suffix = Lib::Int::toString((int)(time*limit_multiplier));
+    std::string new_time_suffix = Lib::Int::toString((int)(time*limit_multiplier));
 
     sNew.push(prefix + "_" + new_time_suffix);
   }
@@ -334,17 +334,17 @@ void PortfolioMode::rescaleScheduleLimits(const Schedule& sOld, Schedule& sNew,
  * 
  * @author Giles, Martin
  */
-void PortfolioMode::addScheduleExtra(const Schedule& sOld, Schedule& sNew, vstring extra)
+void PortfolioMode::addScheduleExtra(const Schedule& sOld, Schedule& sNew, std::string extra)
 {
   Schedule::BottomFirstIterator it(sOld);
   while(it.hasNext()){
-    vstring s = it.next();
+    std::string s = it.next();
 
     auto idx = s.find_last_of("_");
 
-    vstring prefix = s.substr(0,idx);
-    vstring suffix = s.substr(idx,vstring::npos);
-    vstring new_s = prefix + ((prefix.back() != '_') ? ":" : "") + extra + suffix;
+    std::string prefix = s.substr(0,idx);
+    std::string suffix = s.substr(idx,std::string::npos);
+    std::string new_s = prefix + ((prefix.back() != '_') ? ":" : "") + extra + suffix;
 
     sNew.push(new_s);
   }
@@ -454,7 +454,7 @@ bool PortfolioMode::runSchedule(Schedule schedule) {
       }
       ALWAYS(it.hasNext());
 
-      vstring code = it.next();
+      std::string code = it.next();
       pid_t process = Multiprocessing::instance()->fork();
       ASS_NEQ(process, -1);
       if(process == 0)
@@ -546,10 +546,10 @@ bool PortfolioMode::runScheduleAndRecoverProof(Schedule schedule)
 /**
  * Return the intended slice time in deciseconds
  */
-unsigned PortfolioMode::getSliceTime(const vstring &sliceCode)
+unsigned PortfolioMode::getSliceTime(const std::string &sliceCode)
 {
   unsigned pos = sliceCode.find_last_of('_');
-  vstring sliceTimeStr = sliceCode.substr(pos+1);
+  std::string sliceTimeStr = sliceCode.substr(pos+1);
   unsigned sliceTime;
   ALWAYS(Int::stringToUnsignedInt(sliceTimeStr,sliceTime));
 
@@ -560,16 +560,16 @@ unsigned PortfolioMode::getSliceTime(const vstring &sliceCode)
     }
 
     size_t bidx = sliceCode.find(":i=");
-    if (bidx == vstring::npos) {
+    if (bidx == std::string::npos) {
       bidx = sliceCode.find("_i=");
-      if (bidx == vstring::npos) {
+      if (bidx == std::string::npos) {
         return 0; // run (essentially) forever
       }
     } // we have a valid begin index
     bidx += 3; // advance it past the "*i=" bit
     size_t eidx = sliceCode.find_first_of(":_",bidx); // find the end of the number there
-    ASS_NEQ(eidx,vstring::npos);
-    vstring sliceInstrStr = sliceCode.substr(bidx,eidx-bidx);
+    ASS_NEQ(eidx,std::string::npos);
+    std::string sliceInstrStr = sliceCode.substr(bidx,eidx-bidx);
     unsigned sliceInstr;
     ALWAYS(Int::stringToUnsignedInt(sliceInstrStr,sliceInstr));
 
@@ -583,7 +583,7 @@ unsigned PortfolioMode::getSliceTime(const vstring &sliceCode)
 /**
  * Run a slice given by its code using the specified time limit.
  */
-void PortfolioMode::runSlice(vstring sliceCode, int timeLimitInDeciseconds)
+void PortfolioMode::runSlice(std::string sliceCode, int timeLimitInDeciseconds)
 {
   TIME_TRACE("run slice");
 

CASC/PortfolioMode.hpp

@@ -39,18 +39,18 @@ class PortfolioMode {
   static bool perform(Kernel::Problem* problem);
 
   static void rescaleScheduleLimits(const Schedule& sOld, Schedule& sNew, float limit_multiplier);
-  static void addScheduleExtra(const Schedule& sOld, Schedule& sNew, vstring extra);
+  static void addScheduleExtra(const Schedule& sOld, Schedule& sNew, std::string extra);
 
 private:
   // some of these names are kind of arbitrary and should be perhaps changed
-  unsigned getSliceTime(const vstring &sliceCode);
+  unsigned getSliceTime(const std::string &sliceCode);
   bool searchForProof();
   bool prepareScheduleAndPerform(const Shell::Property& prop);
   void getSchedules(const Property& prop, Schedule& quick, Schedule& fallback);
 
   bool runSchedule(Schedule schedule);
   bool runScheduleAndRecoverProof(Schedule schedule);
-  [[noreturn]] void runSlice(vstring sliceCode, int remainingTime);
+  [[noreturn]] void runSlice(std::string sliceCode, int remainingTime);
   [[noreturn]] void runSlice(Options& strategyOpt);
 
 #if VDEBUG

CASC/Schedules.cpp

@@ -34,7 +34,7 @@ using namespace Lib;
 using namespace Shell;
 using namespace CASC;
 
-void Schedules::getScheduleFromFile(const vstring& filename, Schedule& quick)
+void Schedules::getScheduleFromFile(const std::string& filename, Schedule& quick)
 {
   if (filename == "") {
     USER_ERROR("Schedule file was not set.");
@@ -44,7 +44,7 @@ void Schedules::getScheduleFromFile(const vstring& filename, Schedule& quick)
     USER_ERROR("Cannot open schedule file: " + filename);
   }
   ASS(schedule_file.is_open());
-  vstring line;
+  std::string line;
   while (getline(schedule_file, line)) {
     // Allow structuring the schedule file with empty lines.
     // Allow documenting the schedule file with line comments.

CASC/Schedules.hpp

@@ -20,12 +20,12 @@
 
 namespace CASC {
 
-typedef Lib::Stack<Lib::vstring> Schedule;
+typedef Lib::Stack<std::string> Schedule;
 
 class Schedules
 {
 public:
-  static void getScheduleFromFile(const vstring& filename, Schedule& quick);
+  static void getScheduleFromFile(const std::string& filename, Schedule& quick);
 
   static void getHigherOrderSchedule2020(Schedule& quick, Schedule& fallback);
 

DP/SimpleCongruenceClosure.cpp

@@ -35,7 +35,7 @@ using namespace std;
 
 const unsigned SimpleCongruenceClosure::NO_SIG_SYMBOL = 0xFFFFFFFF;
 
-vstring SimpleCongruenceClosure::CEq::toString() const
+std::string SimpleCongruenceClosure::CEq::toString() const
 {
   std::ostringstream res;
   res << c1<<"="<<c2<<" implied by ";
@@ -53,7 +53,7 @@ vstring SimpleCongruenceClosure::CEq::toString() const
   return res.str();
 }
 
-vstring SimpleCongruenceClosure::CEq::toString(SimpleCongruenceClosure& parent) const
+std::string SimpleCongruenceClosure::CEq::toString(SimpleCongruenceClosure& parent) const
 {
   std::ostringstream res;
   res << c1<<"="<<c2<<" implied by ";

DP/SimpleCongruenceClosure.hpp

@@ -95,8 +95,8 @@ class SimpleCongruenceClosure : public DecisionProcedure
      : c1(c1), c2(c2), foOrigin(false), foPremise(nullptr) {}
 
     bool isInvalid() const { ASS_EQ(c1==0, c2==0); return c1==0; }
-    vstring toString() const;
-    vstring toString(SimpleCongruenceClosure& parent) const;
+    std::string toString() const;
+    std::string toString(SimpleCongruenceClosure& parent) const;
 
     unsigned c1;
     unsigned c2;

FMB/FiniteModel.cpp

@@ -137,7 +137,7 @@ bool FiniteModel::isPartial()
   return true;
 }
 
-vstring FiniteModel::toString()
+std::string FiniteModel::toString()
 {
   std::ostringstream modelStm;
 
@@ -179,7 +179,7 @@ vstring FiniteModel::toString()
     unsigned arity = env.signature->functionArity(f);
     if(arity>0) continue;
     if(!printIntroduced && env.signature->getFunction(f)->introduced()) continue;
-    vstring name = env.signature->functionName(f);
+    std::string name = env.signature->functionName(f);
     unsigned res = f_interpretation[f_offsets[f]];
     if(res>0){ 
       modelStm << "fof("<<name<<"_definition,axiom,"<<name<<" = fmb"<< res << ")."<<endl;
@@ -194,7 +194,7 @@ vstring FiniteModel::toString()
     unsigned arity = env.signature->functionArity(f);
     if(arity==0) continue;
     if(!printIntroduced && env.signature->getFunction(f)->introduced()) continue;
-    vstring name = env.signature->functionName(f);
+    std::string name = env.signature->functionName(f);
     modelStm << "fof(function_"<<name<<",axiom,"<<endl;
 
     unsigned offset = f_offsets[f];
@@ -253,7 +253,7 @@ vstring FiniteModel::toString()
     unsigned arity = env.signature->predicateArity(f);
     if(arity>0) continue;
     if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue;
-    vstring name = env.signature->predicateName(f);
+    std::string name = env.signature->predicateName(f);
     unsigned res = p_interpretation[p_offsets[f]];
     if(res==2){
       modelStm << "fof("<<name<<"_definition,axiom,"<<name<< ")."<<endl;
@@ -271,7 +271,7 @@ vstring FiniteModel::toString()
     unsigned arity = env.signature->predicateArity(f);
     if(arity==0) continue;
     if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue;
-    vstring name = env.signature->predicateName(f);
+    std::string name = env.signature->predicateName(f);
     modelStm << "fof(predicate_"<<name<<",axiom,"<<endl;
 
     unsigned offset = p_offsets[f];

FMB/FiniteModel.hpp

@@ -54,7 +54,7 @@ class FiniteModel {
  unsigned evaluateGroundTerm(Term* term);
  bool evaluateGroundLiteral(Literal* literal);
 
- vstring toString();
+ std::string toString();
 
 private:
 
@@ -80,7 +80,7 @@ class FiniteModel {
  {
    Term* t;
    if(_domainConstants.find(c,t)) return t;
-   vstring name = "domainConstant";//+Lib::Int::toString(c);
+   std::string name = "domainConstant";//+Lib::Int::toString(c);
    unsigned f = env.signature->addFreshFunction(0,name.c_str()); 
    t = Term::createConstant(f);
    _domainConstants.insert(c,t);

FMB/FiniteModelBuilder.cpp

@@ -1557,8 +1557,8 @@ MainLoopResult FiniteModelBuilder::runImpl()
 #if VTRACE_FMB
       doPrinting = true;
 #endif
-      vstring min_res = "[";
-      vstring max_res = "[";
+      std::string min_res = "[";
+      std::string max_res = "[";
       for(unsigned s=0;s<_sortedSignature->distinctSorts;s++){
         if(_distinctSortMaxs[s]==UINT_MAX){
           max_res+="max";
@@ -2484,7 +2484,7 @@ bool FiniteModelBuilder::SmtBasedDSAE::init(unsigned _startModelSize, DArray<uns
     // _distinctSortSizes.size() - many int variables
     for(unsigned i=0;i<_sizeConstants.size();i++) {
       _sizeConstants[i] = new z3::expr(_context);
-      *_sizeConstants[i] = _context.int_const((vstring("s")+Int::toString(i)).c_str());
+      *_sizeConstants[i] = _context.int_const((std::string("s")+Int::toString(i)).c_str());
 
       // asserted to be greater than zero
       _smtSolver.add(*_sizeConstants[i] > zero);

FMB/FiniteModelBuilder.hpp

@@ -44,8 +44,8 @@ using namespace SAT;
     unsigned f;
     DArray<unsigned> grounding;
 
-    vstring toString(){
-      vstring ret = Lib::Int::toString(f)+"[";
+    std::string toString(){
+      std::string ret = Lib::Int::toString(f)+"[";
       for(unsigned i=0;i<grounding.size();i++){
         if(i>0) ret +=",";
         ret+=Lib::Int::toString(grounding[i]);

FMB/FiniteModelMultiSorted.cpp

@@ -179,13 +179,13 @@ bool FiniteModelMultiSorted::isPartial()
   return true;
 }
 
-vstring FiniteModelMultiSorted::toString()
+std::string FiniteModelMultiSorted::toString()
 {
   std::ostringstream modelStm;
 
   bool printIntroduced = false;
 
-  static DArray<DArray<vstring>> cnames;
+  static DArray<DArray<std::string>> cnames;
   cnames.ensure(env.signature->typeCons());
 
   //Output sorts and their sizes 
@@ -197,8 +197,8 @@ vstring FiniteModelMultiSorted::toString()
     if(env.signature->isInterpretedNonDefault(s))
       continue;
 
-    vstring sortName = env.signature->typeConName(s);
-    vstring sortNameLabel = (env.signature->isBoolCon(s)) ? "bool" : sortName;
+    std::string sortName = env.signature->typeConName(s);
+    std::string sortNameLabel = (env.signature->isBoolCon(s)) ? "bool" : sortName;
 
     // skip declaring $i, we know what it is
     if(!env.signature->isDefaultSortCon(s))
@@ -212,7 +212,7 @@ vstring FiniteModelMultiSorted::toString()
     for(unsigned i=1;i<=size;i++){
       modelStm << "tff(" << append(prepend("declare_", sortNameLabel), Int::toString(i).c_str()) << ",type,";
       int frep = sortRepr[s][i];
-      vstring cname = prepend("fmb_", sortNameLabel+"_"+Lib::Int::toString(i));
+      std::string cname = prepend("fmb_", sortNameLabel+"_"+Lib::Int::toString(i));
       if(frep >= 0){
         cname = env.signature->functionName(frep);
       }
@@ -258,14 +258,14 @@ vstring FiniteModelMultiSorted::toString()
     unsigned arity = env.signature->functionArity(f);
     if(arity>0) continue;
     if(!printIntroduced && env.signature->getFunction(f)->introduced()) continue;
-    vstring name = env.signature->functionName(f);
+    std::string name = env.signature->functionName(f);
     unsigned res = f_interpretation[f_offsets[f]];
     TermList srtT = env.signature->getFunction(f)->fnType()->result();
     unsigned srt = srtT.term()->functor();
-    vstring cname = cnames[srt][res];
+    std::string cname = cnames[srt][res];
     if(name == cname) continue;
 
-    vstring sortName = env.signature->typeConName(srt);
+    std::string sortName = env.signature->typeConName(srt);
     modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<":"<<sortName<<")."<<endl;
     if(res>0){ 
       modelStm << "tff("<<append(name,"_definition")<<",axiom,"<<name<<" = " << cname << ")."<<endl;
@@ -281,7 +281,7 @@ vstring FiniteModelMultiSorted::toString()
     unsigned arity = env.signature->functionArity(f);
     if(arity==0) continue;
     if(!printIntroduced && env.signature->getFunction(f)->introduced()) continue;
-    vstring name = env.signature->functionName(f);
+    std::string name = env.signature->functionName(f);
 
     OperatorType* sig = env.signature->getFunction(f)->fnType();
     modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": (";
@@ -356,7 +356,7 @@ vstring FiniteModelMultiSorted::toString()
     unsigned arity = env.signature->predicateArity(f);
     if(arity>0) continue;
     if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue;
-    vstring name = env.signature->predicateName(f);
+    std::string name = env.signature->predicateName(f);
     modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": $o)."<<endl;
     unsigned res = p_interpretation[p_offsets[f]];
     if(res==2){
@@ -375,7 +375,7 @@ vstring FiniteModelMultiSorted::toString()
     unsigned arity = env.signature->predicateArity(f);
     if(arity==0) continue;
     if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue;
-    vstring name = env.signature->predicateName(f);
+    std::string name = env.signature->predicateName(f);
 
     OperatorType* sig = env.signature->getPredicate(f)->predType();
     modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": (";