From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 6 Aug 2010 01:59:14 +0000 (+0000)
Subject: Fix slowdown.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a222bb3205555ad7e5ec74c265098523867b0992;p=francis%2Fstp.git

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 1e895c1..67283bb 100644
--- 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()