From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 3 Feb 2011 04:00:54 +0000 (+0000)
Subject: Improvement. Reduce the scope of the bvsolver.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9bc22b611d903a1fcb18eeb9bdce5d3f735f50f2;p=francis%2Fstp.git

Improvement. Reduce the scope of the bvsolver.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1118 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 7051edd..628b806 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -90,6 +90,9 @@ namespace BEEV {
 
     long initial_difficulty_score = DifficultyScore::score(original_input);
 
+    // A heap object so I can easily control its lifetime.
+    BVSolver* bvSolver = new BVSolver(bm,simp);
+
     //round of substitution, solving, and simplification. ensures that
     //DAG is minimized as much as possibly, and ideally should
     //garuntee that all liketerms in BVPLUSes have been combined.
@@ -138,7 +141,7 @@ namespace BEEV {
         if(bm->UserFlags.wordlevel_solve_flag && bm->UserFlags.optimize_flag)
           {
             simplified_solved_InputToSAT = 
-              bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+              bvSolver->TopLevelBVSolve(simplified_solved_InputToSAT);
             bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
           }
 
@@ -203,7 +206,7 @@ namespace BEEV {
         if(bm->UserFlags.wordlevel_solve_flag && bm->UserFlags.optimize_flag)
           {
             simplified_solved_InputToSAT = 
-              bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+              bvSolver->TopLevelBVSolve(simplified_solved_InputToSAT);
             bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
           }
     } while (inputToSAT != simplified_solved_InputToSAT);
@@ -268,9 +271,8 @@ namespace BEEV {
 
 
     // Deleting it clears out all the buckets associated with hashmaps etc. too.
-    delete bvsolver;
-    bvsolver = new BVSolver(bm,simp);
-    //auto_ptr<BVSolver> bvCleaner(bvsolver);
+    delete bvSolver;
+    bvSolver = NULL;
 
     if(bm->UserFlags.stats_flag)
     	simp->printCacheStatus();
diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 6c2a160..e5ee70f 100644
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -34,7 +34,6 @@ namespace BEEV
      ****************************************************************/
     STPMgr * bm;
     Simplifier * simp;
-    BVSolver * bvsolver;
     ArrayTransformer * arrayTransformer;
     ToSAT * tosat;
     AbsRefine_CounterExample * Ctr_Example;
@@ -43,6 +42,21 @@ namespace BEEV
      * Constructor and Destructor                                   *
      ****************************************************************/
 
+    //Constructor
+    STP(STPMgr* b,
+        Simplifier* s,
+        ArrayTransformer * a,
+        ToSAT * ts,
+        AbsRefine_CounterExample * ce)
+    {
+      bm   = b;
+      simp = s;
+      tosat = ts;
+      arrayTransformer = a;
+      Ctr_Example = ce;
+    }// End of constructor
+
+
     //Constructor
     STP(STPMgr* b,
         Simplifier* s,
@@ -54,7 +68,7 @@ namespace BEEV
       bm   = b;
       simp = s;
       tosat = ts;
-      bvsolver = bsolv;
+      delete bsolv; // Remove from the constructor later..
       arrayTransformer = a;
       Ctr_Example = ce;
     }// End of constructor
@@ -62,7 +76,6 @@ namespace BEEV
     ~STP()
     {
       ClearAllTables();
-      delete bvsolver;
       delete Ctr_Example;
       delete arrayTransformer;
       delete tosat;
@@ -94,7 +107,6 @@ namespace BEEV
     void ClearAllTables(void)
     {
       simp->ClearAllTables();
-      bvsolver->ClearAllTables();
       arrayTransformer->ClearAllTables();
       tosat->ClearAllTables();
       Ctr_Example->ClearAllTables();
diff --git a/src/main/main.cpp b/src/main/main.cpp
index e53c879..c7b4688 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -97,8 +97,6 @@ int main(int argc, char ** argv) {
   Simplifier * simp  = new Simplifier(bm);
   auto_ptr<Simplifier> simpCleaner(simp);
 
-  BVSolver* bvsolver = new BVSolver(bm, simp);
-
   ArrayTransformer * arrayTransformer = new ArrayTransformer(bm, simp);
   auto_ptr<ArrayTransformer> atClearner(arrayTransformer);
 
@@ -114,7 +112,6 @@ int main(int argc, char ** argv) {
   GlobalSTP         = 
     new STP(bm, 
             simp, 
-            bvsolver, 
             arrayTransformer, 
             tosat, 
             Ctr_Example);