Cleaning up some bugs in CryptoMS

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

diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h
index ec515fca93933baa385314d524763d3ed5b20c3f..42d55d7ce42f86a0ac9238348b03ee0fae3a7719 100644 (file)
--- a/src/sat/cryptominisat2/Clause.h
+++ b/src/sat/cryptominisat2/Clause.h
@@ -343,15 +343,12 @@ class WatchedBin {
         Lit impliedLit;
 };
 
-#pragma pack(push)
-#pragma pack(1)
 class Watched {
     public:
         Watched(ClauseOffset _clause, Lit _blockedLit) : clause(_clause), blockedLit(_blockedLit) {};
         ClauseOffset clause;
         Lit blockedLit;
 };
-#pragma pack(pop)
 
 }; //NAMESPACE MINISAT
 

diff --git a/src/sat/cryptominisat2/ClauseAllocator.cpp b/src/sat/cryptominisat2/ClauseAllocator.cpp
index f0d7fa66d61c0239e3d79da59f86c23f7fefbde7..99bfaed636c3e80beca336a80402dadf938c5e99 100644 (file)
--- a/src/sat/cryptominisat2/ClauseAllocator.cpp
+++ b/src/sat/cryptominisat2/ClauseAllocator.cpp
@@ -33,6 +33,8 @@ namespace MINISAT
 {
 using namespace MINISAT;
 
+//#define DEBUG_CLAUSEALLOCATOR
+
 ClauseAllocator::ClauseAllocator() :
     clausePoolBin(sizeof(Clause) + 2*sizeof(Lit))
 {}
@@ -107,7 +109,10 @@ void* ClauseAllocator::allocEnough(const uint32_t size)
     }
 
     if (!found) {
-        //std::cout << "c New list in ClauseAllocator" << std::endl;
+        #ifdef DEBUG_CLAUSEALLOCATOR
+        std::cout << "c New list in ClauseAllocator" << std::endl;
+        #endif //DEBUG_CLAUSEALLOCATOR
+        
         uint32_t nextSize; //number of BYTES to allocate
         if (maxSizes.size() != 0)
             nextSize = maxSizes[maxSizes.size()-1]*3*sizeof(uint32_t);
@@ -124,11 +129,13 @@ void* ClauseAllocator::allocEnough(const uint32_t size)
         currentlyUsedSize.push(0);
         which = dataStarts.size()-1;
     }
-    /*std::cout
+    #ifdef DEBUG_CLAUSEALLOCATOR
+    std::cout
     << "selected list = " << which
     << " size = " << sizes[which]
     << " maxsize = " << maxSizes[which]
-    << " diff = " << maxSizes[which] - sizes[which] << std::endl;*/
+    << " diff = " << maxSizes[which] - sizes[which] << std::endl;
+    #endif //DEBUG_CLAUSEALLOCATOR
 
     assert(which != std::numeric_limits<uint32_t>::max());
     Clause* pointer = (Clause*)(dataStarts[which] + sizes[which]);
@@ -202,7 +209,9 @@ void ClauseAllocator::consolidate(Solver* solver)
         sumAlloc += sizes[i];
     }
 
