From a5e7877f5481f296bcdb2d0a4ccdfede713f0601 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 13 Apr 2011 04:41:09 +0000 Subject: [PATCH] Improvement. Look for nodes that are true/false when conjoined to the top. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1270 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 137 ++++++++++++++++++++-------------- src/simplifier/simplifier.h | 4 +- 2 files changed, 81 insertions(+), 60 deletions(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 3b02959..f0786cf 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -190,17 +190,37 @@ namespace BEEV MultInverseMap[key] = value; } - bool Simplifier::CheckAlwaysTrueFormSet(const ASTNode& key) + // Check if key, or NOT(key) is found in the alwaysTrueSet. + bool Simplifier::CheckAlwaysTrueFormSet(const ASTNode& key, bool& result) { - HASHSET::const_iterator it2 = AlwaysTrueHashSet.find(key.GetNodeNum()); HASHSET::const_iterator it_end_2 = AlwaysTrueHashSet.end(); + HASHSET::const_iterator it2 = AlwaysTrueHashSet.find(key.GetNodeNum()); - return it2 != it_end_2; + if(it2 != it_end_2) + { + result = true; // The key should be replaced by TRUE. + return true; + } + + int toSearch; + if (key.GetKind() == NOT) + toSearch = key.GetNodeNum()-1; + else + toSearch = key.GetNodeNum()+1; + + it2 = AlwaysTrueHashSet.find(toSearch); + if(it2 != it_end_2) + { + result = false; + return true; + } + + return false; } void Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key) { - AlwaysTrueHashSet.insert(key.GetNodeNum()); + AlwaysTrueHashSet.insert(key.GetNodeNum()); } ASTNode @@ -1091,15 +1111,14 @@ namespace BEEV return t2; if (t1 == t2) return t1; - if (CheckAlwaysTrueFormSet(t0)) - { - return t1; - } - if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) - || (NOT == t0.GetKind() - && CheckAlwaysTrueFormSet(t0[0]))) + + bool result; + if (CheckAlwaysTrueFormSet(t0,result)) { - return t2; + if (result) + return t1; + else + return t2; } return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2); @@ -1123,16 +1142,16 @@ namespace BEEV return t2; if (t1 == t2) return t1; - if (CheckAlwaysTrueFormSet(t0)) - { - return t1; - } - if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) - || (NOT == t0.GetKind() - && CheckAlwaysTrueFormSet(t0[0]))) + + bool result; + if (CheckAlwaysTrueFormSet(t0,result)) { - return t2; + if (result) + return t1; + else + return t2; } + } ASTNode result = nf->CreateNode(ITE, t0, t1, t2); assert(BVTypeCheck(result)); @@ -1269,10 +1288,14 @@ namespace BEEV //pushnegation if there are odd number of NOTs bool pn = (NotCount % 2 == 0) ? false : true; - if (CheckAlwaysTrueFormSet(o)) + bool alwaysTrue; + if (CheckAlwaysTrueFormSet(o,alwaysTrue)) { - output = pn ? ASTFalse : ASTTrue; - return output; + if (alwaysTrue) + return ( pn ? ASTFalse : ASTTrue); + + // We don't do the false case because it is sometimes + // called at the top level. } if (CheckSimplifyMap(o, output, pn)) @@ -1422,6 +1445,7 @@ namespace BEEV { c0 = SimplifyFormula(a[0], false, VarConstMap); c1 = SimplifyFormula(a[1], false, VarConstMap); + bool atResult; if (ASTFalse == c0) { output = ASTTrue; @@ -1434,28 +1458,25 @@ namespace BEEV { output = ASTTrue; } - else if (CheckAlwaysTrueFormSet(c0)) + else if (CheckAlwaysTrueFormSet(c0, atResult)) { // c0 AND (~c0 OR c1) <==> c1 - // - //applying modus ponens - output = c1; - } - else if (CheckAlwaysTrueFormSet(c1) || - CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c0)) || - (NOT == c0.GetKind() && CheckAlwaysTrueFormSet(c0[0]))) - { //(~c0 AND (~c0 OR c1)) <==> TRUE - // //(c0 AND ~c0->c1) <==> TRUE - output = ASTTrue; - } - else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c1)) || - (NOT == c1.GetKind() && CheckAlwaysTrueFormSet(c1[0]))) - { //(~c1 AND c0->c1) <==> (~c1 AND ~c1->~c0) <==> ~c0 //(c1 AND c0->~c1) <==> (c1 AND c1->~c0) <==> ~c0 - output = nf->CreateNode(NOT, c0); + + if (atResult) + output = c1; + else + output = ASTTrue; + } + else if (CheckAlwaysTrueFormSet(c1, atResult)) + { + if (atResult) + output = ASTTrue; + else + output = nf->CreateNode(NOT, c0); } else { @@ -1495,6 +1516,8 @@ namespace BEEV else c0 = SimplifyFormula(c0, false, VarConstMap); + bool alwaysResult; + if (ASTTrue == c0) { output = c1; @@ -1522,21 +1545,19 @@ namespace BEEV { output = ASTFalse; } - else if (CheckAlwaysTrueFormSet(c0)) - { - output = c1; - } - else if (CheckAlwaysTrueFormSet(c1)) + else if (CheckAlwaysTrueFormSet(c0,alwaysResult)) { - output = c0; - } - else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c0))) - { - output = nf->CreateNode(NOT, c1); + if (alwaysResult) + output = c1; + else + output = nf->CreateNode(NOT, c1); } - else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c1))) + else if (CheckAlwaysTrueFormSet(c1,alwaysResult)) { - output = nf->CreateNode(NOT, c0); + if (alwaysResult) + output = c0; + else + output = nf->CreateNode(NOT, c0); } else { @@ -1577,6 +1598,8 @@ namespace BEEV t2 = SimplifyFormula(a[2], false, VarConstMap); } + bool alwaysTrue; + if (ASTTrue == t0) { output = t1; @@ -1613,14 +1636,12 @@ namespace BEEV { output = nf->CreateNode(AND, t0, t1); } - else if (CheckAlwaysTrueFormSet(t0)) - { - output = t1; - } - else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) || - (NOT == t0.GetKind() && CheckAlwaysTrueFormSet(t0[0]))) + else if (CheckAlwaysTrueFormSet(t0,alwaysTrue)) { - output = t2; + if (alwaysTrue) + output = t1; + else + output = t2; } else { diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 9c0343f..8a337ac 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -99,14 +99,14 @@ namespace BEEV const ASTNode& key, ASTNode& output); - //functions for checking and updating simplifcation map + //functions for checking and updating simplification map bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg, ASTNodeMap* VarConstMap=NULL); void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg, ASTNodeMap* VarConstMap=NULL); - bool CheckAlwaysTrueFormSet(const ASTNode& key); + bool CheckAlwaysTrueFormSet(const ASTNode& key, bool& result); void UpdateAlwaysTrueFormSet(const ASTNode& val); bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); -- 2.47.3