Improvement. Match the difficulty score better to the number of AIG nodes created.

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

diff --git a/src/STPManager/DifficultyScore.cpp b/src/STPManager/DifficultyScore.cpp
new file mode 100644 (file)
index 0000000..bafb4d4
--- /dev/null
+++ b/src/STPManager/DifficultyScore.cpp
@@ -0,0 +1,5 @@
+#include "DifficultyScore.h"
+namespace BEEV
+{
+  map<int, int> DifficultyScore::cache;
+}

diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
index 4e78b55a905c1a2cad8b36db3ebd42d9a0732f4e..4640ba5e3c7c57fdfb86f7bc234aff9e8f7ec35a 100644 (file)
--- a/src/STPManager/DifficultyScore.h
+++ b/src/STPManager/DifficultyScore.h
@@ -11,42 +11,59 @@ namespace BEEV
 {
 struct DifficultyScore
 {
-       typedef map<ASTNode,int> Cache;
+private:
+         // maps from nodeNumber to the previously calculated difficulty score..
+        static map<int, int> cache;
 
-       static bool isLikeMultiplication(const Kind& k)
+       static bool isLikeDivision(const Kind& k)
        {
                return k == BVMULT || k == BVDIV || k == BVMOD || k == SBVDIV || k == SBVREM || k == SBVMOD;
        }
 
-       static int visit(const ASTNode& b, Cache& cache)
+       static int visit(const ASTNode& b, ASTNodeSet& visited)
        {
-               Cache::iterator it;
+               if (b.isAtom())
+                 return 0;
 
-               if ((it = cache.find(b)) != cache.end())
+               ASTNodeSet::iterator it;
+
+               if ((it = visited.find(b)) != visited.end())
                        return 0; // already included.
 
+               visited.insert(b);
+
+               const Kind k =b.GetKind();
+
+               // These scores are approximately the number of AIG nodes created when
+               // no input values are known.
                int score= 0;
-               if (isLikeMultiplication(b.GetKind()))
-                       score += (b.GetValueWidth() * b.GetValueWidth() );
-               else
-                       score += b.GetValueWidth();
+               if (k == BVMULT)
+                   score += (5 * b.GetValueWidth() * b.GetValueWidth() );
+               else if (k == BVMOD)
+                 score += (15 * b.GetValueWidth() * b.GetValueWidth() );
+               else if (isLikeDivision(k))
+                 score += (20 * b.GetValueWidth() * b.GetValueWidth() );
 
                const ASTVec& c = b.GetChildren();
                ASTVec::const_iterator itC = c.begin();
                ASTVec::const_iterator itendC = c.end();
                for (; itC != itendC; itC++)
                {
-                       score += visit(*itC, cache);
+                       score += visit(*itC, visited);
                }
 
-               cache[b] = score;
                return score;
        }
 
+public:
        static int score(const ASTNode& top)
        {
-               Cache cache;
-               int result = visit(top,cache);
+               if (cache.find(top.GetNodeNum()) != cache.end())
+                 return cache.find(top.GetNodeNum())->second;
+
+               ASTNodeSet visited;
+               int result = visit(top,visited);
+               cache.insert(make_pair(top.GetNodeNum(), result));
                return result;
        }
 };