Remove the code for the "ReferenceCount". This was my first attempt to make the simpl...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@765 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index f3d8256c0b0a1f604db715500c38a1aa67b17f4c..467193b3263eb3c2ef3e7614d7aa12d9c7be2d11 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -80,7 +80,6 @@ namespace BEEV
     return false;
   }
 
-  // Push any reference count used by the key to the value.
   void Simplifier::UpdateSimplifyMap(const ASTNode& key, 
                                      const ASTNode& value, 
                                      bool pushNeg, ASTNodeMap* VarConstMap)
@@ -95,20 +94,6 @@ namespace BEEV
     if (0 == key.Degree())
       return;
     
-    // If there are references to the key, add them to the references
-    // of the value.
-    ASTNodeCountMap::const_iterator itKey, itValue;
-    itKey = ReferenceCount->find(key);
-    if (itKey != ReferenceCount->end())
-      {
-        itValue = ReferenceCount->find(value);
-        if (itValue != ReferenceCount->end())
-          (*ReferenceCount)[value] = itValue->second + itKey->second;
-        else
-          (*ReferenceCount)[value] = itKey->second;
-      }
-
-
     if (pushNeg)
       (*SimplifyNegMap)[key] = value;
     else
@@ -215,33 +200,6 @@ namespace BEEV
     return out;
   }
 
-  void Simplifier::BuildReferenceCountMap(const ASTNode& b)
-  {
-    if (b.GetChildren().size() == 0)
-      return;
-
-    ASTNodeCountMap::iterator it, itend;
-
-    it = ReferenceCount->find(b);
-    if (it == ReferenceCount->end())
-      {
-        (*ReferenceCount)[b] = 1;
-      }
-    else
-      {
-        (*ReferenceCount)[b] = it->second + 1;
-        return;
-      }
-
-    const ASTVec& c = b.GetChildren();
-    ASTVec::const_iterator itC = c.begin();
-    ASTVec::const_iterator itendC = c.end();
-    for (; itC != itendC; itC++)
-      {
-        BuildReferenceCountMap(*itC);
-      }
-  }
-
   // The SimplifyMaps on entry to the topLevel functions may contain
   // useful entries.  E.g. The BVSolver calls SimplifyTerm()
   ASTNode Simplifier::SimplifyFormula_TopLevel(const ASTNode& b, 
@@ -249,8 +207,6 @@ namespace BEEV
                                                ASTNodeMap* VarConstMap)
   {
     _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
-    if (_bm->UserFlags.smtlib_parser_flag)
-      BuildReferenceCountMap(b);
     ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
     ResetSimplifyMaps();
     _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel);
@@ -2609,13 +2565,6 @@ namespace BEEV
         swap_flag = true;
       }
 
-    ASTNodeCountMap::const_iterator it;
-    it = ReferenceCount->find(lhs);
-    if (it != ReferenceCount->end())
-      {
-        if (it->second > 1)
-          return eq;
-      }
 
     unsigned int len = lhs.GetValueWidth();
     ASTNode zero = _bm->CreateZeroConst(len);
@@ -3287,22 +3236,16 @@ namespace BEEV
     //SimplifyNegMap->clear();
     delete SimplifyNegMap;
     SimplifyNegMap = new ASTNodeMap();
-
-    //ReferenceCount->clear();
-    delete ReferenceCount;
-    ReferenceCount = new ASTNodeCountMap();
   }
 
   void Simplifier::printCacheStatus()
   {
     cerr << SimplifyMap->size() << endl;
     cerr << SimplifyNegMap->size() << endl;
-    cerr << ReferenceCount->size() << endl;
     //cerr << TermsAlreadySeenMap.size() << endl;
   
     cerr << SimplifyMap->bucket_count() << endl;
     cerr << SimplifyNegMap->bucket_count() << endl;
-    cerr << ReferenceCount->bucket_count() << endl;
     //cerr << TermsAlreadySeenMap.bucket_count() << endl;
   } //printCacheStatus()
 };//end of namespace

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 0a8a876a14f43c2d2fc7539556c67940020f991f..6883735b84c75f1943b4a6ca9f6e6559dfedcf94 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -43,18 +43,6 @@ namespace BEEV
     // Read-Over-Write terms
     ASTNodeMap NewName_ReadOverWrite_Map;
 
-      
-    // The number of direct parents of each node. i.e. the number
-    // of times the pointer is in "children".  When we simplify we
-    // want to be careful sometimes about using the context of a
-    // node. For example, given ((x + 23) = 2), the obvious
-    // simplification is to join the constants. However, if there
-    // are lots of references to the plus node. Then each time we
-    // simplify, we'll create an additional plus.
-    // nextpoweroftwo064.smt is the motivating benchmark. The
-    // splitting increased the number of pluses from 1 to 65.
-    ASTNodeCountMap *ReferenceCount;
-      
     //Ptr to STP Manager
     STPMgr * _bm;
 
@@ -69,7 +57,6 @@ namespace BEEV
       SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
       SolverMap      = new ASTNodeMap(INITIAL_TABLE_SIZE);
       ReadOverWrite_NewName_Map = new ASTNodeMap();
-      ReferenceCount = new ASTNodeCountMap();
 
       ASTTrue  = bm->CreateNode(TRUE);
       ASTFalse = bm->CreateNode(FALSE);
@@ -80,7 +67,6 @@ namespace BEEV
     {
       delete SimplifyMap;
       delete SimplifyNegMap;
-      delete ReferenceCount;
       delete SolverMap;
       delete ReadOverWrite_NewName_Map;
     }
@@ -143,7 +129,6 @@ namespace BEEV
     void CheckSimplifyInvariant(const ASTNode& a, 
                                 const ASTNode& output);
 
-    void BuildReferenceCountMap(const ASTNode& b);
 
     ASTNode SimplifyAtomicFormula(const ASTNode& a, 
                                   bool pushNeg, 
@@ -251,7 +236,6 @@ namespace BEEV
       NewName_ReadOverWrite_Map.clear();
       AlwaysTrueFormMap.clear();
       MultInverseMap.clear();
-      ReferenceCount->clear();
     }
   };//end of class Simplifier
 }; //end of namespace