From da2c6178d4798070cf93e1efef5bfb26ec500c2f Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 22 Feb 2011 11:44:12 +0000
Subject: [PATCH] Refactor. Overcome a temporary static fetish. Now better.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1159 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/DifficultyScore.cpp    | 5 -----
 src/STPManager/DifficultyScore.h      | 6 +++---
 src/STPManager/STP.cpp                | 5 +++--
 src/simplifier/EstablishIntervals.cpp | 8 --------
 src/simplifier/EstablishIntervals.h   | 8 +++++---
 5 files changed, 11 insertions(+), 21 deletions(-)
 delete mode 100644 src/STPManager/DifficultyScore.cpp
 delete mode 100644 src/simplifier/EstablishIntervals.cpp

diff --git a/src/STPManager/DifficultyScore.cpp b/src/STPManager/DifficultyScore.cpp
deleted file mode 100644
index bafb4d4..0000000
--- a/src/STPManager/DifficultyScore.cpp
+++ /dev/null
@@ -1,5 +0,0 @@
-#include "DifficultyScore.h"
-namespace BEEV
-{
-  map<int, int> DifficultyScore::cache;
-}
diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
index 4640ba5..8d61843 100644
--- a/src/STPManager/DifficultyScore.h
+++ b/src/STPManager/DifficultyScore.h
@@ -13,14 +13,14 @@ struct DifficultyScore
 {
 private:
          // maps from nodeNumber to the previously calculated difficulty score..
-        static map<int, int> cache;
+        map<int, int> cache;
 
 	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, ASTNodeSet& visited)
+	int visit(const ASTNode& b, ASTNodeSet& visited)
 	{
 		if (b.isAtom())
 		  return 0;
@@ -56,7 +56,7 @@ private:
 	}
 
 public:
-	static int score(const ASTNode& top)
+	int score(const ASTNode& top)
 	{
 	        if (cache.find(top.GetNodeNum()) != cache.end())
 	          return cache.find(top.GetNodeNum())->second;
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index cb45371..5c32d9b 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -91,7 +91,8 @@ namespace BEEV {
 
     ASTNode simplified_solved_InputToSAT = inputToSAT;
 
-    long initial_difficulty_score = DifficultyScore::score(original_input);
+    DifficultyScore difficulty;
+    long initial_difficulty_score = difficulty.score(original_input);
 
     // A heap object so I can easily control its lifetime.
     BVSolver* bvSolver = new BVSolver(bm,simp);
@@ -257,7 +258,7 @@ namespace BEEV {
     bm->Begin_RemoveWrites = false;
 
 
-    long final_difficulty_score = DifficultyScore::score(simplified_solved_InputToSAT);
+    long final_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
     if (bm->UserFlags.stats_flag)
     {
     	cerr << "Initial Difficulty Score:" << initial_difficulty_score <<endl;
diff --git a/src/simplifier/EstablishIntervals.cpp b/src/simplifier/EstablishIntervals.cpp
deleted file mode 100644
index eafde83..0000000
--- a/src/simplifier/EstablishIntervals.cpp
+++ /dev/null
@@ -1,8 +0,0 @@
-#include "EstablishIntervals.h"
-namespace BEEV
-{
-
-  vector<EstablishIntervals::IntervalType * > EstablishIntervals::toDeleteLater;
-  vector<CBV> EstablishIntervals::likeAutoPtr;
-
-};
diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index dff603d..b08cdb4 100644
--- a/src/simplifier/EstablishIntervals.h
+++ b/src/simplifier/EstablishIntervals.h
@@ -15,6 +15,8 @@ namespace BEEV
 
   class EstablishIntervals
   {
+  private:
+
   public:
     struct IntervalType
     {
@@ -32,8 +34,8 @@ namespace BEEV
       }
     };
 
-    static vector<IntervalType * > toDeleteLater;
-    static vector<CBV> likeAutoPtr;
+    vector<EstablishIntervals::IntervalType * > toDeleteLater;
+    vector<CBV> likeAutoPtr;
 
 private:
 
@@ -44,7 +46,7 @@ private:
       return it;
     }
 
-    static IntervalType * createInterval(CBV min, CBV max)
+    IntervalType * createInterval(CBV min, CBV max)
     {
       IntervalType *it = new IntervalType(min,max);
       toDeleteLater.push_back(it);
-- 
2.47.3