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 0cfc439040505fbbb8c1c8036bf2dbff8cb3eb85..ed0887a6578b8c875d31ba9c708dd6d5a1898a0d 100644 (file)
--- 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 a196237abd48c9949a967ffc82db78716a6ba041..ef1a4f143eeda2152465fc9b798481b6d5b06f5a 100644 (file)
--- 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 a424b5a058d00f8ff3460a13a02cdcb403a7c139..b74d8de0382a7fec5c4d1d3000d131bcfa49c818 100644 (file)
--- 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);