From fd89d56bc478ba9661bfe73b3c8662a2ef4a038d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 5 Aug 2010 05:07:06 +0000 Subject: [PATCH] Bugfix. The prior revision sometimes returned the wrong result (very rarely). In the prior revision I removed some explicit calls to simplifyTerm. Wrongly believing that the term was already simplified at the point. To check that it was simplified I asserted the "hasBeenSimplified" function. But the hasBeenSimplified function only checked that the term was present in the simplifyMap. That is that simplifyTerm had been called on it. Which isn't the same thing as being simplified. i.e. term A is not simplified if in the SimplifyMap it's mapped to term B. It's only simplified if A maps to A. Some simplification functions expect their children to already be simplified. This wasn't the case so we'd get the wrong answer. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@965 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 19 +++++++++++-------- src/simplifier/simplifier.h | 3 +-- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 075a101..7f7f746 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1625,9 +1625,10 @@ namespace BEEV return nf->CreateTerm(k, a.GetValueWidth(), a, b); } - + // If a node is not a leaf, it has only been simplified if it + // maps to itself in the simplifyMap. bool - Simplifier::hasBeenSimplified(ASTNode n) + Simplifier::hasBeenSimplified(const ASTNode& n) { //n has been simplified if, it's a constant: if (n.isConstant()) @@ -1640,8 +1641,12 @@ namespace BEEV if (n.GetKind() == SYMBOL) return true; + ASTNodeMap::const_iterator it; //If it's in the simplification map, it has been simplified. - return (SimplifyMap->find(n) != SimplifyMap->end()); + if ((it = SimplifyMap->find(n)) == SimplifyMap->end()) + return false; + + return (it->second == n); } //This function simplifies terms based on their kind @@ -1656,7 +1661,7 @@ namespace BEEV ASTNode inputterm(actualInputterm); // mutable local copy. - //cout << "SimplifyTerm: input: " << a << endl; + //cout << "SimplifyTerm: input: " << actualInputterm << endl; // if (!optimize_flag) // { // return inputterm; @@ -1714,10 +1719,7 @@ namespace BEEV else output = actualInputterm; - if (inputterm != output) { - UpdateSimplifyMap(inputterm, output, false, VarConstMap); - inputterm = output; - } + inputterm = output; } const ASTVec& children = inputterm.GetChildren(); @@ -2860,6 +2862,7 @@ namespace BEEV output = SimplifyTerm(output); //memoize UpdateSimplifyMap(inputterm, output, false, VarConstMap); + UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); //cerr << "SimplifyTerm: output" << output << endl; // CheckSimplifyInvariant(inputterm,output); diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index b1e4a14..5731f38 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -134,9 +134,8 @@ namespace BEEV bool pushNeg, ASTNodeMap* VarConstMap=NULL); - bool - hasBeenSimplified(ASTNode n); + bool hasBeenSimplified(const ASTNode& n); ASTNode SimplifyTerm(const ASTNode& inputterm, ASTNodeMap* VarConstMap=NULL); -- 2.47.3