From 633ee7a17fe99790e5d9c9bec9bd0418555cb9ef Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 8 Dec 2009 22:32:26 +0000
Subject: [PATCH] completely got rid of abs-refine at boolean clausal level

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@490 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/STP.cpp |  2 +-
 src/to-sat/CallSAT.cpp |  4 ++++
 src/to-sat/ToSAT.cpp   | 48 +++++++++++++++++++++---------------------
 3 files changed, 29 insertions(+), 25 deletions(-)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index a4fe3b5..81ada32 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -30,7 +30,7 @@ namespace BEEV {
       {
 	NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
       }
-    NewSolver.dynamicRestarts = true;
+    NewSolver.dynamicRestarts = false;
 #endif
 #ifdef SIMP
     MINISAT::SimpSolver NewSolver;
diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index a0b4be6..fa1b502 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -25,6 +25,10 @@ namespace BEEV
           {
             cl_size = CLAUSAL_BUCKET_LIMIT;
           }
+	else
+	  {
+	    cl_size = CLAUSAL_BUCKET_LIMIT-1;
+	  }
 
         //If no clauses of size cl_size have been seen, then create a
         //bucket for that size
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 579fa50..3fa51ff 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -134,31 +134,32 @@ namespace BEEV
 #else
         newSolver.addClause(satSolverClause);
 #endif
-        if(enable_clausal_abstraction && 
-	   count++ >= input_clauselist_size*CLAUSAL_ABSTRACTION_CUTOFF)
-          {
-            //Arbitrary adding only 60% of the clauses in the hopes of
-            //terminating early 
-            //      cout << "Percentage clauses added: " 
-            //           << percentage << endl;
-            bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
-            bm->GetRunTimes()->start(RunTimes::Solving);
 
 #if defined CRYPTOMINISAT2
-	    newSolver.set_gaussian_decision_until(300);
-	    newSolver.performReplace = true;
-	    newSolver.xorFinder = true;
+	newSolver.set_gaussian_decision_until(500);
+	newSolver.performReplace = true;
+	newSolver.xorFinder = true;
 #endif
-	    newSolver.solve();
-            bm->GetRunTimes()->stop(RunTimes::Solving);
-            if(!newSolver.okay())
-              {
-                return false;         
-              }
-            count = 0;
-            flag  = 1;
-            bm->GetRunTimes()->start(RunTimes::SendingToSAT);
-          }
+
+	//         if(enable_clausal_abstraction && 
+	// 	   count++ >= input_clauselist_size*CLAUSAL_ABSTRACTION_CUTOFF)
+	//           {
+	//             //Arbitrary adding only x% of the clauses in the hopes of
+	//             //terminating early 
+	//             //      cout << "Percentage clauses added: " 
+	//             //           << percentage << endl;
+	//             bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
+	//             bm->GetRunTimes()->start(RunTimes::Solving);
+	// 	    newSolver.solve();
+	//             bm->GetRunTimes()->stop(RunTimes::Solving);
+	//             if(!newSolver.okay())
+	//               {
+	//                 return false;         
+	//               }
+	//             count = 0;
+	//             flag  = 1;
+	//             bm->GetRunTimes()->start(RunTimes::SendingToSAT);
+	//           }
         if (newSolver.okay())
           {
             continue;
@@ -172,8 +173,7 @@ namespace BEEV
       } // End of For-loop adding the clauses 
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
-    bm->GetRunTimes()->start(RunTimes::Solving);
-    
+    bm->GetRunTimes()->start(RunTimes::Solving);    
     newSolver.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
     bm->PrintStats(newSolver);
-- 
2.47.3