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

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index e23c2fff270160df40c3282410ac0a37bb6709e4..27e1399b0aacf94ac32d69902ee81e5282b78542 100644 (file)
--- 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 a4fe3b52cfe0f2da08dac57878eec3168681523e..bd0646abe34472bdf0b26da0573512ca86052047 100644 (file)
--- 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 df12a908526c76ebf3db90ee833745e821d49035..c3e59892b5a29581a0815d06681534a6762f50e6 100644 (file)
--- 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 3fa51ff2e2ee657f64417355bdda48d076a67e60..bea5b81c639c1e45ff4045d6a303d9a4015f6c91 100644 (file)
--- 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;