From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 20 Dec 2011 02:10:40 +0000 (+0000)
Subject: Improvement. Remove unused parameter. Better hiding.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1189eb8b0787c8596799fec857febf5c24dc9e3d;p=francis%2Fstp.git

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 30ee0b8..a10294b 100644
--- 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 2de2881..ca2d372 100644
--- 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)