Refactor. Move the clause bucket size so it can be adjusted at runtime.

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

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index 2d41e2f9130eee3e674db48587ea95ad5cf02cd5..29170220c7acda5bf36331986b563bea74b8dd3b 100644 (file)
--- a/src/AST/UsefulDefs.h
+++ b/src/AST/UsefulDefs.h
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -45,8 +45,6 @@
 #define HASHSET      hash_set
 #define HASHMULTISET hash_multiset
 #define INITIAL_TABLE_SIZE 100
-#define CLAUSAL_ABSTRACTION_CUTOFF 0.5
-#define CLAUSAL_BUCKET_LIMIT 3
 
 using namespace std;
 namespace BEEV {

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 42dc48eccd729432b257790fb3c31b7e9536b479..07e16277c6747a004b20c7dacebb8a1258b8e306 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -12,6 +12,7 @@
 #include <iostream>
 #include <fstream>
 #include "BBNodeManagerASTNode.h"
+#include "../STPManager/UserDefinedFlags.h"
 
 namespace BEEV
 {
@@ -94,7 +95,7 @@ namespace BEEV
                             bool add_xor_clauses,
                            bool enable_clausal_abstraction)
   {
-    CountersAndStats("SAT Solver", bm);
+         CountersAndStats("SAT Solver", bm);
     bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
     int input_clauselist_size = cll.size();
@@ -270,7 +271,7 @@ namespace BEEV
   } //end of toSATandSolve()
 
   //Bucketize clauses into buckets of size 1,2,...CLAUSAL_BUCKET_LIMIT
-  static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl)
+  ClauseBuckets * ToSAT::Sort_ClauseList_IntoBuckets(ClauseList * cl, int clause_bucket_size)
   {
     ClauseBuckets * cb = new ClauseBuckets();
     ClauseContainer* cc = cl->asList();
@@ -281,9 +282,9 @@ namespace BEEV
       {
         ClausePtr cptr = *it;
         int cl_size = cptr->size();
-        if(cl_size >= CLAUSAL_BUCKET_LIMIT)
+        if(cl_size >= clause_bucket_size)
           {
-            cl_size = CLAUSAL_BUCKET_LIMIT;
+            cl_size = clause_bucket_size;
           }
 
         //If no clauses of size cl_size have been seen, then create a
@@ -355,6 +356,16 @@ namespace BEEV
                file.close();
     }
 
+    //  I suspect that we can't use clause buckets with the simplifying solvers
+    // (simplifying minisat & Cryptominsat).
+    //  Because sometimes simplifying removes a variable that later clauses depend on.
+    //  But when I set the clause_bucket_size to 1 for the other solvers, errors down.
+    int clause_bucket_size;
+    if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER)
+         clause_bucket_size=3;
+    else
+         clause_bucket_size=3;
+
     // The CNFMgr is deleted inside the CallSAT_On_ClauseBuckets,
     // just before the final call to the SAT solver.
 
@@ -362,7 +373,7 @@ namespace BEEV
     ClauseList* cl = cm->convertToCNF(BBFormula);
     ClauseList* xorcl = cm->ReturnXorClauses();
 
-    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
+    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl,clause_bucket_size);
     cl->asList()->clear(); // clause buckets now point to the clauses.
     delete cl;
     bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb, cm);

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index f5622a42716aa5536e0220defd49004e7baec00f..474e372e0e5d70f806454effbcbbd6440dec0447 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -75,6 +75,9 @@ namespace BEEV
                       bool enable_clausal_abstraction=false);
 
 
+    ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl, int clause_bucket_size);
+
+
   public:
     /****************************************************************
      * Public Member Functions                                      *
@@ -86,7 +89,6 @@ namespace BEEV
     {
       CNFFileNameCounter = 0;
       benchFileNameCounter = 0;
-
     }
 
     // Bitblasts, CNF conversion and calls toSATandSolve()