From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 12 May 2012 02:18:08 +0000 (+0000)
Subject: Change -r so that it produces simpler expressions. I changed it in a way I didn't... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=18dd55cedbd1f4507bcd2576ae8f8567c31b648e;p=francis%2Fstp.git

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

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 0507c7a..f3b5454 100644
--- 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 d2bfcfb..1f80ef4 100644
--- 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                                    *
      ****************************************************************/