From 5c05c30f0cd66304d1102393f9b71d462ae47c09 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 11 Apr 2009 08:25:49 +0000 Subject: [PATCH] Reset simplify and expression hashmaps when clearing. If a hashmap got very big, some methods like clear would take a long time (using the hasmap that is linked to on my machine). The clear() function traverses each of the buckets in the hashmap seeing whether it had children. If the hashmap previously had millions of elements, even if it now contains just a single element, then there would still be millions of buckets. The clear() function would take much longer than it needed to. These changes were inspired by testcase15.stp.smt. On my machine, this patch speeds up STP on that benchmark by 20 times. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@67 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.cpp | 12 ++++++------ AST/AST.h | 12 +++++++----- parser/let-funcs.cpp | 32 +++++++++++++++++++++++++------- simplifier/simplifier.cpp | 37 ++++++++++++++++++++++++------------- 4 files changed, 62 insertions(+), 31 deletions(-) diff --git a/AST/AST.cpp b/AST/AST.cpp index f607c1e..1549353 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -2006,15 +2006,15 @@ namespace BEEV { NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); AlreadyPrintedSet.clear(); - SimplifyMap.clear(); - SimplifyNegMap.clear(); + SimplifyMap->clear(); + SimplifyNegMap->clear(); SolverMap.clear(); AlwaysTrueFormMap.clear(); _arrayread_ite.clear(); _arrayread_symbol.clear(); _introduced_symbols.clear(); TransformMap.clear(); - _letid_expr_map.clear(); + _letid_expr_map->clear(); CounterExampleMap.clear(); ComputeFormulaMap.clear(); StatInfoSet.clear(); @@ -2065,15 +2065,15 @@ namespace BEEV { NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); AlreadyPrintedSet.clear(); - SimplifyMap.clear(); - SimplifyNegMap.clear(); + SimplifyMap->clear(); + SimplifyNegMap->clear(); SolverMap.clear(); AlwaysTrueFormMap.clear(); _arrayread_ite.clear(); _arrayread_symbol.clear(); _introduced_symbols.clear(); TransformMap.clear(); - _letid_expr_map.clear(); + _letid_expr_map->clear(); CounterExampleMap.clear(); ComputeFormulaMap.clear(); StatInfoSet.clear(); diff --git a/AST/AST.h b/AST/AST.h index adcce5e..c46c960 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -1477,8 +1477,8 @@ namespace BEEV { void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); private: //memo table for simplifcation - ASTNodeMap SimplifyMap; - ASTNodeMap SimplifyNegMap; + ASTNodeMap *SimplifyMap; + ASTNodeMap *SimplifyNegMap; ASTNodeMap SolverMap; ASTNodeSet AlwaysTrueFormMap; ASTNodeMap MultInverseMap; @@ -1645,7 +1645,7 @@ namespace BEEV { // MAP: This map is from bound IDs that occur in LETs to // expression. The map is useful in checking replacing the IDs // with the corresponding expressions. - ASTNodeMap _letid_expr_map; + ASTNodeMap *_letid_expr_map; public: ASTNode ResolveID(const ASTNode& var); @@ -1823,6 +1823,7 @@ namespace BEEV { //functions for checking and updating simplifcation map bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg); void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg); + void ResetSimplifyMaps(); bool CheckAlwaysTrueFormMap(const ASTNode& key); void UpdateAlwaysTrueFormMap(const ASTNode& val); bool CheckMultInverseMap(const ASTNode& key, ASTNode& output); @@ -1857,8 +1858,6 @@ namespace BEEV { ASTFalse(CreateNode(FALSE)), ASTTrue(CreateNode(TRUE)), ASTUndefined(CreateNode(UNDEFINED)), - SimplifyMap(INITIAL_SIMPLIFY_MAP_SIZE), - SimplifyNegMap(INITIAL_SIMPLIFY_MAP_SIZE), SolverMap(INITIAL_SOLVER_MAP_SIZE), _arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE), _introduced_symbols(INITIAL_INTRODUCED_SYMBOLS_SIZE), @@ -1870,6 +1869,9 @@ namespace BEEV { start_abstracting = false; Begin_RemoveWrites = false; SimplifyWrites_InPlace_Flag = false; + SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); + SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); + _letid_expr_map = new ASTNodeMap(INITIAL_INTRODUCED_SYMBOLS_SIZE); }; //destructor diff --git a/parser/let-funcs.cpp b/parser/let-funcs.cpp index 1de1049..e352cb4 100644 --- a/parser/let-funcs.cpp +++ b/parser/let-funcs.cpp @@ -27,7 +27,7 @@ namespace BEEV { //3. otherwise add the pair to the _letid_expr table. void BeevMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) { ASTNodeMap::iterator it; - if(((it = _letid_expr_map.find(var)) != _letid_expr_map.end()) && + if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && it->second != ASTUndefined) { FatalError("LetExprMgr:The LET-var v has already been defined in this LET scope: v =", var); } @@ -36,13 +36,16 @@ namespace BEEV { FatalError("LetExprMgr:This var is already declared. cannot redeclare as a letvar: v =", var); } - _letid_expr_map[var] = letExpr; + (*_letid_expr_map)[var] = letExpr; } //this function looksup the "var to letexpr map" and returns the //corresponding letexpr. if there is no letexpr, then it simply //returns the var. ASTNode BeevMgr::ResolveID(const ASTNode& v) { + if (_letid_expr_map == NULL) + InitializeLetIDMap(); + if(v.GetKind() != SYMBOL) { return v; } @@ -52,7 +55,7 @@ namespace BEEV { } ASTNodeMap::iterator it; - if((it =_letid_expr_map.find(v)) != _letid_expr_map.end()) { + if((it =_letid_expr_map->find(v)) != _letid_expr_map->end()) { if(it->second == ASTUndefined) FatalError("Unresolved Identifier: ",v); else @@ -66,20 +69,35 @@ namespace BEEV { //declared variables also get stored in this map, but there value //is ASTUndefined. This is really a hack. I don't know how to get //rid of this hack. - _letid_expr_map[v] = ASTUndefined; + (*_letid_expr_map)[v] = ASTUndefined; return v; } // This function simply cleans up the LetID -> LetExpr Map. void BeevMgr::CleanupLetIDMap(void) { - ASTNodeMap::iterator it = _letid_expr_map.begin(); - ASTNodeMap::iterator itend = _letid_expr_map.end(); + + // ext/hash_map::clear() is very expensive on big empty lists. shortcut. + if (_letid_expr_map->size() ==0) + return; + + + ASTNodeMap::iterator it = _letid_expr_map->begin(); + ASTNodeMap::iterator itend = _letid_expr_map->end(); for(;it!=itend;it++) { if(it->second != ASTUndefined) { it->first.SetValueWidth(0); it->first.SetIndexWidth(0); } } - _letid_expr_map.clear(); + + // May contain lots of buckets, so reset. + delete _letid_expr_map; + _letid_expr_map = new ASTNodeMap(); + + } + + void BeevMgr::InitializeLetIDMap(void) + { + _letid_expr_map = new ASTNodeMap(); } }; diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index 68abb93..7725305 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -14,8 +14,8 @@ namespace BEEV { bool BeevMgr::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg) { ASTNodeMap::iterator it, itend; - it = pushNeg ? SimplifyNegMap.find(key) : SimplifyMap.find(key); - itend = pushNeg ? SimplifyNegMap.end() : SimplifyMap.end(); + it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key); + itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end(); if(it != itend) { output = it->second; @@ -23,7 +23,7 @@ namespace BEEV { return true; } - if(pushNeg && (it = SimplifyMap.find(key)) != SimplifyMap.end()) { + if(pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end()) { output = (ASTFalse == it->second) ? ASTTrue : @@ -37,9 +37,9 @@ namespace BEEV { void BeevMgr::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg) { if(pushNeg) - SimplifyNegMap[key] = value; + (*SimplifyNegMap)[key] = value; else - SimplifyMap[key] = value; + (*SimplifyMap)[key] = value; } bool BeevMgr::CheckSubstitutionMap(const ASTNode& key, ASTNode& output) { @@ -189,11 +189,9 @@ namespace BEEV { } ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) { - SimplifyMap.clear(); - SimplifyNegMap.clear(); + ResetSimplifyMaps(); ASTNode out = SimplifyFormula(b,pushNeg); - SimplifyMap.clear(); - SimplifyNegMap.clear(); + ResetSimplifyMaps(); return out; } @@ -1016,11 +1014,9 @@ namespace BEEV { } //end of flattenonelevel() ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b) { - SimplifyMap.clear(); - SimplifyNegMap.clear(); + ResetSimplifyMaps(); ASTNode out = SimplifyTerm(b); - SimplifyNegMap.clear(); - SimplifyMap.clear(); + ResetSimplifyMaps(); return out; } @@ -3133,4 +3129,19 @@ namespace BEEV { TermsAlreadySeenMap[term] = var; return false; } + +// in ext/hash_map, and tr/unordered_map, there is no provision to shrink down +// the number of buckets in a hash map. If the hash_map has previously held a +// lot of data, then it will have a lot of buckets. Slowing down iterators and +// clears() in particular. +void BeevMgr::ResetSimplifyMaps() +{ + delete SimplifyMap; + SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); + + delete SimplifyNegMap; + SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); +} + + };//end of namespace -- 2.47.3