summaryrefslogtreecommitdiff
path: root/src/prop/cryptominisat/Solver/ClauseCleaner.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cryptominisat/Solver/ClauseCleaner.cpp')
-rw-r--r--src/prop/cryptominisat/Solver/ClauseCleaner.cpp261
1 files changed, 261 insertions, 0 deletions
diff --git a/src/prop/cryptominisat/Solver/ClauseCleaner.cpp b/src/prop/cryptominisat/Solver/ClauseCleaner.cpp
new file mode 100644
index 000000000..47dd675f4
--- /dev/null
+++ b/src/prop/cryptominisat/Solver/ClauseCleaner.cpp
@@ -0,0 +1,261 @@
+/***************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+****************************************************************************/
+
+#include "ClauseCleaner.h"
+#include "VarReplacer.h"
+#include "DataSync.h"
+
+//#define DEBUG_CLEAN
+//#define VERBOSE_DEBUG
+
+using namespace CMSat;
+
+ClauseCleaner::ClauseCleaner(Solver& _solver) :
+ solver(_solver)
+{
+ for (uint32_t i = 0; i < 6; i++) {
+ lastNumUnitarySat[i] = solver.get_unitary_learnts_num();
+ lastNumUnitaryClean[i] = solver.get_unitary_learnts_num();
+ }
+}
+
+bool ClauseCleaner::satisfied(const Watched& watched, Lit lit)
+{
+ assert(watched.isBinary());
+ if (solver.value(lit) == l_True) return true;
+ if (solver.value(watched.getOtherLit()) == l_True) return true;
+ return false;
+}
+
+void ClauseCleaner::removeSatisfiedBins(const uint32_t limit)
+{
+ #ifdef DEBUG_CLEAN
+ assert(solver.decisionLevel() == 0);
+ #endif
+
+ if (lastNumUnitarySat[binaryClauses] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ uint32_t numRemovedHalfNonLearnt = 0;
+ uint32_t numRemovedHalfLearnt = 0;
+ uint32_t wsLit = 0;
+ for (vec<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ vec<Watched>& ws = *it;
+
+ vec<Watched>::iterator i = ws.getData();
+ vec<Watched>::iterator j = i;
+ for (vec<Watched>::iterator end2 = ws.getDataEnd(); i != end2; i++) {
+ if (i->isBinary() && satisfied(*i, lit)) {
+ if (i->getLearnt()) numRemovedHalfLearnt++;
+ else {
+ numRemovedHalfNonLearnt++;
+ }
+ } else {
+ *j++ = *i;
+ }
+ }
+ ws.shrink_(i - j);
+ }
+
+ //std::cout << "removedHalfLeart: " << numRemovedHalfLearnt << std::endl;
+ //std::cout << "removedHalfNonLeart: " << numRemovedHalfNonLearnt << std::endl;
+ assert(numRemovedHalfLearnt % 2 == 0);
+ assert(numRemovedHalfNonLearnt % 2 == 0);
+ solver.clauses_literals -= numRemovedHalfNonLearnt;
+ solver.learnts_literals -= numRemovedHalfLearnt;
+ solver.numBins -= (numRemovedHalfLearnt + numRemovedHalfNonLearnt)/2;
+
+ lastNumUnitarySat[binaryClauses] = solver.get_unitary_learnts_num();
+}
+
+void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type, const uint32_t limit)
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Cleaning " << (type==binaryClauses ? "binaryClauses" : "normal clauses" ) << std::endl;
+ #endif //VERBOSE_DEBUG
+
+ Clause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end; s++) {
+ if (s+1 != end) __builtin_prefetch(*(s+1));
+
+ if (cleanClause(*s)) {
+ solver.clauseAllocator.clauseFree(*s);
+ } else {
+ *ss++ = *s;
+ }
+ }
+ cs.shrink(s-ss);
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "cleanClauses(Clause) useful ?? Removed: " << s-ss << endl;
+ #endif
+}
+
+inline bool ClauseCleaner::cleanClause(Clause*& cc)
+{
+ Clause& c = *cc;
+
+ Lit origLit1 = c[0];
+ Lit origLit2 = c[1];
+ uint32_t origSize = c.size();
+ Lit origLit3 = (origSize == 3) ? c[2] : lit_Undef;
+
+ Lit *i, *j, *end;
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ lbool val = solver.value(*i);
+ if (val == l_Undef) {
+ *j++ = *i;
+ continue;
+ }
+
+ if (val == l_True) {
+ solver.detachModifiedClause(origLit1, origLit2, origLit3, origSize, &c);
+ return true;
+ }
+ }
+ c.shrink(i-j);
+
+ assert(c.size() != 1);
+ if (i != j) {
+ if (c.size() == 2) {
+ solver.detachModifiedClause(origLit1, origLit2, origLit3, origSize, &c);
+ solver.attachBinClause(c[0], c[1], c.learnt());
+ solver.numNewBin++;
+ solver.dataSync->signalNewBinClause(c);
+ return true;
+ } else if (c.size() == 3) {
+ solver.detachModifiedClause(origLit1, origLit2, origLit3, origSize, &c);
+ solver.attachClause(c);
+ } else {
+ if (c.learnt())
+ solver.learnts_literals -= i-j;
+ else
+ solver.clauses_literals -= i-j;
+ }
+ }
+
+ return false;
+}
+
+void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type, const uint32_t limit)
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ XorClause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end; s++) {
+ if (s+1 != end)
+ __builtin_prefetch(*(s+1), 1, 0);
+
+ #ifdef DEBUG_ATTACH_FULL
+ XorClause& c = **s;
+ assert(solver.xorClauseIsAttached(c));
+ if (solver.assigns[c[0].var()]!=l_Undef || solver.assigns[c[1].var()]!=l_Undef) {
+ satisfied(**s);
+ }
+ #endif //DEBUG_ATTACH
+
+ if (cleanClause(**s)) {
+ //solver.clauseAllocator.clauseFree(*s);
+ solver.freeLater.push(*s);
+ (*s)->setRemoved();
+ } else {
+ #ifdef DEBUG_ATTACH_FULL
+ assert(solver.xorClauseIsAttached(c));
+ #endif //DEBUG_ATTACH
+ *ss++ = *s;
+ }
+ }
+ cs.shrink(s-ss);
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "cleanClauses(XorClause) useful: ?? Removed: " << s-ss << endl;
+ #endif
+}
+
+inline bool ClauseCleaner::cleanClause(XorClause& c)
+{
+ Lit *i, *j, *end;
+ Var origVar1 = c[0].var();
+ Var origVar2 = c[1].var();
+ uint32_t origSize = c.size();
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ const lbool& val = solver.assigns[i->var()];
+ if (val.isUndef()) {
+ *j = *i;
+ j++;
+ } else c.invert(val.getBool());
+ }
+ c.shrink(i-j);
+
+ assert(c.size() != 1);
+ switch (c.size()) {
+ case 0: {
+ solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
+ return true;
+ }
+ case 2: {
+ c[0] = c[0].unsign();
+ c[1] = c[1].unsign();
+ solver.varReplacer->replace(c, c.xorEqualFalse());
+ solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
+ return true;
+ }
+ default: {
+ if (i-j > 0) {
+ solver.clauses_literals -= i-j;
+ }
+ return false;
+ }
+ }
+
+ assert(false);
+ return false;
+}
+
+bool ClauseCleaner::satisfied(const Clause& c) const
+{
+ for (uint32_t i = 0; i != c.size(); i++)
+ if (solver.value(c[i]) == l_True)
+ return true;
+ return false;
+}
+
+bool ClauseCleaner::satisfied(const XorClause& c) const
+{
+ bool final = c.xorEqualFalse();
+ for (uint32_t k = 0; k != c.size(); k++ ) {
+ const lbool& val = solver.assigns[c[k].var()];
+ if (val.isUndef()) return false;
+ final ^= val.getBool();
+ }
+ return final;
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback