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 7051eddd25036c5540bb424871a9dc890e983631..628b806de699a1b5188dd45aeda303937e2f54d8 100644 (file)
--- 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 6c2a160d993fe3887e4db241990a2da2843e3cc0..e5ee70f5c0ffb7cb87592530fb9e248afa02f3f8 100644 (file)
--- 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 e53c8793d5630dc10357dabaef2a0c05ce6277c3..c7b4688d26c923eaf36d97a8083b35d2aa1fc2ef 100644 (file)
--- 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);