Improvement. Remove unused parameter. Better hiding.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 30ee0b875d50ab171cf735bd53a7027dd14e38aa..a10294bc59d3c75b2f1663e8354b8ccdbf9df7c5 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -74,7 +74,7 @@ namespace BEEV {
     
        SOLVER_RETURN_TYPE result;
     result = TopLevelSTPAux(NewSolver,
-                             original_input, original_input);
+                             original_input);
 
     delete newS;
 
@@ -194,14 +194,14 @@ namespace BEEV {
   //if returned 0 then input is INVALID if returned 1 then input is
   //VALID if returned 2 then UNDECIDED
   SOLVER_RETURN_TYPE
-  STP::TopLevelSTPAux(SATSolver& NewSolver, const ASTNode& modified_input, const ASTNode& original_input)
+  STP::TopLevelSTPAux(SATSolver& NewSolver, const ASTNode& original_input)
   {
 
-    ASTNode inputToSAT = modified_input;
+    ASTNode inputToSAT = original_input;
     ASTNode orig_input = original_input;
-    bm->ASTNodeStats("input asserts and query: ", inputToSAT);
-
     ASTNode simplified_solved_InputToSAT = inputToSAT;
+
+    bm->ASTNodeStats("input asserts and query: ", inputToSAT);
     const bool arrayops = containsArrayOps(original_input);
 
     DifficultyScore difficulty;

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 2de28813d813fc2a8e35a16e0b4710654c446a47..ca2d372ffcd2e75200468d07b978173be9e92e74 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -19,14 +19,12 @@
 #include "../parser/LetMgr.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
 
-/********************************************************************
- *  This file gives the class description of the STP class          *
- ********************************************************************/
-
 namespace BEEV
 {
   class STP {
-  private:
+
+    ArrayTransformer * arrayTransformer;
+
           ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver);
 
           // A copy of all the state we need to restore to a prior expression.
@@ -37,6 +35,15 @@ namespace BEEV
             ArrayTransformer::ArrType backup_arrayToIndexToRead; // array-indices already removed.
           };
 
+          // Accepts query and returns the answer. if query is valid,
+          // returns VALID, else returns INVALID. Automatically constructs
+          // counterexample for invalid queries, and prints them upon
+          // request.
+          SOLVER_RETURN_TYPE TopLevelSTPAux(SATSolver& NewSolver,
+                                            const ASTNode& modified_input
+                                            );
+
+
   public:
           // calls sizeReducing and the bitblasting simplification.
           ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score);
@@ -49,7 +56,6 @@ namespace BEEV
      ****************************************************************/
     STPMgr * bm;
     Simplifier * simp;
-    ArrayTransformer * arrayTransformer;
     ToSAT * tosat;
     AbsRefine_CounterExample * Ctr_Example;
 
@@ -111,18 +117,12 @@ namespace BEEV
     SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts, 
                                    const ASTNode& query);
 
-    // Accepts query and returns the answer. if query is valid,
-    // returns VALID, else returns INVALID. Automatically constructs
-    // counterexample for invalid queries, and prints them upon
-    // request.
-    SOLVER_RETURN_TYPE TopLevelSTPAux(SATSolver& NewSolver,
-                                     const ASTNode& modified_input,
-                                     const ASTNode& original_input);
-
+#if 0
     SOLVER_RETURN_TYPE
     UserGuided_AbsRefine(SATSolver& SatSolver,
                         const ASTNode& original_input);
-         
+#endif
+
     void ClearAllTables(void)
     {
                if (simp != NULL)