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

diff --git a/AST/AST.cpp b/AST/AST.cpp
index f607c1eca986656d2dba599ac3b9268e4b92e85c..154935305b23112f92e8feeca30469c656a122d3 100644 (file)
--- 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 adcce5eae1aa88d7638e5e14a810e99a21cb9d81..c46c9602640472be98cfdf225f3d89a91656c712 100644 (file)
--- 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 1de104924a9e761cc8c43435559f06c76577bfba..e352cb47f636b6047ae1bf21f42077cdbec5a5a4 100644 (file)
--- a/parser/let-funcs.cpp
+++ b/parser/let-funcs.cpp
@@ -27,7 +27,7 @@ namespace BEEV {
   //3. otherwise add the <var,letExpr> 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 68abb935f3b490423322270ba8f87895bde898fa..7725305f2f817f63d7f0932e4b67294c71357152 100644 (file)
--- 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