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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index a4fe3b52cfe0f2da08dac57878eec3168681523e..81ada3293d736c2bdf04c5b265deaf84a4b4b215 100644 (file)
--- 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 a0b4be6d5b75d1b6bad7aed4bd9afd4528e2e954..fa1b50246c5d7c14f5cc1aa02b1ed60e52f7e5b9 100644 (file)
--- 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 579fa5048fb3177bfdd1fb13c39a05502d2b328b..3fa51ff2e2ee657f64417355bdda48d076a67e60 100644 (file)
--- 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);