From 59d45ca9988fba0401b816384a410b7621b92897 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 5 Feb 2011 01:34:36 +0000
Subject: [PATCH] Speedup. When performing constant bit propagation, there is
 now a slow & a fast worklist. The cheap propagators in the slow worklist are
 called first.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1119 e59a4935-1847-0410-ae03-e826735625c1
---
 .../constantBitP/ConstantBitPropagation.cpp   |  2 +-
 src/simplifier/constantBitP/Dependencies.h    | 14 +++++-
 src/simplifier/constantBitP/WorkList.h        | 46 +++++++++++++++----
 3 files changed, 51 insertions(+), 11 deletions(-)

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 94070a4..b8e867e 100644
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -464,7 +464,7 @@ namespace simplifier
 
           if (debug_cBitProp_messages)
             {
-              cerr << "working on" << n.GetNodeNum() << endl;
+              cerr << "[" << workList->size() << "]working on" << n.GetNodeNum() << endl;
             }
 
           // get a copy of the current fixing from the cache.
diff --git a/src/simplifier/constantBitP/Dependencies.h b/src/simplifier/constantBitP/Dependencies.h
index b8c8184..62ab772 100644
--- a/src/simplifier/constantBitP/Dependencies.h
+++ b/src/simplifier/constantBitP/Dependencies.h
@@ -14,8 +14,7 @@ namespace simplifier
     {
     private:
 
-      typedef hash_map<BEEV::ASTNode, set<BEEV::ASTNode>*,
-          BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual>
+      typedef hash_map<BEEV::ASTNode, set<BEEV::ASTNode>*, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual>
           NodeToDependentNodeMap;
       NodeToDependentNodeMap dependents;
 
@@ -122,6 +121,17 @@ namespace simplifier
         const set<ASTNode> *s = getDependents(lower);
         return s->count(higher) > 0;
       }
+
+      void
+      getAllVariables(ASTVec& v)
+      {
+        for (NodeToDependentNodeMap::const_iterator it = dependents.begin(); it != dependents. end(); it++)
+          {
+            if (it->first.GetKind() == SYMBOL)
+              v.push_back(it->first);
+          }
+      }
+
     };
 
   }
diff --git a/src/simplifier/constantBitP/WorkList.h b/src/simplifier/constantBitP/WorkList.h
index df957fe..6df1f60 100644
--- a/src/simplifier/constantBitP/WorkList.h
+++ b/src/simplifier/constantBitP/WorkList.h
@@ -14,7 +14,10 @@ namespace simplifier
 
     private:
 
-      set<BEEV::ASTNode> workList; // Nodes to work on.
+      // select nodes from the cheap_worklist first.
+      set<BEEV::ASTNode> cheap_workList; // Nodes to work on.
+      set<BEEV::ASTNode> expensive_workList; // Nodes to work on.
+
       WorkList(const WorkList&); // Shouldn't needed to copy or assign.
       WorkList&
       operator=(const WorkList&);
@@ -52,6 +55,11 @@ namespace simplifier
         initWorkList(top);
       }
 
+      int size()
+      {
+        return cheap_workList.size() + expensive_workList.size();
+      }
+
       void
       initWorkList(const ASTNode&n)
       {
@@ -67,34 +75,56 @@ namespace simplifier
           return;
 
         //cerr << "WorkList Inserting:" << n.GetNodeNum() << endl;
-        workList.insert(n);
+        if (n.GetKind() == BVMULT || n.GetKind() == BVPLUS || n.GetKind() == BVDIV)
+          expensive_workList.insert(n);
+        else
+          cheap_workList.insert(n);
+
       }
 
       BEEV::ASTNode
       pop()
       {
         assert(!isEmpty());
-        ASTNode ret = *workList.begin();
-        workList.erase(workList.begin());
-        return ret;
+        if (cheap_workList.size() > 0)
+          {
+            ASTNode ret = *cheap_workList.begin();
+            cheap_workList.erase(cheap_workList.begin());
+            return ret;
+          }
+        else
+          {
+            assert (expensive_workList.size() > 0);
+            ASTNode ret = *expensive_workList.begin();
+            expensive_workList.erase(expensive_workList.begin());
+            return ret;
+          }
       }
 
       bool
       isEmpty()
       {
-        return workList.empty();
+        return cheap_workList.empty() && expensive_workList.empty();
       }
 
       void
       print()
       {
         cerr << "+Worklist" << endl;
-        set<BEEV::ASTNode>::const_iterator it = workList.begin();
-        while (it != workList.end())
+        set<BEEV::ASTNode>::const_iterator it = cheap_workList.begin();
+        while (it != cheap_workList.end())
           {
             cerr << *it << " ";
             it++;
           }
+
+        it = expensive_workList.begin();
+        while (it != expensive_workList.end())
+          {
+            cerr << *it << " ";
+            it++;
+          }
+
         cerr << "-Worklist" << endl;
 
       }
-- 
2.47.3