minor

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index a3472ebaff80b5f62b298e41699f9f5327eb452e..0f1eb00f659cb2036dfcede6581f72fabf854f4a 100644 (file)
--- 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 f26884b0f298215fd42d110e3c50476662eb8adb..5055d1eafdeba986e419de2bd65de7d9a62e7884 100644 (file)
--- 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)