Change -r so that it produces simpler expressions. I changed it in a way I didn't...

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 0507c7a44fd4d21843d0a47161474f4cde6b6bd3..f3b5454bf71ba76224353f43fe448d97cf5bc5b4 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -572,8 +572,15 @@ namespace BEEV
               // result is a variable here; it is an ite in the
               // else-branch
             }
-          else
+          else if (bm->UserFlags.isSet("old_ack","0"))
             {
+
+            /* oops.
+             * This version of ack. doesn't do what I thought it did. The STP 0.1 version of Ack. produces simpler
+             * expressions. I've put that in the next block. Trevor's thesis measures AckITE using this implementation,
+             * rather than the next one like it should have!!!!
+             */
+
               // Full Array transform if we're not doing read refinement.
 
               //list of array-read indices corresponding to arrName, seen while
@@ -598,6 +605,34 @@ namespace BEEV
                     simp->CreateSimplifiedTermITE(cond, it2->second.ite, result);
                 }
             }
+          else
+           {
+            // Full Array transform if we're not doing read refinement.
+
+            //list of array-read indices corresponding to arrName, seen while
+            //traversing the AST tree. we need this list to construct the ITEs
+            vector<std::pair<ASTNode, ASTNode > > p = ack_pair[arrName];
+
+            vector<std::pair<ASTNode, ASTNode > >::const_reverse_iterator it2 = p.rbegin();
+            vector<std::pair<ASTNode, ASTNode > >::const_reverse_iterator it2end = p.rend();
+            for (; it2 != it2end; it2++)
+              {
+                ASTNode cond =  simp->CreateSimplifiedEQ(readIndex, it2->first);
+                if (ASTFalse == cond)
+                  continue;
+
+                if (ASTTrue == cond)
+                  {
+                    result = it2->second;
+                    break;
+                  }
+
+                result =
+                  simp->CreateSimplifiedTermITE(cond, it2->second, result);
+              }
+
+           ack_pair[arrName].push_back(make_pair(readIndex,CurrentSymbol));
+           }
 
           assert(arrName.GetType() == ARRAY_TYPE);
           arrayToIndexToRead[arrName].insert(make_pair(readIndex,ArrayRead (result, CurrentSymbol)));
@@ -777,6 +812,9 @@ namespace BEEV
       assert(arrayToIndexToRead[e0[0]].find(e0[1]) ==arrayToIndexToRead[e0[0]].end());
 
       arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e1, e1)));
+
+      ack_pair[e0[0]].push_back(make_pair(e0[1],e1));
+
   }
 
 

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index d2bfcfb799f7030a03b5ff35a555127302d2f0b4..1f80ef4ecab4628adca031da57c8fb2c3101fc2e 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -56,6 +56,8 @@ namespace BEEV
 
   private:
 
+     map<ASTNode, vector<std::pair<ASTNode, ASTNode >  > > ack_pair;
+
     /****************************************************************
      * Private Typedefs and Data                                    *
      ****************************************************************/