Partial refactor. Remove the Arrayread_SymbolMap.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 8f6463cbce8cb7ecee58b920fe20887e8a2dc5ff..97307c524d17c2f68c250bd114d75d6ed316e39b 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -560,7 +560,7 @@ namespace BEEV
               }
           }
 
-          //  Recursively transform read index, which may also contain reads.
+          //  The read index has already been recursively transformed.
           ASTNode processedTerm = 
             nf->CreateTerm(READ, width, arrName, readIndex);
 
@@ -583,14 +583,14 @@ namespace BEEV
           // constant value in the substitution map.
           if (simp->CheckSubstitutionMap(processedTerm, CurrentSymbol))
             {
-              Arrayread_SymbolMap[processedTerm] = CurrentSymbol;
+              //Arrayread_SymbolMap[processedTerm] = CurrentSymbol;
             }
           // Check if it already has an abstract variable.
-          else if ((it1 = Arrayread_SymbolMap.find(processedTerm)) 
-                   != Arrayread_SymbolMap.end())
-            {
-              CurrentSymbol = it1->second;
-            }
+          //else if ((it1 = Arrayread_SymbolMap.find(processedTerm))
+                //   != Arrayread_SymbolMap.end())
+       //     {
+        //      CurrentSymbol = it1->second;
+       //     }
           else
             {
               // Make up a new abstract variable. Build symbolic name
@@ -602,16 +602,15 @@ namespace BEEV
                                  processedTerm.GetValueWidth(),
                                  "array_" + string(arrName.GetName()));
 
-                 Arrayread_SymbolMap[processedTerm] = CurrentSymbol;
+                 //Arrayread_SymbolMap[processedTerm] = CurrentSymbol;
             }
 
-          ASTNode ite = CurrentSymbol;
+          result = CurrentSymbol;
 
           if (bm->UserFlags.arrayread_refinement_flag)
             {
               // ite is really a variable here; it is an ite in the
               // else-branch
-              result = ite;
             }
           else
             {
@@ -625,29 +624,14 @@ namespace BEEV
               map<ASTNode, ArrayRead>::const_iterator it2end = new_read_Indices.end();
               for (; it2 != it2end; it2++)
                 {
-                  ASTNode cond = 
-                    simp->CreateSimplifiedEQ(readIndex, it2->first);
+                  ASTNode cond =  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->first);
-                  assert(BVTypeCheck(arrRead));
-
-                  const ASTNode& arrayreadSymbol = it2->second.ite;
-                  if (arrayreadSymbol.IsNull())
-                    {
-                      FatalError("TransformArray:"\
-                                 "symbolic variable for processedTerm, p,"\
-                                 "does not exist:p = ", arrRead);
-                    }
-                  ite = 
-                    simp->CreateSimplifiedTermITE(cond, arrayreadSymbol, ite);
+                  result =
+                    simp->CreateSimplifiedTermITE(cond, it2->second.ite, result);
                 }
-              result = ite;
-              //}
+
             }
 
           //(*Arrayname_ReadindicesMap)[arrName].push_back(readIndex);
@@ -843,7 +827,7 @@ namespace BEEV
       {
         //(*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;
+        //Arrayread_SymbolMap[e0] = e1;
         arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e1, e1)));
         return;
       }

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 88993bdc3a5b4da2c08b33febe03202361569a01..fbd1b6b0d84e62f280fffa0592669560430a37e5 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -74,7 +74,7 @@ namespace BEEV
     
     // MAP: This is a map from array-reads to symbolic constants. This
     // map is used by the TransformArray()     
-    ASTNodeMap Arrayread_SymbolMap;
+    //ASTNodeMap Arrayread_SymbolMap;
         
     // MAP: This is a map from Array Names to nested ITE constructs,
     // which are built as described below. This map is used by the
@@ -141,7 +141,7 @@ namespace BEEV
     
     // Constructor
     ArrayTransformer(STPMgr * bm, Simplifier* s) : 
-      Arrayread_SymbolMap(),
+      //Arrayread_SymbolMap(),
       bm(bm), 
       simp(s), 
       debug_transform(0),
@@ -182,11 +182,11 @@ namespace BEEV
 //      return Arrayname_ReadindicesMap;
   //  } //End of ArrayName_ReadIndicesMap
 
-    const ASTNode ArrayRead_SymbolMap(const ASTNode& arrread) 
-    {
-      ASTNode symbol = Arrayread_SymbolMap[arrread];
-      return symbol;
-    } //End of ArrayRead_SymbolMap
+    //const ASTNode ArrayRead_SymbolMap(const ASTNode& arrread)
+    //{
+      //ASTNode symbol = Arrayread_SymbolMap[arrread];
+      //return symbol;
+  //  } //End of ArrayRead_SymbolMap
     
     void ClearAllTables(void)
     {
@@ -201,7 +201,7 @@ namespace BEEV
 
       Arrayname_ReadindicesMap->clear();
 */
-      Arrayread_SymbolMap.clear();
+      //Arrayread_SymbolMap.clear();
       //Arrayread_IteMap->clear();
       arrayToIndexToRead.clear();
     }