Speedup. When performing constant bit propagation, there is now a slow & a fast workl...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1119 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 94070a49998bc1bb8c7297d6d45cf332bbd43a16..b8e867e7b5af8da033969f9c54ccdca1975992a9 100644 (file)
--- 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 b8c8184396fb2de283b6b3e895fc7142978d91f7..62ab77257328719aa423e4fdfaf87dcf752623d4 100644 (file)
--- 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 df957fe21c3535c88bce552e3dd07887e8c84ed8..6df1f605ce12a7f701e7a67af18ae9276527a050 100644 (file)
--- 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;
 
       }