Refactoring.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 23ed705fa7aad15910d63cc1ae505dfb75754c88..8cf7ac565bfc4b4c6c31ca4485c293cf08932981 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -637,6 +637,9 @@ namespace BEEV
           (*Arrayname_ReadindicesMap)[arrName].push_back(readIndex);
           //save the ite corresponding to 'processedTerm'
           (*Arrayread_IteMap)[processedTerm] = result;
+
+          assert(arrName.GetType() == ARRAY_TYPE);
+          assert(result.GetValueWidth() == CurrentSymbol.GetValueWidth());
           arrayToIndexToRead[arrName].insert(make_pair(readIndex,ArrayRead (result, CurrentSymbol)));
           break;
         } //end of READ over a SYMBOL

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 23e0fbd9cf6c6c2310dc153deb6ec825ea464efb..accb2dc4a04cf4e668a048b7d1f828575457d66d 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -83,12 +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;
-          
-
-    // Count to keep track of new symbolic constants introduced
-    // corresponding to Array Reads
-    unsigned int _symbol_count;
+  private:
         
     // Memo table used by the transformer while it is transforming the
     // formulas and terms
@@ -148,8 +145,7 @@ namespace BEEV
       bm(bm), 
       simp(s), 
       debug_transform(0),
-      TransformMap(NULL),
-      _symbol_count(0)
+      TransformMap(NULL)
     {
       Arrayread_IteMap = new ASTNodeMap();
       Arrayname_ReadindicesMap = new ASTNodeToVecMap();
@@ -191,10 +187,6 @@ namespace BEEV
       return symbol;
     } //End of ArrayRead_SymbolMap
     
-    const ASTNodeMap * ArrayRead_IteMap()
-    {
-      return Arrayread_IteMap;
-    } //End of ArrayRead_IteMap
 
     ASTNode ArrayRead_Ite(const ASTNode& arrread)
     {

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index d40c7fb50b1d7ca6153b2bca273bc76a2e6ff994..77da0c611a36654fc850d3ae8e8e3e50e90c3e86 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -85,12 +85,12 @@ 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++)
+        ArrayTransform->Arrayread_IteMap->begin(), itend =
+        ArrayTransform->Arrayread_IteMap->end(); it != itend; it++)
       {
         //the array read
-        ASTNode arrayread = it->first;
-        ASTNode value_ite = ArrayTransform->ArrayRead_Ite(arrayread);
+        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