From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 3 Nov 2009 02:09:28 +0000 (+0000)
Subject: bucketization of clauses added, and tested
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=51b29ee9857d6554e03ce5686505897306a70fb1;p=francis%2Fstp.git

bucketization of clauses added, and tested

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 0cfc439..ed0887a 100644
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -80,10 +80,20 @@ namespace BEEV
   // Datatype for Clauselists
   typedef vector<ClausePtr> ClauseList;
 
+  //Needed for defining the MAP below
+  struct ltint
+  {
+    bool operator()(int s1, int s2) const
+    {
+      return s1 < s2;
+    }
+  };
+
   //Datatype for ClauseLists
   typedef MAP<
     int,
-    ClauseList *> ClauseBuckets;
+    ClauseList *,
+    ltint> ClauseBuckets;
   
   // Function to dump contents of ASTNodeMap
   ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index a196237..ef1a4f1 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -8,11 +8,12 @@
  ********************************************************************/
 
 #include "ToSAT.h"
+#define MAX_BUCKET_LIMIT 3
 
 namespace BEEV
 {
-
-  static ClauseBuckets * SortClauseList_IntoBuckets(ClauseList * cl)
+  //Bucketize clauses into buckets of size 1,2,...MAX_BUCKET_LIMIT
+  static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl)
   {
     ClauseBuckets * cb = new ClauseBuckets();
     
@@ -22,7 +23,11 @@ namespace BEEV
       {
 	ClausePtr cptr = *it;
 	int cl_size = cptr->size();
-	
+	if(cl_size >= MAX_BUCKET_LIMIT)
+	  {
+	    cl_size = MAX_BUCKET_LIMIT;
+	  }
+
 	//If no clauses of size cl_size have been seen, then create a
 	//bucket for that size
 	if(cb->find(cl_size) == cb->end())
@@ -41,6 +46,25 @@ namespace BEEV
     return cb;
   } //End of SortClauseList_IntoBuckets()
 
+  bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
+				       ClauseBuckets * cb)
+  {
+    ClauseBuckets::iterator it = cb->begin();
+    ClauseBuckets::iterator itend = cb->end();
+    
+    bool sat = false;
+    for(;it!=itend;it++)
+      {
+	ClauseList *cl = (*it).second;
+	sat = toSATandSolve(SatSolver,*cl);
+	if(!sat)
+	  {
+	    return sat;
+	  }
+      }
+    return sat;
+  }
+
   //Call the SAT solver, and check the result before returning. This
   //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or
   //SOLVER_UNDECIDED
@@ -55,8 +79,9 @@ namespace BEEV
 
     CNFMgr* cm = new CNFMgr(bm);
     ClauseList* cl = cm->convertToCNF(BBFormula);
-    ClauseBuckets * cb = SortClauseList_IntoBuckets(cl);
-    bool sat = toSATandSolve(SatSolver, *cl);
+    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
+    //bool sat = toSATandSolve(SatSolver, *cl);
+    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
     cm->DELETE(cl);
     delete cm;
     return sat;
diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index a424b5a..b74d8de 100644
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -102,6 +102,11 @@ namespace BEEV
     bool CallSAT(MINISAT::Solver& SatSolver, 
                  const ASTNode& modified_input,
                  const ASTNode& original_input);
+
+    //Iteratively goes through the Clause Buckets, and calls
+    //toSATandSolve()
+    bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
+				  ClauseBuckets * cb);
     
     // Converts the clause to SAT and calls SAT solver
     bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll);