From aa5ea13fec00c32eb149396c9b0bdbbeaf0b7ca8 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 8 Dec 2009 23:59:37 +0000
Subject: [PATCH] good options of CMS2 set

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@493 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/UsefulDefs.h   |  2 +-
 src/STPManager/STP.cpp |  5 ++++-
 src/to-sat/CallSAT.cpp | 10 +++++-----
 src/to-sat/ToSAT.cpp   | 44 +++++++++++++++++++++---------------------
 4 files changed, 32 insertions(+), 29 deletions(-)

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index e23c2ff..27e1399 100644
--- a/src/AST/UsefulDefs.h
+++ b/src/AST/UsefulDefs.h
@@ -46,7 +46,7 @@
 #define HASHMULTISET hash_multiset
 #define INITIAL_TABLE_SIZE 100
 #define CLAUSAL_ABSTRACTION_CUTOFF 0.5
-#define CLAUSAL_BUCKET_LIMIT 4
+#define CLAUSAL_BUCKET_LIMIT 3
 
 using namespace std;
 namespace BEEV {
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index a4fe3b5..bd0646a 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -24,17 +24,20 @@ namespace BEEV {
 #if defined CORE || defined CRYPTOMINISAT
     MINISAT::Solver NewSolver;
 #endif
+
 #if defined CRYPTOMINISAT2
     MINISAT::Solver NewSolver;
     if(bm->UserFlags.print_cnf_flag)
       {
 	NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
       }
-    NewSolver.dynamicRestarts = true;
+    NewSolver.dynamicRestarts = false;
 #endif
+
 #ifdef SIMP
     MINISAT::SimpSolver NewSolver;
 #endif
+
 #ifdef UNSOUND
     MINISAT::UnsoundSimpSolver NewSolver;
 #endif
diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index df12a90..c3e5989 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -58,11 +58,11 @@ namespace BEEV
     for(int count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
-	// if(CLAUSAL_BUCKET_LIMIT == count)
-	// 	  {
-	// 	    sat = toSATandSolve(SatSolver,*cl, false, true);
-	// 	  }
-	// 	else
+	if(CLAUSAL_BUCKET_LIMIT == count)
+	  {
+	    sat = toSATandSolve(SatSolver,*cl, false, true);
+	  }
+	else
 	  {
 	    sat = toSATandSolve(SatSolver,*cl);
 	  }
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 3fa51ff..bea5b81 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -136,30 +136,30 @@ namespace BEEV
 #endif
 
 #if defined CRYPTOMINISAT2
-	newSolver.set_gaussian_decision_until(500);
-	newSolver.performReplace = true;
-	newSolver.xorFinder = true;
+	newSolver.set_gaussian_decision_until(50);
+	newSolver.performReplace = false;
+	newSolver.xorFinder = false;
 #endif
 
-	//         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(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;
-- 
2.47.3