From aecaa07183745ada96cb85cfcfc9b0d69c4e21f1 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 10 Mar 2011 02:01:49 +0000 Subject: [PATCH] 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 --- src/STPManager/DifficultyScore.h | 4 ++++ src/STPManager/STP.cpp | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h index 8d61843..aa38ba9 100644 --- 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 da3137e..9c37d79 100644 --- 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 -- 2.47.3