From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 10 Mar 2011 05:12:44 +0000 (+0000)
Subject: Fiddle with the difficulty scorer.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=67e7cb9acc0b487d4cf8f649df7d4ef9c06ee4a3;p=francis%2Fstp.git

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 aa38ba9..a7e550f 100644
--- 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;