From cc5f902267faf5ee27a16752211b84a925317453 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 3 Mar 2011 06:03:24 +0000 Subject: [PATCH] Fixes / Improvements. * Fix. No longer create NOT(NOT(..)) nodes because their node numbers aren't unique. * Improvement. Change the AlwaysTrueFormMap (which was a set), to use node numbers ---which allows the nodes to be garbage collected. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1184 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/NodeFactory/HashingNodeFactory.cpp | 6 +++ src/STPManager/STPManager.cpp | 6 ++- src/simplifier/SubstitutionMap.cpp | 8 ++- src/simplifier/SubstitutionMap.h | 3 +- src/simplifier/simplifier.cpp | 61 ++++++++++------------ src/simplifier/simplifier.h | 10 ++-- 6 files changed, 52 insertions(+), 42 deletions(-) diff --git a/src/AST/NodeFactory/HashingNodeFactory.cpp b/src/AST/NodeFactory/HashingNodeFactory.cpp index e584ac7..198b1fa 100644 --- a/src/AST/NodeFactory/HashingNodeFactory.cpp +++ b/src/AST/NodeFactory/HashingNodeFactory.cpp @@ -26,6 +26,12 @@ BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind, const BEEV::ASTVec SortByArith(children); } + // We can't create NOT(NOT (..)) nodes because of how the numbering scheme we use works. + // So you can't trust the hashiing node factory even to return nodes of the same kind that + // you ask for. + if (kind == BEEV::NOT && children[0].GetKind() == BEEV::NOT) + return children[0][0]; + // insert all of children at end of new_children. ASTNode n(bm.CreateInteriorNode(kind, n_ptr, children)); return n; diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 31c1527..dd8c134 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -27,7 +27,11 @@ namespace BEEV // have alpha.nodenum + 1. if (n_ptr->GetKind() == NOT) { - n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum() + 1); + // The internal node can't be a NOT, because then we'd add + // 1 to the NOT's node number, meaning we'd hit an even number, + // which could duplicate the next newNodeNum(). + assert(n_ptr->GetChildren()[0].GetKind() != NOT); + n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum() + 1); } else { diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index a6e2565..932811d 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -74,6 +74,12 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform if (CheckSubstitutionMap(a, output)) return output; + if (!alreadyVisited.insert(a.GetNodeNum()).second) + { + return a; + } + + //traverse a and populate the SubstitutionMap const Kind k = a.GetKind(); if (SYMBOL == k && BOOLEAN_TYPE == a.GetType()) @@ -162,7 +168,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform it = c.begin(), itend = c.end(); it != itend; it++) { - simp->UpdateAlwaysTrueFormMap(*it); + simp->UpdateAlwaysTrueFormSet(*it); ASTNode aaa = CreateSubstitutionMap(*it,at); if (ASTTrue != aaa) diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 5c2bac1..ad40590 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -31,6 +31,7 @@ class SubstitutionMap { ASTNodeSet rhs; // All the rhs that have been seeen. set rhsAlreadyAdded; VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already. + HASHSET alreadyVisited; int loopCount; @@ -68,6 +69,7 @@ public: { SolverMap->clear(); haveAppliedSubstitutionMap(); + alreadyVisited.clear(); } virtual ~SubstitutionMap(); @@ -83,7 +85,6 @@ public: return false; } - //update solvermap with (key,value) pair bool UpdateSolverMap(const ASTNode& key, const ASTNode& value) { ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 1cffce5..a2d1899 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -180,24 +180,17 @@ namespace BEEV MultInverseMap[key] = value; } - bool Simplifier::CheckAlwaysTrueFormMap(const ASTNode& key) + bool Simplifier::CheckAlwaysTrueFormSet(const ASTNode& key) { - ASTNodeSet::iterator it = AlwaysTrueFormMap.find(key); - ASTNodeSet::iterator itend = AlwaysTrueFormMap.end(); + HASHSET::const_iterator it2 = AlwaysTrueHashSet.find(key.GetNodeNum()); + HASHSET::const_iterator it_end_2 = AlwaysTrueHashSet.end(); - if (it != itend) - { - //cerr << "found:" << *it << endl; - CountersAndStats("Successful_CheckAlwaysTrueFormMap", _bm); - return true; - } - - return false; + return it2 != it_end_2; } - void Simplifier::UpdateAlwaysTrueFormMap(const ASTNode& key) + void Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key) { - AlwaysTrueFormMap.insert(key); + AlwaysTrueHashSet.insert(key.GetNodeNum()); } ASTNode @@ -1050,13 +1043,13 @@ namespace BEEV return t2; if (t1 == t2) return t1; - if (CheckAlwaysTrueFormMap(t0)) + if (CheckAlwaysTrueFormSet(t0)) { return t1; } - if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, t0)) + if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) || (NOT == t0.GetKind() - && CheckAlwaysTrueFormMap(t0[0]))) + && CheckAlwaysTrueFormSet(t0[0]))) { return t2; } @@ -1082,13 +1075,13 @@ namespace BEEV return t2; if (t1 == t2) return t1; - if (CheckAlwaysTrueFormMap(t0)) + if (CheckAlwaysTrueFormSet(t0)) { return t1; } - if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, t0)) + if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) || (NOT == t0.GetKind() - && CheckAlwaysTrueFormMap(t0[0]))) + && CheckAlwaysTrueFormSet(t0[0]))) { return t2; } @@ -1228,7 +1221,7 @@ namespace BEEV //pushnegation if there are odd number of NOTs bool pn = (NotCount % 2 == 0) ? false : true; - if (CheckAlwaysTrueFormMap(o)) + if (CheckAlwaysTrueFormSet(o)) { output = pn ? ASTFalse : ASTTrue; return output; @@ -1393,24 +1386,24 @@ namespace BEEV { output = ASTTrue; } - else if (CheckAlwaysTrueFormMap(c0)) + else if (CheckAlwaysTrueFormSet(c0)) { // c0 AND (~c0 OR c1) <==> c1 // //applying modus ponens output = c1; } - else if (CheckAlwaysTrueFormMap(c1) || - CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c0)) || - (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0]))) + 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 (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c1)) || - (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0]))) + 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 @@ -1481,19 +1474,19 @@ namespace BEEV { output = ASTFalse; } - else if (CheckAlwaysTrueFormMap(c0)) + else if (CheckAlwaysTrueFormSet(c0)) { output = c1; } - else if (CheckAlwaysTrueFormMap(c1)) + else if (CheckAlwaysTrueFormSet(c1)) { output = c0; } - else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c0))) + else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c0))) { output = nf->CreateNode(NOT, c1); } - else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c1))) + else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c1))) { output = nf->CreateNode(NOT, c0); } @@ -1572,12 +1565,12 @@ namespace BEEV { output = nf->CreateNode(AND, t0, t1); } - else if (CheckAlwaysTrueFormMap(t0)) + else if (CheckAlwaysTrueFormSet(t0)) { output = t1; } - else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, t0)) || - (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) + else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) || + (NOT == t0.GetKind() && CheckAlwaysTrueFormSet(t0[0]))) { output = t2; } @@ -3907,7 +3900,7 @@ namespace BEEV { cerr << "SimplifyMap:" << SimplifyMap->size() << ":" << SimplifyMap->bucket_count() << endl; cerr << "SimplifyNegMap:" << SimplifyNegMap->size() << ":" << SimplifyNegMap->bucket_count() << endl; - cerr << "AlwaysTrueFormMap" << AlwaysTrueFormMap.size() << ":" << AlwaysTrueFormMap.bucket_count() << endl; + cerr << "AlwaysTrueFormSet" << AlwaysTrueHashSet.size() << ":" << AlwaysTrueHashSet.bucket_count() << endl; cerr << "MultInverseMap" << MultInverseMap.size() << ":" << MultInverseMap.bucket_count() << endl; cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":" << ReadOverWrite_NewName_Map->bucket_count() << endl; cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":" << NewName_ReadOverWrite_Map.bucket_count() << endl; diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 0e0d640..655da35 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -36,7 +36,7 @@ namespace BEEV // value is simplified node. ASTNodeMap * SimplifyMap; ASTNodeMap * SimplifyNegMap; - ASTNodeSet AlwaysTrueFormMap; + HASHSET AlwaysTrueHashSet; ASTNodeMap MultInverseMap; // For ArrayWrite Abstraction: map from read-over-write term to @@ -101,8 +101,8 @@ namespace BEEV void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg, ASTNodeMap* VarConstMap=NULL); - bool CheckAlwaysTrueFormMap(const ASTNode& key); - void UpdateAlwaysTrueFormMap(const ASTNode& val); + bool CheckAlwaysTrueFormSet(const ASTNode& key); + void UpdateAlwaysTrueFormSet(const ASTNode& val); bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); @@ -260,7 +260,7 @@ namespace BEEV SimplifyNegMap->clear(); ReadOverWrite_NewName_Map->clear(); NewName_ReadOverWrite_Map.clear(); - AlwaysTrueFormMap.clear(); + AlwaysTrueHashSet.clear(); MultInverseMap.clear(); substitutionMap.clear(); } @@ -269,7 +269,7 @@ namespace BEEV // These can be cleared (to save memory) without changing the answer. void ClearCaches() { - AlwaysTrueFormMap.clear(); + AlwaysTrueHashSet.clear(); MultInverseMap.clear(); SimplifyMap->clear(); SimplifyNegMap->clear(); -- 2.47.3