remove InverseLookup, not useful

CMakeLists.txt

@@ -156,7 +156,6 @@ set(VAMPIRE_LIB_SOURCES
     Lib/Int.hpp
     Lib/IntNameTable.hpp
     Lib/IntUnionFind.hpp
-    Lib/InverseLookup.hpp
     Lib/List.hpp
     Lib/Map.hpp
     Lib/MaybeBool.hpp

InstGen/IGAlgorithm.cpp

@@ -560,7 +560,6 @@ void IGAlgorithm::selectAndAddToIndex(Clause* cl)
 {
   CALL("IGAlgorithm::selectAndAddToIndex");
 
-  bool modified = false;
   unsigned selIdx = 0;
 
   unsigned clen = cl->length();
@@ -570,15 +569,11 @@ void IGAlgorithm::selectAndAddToIndex(Clause* cl)
     }
 
     if(selIdx!=i) {
-      modified = true;
       swap((*cl)[i], (*cl)[selIdx]);
     }
     selIdx++;
   }
   ASS_REP(selIdx>0, cl->toString());
-  if(modified) {
-    cl->notifyLiteralReorder();
-  }
 
   if (_doLookahead) {
     unsigned selCnt = selIdx>1 ? lookaheadSelection(cl,selIdx) : 1;

Kernel/Clause.cpp

@@ -72,7 +72,6 @@ Clause::Clause(unsigned length,const Inference& inf)
     _weightForClauseSelection(0),
     _refCnt(0),
     _reductionTimestamp(0),
-    _literalPositions(0),
     _numActiveSplits(0),
     _auxTimestamp(0)
 {
@@ -121,10 +120,6 @@ void Clause::operator delete(void* ptr,unsigned length)
 
 void Clause::destroyExceptInferenceObject()
 {
-  if (_literalPositions) {
-    delete _literalPositions;
-  }
-
   RSTAT_CTR_INC("clauses deleted");
 
   //We have to get sizeof(Clause) + (_length-1)*sizeof(Literal*)
@@ -709,83 +704,13 @@ unsigned Clause::numPositiveLiterals()
   return count;
 }
 
-/**
- * Return index of @b lit in the clause
- *
- * @b lit has to be present in the clause
- */
-unsigned Clause::getLiteralPosition(Literal* lit)
-{
-  switch(length()) {
-  case 1:
-    ASS_EQ(lit,(*this)[0]);
-    return 0;
-  case 2:
-    if (lit==(*this)[0]) {
-      return 0;
-    } else {
-      ASS_EQ(lit,(*this)[1]);
-      return 1;
-    }
-  case 3:
-    if (lit==(*this)[0]) {
-      return 0;
-    } else if (lit==(*this)[1]) {
-      return 1;
-    } else {
-      ASS_EQ(lit,(*this)[2]);
-      return 2;
-    }
-#if VDEBUG
-  case 0:
-    ASSERTION_VIOLATION;
-#endif
-  default:
-    if (!_literalPositions) {
-      _literalPositions=new InverseLookup<Literal>(_literals,length());
-    }
-    return static_cast<unsigned>(_literalPositions->get(lit));
-  }
-}
-
-/**
- * This method should be called when literals of the clause are
- * reordered (e.g. after literal selection), so that the information
- * about literal positions can be updated.
- */
-void Clause::notifyLiteralReorder()
-{
-  CALL("Clause::notifyLiteralReorder");
-  if (_literalPositions) {
-    _literalPositions->update(_literals);
-  }
-}
-
 #if VDEBUG
-
 void Clause::assertValid()
 {
   ASS_ALLOC_TYPE(this, "Clause");
-  if (_literalPositions) {
-    unsigned clen=length();
-    for (unsigned i = 0; i<clen; i++) {
-      ASS_EQ(getLiteralPosition((*this)[i]),i);
-    }
-  }
 }
-
 #endif
 
-bool Clause::contains(Literal* lit)
-{
-  for (int i = _length-1; i >= 0; i--) {
-    if (_literals[i]==lit) {
-      return true;
-    }
-  }
-  return false;
-}
-
 std::ostream& operator<<(std::ostream& out, Clause::Store const& store) 
 {
   switch (store) {

Kernel/Clause.hpp

@@ -23,7 +23,6 @@
 
 #include "Lib/Allocator.hpp"
 #include "Lib/Event.hpp"
-#include "Lib/InverseLookup.hpp"
 #include "Lib/Metaiterators.hpp"
 #include "Lib/Reflection.hpp"
 #include "Lib/Stack.hpp"
@@ -148,7 +147,6 @@ class Clause
     ASS(s >= 0);
     ASS(s <= _length);
     _numSelected = s;
-    notifyLiteralReorder();
   }
 
   /** Return the weight */
@@ -200,8 +198,17 @@ class Clause
 
   bool skip() const;
 
-  unsigned getLiteralPosition(Literal* lit);
-  void notifyLiteralReorder();
+  /**
+   * Return index of @b lit in the clause
+   *
+   * @b lit has to be present in the clause
+   */
+  unsigned getLiteralPosition(Literal* lit) {
+    for(unsigned i = 0; i < length(); i++)
+      if(literals()[i] == lit)
+        return i;
+    ASSERTION_VIOLATION;
+  }
 
   bool shouldBeDestroyed();
   void destroyIfUnnecessary();
@@ -246,7 +253,13 @@ class Clause
 
   VirtualIterator<unsigned> getVariableIterator();
 
-  bool contains(Literal* lit);
+  bool contains(Literal* lit) {
+    for (unsigned i = 0; i < length(); i++)
+      if (_literals[i] == lit)
+        return true;
+    return false;
+  }
+
 #if VDEBUG
   void assertValid();
 #endif
@@ -385,8 +398,6 @@ class Clause
   unsigned _refCnt;
   /** for splitting: timestamp marking when has the clause been reduced or restored by splitting */
   unsigned _reductionTimestamp;
-  /** a map that translates Literal* to its index in the clause */
-  InverseLookup<Literal>* _literalPositions;
 
   int _numActiveSplits;
 
@@ -398,8 +409,6 @@ class Clause
   static bool _auxInUse;
 #endif
 
-//#endif
-
   /** Array of literals of this unit */
   Literal* _literals[1];
 }; // class Clause

Kernel/LiteralSelector.cpp

@@ -208,27 +208,21 @@ void LiteralSelector::select(Clause* c, unsigned eligibleInp)
 
   unsigned eligible=1;
   int maxPriority=getSelectionPriority((*c)[0]);
-  bool modified=false;
 
   for (unsigned i = 1; i < eligibleInp; i++) {
     int priority = getSelectionPriority((*c)[i]);
     if (priority == maxPriority) {
       if (eligible != i) {
         swap((*c)[i], (*c)[eligible]);
-        modified = true;
       }
       eligible++;
     } else if (priority > maxPriority) {
       maxPriority = priority;
       eligible = 1;
       swap((*c)[i], (*c)[0]);
-      modified = true;
     }
   }
   ASS_LE(eligible,eligibleInp);
-  if(modified) {
-    c->notifyLiteralReorder();
-  }
 
   if(eligible==1) {
     c->setSelected(eligible);

Shell/Normalisation.cpp

@@ -111,7 +111,6 @@ void Normalisation::normalise (Unit* unit)
     clause[i] = srt[i];
   }
 
-  clause.notifyLiteralReorder();
   return;
 } // Normalisation::normalise(Unit*)
 

Shell/Shuffling.cpp

@@ -134,8 +134,6 @@ void Shuffling::shuffle(Clause* clause)
   shuffleArray(clause->literals()+s,clause->length()-s);
 
   // literals must be shared in typical clauses (I think), so let's not even try shuffling them
-
-  clause->notifyLiteralReorder();
 }
 
 // iterative implementation of shuffling Formula* / Literal* / TermList