Removing unused inputs to the ToSAT class.

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

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 80f92b3f230f36609662f1de587a9679b6316e26..35796be187ff1aeda197c42eea458a6957d2332a 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -993,8 +993,7 @@ namespace BEEV
                       const ASTNode& original_input)
   {
     bool sat = tosat->CallSAT(SatSolver,
-                              modified_input,
-                              original_input);
+                              modified_input);
     if (!sat)
       {
         //PrintOutput(true);

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index caae1856684360be897bd96c8d7353d5290f5b60..363a9cbaf33e654af0d8bab944dd4b457cf01176 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -158,7 +158,7 @@ VC vc_createValidityChecker(void) {
   BEEV::STPMgr * bm       = new BEEV::STPMgr();
   BEEV::Simplifier * simp  = new BEEV::Simplifier(bm);
   BEEV::BVSolver* bvsolver = new BEEV::BVSolver(bm, simp);
-  BEEV::ToSAT * tosat      = new BEEV::ToSAT(bm, simp);
+  BEEV::ToSAT * tosat      = new BEEV::ToSAT(bm);
   BEEV::ArrayTransformer * arrayTransformer = 
     new BEEV::ArrayTransformer(bm, simp);
   BEEV::AbsRefine_CounterExample * Ctr_Example = 

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8158a5f68b92a4052bae72d9fa58d3610dad7cb9..1122d0c61859fba12fec8e8ba48dc9152964d5be 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -56,7 +56,7 @@ int main(int argc, char ** argv) {
   Simplifier * simp  = new Simplifier(bm);
   BVSolver* bvsolver = new BVSolver(bm, simp);
   ArrayTransformer * arrayTransformer = new ArrayTransformer(bm, simp);
-  ToSAT * tosat      = new ToSAT(bm, simp);
+  ToSAT * tosat      = new ToSAT(bm);
   AbsRefine_CounterExample * Ctr_Example = 
     new AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat);      
   itimerval timeout; 

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index d5146d289d244f4d9f1dfa8b132791f4ae428aa4..794a8331b31a5ab495bb89d64350fb42d6b92e63 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -256,15 +256,14 @@ namespace BEEV
   //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or
   //SOLVER_UNDECIDED
   bool ToSAT::CallSAT(MINISAT::Solver& SatSolver,
-                      const ASTNode& modified_input,
-                      const ASTNode& original_input)
+                      const ASTNode& input)
   {
     bm->GetRunTimes()->start(RunTimes::BitBlasting);
 
 
     BitBlasterNew BB(bm);
     BBNodeSet set;
-    ASTNode BBFormula = BB.BBForm(modified_input,set);
+    ASTNode BBFormula = BB.BBForm(input,set);
     assert(set.size() == 0); // doesn't yet work.
 
     bm->ASTNodeStats("after bitblasting: ", BBFormula);
@@ -298,6 +297,7 @@ namespace BEEV
       }
 #endif
 
+
     cm->DELETE(cl);
     cm->DELETE(xorcl);
     delete cm;

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 844612914f273c334dcadaae7cd04eb656ec910d..dfc0667d17dcac9039bb456cf8cedfda4ffa716c 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -51,9 +51,6 @@ namespace BEEV
     // Ptr to STPManager
     STPMgr * bm;
 
-    // Ptr to Simplifier
-    Simplifier * simp;
-
 #if 0
     // Memo table to check the functioning of bitblaster and CNF
     // converter
@@ -105,9 +102,8 @@ namespace BEEV
      ****************************************************************/
     
     // Constructor
-    ToSAT(STPMgr * bm, Simplifier * s) :
-      bm(bm), 
-      simp(s)
+    ToSAT(STPMgr * bm) :
+      bm(bm)
 #if 0
       ,CheckBBandCNFMemo()
 #endif
@@ -119,8 +115,7 @@ namespace BEEV
 
     // Bitblasts, CNF conversion and calls toSATandSolve()
     bool CallSAT(MINISAT::Solver& SatSolver, 
-                 const ASTNode& modified_input,
-                 const ASTNode& original_input);
+                 const ASTNode& input);
 
     //print the STP solver output
     void PrintOutput(SOLVER_RETURN_TYPE ret);
@@ -138,12 +133,11 @@ namespace BEEV
 
     ~ToSAT()
     {
-      _ASTNode_to_SATVar_Map.clear();
+       ClearAllTables();
 #if 0
       RepLitMap.clear();
       CheckBBandCNFMemo.clear();
 #endif
-      _SATVar_to_AST_Vector.clear();
     }
   }; //end of class ToSAT
 }; //end of namespace