cryptominisat2 is now the official SAT solver of STP

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

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index 060764a105cd4fab52c88fd7cd7338214cb2d7d9..27e1399b0aacf94ac32d69902ee81e5282b78542 100644 (file)
--- a/src/AST/UsefulDefs.h
+++ b/src/AST/UsefulDefs.h
@@ -46,7 +46,7 @@
 #define HASHMULTISET hash_multiset
 #define INITIAL_TABLE_SIZE 100
 #define CLAUSAL_ABSTRACTION_CUTOFF 0.5
-#define MAX_BUCKET_LIMIT 3
+#define CLAUSAL_BUCKET_LIMIT 3
 
 using namespace std;
 namespace BEEV {

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index f5572257b65064d83a8e1e8df43cd7a0f02705bd..d3c7cf5f2787f9f478c4fbc7d33b453306570f9a 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -729,15 +729,19 @@ namespace BEEV
     // worth doing explicitly (e.g., a = b, a = ~b, etc.)
     else
       {
-        //         return _bm->CreateSimpForm(OR, 
-        //                                    _bm->CreateSimpForm(AND, a, b), 
-        //                                    _bm->CreateSimpForm(AND, b, c), 
-        //                                    _bm->CreateSimpForm(AND, a, c));
-        return _bm->CreateSimpForm(AND, 
-                                   _bm->CreateSimpForm(OR, a, b), 
-                                   _bm->CreateSimpForm(OR, b, c), 
-                                   _bm->CreateSimpForm(OR, a, c));
-      
+//     return _bm->CreateSimpForm(OR, 
+//                                _bm->CreateSimpForm(AND, a, b), 
+//                                _bm->CreateSimpForm(AND, b, c), 
+//                                _bm->CreateSimpForm(AND, a, c));
+        return 
+         _bm->CreateSimpForm(AND, 
+                             _bm->CreateSimpForm(OR, a, b),
+                             //_bm->CreateSimpForm(XOR,a,b)),
+                             _bm->CreateSimpForm(OR, b, c),
+                             //_bm->CreateSimpForm(XOR,b,c)),
+                             _bm->CreateSimpForm(OR, a, c)
+                             //_bm->CreateSimpForm(XOR,a,c)
+                             );      
       }
   }
 
