From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Feb 2011 13:43:18 +0000 (+0000)
Subject: Partial Refactor. I'm reducing the number of collections in the ArrayTransformer... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=93343f81b762ffce615cd42d012fe09bd4fa6902;p=francis%2Fstp.git

Partial Refactor. I'm reducing the number of collections in the ArrayTransformer class, but it's causing difficult to find defects. This adds a new collection. I'll remove the old ones later.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 78c8691..78cded9 100644
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -637,6 +637,7 @@ namespace BEEV
           (*Arrayname_ReadindicesMap)[arrName].push_back(readIndex);
           //save the ite corresponding to 'processedTerm'
           (*Arrayread_IteMap)[processedTerm] = result;
+          arrayToIndexToRead[arrName].insert(make_pair(readIndex,ArrayRead (result, CurrentSymbol)));
           break;
         } //end of READ over a SYMBOL
       case WRITE:
@@ -824,6 +825,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;
+        arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e0[1], e0[1])));
         return;
       }
 
diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index c9bf61a..23e0fbd 100644
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -20,6 +20,36 @@ namespace BEEV
 
   class ArrayTransformer 
   {
+  public:
+
+      // These map from array and index to ITE and Symbol.
+      struct ArrayRead
+      {
+        ArrayRead(ASTNode _ite, ASTNode _symbol)
+        {
+          assert(! _symbol.IsNull());
+          assert ((SYMBOL == _symbol.GetKind() || BVCONST == _symbol.GetKind()));
+
+          ite = _ite;
+          symbol = _symbol;
+        }
+
+        ASTNode ite;  // if not using refinement this will be the ITE for the read. Otherwise == symbol.
+        ASTNode symbol; // each read is allocated a distinct fresh variable.
+      };
+
+      // MAP: This maps from arrays to their indexes.
+      // This map is used by the TransformArray()
+      // function ,as well as the counter example, and refinement.
+      // This map is useful in converting array reads into
+      // nested ITE constructs. Suppose there are two 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)
+
+      typedef map<ASTNode, map<ASTNode, ArrayRead> > ArrType ;
+      ArrType arrayToIndexToRead;
+
   private:
 
     /****************************************************************
diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index ffd7641..40ece0c 100644
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -57,47 +57,49 @@ namespace BEEV
     //are no more axioms to add
     //
     //for each array, fetch its list of indices seen so far
-    for (ASTNodeToVecMap::const_iterator 
-           iset = ArrayTransform->ArrayName_ReadIndicesMap()->begin(),
-           iset_end = ArrayTransform->ArrayName_ReadIndicesMap()->end(); 
+    for (ArrayTransformer::ArrType::const_iterator
+           iset = ArrayTransform->arrayToIndexToRead.begin(),
+           iset_end = ArrayTransform->arrayToIndexToRead.end();
          iset != iset_end; iset++)
       {
     	const ASTNode& ArrName = iset->first;
-    	const ASTVec& listOfIndices = iset->second;
+    	const map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
+
+        vector<ASTNode> listOfIndices;
+        listOfIndices.reserve(mapper.size());
 
     	// Make a vector of the read symbols.
     	ASTVec read_node_symbols;
     	read_node_symbols.reserve(listOfIndices.size());
 
     	vector<Kind> jKind;
-    	jKind.reserve(listOfIndices.size());
+    	jKind.reserve(mapper.size());
 
     	vector<ASTNode> concreteIndexes;
-    	concreteIndexes.reserve(listOfIndices.size());
+    	concreteIndexes.reserve(mapper.size());
 
     	vector<ASTNode> concreteValues;
-    	concreteValues.reserve(listOfIndices.size());
-
+    	concreteValues.reserve(mapper.size());
 
-    	for (int i = 0; i < listOfIndices.size(); i++)
+    	int i =0;
+    	for (map<ASTNode, ArrayTransformer::ArrayRead>::const_iterator it =mapper.begin() ; it != mapper.end();it++)
     	{
-        	const ASTNode& the_index = listOfIndices[i];
-
-        	ASTNode arr_read =
-              bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index);
 
-        	ASTNode arrsym = ArrayTransform->ArrayRead_SymbolMap(arr_read);
-        	assert ((SYMBOL == arrsym.GetKind() || BVCONST == arrsym.GetKind()));
+    	    const ASTNode& the_index = it->first;
+            listOfIndices.push_back(it->first);
 
-        	read_node_symbols.push_back(arrsym);
+            ASTNode arrsym = it->second.symbol;
+            read_node_symbols.push_back(arrsym);
 
-        	jKind.push_back(listOfIndices[i].GetKind());
-
-        	concreteIndexes.push_back(TermToConstTermUsingModel(the_index));
-        	concreteValues.push_back(TermToConstTermUsingModel(arrsym));
+            jKind.push_back(the_index.GetKind());
 
+            concreteIndexes.push_back(TermToConstTermUsingModel(the_index));
+            concreteValues.push_back(TermToConstTermUsingModel(arrsym));
+            i++;
     	}
 
+    	assert(listOfIndices.size() == mapper.size());
+
         //loop over the list of indices for the array and create LA,
         //and add to inputAlreadyInSAT
         for (int i = 0; i < listOfIndices.size(); i++)