Partial Refactor. I'm reducing the number of collections in the ArrayTransformer...

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 78c86911f3abe60d27113f1337e1b649e70de722..78cded97b8cf903c52b4e6de366ab551c1312b5c 100644 (file)
--- 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 c9bf61aade7386000628bfc8d23c9d2422ed3cda..23e0fbd9cf6c6c2310dc153deb6ec825ea464efb 100644 (file)
--- 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 ffd76414de763d203a9de5a14a6e758acd5a374d..40ece0ca2c6a51fee97c9443461d1e8c85e0f1b7 100644 (file)
--- 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++)