From e597d7aff3feba237bf24bc761e4468c7c4983ab Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 13 May 2010 05:40:09 +0000 Subject: [PATCH] Remove the code for the "ReferenceCount". This was my first attempt to make the simplifications DAG-aware (sometimes called sharing-aware). The approach I chose was fundamentally broken (oops). I'm working on a new approach. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@765 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 57 ----------------------------------- src/simplifier/simplifier.h | 16 ---------- 2 files changed, 73 deletions(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index f3d8256..467193b 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -80,7 +80,6 @@ namespace BEEV return false; } - // Push any reference count used by the key to the value. void Simplifier::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg, ASTNodeMap* VarConstMap) @@ -95,20 +94,6 @@ namespace BEEV if (0 == key.Degree()) return; - // If there are references to the key, add them to the references - // of the value. - ASTNodeCountMap::const_iterator itKey, itValue; - itKey = ReferenceCount->find(key); - if (itKey != ReferenceCount->end()) - { - itValue = ReferenceCount->find(value); - if (itValue != ReferenceCount->end()) - (*ReferenceCount)[value] = itValue->second + itKey->second; - else - (*ReferenceCount)[value] = itKey->second; - } - - if (pushNeg) (*SimplifyNegMap)[key] = value; else @@ -215,33 +200,6 @@ namespace BEEV return out; } - void Simplifier::BuildReferenceCountMap(const ASTNode& b) - { - if (b.GetChildren().size() == 0) - return; - - ASTNodeCountMap::iterator it, itend; - - it = ReferenceCount->find(b); - if (it == ReferenceCount->end()) - { - (*ReferenceCount)[b] = 1; - } - else - { - (*ReferenceCount)[b] = it->second + 1; - return; - } - - const ASTVec& c = b.GetChildren(); - ASTVec::const_iterator itC = c.begin(); - ASTVec::const_iterator itendC = c.end(); - for (; itC != itendC; itC++) - { - BuildReferenceCountMap(*itC); - } - } - // The SimplifyMaps on entry to the topLevel functions may contain // useful entries. E.g. The BVSolver calls SimplifyTerm() ASTNode Simplifier::SimplifyFormula_TopLevel(const ASTNode& b, @@ -249,8 +207,6 @@ namespace BEEV ASTNodeMap* VarConstMap) { _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); - if (_bm->UserFlags.smtlib_parser_flag) - BuildReferenceCountMap(b); ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); ResetSimplifyMaps(); _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel); @@ -2609,13 +2565,6 @@ namespace BEEV swap_flag = true; } - ASTNodeCountMap::const_iterator it; - it = ReferenceCount->find(lhs); - if (it != ReferenceCount->end()) - { - if (it->second > 1) - return eq; - } unsigned int len = lhs.GetValueWidth(); ASTNode zero = _bm->CreateZeroConst(len); @@ -3287,22 +3236,16 @@ namespace BEEV //SimplifyNegMap->clear(); delete SimplifyNegMap; SimplifyNegMap = new ASTNodeMap(); - - //ReferenceCount->clear(); - delete ReferenceCount; - ReferenceCount = new ASTNodeCountMap(); } void Simplifier::printCacheStatus() { cerr << SimplifyMap->size() << endl; cerr << SimplifyNegMap->size() << endl; - cerr << ReferenceCount->size() << endl; //cerr << TermsAlreadySeenMap.size() << endl; cerr << SimplifyMap->bucket_count() << endl; cerr << SimplifyNegMap->bucket_count() << endl; - cerr << ReferenceCount->bucket_count() << endl; //cerr << TermsAlreadySeenMap.bucket_count() << endl; } //printCacheStatus() };//end of namespace diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 0a8a876..6883735 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -43,18 +43,6 @@ namespace BEEV // Read-Over-Write terms ASTNodeMap NewName_ReadOverWrite_Map; - - // The number of direct parents of each node. i.e. the number - // of times the pointer is in "children". When we simplify we - // want to be careful sometimes about using the context of a - // node. For example, given ((x + 23) = 2), the obvious - // simplification is to join the constants. However, if there - // are lots of references to the plus node. Then each time we - // simplify, we'll create an additional plus. - // nextpoweroftwo064.smt is the motivating benchmark. The - // splitting increased the number of pluses from 1 to 65. - ASTNodeCountMap *ReferenceCount; - //Ptr to STP Manager STPMgr * _bm; @@ -69,7 +57,6 @@ namespace BEEV SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); ReadOverWrite_NewName_Map = new ASTNodeMap(); - ReferenceCount = new ASTNodeCountMap(); ASTTrue = bm->CreateNode(TRUE); ASTFalse = bm->CreateNode(FALSE); @@ -80,7 +67,6 @@ namespace BEEV { delete SimplifyMap; delete SimplifyNegMap; - delete ReferenceCount; delete SolverMap; delete ReadOverWrite_NewName_Map; } @@ -143,7 +129,6 @@ namespace BEEV void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); - void BuildReferenceCountMap(const ASTNode& b); ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, @@ -251,7 +236,6 @@ namespace BEEV NewName_ReadOverWrite_Map.clear(); AlwaysTrueFormMap.clear(); MultInverseMap.clear(); - ReferenceCount->clear(); } };//end of class Simplifier }; //end of namespace -- 2.47.3