Fiddle with the difficulty scorer to better estimate how hard the problem becomes.

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

diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
index 8d618438913d41208a36c0f9ee49b39f72df329d..aa38ba9ccc8eb914accac28aa06676c718ae5c75 100644 (file)
--- a/src/STPManager/DifficultyScore.h
+++ b/src/STPManager/DifficultyScore.h
@@ -43,6 +43,10 @@ private:
                  score += (15 * b.GetValueWidth() * b.GetValueWidth() );
                else if (isLikeDivision(k))
                  score += (20 * b.GetValueWidth() * b.GetValueWidth() );
+               else
+               {
+                       score = std::max(b.GetValueWidth(),1u) * (b.Degree());
+               }
 
                const ASTVec& c = b.GetChildren();
                ASTVec::const_iterator itC = c.begin();

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index da3137ea776ad58d50cd4ce1cf8b5f2e456a1e32..9c37d791a9b6ba6f97c083bad5afcf3f21397205 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -293,7 +293,7 @@ namespace BEEV {
 
     const bool arrayops = containsArrayOps(original_input);
     bool optimize_enabled = bm->UserFlags.optimize_flag;
-    if (final_difficulty_score > 2 *initial_difficulty_score  && !arrayops)
+    if (final_difficulty_score > 1.1 *initial_difficulty_score  && !arrayops)
     {
        // If the simplified problem is harder, than the
        // initial problem we revert back to the initial