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

diff --git a/src/STPManager/DifficultyScore.cpp b/src/STPManager/DifficultyScore.cpp
deleted file mode 100644 (file)
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 4640ba5e3c7c57fdfb86f7bc234aff9e8f7ec35a..8d618438913d41208a36c0f9ee49b39f72df329d 100644 (file)
--- 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 cb453718823517dccaff68724cbd4f7c481ce252..5c32d9be71e7a70bf31e43f41559cee79269ff65 100644 (file)
--- 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 (file)
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 dff603d88181291638fcc2c8d08ed29bfc385bc6..b08cdb449b2c60fd79fde5c1fcbf956733baea78 100644 (file)
--- 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);