]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
Bugfix. The prior revision sometimes returned the wrong result (very rarely).
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Thu, 5 Aug 2010 05:07:06 +0000 (05:07 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Thu, 5 Aug 2010 05:07:06 +0000 (05:07 +0000)
commitfd89d56bc478ba9661bfe73b3c8662a2ef4a038d
tree45fbce1ce3455368142567f0dc9fa907cdcd0e3e
parentfb4eb4a3b1d3db3e82c120eac5612b5dc401cc77
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
src/simplifier/simplifier.h