From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 31 Jan 2012 03:19:13 +0000 (+0000)
Subject: Improvement, if there are < 10 array reads, write them away upfront.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a08765a42e9ca48f50f59641e3a9d4680225e50e;p=francis%2Fstp.git

Improvement, if there are < 10 array reads, write them away upfront.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index b05ddd8..142f593 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -43,6 +43,10 @@ namespace BEEV {
   SOLVER_RETURN_TYPE STP::TopLevelSTP(const ASTNode& inputasserts, 
 				      const ASTNode& query)
   {      
+
+    // Unfortunatey this is a global variable,which the aux function needs to overwrite sometimes.
+    bool saved_ack = bm->UserFlags.ackermannisation;
+
     ASTNode original_input;
 
     if (query != bm->ASTFalse)
@@ -83,6 +87,7 @@ namespace BEEV {
 
     delete newS;
 
+    bm->UserFlags.ackermannisation =saved_ack;
     return result;
 
   } //End of TopLevelSTP()
@@ -220,12 +225,14 @@ namespace BEEV {
     // The bit-vector simplifications are more thorough than the array simplifications. For example,
     // we don't currently do unconstrained elimination on arrays--- but we do for bit-vectors.
     // A better way to do this would be to estimate the number of axioms introduced.
-    // TODO: Should be enabled irrespective of whether refinement is enabled.
     // TODO: I chose the number of reads we perform this operation at randomly.
     bool removed = false;
-    if ((bm->UserFlags.ackermannisation && numberOfReadsLessThan(simplified_solved_InputToSAT,50)) || bm->UserFlags.isSet("upfront-ack", "0"))
+    if (((bm->UserFlags.ackermannisation && numberOfReadsLessThan(simplified_solved_InputToSAT,50)) || bm->UserFlags.isSet("upfront-ack", "0"))
+        || numberOfReadsLessThan(simplified_solved_InputToSAT,10)
+    )
       {
-          // If the number of axioms that would be added it small. Remove them.
+              // If the number of axioms that would be added it small. Remove them.
+              bm->UserFlags.ackermannisation = true;
               simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT);
               if (bm->UserFlags.stats_flag)
                 cerr << "Have removed array operations" << endl;