From: msoos Date: Thu, 15 Apr 2010 12:52:17 +0000 (+0000) Subject: Merge branch 'newcrypto' X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8e6268f8ab32aeb0d96b3cefd607e41f21c795af;p=francis%2Fstp.git Merge branch 'newcrypto' updated CMS2 so that segfault will no longer happen when UNSAT is found in the middle of a varreplacement. The clause database was left in an undefined state, which caused ~Solver to double-free some clauses no longer be create Conflicts: src/sat/cryptominisat2/PartHandler.cpp src/sat/cryptominisat2/Solver.cpp src/sat/cryptominisat2/Solver.h src/sat/cryptominisat2/Subsumer.cpp src/sat/cryptominisat2/VERSION src/sat/cryptominisat2/VarReplacer.cpp src/sat/cryptominisat2/mtl/Vec.h git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@678 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp index 8fb9771..dddc7ff 100644 --- a/src/sat/cryptominisat2/PartHandler.cpp +++ b/src/sat/cryptominisat2/PartHandler.cpp @@ -276,6 +276,7 @@ void PartHandler::addSavedState() solver.uncheckedEnqueue(Lit(var, savedState[var] == l_False)); assert(solver.assigns[var] == savedState[var]); savedState[var] = l_Undef; + solver.polarity[var] = (solver.assigns[var] == l_False); } } diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index b98ef36..a0f4f24 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -82,6 +82,8 @@ Solver::Solver() : , doPartHandler (true) , doHyperBinRes (true) , doBlockedClause (true) + , doVarElim (true) + , doSubsume1 (true) , failedVarSearch (true) , libraryUsage (true) , greedyUnbound (false) @@ -140,7 +142,6 @@ Solver::~Solver() for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseFree(binaryClauses[i]); for (uint32_t i = 0; i != xorclauses.size(); i++) free(xorclauses[i]); clearGaussMatrixes(); - for (uint32_t i = 0; i != freeLater.size(); i++) free(freeLater[i]); delete varReplacer; delete conglomerate; delete clauseCleaner; @@ -350,6 +351,15 @@ Clause* Solver::addClauseInt(T& ps, uint group) template Clause* Solver::addClauseInt(Clause& ps, const uint group); template Clause* Solver::addClauseInt(vec& ps, const uint group); +template +bool Solver::addClause(T& ps, const uint group, char* group_name) +{ + assert(decisionLevel() == 0); + if (ps.size() > (0x01UL << 18)) { + std::cout << "Too long clause!" << std::endl; + exit(-1); + } + template bool Solver::addClause(T& ps, const uint group, char* group_name) { @@ -1021,6 +1031,7 @@ Clause* Solver::propagate(const bool update) confl = k->clause; //goto EndPropagate; } + } } } if (confl != NULL) @@ -1325,6 +1336,14 @@ void Solver::dumpSortedLearnts(const char* file, const uint32_t maxSize) } } + fprintf(outfile, "c clauses from binaryClauses\n"); + if (maxSize >= 2) { + for (uint i = 0; i != binaryClauses.size(); i++) { + if (binaryClauses[i]->learnt()) + binaryClauses[i]->plainPrint(outfile); + } + } + fprintf(outfile, "c clauses from learnts\n"); std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt()); for (int i = learnts.size()-1; i >= 0 ; i--) { @@ -1407,6 +1426,8 @@ lbool Solver::simplify() lastNbBin = nbBin; becameBinary = 0; } + if (performReplace && varReplacer->performReplace() == false) + return l_False; // Remove satisfied clauses: clauseCleaner->removeAndCleanAll(); @@ -1945,11 +1966,11 @@ lbool Solver::solve(const vec& assumps) assumps.copyTo(assumptions); int nof_conflicts = restart_first; - int nof_conflicts_fullrestart = (double)restart_first * (double)FULLRESTART_MULTIPLIER; + int nof_conflicts_fullrestart = (double)restart_first * (double)FULLRESTART_MULTIPLIER + conflicts; //nof_conflicts_fullrestart = -1; uint lastFullRestart = starts; lbool status = l_Undef; - uint64_t nextSimplify = 30000; + uint64_t nextSimplify = 30000 + conflicts; if (nClauses() * learntsize_factor < nbclausesbeforereduce) { if (nClauses() * learntsize_factor < nbclausesbeforereduce/2) @@ -1998,9 +2019,6 @@ lbool Solver::solve(const vec& assumps) for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; gauss_matrixes.clear(); - for (uint i = 0; i < freeLater.size(); i++) - free(freeLater[i]); - freeLater.clear(); if (status == l_True) { if (greedyUnbound) { @@ -2075,6 +2093,7 @@ lbool Solver::solve(const vec& assumps) cancelUntil(0); if (doPartHandler && status != l_False) partHandler->readdRemovedClauses(); + restartTypeChooser->reset(); return status; } diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 3cab2f9..a39ea99 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -138,6 +138,8 @@ public: bool doPartHandler; // Should try to subsume clauses bool doHyperBinRes; // Should try carry out hyper-binary resolution bool doBlockedClause; // Should try to remove blocked clauses + bool doVarElim; // Perform variable elimination + bool doSubsume1; // Perform clause contraction through resolution bool failedVarSearch; // Should search for failed vars and doulbly propagated vars bool libraryUsage; // Set true if not used as a library bool sateliteUsed; // whether satielite was used on CNF before calling @@ -213,7 +215,6 @@ protected: vec binaryClauses; // Binary clauses are regularly moved here vec xorclauses; // List of problem xor-clauses. Will be freed vec learnts; // List of learnt clauses. - vec freeLater; // List of xorclauses to free at the end (due to matrixes, they cannot be freed immediately) vec activity; // A heuristic measurement of the activity of a variable. double var_inc; // Amount to bump next variable with. vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). @@ -300,8 +301,8 @@ protected: void detachClause (const Clause& c); // Detach a clause to watcher lists. void detachModifiedClause(const Lit lit1, const Lit lit2, const uint size, const Clause* address); void detachModifiedClause(const Var var1, const Var var2, const uint origSize, const XorClause* address); - void removeClause(Clause& c); // Detach and free a clause. - void removeClause(XorClause& c); // Detach and free a clause. + template + void removeClause(T& c); // Detach and free a clause. bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true @@ -563,16 +564,20 @@ inline void Solver::reverse_binary_clause(Clause& c) const { } }*/ -inline void Solver::removeClause(Clause& c) + } + if (final) + c[0] = c[0].unsign() ^ !assigns[c[0].var()].getBool(); + + c.setUpdateNeeded(false); + } +}*/ + +template +inline void Solver::removeClause(T& c) { detachClause(c); clauseFree(&c); } -inline void Solver::removeClause(XorClause& c) -{ - detachClause(c); - freeLater.push(&c); -} //================================================================================================= diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp index 0295fd8..29b0419 100644 --- a/src/sat/cryptominisat2/Subsumer.cpp +++ b/src/sat/cryptominisat2/Subsumer.cpp @@ -825,10 +825,14 @@ const bool Subsumer::simplifyBySubsumption() else numMaxSubsume0 = 2000000 * (1+numCalls/2); - if (clauses.size() > 3500000) - numMaxSubsume1 = 100000 * (1+numCalls/2); - else - numMaxSubsume1 = 500000 * (1+numCalls/2); + if (solver.doSubsume1) { + if (clauses.size() > 3500000) + numMaxSubsume1 = 100000 * (1+numCalls/2); + else + numMaxSubsume1 = 500000 * (1+numCalls/2); + } else { + numMaxSubsume1 = 0; + } if (clauses.size() > 3500000) numMaxElim = (uint32_t)((double)solver.order_heap.size() / 5.0 * (0.8+(double)(numCalls)/4.0)); @@ -913,6 +917,11 @@ const bool Subsumer::simplifyBySubsumption() #ifdef BIT_MORE_VERBOSITY std::cout << "c time until the end of almost_all/smaller: " << cpuTime() - myTime << std::endl; + #endif + + if (!solver.doVarElim) break; + + #ifdef BIT_MORE_VERBOSITY printf("c VARIABLE ELIMINIATION\n"); std::cout << "c toucheds list size:" << touched_list.size() << std::endl; #endif diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 9f06d3b..aaf632c 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: e2b5fe1abd1777f753c775026d905a10006ce79b +GIT revision: 7aa24081ccebef355347957349c09b0c00fe5512 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 6a23e22..9e36ca3 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -151,7 +151,7 @@ const bool VarReplacer::replace_set(vec& cs, const bool isAttached) { XorClause **a = cs.getData(); XorClause **r = a; - for (XorClause **end = a + cs.size(); r != end;) { + for (XorClause **end = a + cs.size(); r != end; r++) { XorClause& c = **r; bool changed = false; @@ -169,11 +169,14 @@ const bool VarReplacer::replace_set(vec& cs, const bool isAttached) } if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) { - if (solver.ok == false) return false; - solver.freeLater.push(&c); - r++; + if (solver.ok == false) { + for(;r != end; r++) + free(*r); + cs.shrink(r-a); + return false; + } } else { - *a++ = *r++; + *a++ = *r; } } cs.shrink(r-a); @@ -240,7 +243,7 @@ const bool VarReplacer::replace_set(vec& cs) { Clause **a = cs.getData(); Clause **r = a; - for (Clause **end = a + cs.size(); r != end; ) { + for (Clause **end = a + cs.size(); r != end; r++) { Clause& c = **r; bool changed = false; Lit origLit1 = c[0]; @@ -255,11 +258,14 @@ const bool VarReplacer::replace_set(vec& cs) } if (changed && handleUpdatedClause(c, origLit1, origLit2)) { - if (solver.ok == false) return false; - clauseFree(&c); - r++; + if (solver.ok == false) { + for(;r != end; r++) + free(*r); + cs.shrink(r-a); + return false; + } } else { - *a++ = *r++; + *a++ = *r; } } cs.shrink(r-a); diff --git a/src/sat/cryptominisat2/mtl/Vec.h b/src/sat/cryptominisat2/mtl/Vec.h index 1c6c1ae..560f0a1 100644 --- a/src/sat/cryptominisat2/mtl/Vec.h +++ b/src/sat/cryptominisat2/mtl/Vec.h @@ -88,7 +88,7 @@ public: void capacity (uint32_t size) { grow(size); } // Stack interface: - void reserve(uint32_t res) { if (cap < res) {cap = res; data = (T*)realloc(data, cap * sizeof(T));}} + void reserve(uint32_t res) { grow(res);} void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; } void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; } void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }