From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Feb 2011 14:54:22 +0000 (+0000)
Subject: Refactoring.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=723f18098f63d9f95514fa2957a09215888edb74;p=francis%2Fstp.git

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 23ed705..8cf7ac5 100644
--- 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 23e0fbd..accb2dc 100644
--- 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 d40c7fb..77da0c6 100644
--- 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