Fix slowdown.

r965 removed a cache update that caused bitblaster.cvc to run 10 times slower. This update adds back in the cache update as well as changes to ensure that by the end of SimplifyTerm the invariant that actualInput maps to something that hasBeenSimplified(output) holds for.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 1e895c178c228806715f99522336730baf057cce..67283bb8ff8a3a8bbb6f0f8c340e1c4a7c87c65a 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1725,13 +1725,18 @@ namespace BEEV
                        else
                                output = actualInputterm;
 
-                       inputterm = output;
+                       if (inputterm != output)
+                         {
+                             UpdateSimplifyMap(inputterm,output,false);
+                             inputterm = output;
+                         }
                }
 
                const ASTVec& children = inputterm.GetChildren();
                k = inputterm.GetKind();
 
                // Perform constant propagation if possible.
+               // This should do nothing if the simplifyingnodefactory is used.
                if (k != BEEV::UNDEFINED && k != BEEV::SYMBOL) {
                        bool allConstant = true;
 
@@ -1755,6 +1760,7 @@ namespace BEEV
     if (pulledUp != inputterm)
       {
         ASTNode r = SimplifyTerm(pulledUp);
+        UpdateSimplifyMap(actualInputterm,r,NULL);
         UpdateSimplifyMap(inputterm,r,NULL);
         return r;
       }
@@ -2464,6 +2470,7 @@ namespace BEEV
                   output = annihilator;
                   //memoize
                   UpdateSimplifyMap(inputterm, output, false, VarConstMap);
+                  UpdateSimplifyMap(actualInputterm, output, false, VarConstMap);
                   //cerr << "output of SimplifyTerm: " << output << endl;
                   return output;
                 }
@@ -2479,6 +2486,7 @@ namespace BEEV
               {
                  output = annihilator;
                  UpdateSimplifyMap(inputterm, output, false, VarConstMap);
+                 UpdateSimplifyMap(actualInputterm, output, false, VarConstMap);
                   return output;
               }
 
@@ -2876,6 +2884,7 @@ namespace BEEV
     assert(!output.IsNull());
     assert(inputterm.GetValueWidth() == output.GetValueWidth());
     assert(inputterm.GetIndexWidth() == output.GetIndexWidth());
+    assert(hasBeenSimplified(output));
 
     return output;
   } //end of SimplifyTerm()