-    //std::cout << "c ratio:" << (double)sum/(double)sumAlloc << std::endl;
+    #ifdef DEBUG_CLAUSEALLOCATOR
+    std::cout << "c ratio:" << (double)sum/(double)sumAlloc << std::endl;
+    #endif //DEBUG_CLAUSEALLOCATOR
     
     if ((double)sum/(double)sumAlloc > 0.7 /*&& sum > 10000000*/) {
         if (solver->verbosity >= 2) {

diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp
index 58baec55d765778785a789d62a930b48617dba35..65e01e9da821e15b8fa5d23e164640d28ea0d18b 100644 (file)
--- a/src/sat/cryptominisat2/ClauseCleaner.cpp
+++ b/src/sat/cryptominisat2/ClauseCleaner.cpp
@@ -141,6 +141,7 @@ inline const bool ClauseCleaner::cleanClause(Clause*& cc)
     }
     c.shrink(i-j);
 
+    assert(c.size() != 1);
     if (i != j) {
         c.setStrenghtened();
         if (c.size() == 2) {
@@ -149,12 +150,6 @@ inline const bool ClauseCleaner::cleanClause(Clause*& cc)
             solver.clauseAllocator.clauseFree(&c);
             cc = c2;
             solver.attachClause(*c2);
-        /*} else if (c.size() == 3) {
-            solver.detachModifiedClause(origLit1, origLit2, origSize, &c);
-            Clause *c2 = Clause_new(c);
-            clauseFree(&c);
-            cc = c2;
-            solver.attachClause(*c2);*/
         } else {
             if (c.learnt())
                 solver.learnts_literals -= i-j;

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 1afa7cf0dc3d9a34f9e7e4ed31e88a38d019b32b..d3c353f95d01cf669175393591f24929db4802b9 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -159,15 +159,10 @@ Solver::Solver() :
 
 Solver::~Solver()
 {
-    for (uint32_t i = 0; i != learnts.size(); i++) clauseAllocator.clauseFree(learnts[i]);
-    for (uint32_t i = 0; i != clauses.size(); i++) clauseAllocator.clauseFree(clauses[i]);
-    for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseAllocator.clauseFree(binaryClauses[i]);
-    for (uint32_t i = 0; i != xorclauses.size(); i++) clauseAllocator.clauseFree(xorclauses[i]);
     #ifdef USE_GAUSS
     clearGaussMatrixes();
     delete matrixFinder;
     #endif
-    //for (uint32_t i = 0; i != freeLater.size(); i++) clauseAllocator.clauseFree(freeLater[i]);
     
     delete varReplacer;
     delete clauseCleaner;

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index d2b3f0c9ba158354ce42ec79a9b00a69ba0a787a..27126c22207947748d87642a2191b09f847d0c39 100644 (file)
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -834,7 +834,8 @@ void Subsumer::addBackToSolver()
     #ifdef HYPER_DEBUG2
     uint32_t binaryLearntAdded = 0;
     #endif
-    
+
+    assert(solver.clauses.size() == 0);
     for (uint32_t i = 0; i < clauses.size(); i++) {
         if (clauses[i].clause != NULL) {
             assert(clauses[i].clause->size() > 1);
@@ -1058,7 +1059,7 @@ const bool Subsumer::subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNo
 {
     #ifdef VERBOSE_DEBUG
     std::cout << "subsWNonExistBins called with lit "; lit.print();
-    std::cout << " startUp: " << startUp << std::endl;
+    std::cout << std::endl;
     #endif //VERBOSE_DEBUG
     toVisit.clear();
     solver.newDecisionLevel();
@@ -1085,14 +1086,17 @@ const bool Subsumer::subsWNonExistBins(const Lit& lit, OnlyNonLearntBins* onlyNo
             #endif //VERBOSE_DEBUG
             subsume0(ps2, calcAbstraction(ps2));
             subsume1Partial(ps2);
+            if (!solver.ok) goto end;
         }
     } else {
         subsume0BIN(~lit, toVisitAll);
     }
+
+    end:
     for (uint32_t i = 0; i < toVisit.size(); i++)
         toVisitAll[toVisit[i].toInt()] = false;
 
-    return true;
+    return solver.ok;
 }
 
 void Subsumer::clearAll()
@@ -1127,11 +1131,9 @@ const bool Subsumer::simplifyBySubsumption(const bool alsoLearnt)
     
     //if (solver.xorclauses.size() < 30000 && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/10) addAllXorAsNorm();
 
-    solver.testAllClauseAttach();
     if (solver.performReplace && !solver.varReplacer->performReplace(true))
         return false;
     fillCannotEliminate();
-    solver.testAllClauseAttach();
 
     uint32_t expected_size;
     if (!alsoLearnt)
@@ -1145,9 +1147,14 @@ const bool Subsumer::simplifyBySubsumption(const bool alsoLearnt)
     if (clauses.size() < 200000) fullSubsume = true;
     else fullSubsume = false;
     if (alsoLearnt) fullSubsume = true;
-    
+
+    solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts);
+    addFromSolver<true>(solver.learnts, alsoLearnt);
     solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
     addFromSolver<true>(solver.clauses, alsoLearnt);
+
+    //It is IMPERATIVE to add binaryClauses last. The non-binary clauses can
+    //move to binaryClauses during cleaning!!!!
     solver.clauseCleaner->removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses);
     addFromSolver<true>(solver.binaryClauses, alsoLearnt);
     

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 37b8c68597501831dc3573b0cb74be20ee9a130b..92f1ee215d2557892dc55d040f1589a3022ff972 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 819a9f4377ef8c9ed0f4b493517a84c853b30a98
+GIT revision: e540792aa3a01ec047b005b6351247fa87ae6eb6