From 0daef886b5269c246f64a67180897a3939eff8e9 Mon Sep 17 00:00:00 2001 From: msoos Date: Sun, 4 Jul 2010 18:17:55 +0000 Subject: [PATCH] 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 --- src/sat/cryptominisat2/Clause.h | 3 --- src/sat/cryptominisat2/ClauseAllocator.cpp | 17 +++++++++++++---- src/sat/cryptominisat2/ClauseCleaner.cpp | 7 +------ src/sat/cryptominisat2/Solver.cpp | 5 ----- src/sat/cryptominisat2/Subsumer.cpp | 19 +++++++++++++------ src/sat/cryptominisat2/VERSION | 2 +- 6 files changed, 28 insertions(+), 25 deletions(-) diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index ec515fc..42d55d7 100644 --- 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 f0d7fa6..99bfaed 100644 --- 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::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 58baec5..65e01e9 100644 --- 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 1afa7cf..d3c353f 100644 --- 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 d2b3f0c..27126c2 100644 --- 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(solver.learnts, alsoLearnt); solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses); addFromSolver(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(solver.binaryClauses, alsoLearnt); diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 37b8c68..92f1ee2 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: 819a9f4377ef8c9ed0f4b493517a84c853b30a98 +GIT revision: e540792aa3a01ec047b005b6351247fa87ae6eb6 -- 2.47.3