removed VarManager (was only ever used in a trivial way)

CMakeLists.txt

@@ -580,7 +580,6 @@ set(VAMPIRE_SHELL_SOURCES
     Shell/TPTPPrinter.cpp
     Shell/TweeGoalTransformation.cpp
     Shell/UIHelper.cpp
-    Shell/VarManager.cpp
     Shell/Lexer.cpp
     Shell/Preprocess.cpp
     Shell/AnswerLiteralManager.hpp
@@ -631,7 +630,6 @@ set(VAMPIRE_SHELL_SOURCES
     Shell/TPTPPrinter.hpp
     Shell/TweeGoalTransformation.hpp
     Shell/UIHelper.hpp
-    Shell/VarManager.hpp
     Shell/Lexer.hpp
     Shell/Preprocess.hpp
     Shell/SubexpressionIterator.cpp

Makefile

@@ -379,7 +379,6 @@ VS_OBJ = Shell/AnswerLiteralManager.o\
          Shell/Token.o\
          Shell/TPTPPrinter.o\
          Shell/UIHelper.o\
-         Shell/VarManager.o\
          Shell/Lexer.o\
          Shell/Preprocess.o\
          version.o

Shell/NewCNF.cpp

@@ -962,15 +962,15 @@ Term* NewCNF::createSkolemTerm(unsigned var, VarSet* free)
   Term* res;
   bool isPredicate = (rangeSort == AtomicSort::boolSort());
   if (isPredicate) {
-    unsigned pred = Skolem::addSkolemPredicate(arity, domainSorts.begin(), var);
+    unsigned pred = Skolem::addSkolemPredicate(arity, 0, domainSorts.begin());
     Signature::Symbol *sym = env.signature->getPredicate(pred);
     sym->markSkipCongruence();
     if(_beingClausified->derivedFromGoal()){
       sym->markInGoal();
     }
     res = Term::createFormula(new AtomicFormula(Literal::create(pred, arity, true, false, fnArgs.begin())));
   } else {
-    unsigned fun = Skolem::addSkolemFunction(arity, domainSorts.begin(), rangeSort, var);
+    unsigned fun = Skolem::addSkolemFunction(arity, 0, domainSorts.begin(), rangeSort);
     Signature::Symbol *sym = env.signature->getFunction(fun);
     sym->markSkipCongruence();
     if(_beingClausified->derivedFromGoal()){

Shell/Rectify.cpp

@@ -28,8 +28,6 @@
 
 #include "Indexing/TermSharing.hpp"
 
-#include "VarManager.hpp"
-
 #include "Rectify.hpp"
 
 using namespace std;
@@ -62,7 +60,7 @@ Rectify::VarWithUsageInfo Rectify::Renaming::getBoundAndUsage(int var) const
  * Rectify the formula from this unit. If the input type of this unit
  * contains free variables, then ask Signature::sig to create an answer
  * atom.
- * 
+ *
  * @since 23/01/2004 Manchester, changed to use non-static objects
  * @since 06/06/2007 Manchester, changed to use new datastructures
  */
@@ -512,19 +510,8 @@ void Rectify::Renaming::undoBinding (unsigned var)
  */
 unsigned Rectify::Renaming::bind (unsigned var)
 {
-  unsigned result;
+  unsigned result = _nextVar++;
 
-  if(VarManager::varNamePreserving()) {
-    if(_used->insert(var)) {
-      result=var;
-    }
-    else {
-      result=VarManager::getVarAlias(var);
-    }
-  }
-  else {
-    result = _nextVar++;
-  }
   VarUsageTrackingList::push(make_pair(result,false), get(var));
 
   return result;

Shell/Rectify.hpp

@@ -71,11 +71,6 @@ class Rectify
     virtual void fillInterval (size_t start,size_t end);
     /** next variable to rename to */
     unsigned _nextVar;
-    /** Variables that already appeared in the formula
-     *
-     * This field is used only when VarManager::varNamePreserving()
-     * is true. */
-    Recycled<DHSet<unsigned>> _used;
   };
 
   void reset();

Shell/Skolem.cpp

@@ -33,7 +33,6 @@
 #include "Options.hpp"
 #include "Rectify.hpp"
 #include "Skolem.hpp"
-#include "VarManager.hpp"
 
 using namespace std;
 using namespace Kernel;
@@ -119,18 +118,6 @@ FormulaUnit* Skolem::skolemiseImpl (FormulaUnit* unit, bool appify)
   return res;
 }
 
-unsigned Skolem::addSkolemFunction(unsigned arity, TermList* domainSorts,
-    TermList rangeSort, unsigned var, unsigned taArity)
-{
-  if(VarManager::varNamePreserving()) {
-    std::string varName=VarManager::getVarName(var);
-    return addSkolemFunction(arity, taArity, domainSorts, rangeSort, varName.c_str());
-  }
-  else {
-    return addSkolemFunction(arity, taArity, domainSorts, rangeSort);
-  }
-}
-
 unsigned Skolem::addSkolemFunction(unsigned arity, unsigned taArity, TermList* domainSorts,
     TermList rangeSort, const char* suffix)
 {
@@ -144,17 +131,6 @@ unsigned Skolem::addSkolemFunction(unsigned arity, unsigned taArity, TermList* d
   return fun;
 }
 
-unsigned Skolem::addSkolemTypeCon(unsigned arity, unsigned var)
-{
-  if(VarManager::varNamePreserving()) {
-    std::string varName=VarManager::getVarName(var);
-    return addSkolemTypeCon(arity, varName.c_str());
-  }
-  else {
-    return addSkolemTypeCon(arity);
-  }
-}
-
 unsigned Skolem::addSkolemTypeCon(unsigned arity, const char* suffix)
 {
   unsigned typeCon = env.signature->addSkolemTypeCon(arity, suffix);
@@ -164,21 +140,8 @@ unsigned Skolem::addSkolemTypeCon(unsigned arity, const char* suffix)
   return typeCon;
 }
 
-unsigned Skolem::addSkolemPredicate(unsigned arity, TermList* domainSorts, unsigned var, unsigned taArity)
-{
-  if(VarManager::varNamePreserving()) {
-    std::string varName=VarManager::getVarName(var);
-    return addSkolemPredicate(arity, taArity, domainSorts, varName.c_str());
-  }
-  else {
-    return addSkolemPredicate(arity, taArity, domainSorts);
-  }
-}
-
 unsigned Skolem::addSkolemPredicate(unsigned arity, unsigned taArity, TermList* domainSorts, const char* suffix)
 {
-  //ASS(arity==0 || domainSorts!=0);
-
   unsigned pred = env.signature->addSkolemPredicate(arity, suffix);
   Signature::Symbol* pSym = env.signature->getPredicate(pred);
   OperatorType* ot = OperatorType::getPredicateType(arity - taArity, domainSorts, taArity);
@@ -475,14 +438,14 @@ Formula* Skolem::skolemise (Formula* f)
             sym = addSkolemTypeCon(arity);
             skolemTerm = AtomicSort::create(sym, arity, allVars.begin());
           } else {
-            sym = addSkolemFunction(arity, termVarSorts.begin(), rangeSort, v, typeVars.size());
+            sym = addSkolemFunction(arity, typeVars.size(), termVarSorts.begin(), rangeSort);
             skolemTerm = Term::create(sym, arity, allVars.begin());
           }
         } else {
           //The higher-order case. Create the term
           //sk(typevars) @ termvar_1 @ termvar_2 @ ... @ termvar_n
           TermList skSymSort = AtomicSort::arrowSort(termVarSorts, rangeSort);
-          sym = addSkolemFunction(typeVars.size(), 0, skSymSort, v, typeVars.size());
+          sym = addSkolemFunction(typeVars.size(), typeVars.size(), nullptr, skSymSort);
           TermList head = TermList(Term::create(sym, typeVars.size(), typeVars.begin()));
           skolemTerm = ApplicativeHelper::createAppTerm(
             SortHelper::getResultSort(head.term()), head, termVars).term();

Shell/Skolem.hpp

@@ -43,11 +43,8 @@ class Skolem
 {
 public:
   static FormulaUnit* skolemise(FormulaUnit*, bool appify = false);
-  static unsigned addSkolemFunction(unsigned arity, TermList* domainSorts, TermList rangeSort, unsigned var, unsigned taArity = 0);
   static unsigned addSkolemFunction(unsigned arity, unsigned taArity, TermList* domainSorts, TermList rangeSort, const char* suffix=0);
-  static unsigned addSkolemTypeCon(unsigned arity, unsigned var);
-  static unsigned addSkolemTypeCon(unsigned arity, const char* suffix=0);  
-  static unsigned addSkolemPredicate(unsigned arity, TermList* domainSorts, unsigned var, unsigned taArity = 0);
+  static unsigned addSkolemTypeCon(unsigned arity, const char* suffix=0);
   static unsigned addSkolemPredicate(unsigned arity, unsigned taArity, TermList* domainSorts, const char* suffix=0);
 private:
   /** Initialise a Skolem object */