@@ -745,31 +749,12 @@ namespace BEEV
                           const ASTNode& yi,
                           const ASTNode& cin)
   {
-    // For some unexplained reason, XORs are faster than converting
-    // them to cluases at this point
     ASTNode S0 = _bm->CreateSimpForm(XOR,
-                                     _bm->CreateSimpForm(XOR, xi, yi),
+                                     //_bm->CreateSimpForm(XOR, xi, yi),
+                                    xi,
+                                    yi,
                                      cin);
     return S0;
-    // ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin);
-    //     ASTNode S2 = _bm->CreateSimpForm(OR,
-    //                               _bm->CreateSimpForm(NOT,xi),
-    //                               _bm->CreateSimpForm(NOT,yi),
-    //                               cin);
-    //     ASTNode S3 = _bm->CreateSimpForm(OR,
-    //                               _bm->CreateSimpForm(NOT,xi),
-    //                               yi,
-    //                               _bm->CreateSimpForm(NOT,cin));
-    //     ASTNode S4 = _bm->CreateSimpForm(OR,
-    //                               xi,
-    //                               _bm->CreateSimpForm(NOT,yi),
-    //                               _bm->CreateSimpForm(NOT,cin));
-    //     ASTVec S;
-    //     S.push_back(S1);
-    //     S.push_back(S2);
-    //     S.push_back(S3);
-    //     S.push_back(S4);
-    //     return _bm->CreateSimpForm(AND,S);
   }
 
   // Bitwise complement

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 2df4a41e6a2f6b187cf9a8143079c9b1ec02f37b..984b8f4aaac51aea4f33110aec803d497de6800a 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -10,7 +10,7 @@
 
 namespace BEEV
 {
-  //Bucketize clauses into buckets of size 1,2,...MAX_BUCKET_LIMIT
+  //Bucketize clauses into buckets of size 1,2,...CLAUSAL_BUCKET_LIMIT
   static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl)
   {
     ClauseBuckets * cb = new ClauseBuckets();
@@ -21,9 +21,9 @@ namespace BEEV
       {
         ClausePtr cptr = *it;
         int cl_size = cptr->size();
-        if(cl_size >= MAX_BUCKET_LIMIT)
+        if(cl_size >= CLAUSAL_BUCKET_LIMIT)
           {
-            cl_size = MAX_BUCKET_LIMIT;
+            cl_size = CLAUSAL_BUCKET_LIMIT;
           }
 
         //If no clauses of size cl_size have been seen, then create a
@@ -51,10 +51,17 @@ namespace BEEV
     ClauseBuckets::iterator itend = cb->end();
     
     bool sat = false;
-    for(;it!=itend;it++)
+    for(int count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
-        sat = toSATandSolve(SatSolver,*cl);
+//     if(CLAUSAL_BUCKET_LIMIT == count)
+//       {
+//         sat = toSATandSolve(SatSolver,*cl, false, true);
+//       }
+//     else
+         {
+           sat = toSATandSolve(SatSolver,*cl);
+         }
         if(!sat)
           {
             return sat;

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index 977de28e8a94e671b72240a3876db25da6ce88ab..5b1ae409683da1b1d118688ee6ea100fa941b304 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -38,7 +38,7 @@ namespace BEEV
           case AND:
             return CreateSimpAndOr(1, children);
             break;
-          case OR:
+          case OR:                 
             return CreateSimpAndOr(0, children);
             break;
           case NAND:
@@ -148,10 +148,6 @@ namespace BEEV
       }
   }
 
-  // I don't think this is even called, since it called
-  // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no ill
-  // effects.  Calls seem to go to the version that takes a vector of
-  // children.
   ASTNode STPMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2)
   {
     ASTVec children;

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 8cd957f451a6edf1d18d8c3775e0ddddd3806bfd..2994a5f9d0268965d8835ada2399c14fc57db661 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -66,7 +66,9 @@ namespace BEEV
    * unsat. else continue.
    */
   bool ToSAT::toSATandSolve(MINISAT::Solver& newSolver,
-                            ClauseList& cll, bool add_xor_clauses)
+                            ClauseList& cll, 
+                           bool add_xor_clauses,
+                           bool enable_clausal_abstraction)
   {
     CountersAndStats("SAT Solver", bm);
     bm->GetRunTimes()->start(RunTimes::SendingToSAT);
@@ -88,7 +90,7 @@ namespace BEEV
 
     if(bm->UserFlags.print_cnf_flag)
       {
-       #define DEBUG_LIB
+       //newSolver.cnfDump = true;
       }
 #ifdef CRYPTOMINISAT
     newSolver.startClauseAdding();
@@ -134,8 +136,8 @@ namespace BEEV
 #else
         newSolver.addClause(satSolverClause);
 #endif
-        float percentage=CLAUSAL_ABSTRACTION_CUTOFF;
-        if(count++ >= input_clauselist_size*percentage)
+        if(enable_clausal_abstraction && 
+          count++ >= input_clauselist_size*CLAUSAL_ABSTRACTION_CUTOFF)
           {
             //Arbitrary adding only 60% of the clauses in the hopes of
             //terminating early 
@@ -146,8 +148,8 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
            newSolver.set_gaussian_decision_until(100);
-           newSolver.performReplace = false;
-           newSolver.xorFinder = false;
+           //newSolver.performReplace = true;
+           //newSolver.xorFinder = true;
 #endif
            newSolver.solve();
             bm->GetRunTimes()->stop(RunTimes::Solving);

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index b83377b6a4584267d90ce3f296259cd27de106fb..af535904cc977463a0432ed27bf0f2cb4d4b7477 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -110,7 +110,9 @@ namespace BEEV
     
     // Converts the clause to SAT and calls SAT solver
     bool toSATandSolve(MINISAT::Solver& S,
-                       ClauseList& cll, bool add_xor_clauses=false);
+                       ClauseList& cll, 
+                      bool add_xor_clauses=false,
+                      bool enable_clausal_abstraction=false);
     
     //print the STP solver output
     void PrintOutput(SOLVER_RETURN_TYPE ret);