Improvement. Better manage the data stored to revert based on difficulty.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index c6f450572e65ecf1d295aeaed70cc951c2f512b7..30ee0b875d50ab171cf735bd53a7027dd14e38aa 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -230,16 +230,14 @@ namespace BEEV {
     if (bm->UserFlags.stats_flag)
       cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl;
 
-    // Copy the solver map incase we need to revert.
-    ASTNodeMap initialSolverMap;
-    ASTNode toRevertTo;
-    ArrayTransformer::ArrType backup_arrayToIndexToRead;
+    // So we can delete the object and release all the hash-buckets storage.
+    Revert_to* revert = new Revert_to();
 
     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;
+        revert->initialSolverMap.insert(simp->Return_SolverMap()->begin(), simp->Return_SolverMap()->end());
+        revert->backup_arrayToIndexToRead.insert(arrayTransformer->arrayToIndexToRead.begin(),arrayTransformer->arrayToIndexToRead.end());
+        revert->toRevertTo = simplified_solved_InputToSAT;
       }
 
     //round of substitution, solving, and simplification. ensures that
@@ -417,24 +415,25 @@ namespace BEEV {
 
         if (bm->UserFlags.stats_flag)
           cerr << "simplification made the problem harder, reverting." << endl;
-        simplified_solved_InputToSAT = toRevertTo;
+        simplified_solved_InputToSAT = revert->toRevertTo;
 
         // I do this to clear the substitution/solver map.
         // Not sure what would happen if it contained simplifications
         // that haven't been applied.
         simp->ClearAllTables();
 
-        simp->Return_SolverMap()->insert(initialSolverMap.begin(), initialSolverMap.end());
-        initialSolverMap.clear();
+        simp->Return_SolverMap()->insert(revert->initialSolverMap.begin(), revert->initialSolverMap.end());
+        revert->initialSolverMap.clear();
 
         // Copy back what we knew about arrays at the start..
         arrayTransformer->arrayToIndexToRead.clear();
-        arrayTransformer->arrayToIndexToRead.insert(backup_arrayToIndexToRead.begin(), backup_arrayToIndexToRead.end());
+        arrayTransformer->arrayToIndexToRead.insert(revert->backup_arrayToIndexToRead.begin(), revert->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;
       }
+    delete revert;
 
     simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT);
     bm->ASTNodeStats("after transformation: ", simplified_solved_InputToSAT);

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 9de176e31d445c375ac149c1778366e7796a2d04..2de28813d813fc2a8e35a16e0b4710654c446a47 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -29,6 +29,14 @@ namespace BEEV
   private:
           ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver);
 
+          // A copy of all the state we need to restore to a prior expression.
+          struct Revert_to
+          {
+            ASTNodeMap initialSolverMap; // Map from variables to expressions they were replaced with.
+            ASTNode toRevertTo;          // The original expression.
+            ArrayTransformer::ArrType backup_arrayToIndexToRead; // array-indices already removed.
+          };
+
   public:
           // calls sizeReducing and the bitblasting simplification.
           ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score);