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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 19d48ebc86842c48073481dda86f714d74da7446..0cfc439040505fbbb8c1c8036bf2dbff8cb3eb85 100644 (file)
--- 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 8b42a9a824d4b61800812be07d8fc4e5a29d89c4..716553c41d6f396bc6d9144a26b73d78e1de1f59 100644 (file)
--- 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 90246aff18822e530d03e12922ae68c91d7ef229..a196237abd48c9949a967ffc82db78716a6ba041 100644 (file)
--- 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 907e8e017f7b979b929bf9053daac42081350495..f46bb620a256ec82825571c6951739a91df902ef 100644 (file)
--- 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 bc707b53c795e4c1ee3634135ed473566089af16..f50e90e8352efce1158853afa5ccf459558f885c 100644 (file)
--- 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