--- /dev/null
+#include "ClauseCleaner.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+ClauseCleaner::ClauseCleaner(Solver& _solver) :
+ solver(_solver)
+{
+ for (uint i = 0; i < 4; i++) {
+ lastNumUnitarySat[i] = solver.get_unitary_learnts_num();
+ lastNumUnitaryClean[i] = solver.get_unitary_learnts_num();
+ }
+}
+
+void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type)
+{
+ if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num())
+ return;
+
+ int i,j;
+ for (i = j = 0; i < cs.size(); i++) {
+ if (satisfied(*cs[i]))
+ solver.removeClause(*cs[i]);
+ else
+ cs[j++] = cs[i];
+ }
+ cs.shrink(i - j);
+
+ lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
+}
+
+void ClauseCleaner::removeSatisfied(vec<Clause*>& cs, ClauseSetType type)
+{
+ if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num())
+ return;
+
+ int i,j;
+ for (i = j = 0; i < cs.size(); i++) {
+ if (satisfied(*cs[i]))
+ solver.removeClause(*cs[i]);
+ else
+ cs[j++] = cs[i];
+ }
+ cs.shrink(i - j);
+
+ lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
+}
+
+bool ClauseCleaner::cleanClause(Clause& c)
+{
+ assert(c.size() >= 2);
+ Lit first = c[0];
+ Lit second = c[1];
+
+ Lit *i, *j, *end;
+ uint at = 0;
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
+ if (solver.value(*i) == l_Undef) {
+ *j = *i;
+ j++;
+ } else assert(at > 1);
+ assert(solver.value(*i) != l_True);
+ }
+ if ((c.size() > 2) && (c.size() - (i-j) == 2)) {
+ solver.detachModifiedClause(first, second, c.size(), &c);
+ c.shrink(i-j);
+ solver.attachClause(c);
+ } else
+ c.shrink(i-j);
+
+ assert(c.size() > 1);
+
+ return (i-j > 0);
+}
+
+void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type)
+{
+ if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num())
+ return;
+
+ uint useful = 0;
+ for (int s = 0; s < cs.size(); s++)
+ useful += cleanClause(*cs[s]);
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "cleanClauses(Clause) useful:" << useful << endl;
+ #endif
+}
+
+void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type)
+{
+ if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num())
+ return;
+
+ uint useful = 0;
+ XorClause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end;) {
+ XorClause& c = **s;
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Cleaning clause:";
+ c.plain_print();
+ solver.printClause(c);std::cout << std::endl;
+ #endif
+
+ Lit *i, *j, *end;
+ uint at = 0;
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
+ const lbool& val = solver.assigns[i->var()];
+ if (val.isUndef()) {
+ *j = *i;
+ j++;
+ } else /*assert(at>1),*/ c.invert(val.getBool());
+ }
+ c.shrink(i-j);
+ if (i-j > 0) useful++;
+
+ if (c.size() == 2) {
+ vec<Lit> ps(2);
+ ps[0] = c[0];
+ ps[1] = c[1];
+ solver.toReplace->replace(ps, c.xor_clause_inverted(), c.group);
+ solver.removeClause(c);
+ s++;
+ } else
+ *ss++ = *s++;
+
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Cleaned clause:";
+ c.plain_print();
+ solver.printClause(c);std::cout << std::endl;
+ #endif
+ assert(c.size() > 1);
+ }
+ cs.shrink(s-ss);
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "cleanClauses(XorClause) useful:" << useful << endl;
+ #endif
+}
+
+bool ClauseCleaner::satisfied(const Clause& c) const
+{
+ for (uint 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.xor_clause_inverted();
+ for (uint k = 0; k < c.size(); k++ ) {
+ const lbool& val = solver.assigns[c[k].var()];
+ if (val.isUndef()) return false;
+ final ^= val.getBool();
+ }
+ return final;
+}
+
+};
--- /dev/null
+/***********************************************************************************
+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/>.
+**************************************************************************************************/
+
+#ifndef CLAUSECLEANER_H
+#define CLAUSECLEANER_H
+
+#include "Solver.h"
+
+namespace MINISAT
+{
+
+class ClauseCleaner
+{
+ public:
+ ClauseCleaner(Solver& solver);
+
+ enum ClauseSetType {clauses, xorclauses, learnts, conglomerate};
+
+ void cleanClauses(vec<Clause*>& cs, ClauseSetType type);
+ void cleanClauses(vec<XorClause*>& cs, ClauseSetType type);
+ void removeSatisfied(vec<Clause*>& cs, ClauseSetType type);
+ void removeSatisfied(vec<XorClause*>& cs, ClauseSetType type);
+ bool satisfied(const Clause& c) const;
+ bool satisfied(const XorClause& c) const;
+
+ private:
+ bool cleanClause(Clause& c);
+
+ uint lastNumUnitarySat[4];
+ uint lastNumUnitaryClean[4];
+
+ Solver& solver;
+};
+
+};
+
+#endif //CLAUSECLEANER_H
#include "Conglomerate.h"
#include "Solver.h"
#include "VarReplacer.h"
+#include "ClauseCleaner.h"
#include <utility>
#include <algorithm>
free(calcAtFinish[i]);
}
+const vector<bool>& Conglomerate::getRemovedVars() const
+{
+ return removedVars;
+}
+
const vec<XorClause*>& Conglomerate::getCalcAtFinish() const
{
return calcAtFinish;
for (Lit* it = &(S->trail[0]), *end = it + S->trail.size(); it != end; it++)
blocked[it->var()] = true;
- const vec<Clause*>& tmp = S->toReplace->getToRemove();
- for (Clause *const*it = tmp.getData(), *const*end = it + tmp.size(); it != end; it++) {
+ const vec<Clause*>& clauses = S->toReplace->getClauses();
+ for (Clause *const*it = clauses.getData(), *const*end = it + clauses.size(); it != end; it++) {
const Clause& c = **it;
for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) {
blocked[a->var()] = true;
{
if (S->xorclauses.size() == 0)
return 0;
- toRemove.clear();
- toRemove.resize(S->xorclauses.size(), false);
#ifdef VERBOSE_DEBUG
cout << "Finding conglomerate xors started" << endl;
#endif
- S->removeSatisfied(S->xorclauses);
- S->cleanClauses(S->xorclauses);
+ S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
+ S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
+
+ toRemove.clear();
+ toRemove.resize(S->xorclauses.size(), false);
fillVarToXor();
}
S->setDecisionVar(var, false);
+ removedVars[var] = true;
if (c.size() == 0) {
varToXor.erase(it);
void Conglomerate::clearToRemove()
{
+ assert(toRemove.size() == S->xorclauses.size());
+
XorClause **a = S->xorclauses.getData();
XorClause **r = a;
XorClause **end = a + S->xorclauses.size();
for (uint i = 0; r != end; i++) {
if (!toRemove[i])
*a++ = *r++;
- else
+ else {
+ (**a).mark(1);
r++;
+ }
}
S->xorclauses.shrink(r-a);
+
+ clearLearntsFromToRemove();
+}
+
+void Conglomerate::clearLearntsFromToRemove()
+{
+ Clause **a = S->learnts.getData();
+ Clause **r = a;
+ Clause **end = a + S->learnts.size();
+ for (; r != end;) {
+ const Clause& c = **r;
+ bool inside = false;
+ if (!S->locked(c)) {
+ for (uint i = 0; i < c.size(); i++) {
+ if (removedVars[c[i].var()]) {
+ inside = true;
+ break;
+ }
+ }
+ }
+ if (!inside)
+ *a++ = *r++;
+ else {
+ S->removeClause(**r);
+ r++;
+ }
+ }
+ S->learnts.shrink(r-a);
}
void Conglomerate::doCalcAtFinish()
}
if (toAssign.size() > 1) {
cout << "Double assign!" << endl;
+ for (uint i = 1; i < toAssign.size(); i++) {
+ cout << "-> extra Var " << toAssign[i]+1 << endl;
+ }
}
#endif
assert(toAssign.size() > 0);
for (uint i = 1; i < toAssign.size(); i++) {
- S->uncheckedEnqueue(Lit(toAssign[i], false), &c);
+ S->uncheckedEnqueue(Lit(toAssign[i], true), &c);
}
S->uncheckedEnqueue(Lit(toAssign[0], final), &c);
+ assert(S->clauseCleaner->satisfied(c));
}
}
ps.clear();
for(uint i2 = 0; i2 != c.size() ; i2++) {
- ps.push(c[i2]);
- S->setDecisionVar(c[i2].var(), true);
+ ps.push(Lit(c[i2].var(), false));
}
- S->addXorClause(ps, c.xor_clause_inverted(), c.group, tmp);
+ S->addXorClause(ps, c.xor_clause_inverted(), c.group, tmp, true);
free(&c);
}
calcAtFinish.clear();
+ for (uint i = 0; i < removedVars.size(); i++) {
+ if (removedVars[i]) {
+ removedVars[i] = false;
+ S->setDecisionVar(i, true);
+ }
+ }
+}
+
+void Conglomerate::newVar()
+{
+ removedVars.resize(removedVars.size()+1, false);
}
};
#include <vector>
#include <map>
+#include <set>
#include "Clause.h"
#include "VarReplacer.h"
using std::vector;
using std::pair;
using std::map;
+using std::set;
class Solver;
void doCalcAtFinish(); ///<Calculate variables removed during conglomeration
const vec<XorClause*>& getCalcAtFinish() const;
vec<XorClause*>& getCalcAtFinish();
+ const vector<bool>& getRemovedVars() const;
+ void newVar();
private:
void fillVarToXor();
void clearDouble(vec<Lit>& ps) const;
void clearToRemove();
+ void clearLearntsFromToRemove();
bool dealWithNewClause(vec<Lit>& ps, const bool inverted, const uint old_group);
typedef map<uint, vector<pair<XorClause*, uint> > > varToXorMap;
varToXorMap varToXor;
vector<bool> blocked;
vector<bool> toRemove;
+ vector<bool> removedVars;
vec<XorClause*> calcAtFinish;
#include <iomanip>
#include "Clause.h"
#include <algorithm>
+#include "ClauseCleaner.h"
using std::ostream;
using std::cout;
using std::endl;
bool do_again_gauss = true;
while (do_again_gauss) {
do_again_gauss = false;
- solver.removeSatisfied(solver.xorclauses);
- solver.cleanClauses(solver.xorclauses);
+ solver.clauseCleaner->removeSatisfied(solver.xorclauses, ClauseCleaner::xorclauses);
+ solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
init();
Clause* confl;
gaussian_ret g = gaussian(confl);
, decision_until(0)
, starts_from(3)
{
- if (PackedRow::tmp_row == NULL)
- PackedRow::tmp_row = new uint64_t[1000];
}
~GaussianConfig()
{
- delete[] PackedRow::tmp_row;
}
//tuneable gauss parameters
uint decision_until; //do Gauss until this level
uint starts_from; //Gauss elimination starts from this restart number
};
+
};
#endif //GAUSSIANCONFIG_H
branch_depth_distrib.clear();
learnt_unitary_clauses = 0;
}
+
};
MTL = mtl
MTRAND = MTRand
-SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp
+SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp ClauseCleaner.cpp
OBJECTS = $(SOURCES:.cpp=.o)
LIB = libminisat.a
CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
#include "Solver.h"
#include "Gaussian.h"
#include "GaussianConfig.h"
+#include "ClauseCleaner.h"
#include <set>
#include <map>
unAssigned(_S->nVars() + 1)
, S(_S)
{
- table.resize(S->nVars(), unAssigned);
- matrix_no = 0;
}
inline const Var MatrixFinder::fingerprint(const XorClause& c) const
const uint MatrixFinder::findMatrixes()
{
+ table.clear();
+ table.resize(S->nVars(), unAssigned);
+ reverseTable.clear();
+ matrix_no = 0;
+
if (S->xorclauses.size() == 0)
return 0;
- S->removeSatisfied(S->xorclauses);
- S->cleanClauses(S->xorclauses);
+ S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
+ S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) {
set<uint> tomerge;
namespace MINISAT
{
-__thread uint64_t* PackedRow::tmp_row = NULL;
-
std::ostream& operator << (std::ostream& os, const PackedRow& m)
{
for(uint i = 0; i < m.size*64; i++) {
}
friend std::ostream& operator << (std::ostream& os, const PackedRow& m);
-
- static __thread uint64_t *tmp_row;
private:
friend class PackedMatrix;
#include "MatrixFinder.h"
#include "Conglomerate.h"
#include "XorFinder.h"
+#include "ClauseCleaner.h"
//#define DEBUG_LIB
{
toReplace = new VarReplacer(this);
conglomerate = new Conglomerate(this);
+ clauseCleaner = new ClauseCleaner(*this);
logger.setSolver(this);
#ifdef DEBUG_LIB
for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]);
delete toReplace;
delete conglomerate;
+ delete clauseCleaner;
#ifdef DEBUG_LIB
fclose(myoutputfile);
decision_var.push_back(dvar);
toReplace->newVar();
+ conglomerate->newVar();
insertVarOrder(v);
if (dynamic_behaviour_analysis)
logger.new_var(v);
+
+ #ifdef DEBUG_LIB
+ fprintf(myoutputfile, "c Solver::newVar() called\n");
+ #endif //DEBUG_LIB
return v;
}
-bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint group, char* group_name)
+bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint group, char* group_name, const bool internal)
{
assert(decisionLevel() == 0);
#ifdef DEBUG_LIB
- fprintf(myoutputfile, "x");
- for (uint i = 0; i < ps.size(); i++) {
- fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1);
+ if (!internal) {
+ fprintf(myoutputfile, "x");
+ for (uint i = 0; i < ps.size(); i++) {
+ fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1);
+ }
+ fprintf(myoutputfile, "0\n");
}
- fprintf(myoutputfile, "0\n");
#endif //DEBUG_LIB
if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name);
xorclauses.push(c);
attachClause(*c);
- toReplace->newClause();
+ if (!internal)
+ toReplace->newClause();
break;
}
}
else clauses_literals -= origSize;
}
-
-bool Solver::satisfied(const Clause& c) const
-{
- for (uint i = 0; i < c.size(); i++)
- if (value(c[i]) == l_True)
- return true;
- return false;
-}
-
-bool Solver::satisfied(const XorClause& c) const
-{
- bool final = c.xor_clause_inverted();
- for (uint k = 0; k < c.size(); k++ ) {
- const lbool& val = assigns[c[k].var()];
- if (val.isUndef()) return false;
- final ^= val.getBool();
- }
- return final;
-}
-
-
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
//
void Solver::cancelUntil(int level)
maxRestarts = num;
}
-bool Solver::cleanClause(Clause& c)
-{
- assert(c.size() >= 2);
- Lit first = c[0];
- Lit second = c[1];
-
- Lit *i, *j, *end;
- uint at = 0;
- for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
- if (value(*i) == l_Undef) {
- *j = *i;
- j++;
- } else assert(at > 1);
- assert(value(*i) != l_True);
- }
- if ((c.size() > 2) && (c.size() - (i-j) == 2)) {
- detachModifiedClause(first, second, c.size(), &c);
- c.shrink(i-j);
- attachClause(c);
- } else
- c.shrink(i-j);
- return (i-j > 0);
-}
-
-void Solver::cleanClauses(vec<Clause*>& cs)
-{
- uint useful = 0;
- for (int s = 0; s < cs.size(); s++)
- useful += cleanClause(*cs[s]);
- #ifdef VERBOSE_DEBUG
- cout << "cleanClauses(Clause) useful:" << useful << endl;
- #endif
-}
-
-void Solver::cleanClauses(vec<XorClause*>& cs)
-{
- uint useful = 0;
- XorClause **s, **ss, **end;
- for (s = ss = cs.getData(), end = s + cs.size(); s != end;) {
- XorClause& c = **s;
- #ifdef VERBOSE_DEBUG
- std::cout << "Cleaning clause:";
- c.plain_print();
- printClause(c);std::cout << std::endl;
- #endif
-
- Lit *i, *j, *end;
- uint at = 0;
- for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
- const lbool& val = assigns[i->var()];
- if (val.isUndef()) {
- *j = *i;
- j++;
- } else /*assert(at>1),*/ c.invert(val.getBool());
- }
- c.shrink(i-j);
- if (i-j > 0) useful++;
-
- if (c.size() == 2) {
- vec<Lit> ps(2);
- ps[0] = c[0];
- ps[1] = c[1];
- toReplace->replace(ps, c.xor_clause_inverted(), c.group);
- removeClause(c);
- s++;
- } else
- *ss++ = *s++;
-
- #ifdef VERBOSE_DEBUG
- std::cout << "Cleaned clause:";
- c.plain_print();
- printClause(c);std::cout << std::endl;
- #endif
- assert(c.size() > 1);
- }
- cs.shrink(s-ss);
-
- #ifdef VERBOSE_DEBUG
- cout << "cleanClauses(XorClause) useful:" << useful << endl;
- #endif
-}
-
/*_________________________________________________________________________________________________
|
| simplify : [void] -> [bool]
}
// Remove satisfied clauses:
- removeSatisfied(learnts);
+ clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts);
if (remove_satisfied) { // Can be turned off.
- removeSatisfied(clauses);
- removeSatisfied(xorclauses);
+ clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses);
+ clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses);
}
// Remove fixed variables from the variable heap:
simpDB_assigns = nAssigns();
simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
- //cleanClauses(clauses);
- //cleanClauses(xorclauses);
- //cleanClauses(learnts);
+ //clauseCleaner->cleanClauses(clauses);
+ //clauseCleaner->cleanClauses(xorclauses);
+ //clauseCleaner->cleanClauses(learnts);
return l_Undef;
}
double time;
if (clauses.size() < 400000) {
time = cpuTime();
- removeSatisfied(clauses);
- cleanClauses(clauses);
+ clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses);
+ clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses);
uint sumLengths = 0;
XorFinder xorFinder(this, clauses);
uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10);
}
}
- 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 (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) {
double time = cpuTime();
MatrixFinder m(this);
// Search:
while (status == l_Undef && starts < maxRestarts) {
- removeSatisfied(clauses);
- removeSatisfied(xorclauses);
- removeSatisfied(learnts);
+ clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses);
+ clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses);
+ clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts);
- cleanClauses(clauses);
- cleanClauses(xorclauses);
- cleanClauses(learnts);
+ clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses);
+ clauseCleaner->cleanClauses(xorclauses, ClauseCleaner::xorclauses);
+ clauseCleaner->cleanClauses(learnts, ClauseCleaner::learnts);
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nbclausesbeforereduce*curRestart, nLearnts(), (double)learnts_literals/nLearnts());
printf("====================================================================");
print_gauss_sum_stats();
}
+
+ 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) {
conglomerate->doCalcAtFinish();
class VarReplacer;
class XorFinder;
class FindUndef;
+class ClauseCleaner;
//#define VERBOSE_DEBUG_XOR
//#define VERBOSE_DEBUG
//
Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
bool addClause (vec<Lit>& ps, const uint group, char* group_name); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
- bool addXorClause (vec<Lit>& ps, bool xor_clause_inverted, const uint group, char* group_name); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method!
+ bool addXorClause (vec<Lit>& ps, bool xor_clause_inverted, const uint group, char* group_name, const bool internal = false); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method!
// Solving:
//
bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
lbool search (int nof_conflicts); // Search for a given number of conflicts.
void reduceDB (); // Reduce the set of learnt clauses.
- template<class T>
- void removeSatisfied (vec<T*>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
- void cleanClauses (vec<XorClause*>& cs);
- bool cleanClause (Clause& c);
- void cleanClauses (vec<Clause*>& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses
llbool handle_conflict (vec<Lit>& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause
llbool new_decision (int& nof_conflicts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made
void removeClause(Clause& c); // Detach and free a clause.
void removeClause(XorClause& 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.
- bool satisfied (const XorClause& c) const; // Returns TRUE if the clause is satisfied in the current state
- bool satisfied (const Clause& c) const; // Returns TRUE if the clause is satisfied in the current state.
void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true
// Misc:
friend class Conglomerate;
friend class MatrixFinder;
friend class VarReplacer;
+ friend class ClauseCleaner;
Conglomerate* conglomerate;
VarReplacer* toReplace;
+ ClauseCleaner* clauseCleaner;
// Debug:
void printLit (const Lit l) const;
{
if (decisionLevel() > 0)
return trail_lim[0];
- return 0;
-}
-template<class T>
-void Solver::removeSatisfied(vec<T*>& cs)
-{
- int i,j;
- for (i = j = 0; i < cs.size(); i++) {
- if (satisfied(*cs[i]))
- removeClause(*cs[i]);
- else
- cs[j++] = cs[i];
- }
- cs.shrink(i - j);
+ else
+ return trail.size();
}
template <class T>
inline void Solver::removeWatchedCl(vec<T> &ws, const Clause *c) {
CryptoMiniSat
-SVN revision:
-GIT revision: 63f0b6f7e4927759643c97913060c37f8ae4c82a
-
+SVN revision: 561
+GIT revision: 56d0a713979afbe737a7da1670f39eaf8c6f53a5
#include "Solver.h"
#include "Conglomerate.h"
+#include "ClauseCleaner.h"
//#define VERBOSE_DEBUG
VarReplacer::~VarReplacer()
{
- for (uint i = 0; i < toRemove.size(); i++)
- free(toRemove[i]);
+ for (uint i = 0; i < clauses.size(); i++)
+ free(clauses[i]);
}
void VarReplacer::performReplace()
{
#ifdef VERBOSE_DEBUG
cout << "Replacer started." << endl;
+ {
+ uint i = 0;
+ for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, i++) {
+ if (it->var() == i) continue;
+ cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl;
+ }
+ }
+ #endif
+
uint i = 0;
+ const vector<bool>& removedVars = S->conglomerate->getRemovedVars();
for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, i++) {
if (it->var() == i) continue;
- cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") << it->var()+1 << endl;
+ S->setDecisionVar(i, false);
+ if (!removedVars[it->var()])
+ S->setDecisionVar(it->var(), true);
}
- #endif
-
+
if (!addedNewClause || replacedVars == 0) return;
- S->removeSatisfied(S->clauses);
- S->removeSatisfied(S->xorclauses);
- S->cleanClauses(S->clauses);
- S->cleanClauses(S->xorclauses);
- for (uint i = 0; i < toRemove.size(); i++)
- S->removeClause(*toRemove[i]);
- toRemove.clear();
+ S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses);
+ S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts);
+ S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
+
+ S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses);
+ S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts);
+ S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
+ for (uint i = 0; i < clauses.size(); i++)
+ S->removeClause(*clauses[i]);
+ clauses.clear();
replace_set(S->clauses);
replace_set(S->learnts);
p = lit_Undef;
if (!S->assigns[c[i].var()].isUndef())
c.invert(S->assigns[c[i].var()].getBool());
- } else if (S->value(c[i]) == l_Undef) //just add
+ } else if (S->assigns[c[i].var()].isUndef()) //just add
c[j++] = p = c[i];
- else c.invert(S->value(c[i]) == l_True); //modify xor_clause_inverted instead of adding
+ else c.invert(S->assigns[c[i].var()].getBool()); //modify xor_clause_inverted instead of adding
}
c.shrink(i - j);
r++;
break;
case 1:
- S->uncheckedEnqueue(Lit(c[0].var(), !c.xor_clause_inverted()));
+ S->uncheckedEnqueue(c[0] ^ c.xor_clause_inverted());
+ r++;
+ break;
+ case 2: {
+ vec<Lit> ps(2);
+ ps[0] = c[0];
+ ps[1] = c[1];
+ addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true);
+ c.mark(1);
r++;
break;
+ }
default:
- if (c.size() == 2) {
- vec<Lit> ps(2);
- ps[0] = c[0];
- ps[1] = c[1];
- addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true);
- c.mark(1);
- r++;
- } else {
- S->attachClause(c);
- *a++ = *r++;
- }
+ S->attachClause(c);
+ *a++ = *r++;
break;
}
} else {
S->uncheckedEnqueue(c[0]);
S->detachModifiedClause(origLit1, origLit2, origSize, &c);
return true;
+ case 2:
+ S->detachModifiedClause(origLit1, origLit2, origSize, &c);
+ S->attachClause(c);
+ return false;
default:
if (origLit1 != c[0] || origLit2 != c[1]) {
S->detachModifiedClause(origLit1, origLit2, origSize, &c);
return replacingVars;
}
-const vec<Clause*>& VarReplacer::getToRemove() const
+const vec<Clause*>& VarReplacer::getClauses() const
{
- return toRemove;
+ return clauses;
}
void VarReplacer::extendModel() const
setAllThatPointsHereTo(lit1.var(), Lit(lit.var(), lit1.sign()));
table[lit1.var()] = Lit(lit.var(), lit1.sign());
reverseTable[lit.var()].push_back(lit1.var());
- S->setDecisionVar(lit1.var(), false);
setAllThatPointsHereTo(lit2.var(), lit ^ lit2.sign());
table[lit2.var()] = lit ^ lit2.sign();
reverseTable[lit.var()].push_back(lit2.var());
- S->setDecisionVar(lit2.var(), false);
table[lit.var()] = Lit(lit.var(), false);
- S->setDecisionVar(lit.var(), true);
return;
}
}
table[var] = lit;
reverseTable[lit.var()].push_back(var);
- S->setDecisionVar(var, false);
}
void VarReplacer::addBinaryXorClause(vec<Lit>& ps, const bool xor_clause_inverted, const uint group, const bool internal)
if (internal)
S->clauses.push(c);
else
- toRemove.push(c);
+ clauses.push(c);
S->attachClause(*c);
ps[0] ^= true;
if (internal)
S->clauses.push(c);
else
- toRemove.push(c);
+ clauses.push(c);
S->attachClause(*c);
}
const uint getNumReplacedVars() const;
const vector<Var> getReplacingVars() const;
const vector<Lit>& getReplaceTable() const;
- const vec<Clause*>& getToRemove() const;
+ const vec<Clause*>& getClauses() const;
void newClause();
void newVar();
vector<Lit> table;
map<Var, vector<Var> > reverseTable;
- vec<Clause*> toRemove;
+ vec<Clause*> clauses;
uint replacedLits;
uint replacedVars;
void XorFinder::clearToRemove()
{
+ assert(toRemove.size() == cls.size());
+
Clause **a = cls.getData();
Clause **r = cls.getData();
Clause **cend = cls.getData() + cls.size();
projects / francis / stp.git / commitdiff