From 6efa3cb68098c43fe44dfc79ff8904edef43b2b1 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 26 Feb 2011 02:54:10 +0000 Subject: [PATCH] Bugfix. Terrible! STP r1149 to here will sometimes return the wrong answer. I was wrong about the semantics of .insert(..), I thought it replaced the new value if it was already present. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1169 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/FindPureLiterals.h | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h index fd0a769..61fd505 100644 --- a/src/simplifier/FindPureLiterals.h +++ b/src/simplifier/FindPureLiterals.h @@ -60,7 +60,7 @@ public: stp->GetRunTimes()->start(RunTimes::PureLiterals); build(n , truePolarity); - bool changed; + bool changed = false; map::const_iterator it = nodeToPolarity.begin(); while (it != nodeToPolarity.end()) @@ -69,11 +69,13 @@ public: const int polarity = it->second; if (n.GetType() == BOOLEAN_TYPE && n.GetKind() == SYMBOL && polarity != bothPolarity) { - //cerr << "--> Pure Literal" << n.GetName() << " " << polarity << endl; - if (polarity == truePolarity) - simplifier->UpdateSubstitutionMap(n,n.GetSTPMgr()->ASTTrue); - if (polarity == falsePolarity) - simplifier->UpdateSubstitutionMap(n,n.GetSTPMgr()->ASTFalse); + if (polarity == truePolarity) + simplifier->UpdateSubstitutionMap(n,n.GetSTPMgr()->ASTTrue); + else + { + assert (polarity == falsePolarity); + simplifier->UpdateSubstitutionMap(n,n.GetSTPMgr()->ASTFalse); + } changed = true; } it++; @@ -88,14 +90,15 @@ public: if (n.isConstant()) return; - map::const_iterator it = nodeToPolarity.find(n); + map::iterator it = nodeToPolarity.find(n); if (it != nodeToPolarity.end()) { int lookupPolarity = it->second; - if (polarity & lookupPolarity !=0 ) + if ((polarity & lookupPolarity) !=0 ) return; // already traversed. + lookupPolarity |= polarity; - nodeToPolarity.insert(make_pair(n,lookupPolarity)); + it->second = lookupPolarity; } else { -- 2.47.3