From 4daec3033ea2f3e5ad93e4e72515d5e881e1f457 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 26 Sep 2009 01:32:37 +0000
Subject: [PATCH] minor

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@257 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/simplifier.cpp |  5 +++--
 src/to-sat/ToSAT.cpp          | 40 ++++++++++++++++++++++++++++-------
 2 files changed, 35 insertions(+), 10 deletions(-)

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index a3472eb..0f1eb00 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -310,9 +310,10 @@ ASTNode Flatten(const ASTNode& a)
 
   // The SimplifyMaps on entry to the topLevel functions may contain useful entries.
   // E.g. The BVSolver calls SimplifyTerm()
-  ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
+  ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, 
+					    bool pushNeg, ASTNodeMap* VarConstMap)
   {
-	runTimes.start(RunTimes::SimplifyTopLevel);
+    runTimes.start(RunTimes::SimplifyTopLevel);
     if (smtlib_parser_flag)
     BuildReferenceCountMap(b);
     ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index f26884b..5055d1e 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -990,7 +990,7 @@ namespace BEEV
 
 	if(optimize_flag) 
 	  {
-		runTimes.start(RunTimes::CreateSubstitutionMap);
+	    runTimes.start(RunTimes::CreateSubstitutionMap);
 	    simplified_solved_InputToSAT = 
 	      CreateSubstitutionMap(simplified_solved_InputToSAT);
 	    runTimes.stop(RunTimes::CreateSubstitutionMap);
@@ -1022,7 +1022,31 @@ namespace BEEV
       }
 
     TermsAlreadySeenMap.clear();
-
+    // do
+    //       {
+    //         inputToSAT = simplified_solved_InputToSAT;
+    
+    // 	if(optimize_flag) 
+    // 	  {
+    // 	    runTimes.start(RunTimes::CreateSubstitutionMap);
+    // 	    simplified_solved_InputToSAT = 
+    // 	      CreateSubstitutionMap(simplified_solved_InputToSAT);
+    // 	    runTimes.stop(RunTimes::CreateSubstitutionMap);
+    // 	    ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+    
+    // 	    simplified_solved_InputToSAT = 
+    // 	      SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+    // 	    ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+    // 	  }
+    
+    // 	if(wordlevel_solve_flag)
+    // 	  {
+    // 	    simplified_solved_InputToSAT = 
+    // 	      bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+    // 	    ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+    // 	  }
+    //       } while (inputToSAT != simplified_solved_InputToSAT);
+    
     if (start_abstracting)
       {
         ASTNodeStats("After abstraction: ", simplified_solved_InputToSAT);
@@ -1053,12 +1077,12 @@ namespace BEEV
         return res;
       }
 
-    res = SATBased_AllFiniteLoops_Refinement(newS, orig_input);
-    if (SOLVER_UNDECIDED != res)
-      {
-	CountersAndStats("print_func_stats");
-        return res;      
-      }
+    // res = SATBased_AllFiniteLoops_Refinement(newS, orig_input);
+    //     if (SOLVER_UNDECIDED != res)
+    //       {
+    // 	CountersAndStats("print_func_stats");
+    //         return res;      
+    //       }
 
     res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input);
     if (SOLVER_UNDECIDED != res)
-- 
2.47.3