From 91d18d93ebc3e5fb6d1b9799792c1c0a03b703db Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 3 Nov 2009 00:34:22 +0000
Subject: [PATCH] Added funcion in CallSAT.cpp to bucketize the clauselist

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@373 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/AST.h          |  5 +++++
 src/AST/UsefulDefs.h   |  1 +
 src/to-sat/CallSAT.cpp | 31 +++++++++++++++++++++++++++++++
 src/to-sat/ToCNF.cpp   |  2 +-
 src/to-sat/ToCNF.h     |  5 +++--
 5 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 19d48eb..0cfc439 100644
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -79,6 +79,11 @@ namespace BEEV
   
   // Datatype for Clauselists
   typedef vector<ClausePtr> ClauseList;
+
+  //Datatype for ClauseLists
+  typedef MAP<
+    int,
+    ClauseList *> ClauseBuckets;
   
   // Function to dump contents of ASTNodeMap
   ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index 8b42a9a..716553c 100644
--- a/src/AST/UsefulDefs.h
+++ b/src/AST/UsefulDefs.h
@@ -40,6 +40,7 @@
 #include <hash_map>
 #endif
 
+#define MAP          map
 #define HASHMAP      hash_map
 #define HASHSET      hash_set
 #define HASHMULTISET hash_multiset
diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 90246af..a196237 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -11,6 +11,36 @@
 
 namespace BEEV
 {
+
+  static ClauseBuckets * SortClauseList_IntoBuckets(ClauseList * cl)
+  {
+    ClauseBuckets * cb = new ClauseBuckets();
+    
+    //Sort the clauses, and bucketize by the size of the clauses
+    for(ClauseList::iterator it = cl->begin(), itend = cl->end(); 
+	it!=itend; it++)
+      {
+	ClausePtr cptr = *it;
+	int cl_size = cptr->size();
+	
+	//If no clauses of size cl_size have been seen, then create a
+	//bucket for that size
+	if(cb->find(cl_size) == cb->end())
+	  {
+	    ClauseList * cllist = new ClauseList();
+	    cllist->push_back(cptr);
+	    (*cb)[cl_size] = cllist;
+	  }
+	else
+	  {
+	    ClauseList * cllist = (*cb)[cl_size];
+	    cllist->push_back(cptr);
+	  }
+      }
+    
+    return cb;
+  } //End of SortClauseList_IntoBuckets()
+
   //Call the SAT solver, and check the result before returning. This
   //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or
   //SOLVER_UNDECIDED
@@ -25,6 +55,7 @@ namespace BEEV
 
     CNFMgr* cm = new CNFMgr(bm);
     ClauseList* cl = cm->convertToCNF(BBFormula);
+    ClauseBuckets * cb = SortClauseList_IntoBuckets(cl);
     bool sat = toSATandSolve(SatSolver, *cl);
     cm->DELETE(cl);
     delete cm;
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 907e8e0..f46bb62 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Mike Katelman
  *
  * BEGIN DATE: November, 2005
  *
diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index bc707b5..f50e90e 100644
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -24,7 +24,8 @@ namespace BEEV
     //########################################
     // data types
 
-    // for the meaning of control bits, see "utilities for contol bits".
+    // for the meaning of control bits, see "utilities for contol
+    // bits".
     typedef struct
     {
       int control;
@@ -55,7 +56,7 @@ namespace BEEV
     STPMgr *bm;
     ASTNodeToCNFInfoMap info;
     ASTNodeToASTNodePtrMap store;
-
+      
     //########################################
     //########################################
     // utility predicates
-- 
2.47.3