From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 28 Nov 2011 05:33:34 +0000 (+0000)
Subject: Improvement. If simplifications make the problem containing arrays harder, then rever... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b958615bb48711d2d2591aee7399f6ea96007453;p=francis%2Fstp.git

Improvement. If simplifications make the problem containing arrays harder, then revert it. Prevsiously it only did this for bit-vector only problems. This uses extra memory. It seems justified.



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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index de7950c..c6f4505 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -211,6 +211,7 @@ namespace BEEV {
     // A heap object so I can easily control its lifetime.
     BVSolver* bvSolver = new BVSolver(bm, simp);
 
+    // Run size reducing just once.
     simplified_solved_InputToSAT = sizeReducing(inputToSAT, bvSolver);
 
     unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
@@ -219,8 +220,10 @@ namespace BEEV {
     // Currently we discards all the state each time sizeReducing is called,
     // so it's expensive to call.
     if (!arrayops && initial_difficulty_score < 1000000)
+           simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver, initial_difficulty_score);
+
+    if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
       {
-        simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver, initial_difficulty_score);
         initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
       }
 
@@ -230,9 +233,12 @@ namespace BEEV {
     // Copy the solver map incase we need to revert.
     ASTNodeMap initialSolverMap;
     ASTNode toRevertTo;
-    if (!arrayops) // we don't revert for Array problems yet, so don't copy it.
+    ArrayTransformer::ArrType backup_arrayToIndexToRead;
+
+    if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
       {
         initialSolverMap.insert(simp->Return_SolverMap()->begin(), simp->Return_SolverMap()->end());
+        backup_arrayToIndexToRead.insert(arrayTransformer->arrayToIndexToRead.begin(),arrayTransformer->arrayToIndexToRead.end());
         toRevertTo = simplified_solved_InputToSAT;
       }
 
@@ -401,8 +407,9 @@ namespace BEEV {
       }
 
     bool optimize_enabled = bm->UserFlags.optimize_flag;
-    if (final_difficulty_score > 1.1 * initial_difficulty_score && !arrayops && bm->UserFlags.isSet(
-        "difficulty-reversion", "1"))
+    if (final_difficulty_score > 1.1 * initial_difficulty_score &&
+       (!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")) &&
+       bm->UserFlags.isSet("difficulty-reversion", "1"))
       {
         // If the simplified problem is harder, than the
         // initial problem we revert back to the initial
@@ -420,6 +427,10 @@ namespace BEEV {
         simp->Return_SolverMap()->insert(initialSolverMap.begin(), initialSolverMap.end());
         initialSolverMap.clear();
 
+        // Copy back what we knew about arrays at the start..
+        arrayTransformer->arrayToIndexToRead.clear();
+        arrayTransformer->arrayToIndexToRead.insert(backup_arrayToIndexToRead.begin(), backup_arrayToIndexToRead.end());
+
         // The arrayTransformer calls simplify. We don't want
         // it to put back in all the bad simplifications.
         bm->UserFlags.optimize_flag = false;