Partial refactoring. Removing the arrayread_itemap.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 8cf7ac565bfc4b4c6c31ca4485c293cf08932981..51c5ca7e33b55bcffff84ed953470011da239cd7 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -547,12 +547,26 @@ namespace BEEV
            *                        .....
            */
 
+          {
+            ArrType::const_iterator it;
+            if ((it = arrayToIndexToRead.find(arrName)) != arrayToIndexToRead.end())
+              {
+                map<ASTNode, ArrayRead>::const_iterator it2;
+                  if ((it2 = it->second.find(readIndex)) != it->second.end())
+                    {
+                      result = it2->second.ite;
+                      break;
+                    }
+              }
+          }
+
           //  Recursively transform read index, which may also contain reads.
           ASTNode processedTerm = 
             nf->CreateTerm(READ, width, arrName, readIndex);
 
           //check if the 'processedTerm' has a corresponding ITE construct
           //already. if so, return it. else continue processing.
+          /*
           ASTNodeMap::const_iterator it;
           if ((it = Arrayread_IteMap->find(processedTerm))
               != Arrayread_IteMap->end())
@@ -560,6 +574,8 @@ namespace BEEV
               result = it->second;
               break;
             }
+            */
+
           //Constructing Symbolic variable corresponding to 'processedTerm'
           ASTNode CurrentSymbol;
           ASTNodeMap::const_iterator it1;
@@ -636,7 +652,7 @@ namespace BEEV
 
           (*Arrayname_ReadindicesMap)[arrName].push_back(readIndex);
           //save the ite corresponding to 'processedTerm'
-          (*Arrayread_IteMap)[processedTerm] = result;
+          //(*Arrayread_IteMap)[processedTerm] = result;
 
           assert(arrName.GetType() == ARRAY_TYPE);
           assert(result.GetValueWidth() == CurrentSymbol.GetValueWidth());

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index accb2dc4a04cf4e668a048b7d1f828575457d66d..d3451fe88d211452ff30ea1f63b7fc8cb2521f46 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -83,9 +83,9 @@ namespace BEEV
     // array reads in the input Read(A,i) and Read(A,j). Then
     // Read(A,i) is replaced with a symbolic constant, say v1, and
     // Read(A,j) is replaced with the following ITE: ITE(i=j,v1,v2)
-  public:
-    ASTNodeMap * Arrayread_IteMap;
-  private:
+
+    //ASTNodeMap * Arrayread_IteMap;
+
         
     // Memo table used by the transformer while it is transforming the
     // formulas and terms
@@ -147,7 +147,7 @@ namespace BEEV
       debug_transform(0),
       TransformMap(NULL)
     {
-      Arrayread_IteMap = new ASTNodeMap();
+      //Arrayread_IteMap = new ASTNodeMap();
       Arrayname_ReadindicesMap = new ASTNodeToVecMap();
       nf = bm->defaultNodeFactory;
 
@@ -160,8 +160,8 @@ namespace BEEV
     // Destructor
     ~ArrayTransformer()
     {
-      Arrayread_IteMap->clear();
-      delete Arrayread_IteMap;
+      //Arrayread_IteMap->clear();
+      //delete Arrayread_IteMap;
       ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin();
       ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end();
       for(;it!=itend;it++)
@@ -187,13 +187,6 @@ namespace BEEV
       return symbol;
     } //End of ArrayRead_SymbolMap
     
-
-    ASTNode ArrayRead_Ite(const ASTNode& arrread)
-    {
-      return (*Arrayread_IteMap)[arrread];
-    } //End of ArrayRead_Ite
-
-
     void ClearAllTables(void)
     {
 
@@ -207,7 +200,8 @@ namespace BEEV
 
       Arrayname_ReadindicesMap->clear();
       Arrayread_SymbolMap.clear();
-      Arrayread_IteMap->clear();
+      //Arrayread_IteMap->clear();
+      arrayToIndexToRead.clear();
     }
   }; //end of class Transformer
 

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 77da0c611a36654fc850d3ae8e8e3e50e90c3e86..726977ba0a50065b3c55dffc977345f74ff41f11 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -82,30 +82,32 @@ namespace BEEV
         }
       }
 
-    //In this loop, we compute the value of each array read, the
-    //corresponding ITE against the counterexample generated above.
-    for (ASTNodeMap::const_iterator it =
-        ArrayTransform->Arrayread_IteMap->begin(), itend =
-        ArrayTransform->Arrayread_IteMap->end(); it != itend; it++)
+        for (ArrayTransformer::ArrType::const_iterator it = ArrayTransform->arrayToIndexToRead.begin(), itend =
+        ArrayTransform->arrayToIndexToRead.end(); it != itend; it++)
       {
-        //the array read
-        const ASTNode& arrayread = it->first;
-        const ASTNode& value_ite = it->second;
-
-        //convert it to a constant array-read and store it in the
-        //counter-example. First convert the index into a constant. then
-        //construct the appropriate array-read and store it in the
-        //counterexample
-        ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1],false);
-        ASTNode key = bm->CreateTerm(READ, arrayread.GetValueWidth(),
-                                     arrayread[0], arrayread_index);
-
-        //Get the ITE corresponding to the array-read and convert it
-        //to a constant against the model
-        ASTNode value = TermToConstTermUsingModel(value_ite);
-        //save the result in the counter_example
-        if (!simp->CheckSubstitutionMap(key))
-          CounterExampleMap[key] = value;
+        const ASTNode& array = it->first;
+        const map<ASTNode, ArrayTransformer::ArrayRead>& mapper = it->second;
+
+        for (map<ASTNode, ArrayTransformer::ArrayRead>::const_iterator it2 = mapper.begin(), it2end = mapper.end(); it2
+            != it2end; it2++)
+          {
+            const ASTNode& index = it2->first;
+            const ASTNode& value_ite = it2->second.ite;
+
+            //convert it to a constant array-read and store it in the
+            //counter-example. First convert the index into a constant. then
+            //construct the appropriate array-read and store it in the
+            //counterexample
+            ASTNode arrayread_index = TermToConstTermUsingModel(index, false);
+            ASTNode key = bm->CreateTerm(READ, array.GetValueWidth(), array, arrayread_index);
+
+            //Get the ITE corresponding to the array-read and convert it
+            //to a constant against the model
+            ASTNode value = TermToConstTermUsingModel(value_ite);
+            //save the result in the counter_example
+            if (!simp->CheckSubstitutionMap(key))
+              CounterExampleMap[key] = value;
+          }
       }
   } //End of ConstructCounterExample