From b163d5ef9c5715607ee191f7fe53cc68c9ff7dad Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 23 Jan 2011 12:52:36 +0000
Subject: [PATCH] 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
---
 src/AST/UsefulDefs.h |  4 +---
 src/to-sat/ToSAT.cpp | 21 ++++++++++++++++-----
 src/to-sat/ToSAT.h   |  4 +++-
 3 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index 2d41e2f..2917022 100644
--- 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 42dc48e..07e1627 100644
--- 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 f5622a4..474e372 100644
--- 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()
-- 
2.47.3