Partial refactor. Removing the Arrayname_ReadindicesMap.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 51c5ca7e33b55bcffff84ed953470011da239cd7..8f6463cbce8cb7ecee58b920fe20887e8a2dc5ff 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -618,25 +618,25 @@ namespace BEEV
               //list of array-read indices corresponding to arrName, seen while
               //traversing the AST tree. we need this list to construct the ITEs
               // Dill: we hope to make this irrelevant.  Harmless for now.
-              const ASTVec & readIndices = (*Arrayname_ReadindicesMap)[arrName];
+              const map<ASTNode, ArrayRead>& new_read_Indices = arrayToIndexToRead[arrName];
 
-                 // Full Array transform if we're not doing read refinement.
-              ASTVec::const_reverse_iterator it2 = readIndices.rbegin();
-              ASTVec::const_reverse_iterator it2end = readIndices.rend();
+              // Full Array transform if we're not doing read refinement.
+              map<ASTNode, ArrayRead>::const_iterator it2 = new_read_Indices.begin();
+              map<ASTNode, ArrayRead>::const_iterator it2end = new_read_Indices.end();
               for (; it2 != it2end; it2++)
                 {
                   ASTNode cond = 
-                    simp->CreateSimplifiedEQ(readIndex, *it2);
+                    simp->CreateSimplifiedEQ(readIndex, it2->first);
                   if (ASTFalse == cond)
                     continue;
 
                                  // This could be made faster by storing these, rather than
                   // creating each one n times.
                    ASTNode arrRead =
-                    nf->CreateTerm(READ, width, arrName, *it2);
+                    nf->CreateTerm(READ, width, arrName, it2->first);
                   assert(BVTypeCheck(arrRead));
 
-                  const ASTNode& arrayreadSymbol = Arrayread_SymbolMap[arrRead];
+                  const ASTNode& arrayreadSymbol = it2->second.ite;
                   if (arrayreadSymbol.IsNull())
                     {
                       FatalError("TransformArray:"\
@@ -650,7 +650,7 @@ namespace BEEV
               //}
             }
 
-          (*Arrayname_ReadindicesMap)[arrName].push_back(readIndex);
+          //(*Arrayname_ReadindicesMap)[arrName].push_back(readIndex);
           //save the ite corresponding to 'processedTerm'
           //(*Arrayread_IteMap)[processedTerm] = result;
 
@@ -841,7 +841,7 @@ namespace BEEV
 
     if (!simp->CheckSubstitutionMap(e0))
       {
-        (*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]);
+        //(*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]);
         //e0 is the array read : READ(A,i) and e1 is a bvconst
         Arrayread_SymbolMap[e0] = e1;
         arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e1, e1)));

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index d3451fe88d211452ff30ea1f63b7fc8cb2521f46..88993bdc3a5b4da2c08b33febe03202361569a01 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -70,7 +70,7 @@ namespace BEEV
     // CAUTION: I tried using a set instead of vector for read
     // indicies. for some odd reason the performance went down
     // considerably. this is totally inexplicable.
-    ASTNodeToVecMap * Arrayname_ReadindicesMap;
+    //ASTNodeToVecMap * Arrayname_ReadindicesMap;
     
     // MAP: This is a map from array-reads to symbolic constants. This
     // map is used by the TransformArray()     
@@ -148,7 +148,7 @@ namespace BEEV
       TransformMap(NULL)
     {
       //Arrayread_IteMap = new ASTNodeMap();
-      Arrayname_ReadindicesMap = new ASTNodeToVecMap();
+      //Arrayname_ReadindicesMap = new ASTNodeToVecMap();
       nf = bm->defaultNodeFactory;
 
       runTimes = bm->GetRunTimes();
@@ -162,7 +162,7 @@ namespace BEEV
     {
       //Arrayread_IteMap->clear();
       //delete Arrayread_IteMap;
-      ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin();
+      /*ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin();
       ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end();
       for(;it!=itend;it++)
         {
@@ -170,16 +170,17 @@ namespace BEEV
         }
       Arrayname_ReadindicesMap->clear();
       delete Arrayname_ReadindicesMap;
+      */
     }
 
     // Takes a formula, transforms it by replacing array reads with
     // variables, and returns the transformed formula
     ASTNode TransformFormula_TopLevel(const ASTNode& form);
 
-    const ASTNodeToVecMap * ArrayName_ReadIndicesMap()
-    {
-      return Arrayname_ReadindicesMap;
-    } //End of ArrayName_ReadIndicesMap
+    //const ASTNodeToVecMap * ArrayName_ReadIndicesMap()
+    //{
+//      return Arrayname_ReadindicesMap;
+  //  } //End of ArrayName_ReadIndicesMap
 
     const ASTNode ArrayRead_SymbolMap(const ASTNode& arrread) 
     {
@@ -190,7 +191,7 @@ namespace BEEV
     void ClearAllTables(void)
     {
 
-      for (ASTNodeToVecMap::iterator
+      /*for (ASTNodeToVecMap::iterator
              iset = Arrayname_ReadindicesMap->begin(), 
              iset_end = Arrayname_ReadindicesMap->end(); 
            iset != iset_end; iset++)
@@ -199,6 +200,7 @@ namespace BEEV
         }
 
       Arrayname_ReadindicesMap->clear();
+*/
       Arrayread_SymbolMap.clear();
       //Arrayread_IteMap->clear();
       arrayToIndexToRead.clear();