From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 22 Feb 2011 11:34:18 +0000 (+0000)
Subject: Improvement. Match the difficulty score better to the number of AIG nodes created.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a57c634557cdf6d9df76d9b57082fd993caa8c3f;p=francis%2Fstp.git

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
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 4e78b55..4640ba5 100644
--- 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;
 	}
 };