Fiddle with the difficulty scorer.

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

diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
index aa38ba9ccc8eb914accac28aa06676c718ae5c75..a7e550f448e6cf6bad6b53b8026b2578c50ced20 100644 (file)
--- a/src/STPManager/DifficultyScore.h
+++ b/src/STPManager/DifficultyScore.h
@@ -38,11 +38,18 @@ private:
                // no input values are known.
                int score= 0;
                if (k == BVMULT)
-                   score += (5 * b.GetValueWidth() * b.GetValueWidth() );
+                   score = (5 * b.GetValueWidth() * b.GetValueWidth() );
                else if (k == BVMOD)
-                 score += (15 * b.GetValueWidth() * b.GetValueWidth() );
+                 score = (15 * b.GetValueWidth() * b.GetValueWidth() );
                else if (isLikeDivision(k))
-                 score += (20 * b.GetValueWidth() * b.GetValueWidth() );
+                 score = (20 * b.GetValueWidth() * b.GetValueWidth() );
+               else if (k == BVCONCAT || k == BVEXTRACT || k == NOT)
+               {} // no harder.
+               else if (k == EQ || k == BVGE || k == BVGT|| k == BVSGE || k == BVSGT )
+               {
+                       // without getting the width of the child it'd always be 2.
+                       score = std::max(b[0].GetValueWidth(),1u) * (b.Degree());
+               }
                else
                {
                        score = std::max(b.GetValueWidth(),1u) * (b.Degree());
@@ -62,7 +69,7 @@ private:
 public:
        int score(const ASTNode& top)
        {
-               if (cache.find(top.GetNodeNum()) != cache.end())
+               if (cache.find(top.GetNodeNum()) != cache.end())
                  return cache.find(top.GetNodeNum())->second;
 
                ASTNodeSet visited;