From a222bb3205555ad7e5ec74c265098523867b0992 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 6 Aug 2010 01:59:14 +0000 Subject: [PATCH] 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 --- src/simplifier/simplifier.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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() -- 2.47.3