0th bit bool learnt clause
1st - 2nd bit 2bit int marking
3rd bit bool inverted xor
- 4th-15th bit 12bit int matrix number
- 16th -31st bit 16bit int size
+ 4th -31st bit 28bit uint size
*/
uint32_t size_etc;
union { int act; uint32_t abst; } extra;
friend Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);
uint size () const {
- return size_etc >> 16;
+ return size_etc >> 4;
}
void shrink (uint i) {
assert(i <= size());
- size_etc = (((size_etc >> 16) - i) << 16) | (size_etc & ((1 << 16)-1));
+ size_etc = (((size_etc >> 4) - i) << 4) | (size_etc & ((1 << 4)-1));
}
void pop () {
shrink(1);
void calcAbstraction() {
uint32_t abstraction = 0;
- for (int i = 0; i < size(); i++)
- abstraction |= 1 << (data[i].var() & 31);
+ for (uint32_t i = 0; i != size(); i++)
+ abstraction |= 1 << (data[i].var() & 31);
extra.abst = abstraction;
}
}
protected:
void setSize(uint32_t size) {
- size_etc = (size_etc & ((1 << 16)-1)) + (size << 16);
+ size_etc = (size_etc & ((1 << 4)-1)) + (size << 4);
}
void setLearnt(bool learnt) {
size_etc = (size_etc & ~1) + learnt;
{
size_etc ^= (uint32_t)b << 3;
}
-
- inline uint32_t getMatrix() const
- {
- return ((size_etc >> 4) & ((1 << 12)-1));
- }
void print() {
printf("XOR Clause group: %d, size: %d, learnt:%d, lits:\"", group, size(), learnt());
friend class MatrixFinder;
protected:
- inline void setMatrix (uint32_t toset) {
- assert(toset < (1 << 12));
- size_etc = (size_etc & 15) + (toset << 4) + (size_etc & ~((1 << 16)-1));
- }
inline void setInverted(bool inverted)
{
size_etc = (size_etc & 7) + ((uint32_t)inverted << 3) + (size_etc & ~15);
const Lit* c = this->getData();
const Lit* d = other.getData();
- for (int i = 0; i < size(); i++) {
+ for (uint32_t i = 0; i != size(); i++) {
// search for c[i] or ~c[i]
- for (int j = 0; j < other.size(); j++)
+ for (uint32_t j = 0; j != other.size(); j++)
if (c[i] == d[j])
goto ok;
else if (ret == lit_Undef && c[i] == ~d[j]){
Lit impliedLit;
Clause *clause;
};
+
+class Watched {
+ public:
+ Watched(Clause *_clause, Lit _blockedLit) : blockedLit(_blockedLit), clause(_clause) {};
+ Lit blockedLit;
+ Clause *clause;
+};
+
};
#endif //CLAUSE_H
else
cs[j++] = cs[i];
}
- cs.shrink(i - j);
+ cs.shrink_(i - j);
lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
}
else
cs[j++] = cs[i];
}
- cs.shrink(i - j);
+ cs.shrink_(i - j);
lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
}
solver.detachModifiedClause(origLit1, origLit2, c.size(), &c);
c.shrink(i-j);
solver.attachClause(c);
- } else
+ } else {
c.shrink(i-j);
+ if (c.learnt())
+ solver.learnts_literals -= i-j;
+ else
+ solver.clauses_literals -= i-j;
+ }
return false;
}
return true;
}
default:
+ solver.clauses_literals -= i-j;
return false;
}
}
bool ClauseCleaner::satisfied(const Clause& c) const
{
- for (uint i = 0; i < c.size(); i++)
+ 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++ ) {
+ for (uint k = 0; k != c.size(); k++ ) {
const lbool& val = solver.assigns[c[k].var()];
if (val.isUndef()) return false;
final ^= val.getBool();
inline void ClauseCleaner::removeAndCleanAll()
{
- uint limit = (double)solver.order_heap.size() * PERCENTAGEPERFORMREPLACE;
+ uint limit = (double)solver.order_heap.size() * PERCENTAGECLEANCLAUSES;
cleanClauses(solver.clauses, ClauseCleaner::clauses, limit);
cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses, limit);
#ifdef VERBOSE_DEBUG
cout << "- Removing: ";
- x.plain_print();
+ x.plainPrint();
cout << "Adding var " << var+1 << " to calcAtFinish" << endl;
#endif
#ifdef VERBOSE_DEBUG
cout << "- Removing: ";
- x.plain_print();
+ x.plainPrint();
#endif
const uint old_group = x.group;
#ifdef VERBOSE_DEBUG
cout << "--> xor is 2-long, must later replace variable, adding var " << ps[0].var() + 1 << " to calcAtFinish:" << endl;
XorClause* newX = XorClause_new(ps, inverted, old_group);
- newX->plain_print();
+ newX->plainPrint();
free(newX);
#endif
#ifdef VERBOSE_DEBUG
cout << "- Adding: ";
- newX->plain_print();
+ newX->plainPrint();
#endif
S->xorclauses.push(newX);
#ifdef VERBOSE_DEBUG
cout << "doCalcFinish for xor-clause:";
- S->printClause(c); cout << endl;
+ c.plainPrint();
#endif
bool final = c.xor_clause_inverted();
XorClause& c = *calcAtFinish[i];
#ifdef VERBOSE_DEBUG
cout << "readding already removed (conglomerated) clause: ";
- c.plain_print();
+ c.plainPrint();
#endif
ps.clear();
ostream& operator << (ostream& os, const vec<Lit>& v)
{
- for (int i = 0; i < v.size(); i++) {
+ for (uint32_t i = 0; i != v.size(); i++) {
if (v[i].sign()) os << "-";
os << v[i].var()+1 << " ";
}
var_to_col.resize(solver.nVars(), unassigned_col);
uint num_xorclauses = 0;
- for (int i = 0; i != xorclauses.size(); i++) {
+ for (uint32_t i = 0; i != xorclauses.size(); i++) {
#ifdef DEBUG_GAUSS
assert(xorclauses[i]->mark() || !solver.satisfied(*xorclauses[i]));
#endif
origMat.removeable_cols = 0;
origMat.least_column_changed = -1;
origMat.matrix.resize(origMat.num_rows, origMat.num_cols);
- origMat.varset.resize(origMat.num_rows, origMat.num_cols);
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")matrix size:" << origMat.num_rows << "," << origMat.num_cols << endl;
#endif
uint matrix_row = 0;
- for (int i = 0; i < xorclauses.size(); i++) {
+ for (uint32_t i = 0; i != xorclauses.size(); i++) {
const XorClause& c = *xorclauses[i];
if (!c.mark()) {
- origMat.varset[matrix_row].set(c, var_to_col, origMat.num_cols);
- origMat.matrix[matrix_row].set(c, var_to_col, origMat.num_cols);
+ origMat.matrix.getVarsetAt(matrix_row).set(c, var_to_col, origMat.num_cols);
+ origMat.matrix.getMatrixAt(matrix_row).set(c, var_to_col, origMat.num_cols);
matrix_row++;
}
}
#endif
m.least_column_changed = std::min(m.least_column_changed, (int)col);
- PackedMatrix::iterator this_row = m.matrix.begin();
+ PackedMatrix::iterator this_row = m.matrix.beginMatrix();
uint row_num = 0;
if (solver.assigns[var].getBool()) {
- for (PackedMatrix::iterator end = this_row + std::min(m.last_one_in_col[col], m.num_rows); this_row != end; ++this_row, row_num++) {
- PackedRow r = *this_row;
- if (r[col]) {
+ for (uint end = m.last_one_in_col[col]; row_num != end && row_num != m.num_rows; ++this_row, row_num++) {
+ if ((*this_row)[col]) {
changed_rows.setBit(row_num);
- r.invert_xor_clause_inverted();
- r.clearBit(col);
+ (*this_row).invert_is_true();
+ (*this_row).clearBit(col);
}
}
} else {
- for (PackedMatrix::iterator end = this_row + std::min(m.last_one_in_col[col], m.num_rows); this_row != end; ++this_row, row_num++) {
- PackedRow r = *this_row;
- if (r[col]) {
+ for (uint end = m.last_one_in_col[col]; row_num != end && row_num != m.num_rows; ++this_row, row_num++) {
+ if ((*this_row)[col]) {
changed_rows.setBit(row_num);
- r.clearBit(col);
+ (*this_row).clearBit(col);
}
}
}
uint16_t until = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows);
if (j > m.past_the_end_last_one_in_col)
until = m.num_rows;
- for (;i != until; i++) if (changed_rows[i] && m.matrix[i].popcnt_is_one())
+ for (;i != until; i++) if (changed_rows[i] && m.matrix.getMatrixAt(i).popcnt_is_one())
propagatable_rows.push(i);
}
continue;
}
- PackedMatrix::iterator this_matrix_row = m.matrix.begin() + i;
- PackedMatrix::iterator end = m.matrix.begin() + std::min(m.last_one_in_col[j], m.num_rows);
+ PackedMatrix::iterator this_matrix_row = m.matrix.beginMatrix() + i;
+ PackedMatrix::iterator end = m.matrix.beginMatrix() + std::min(m.last_one_in_col[j], m.num_rows);
for (; this_matrix_row != end; ++this_matrix_row) {
if ((*this_matrix_row)[j])
break;
}
- uint best_row = this_matrix_row - m.matrix.begin();
+ uint best_row = this_matrix_row - m.matrix.beginMatrix();
if (this_matrix_row != end) {
- PackedRow matrix_row_i = m.matrix[i];
- PackedRow varset_row_i = m.varset[i];
- PackedMatrix::iterator this_varset_row = m.varset.begin() + best_row;
+ PackedRow matrix_row_i = m.matrix.getMatrixAt(i);
//swap rows i and maxi, but do not change the value of i;
if (i != best_row) {
#endif
//Would early abort, but would not find the best conflict (and would be expensive)
- //if (!matrix_row_i.get_xor_clause_inverted() && matrix_row_i.isZero()) {
+ //if (matrix_row_i.is_true() && matrix_row_i.isZero()) {
// conflict_row = i;
// return 0;
//}
- matrix_row_i.swap(*this_matrix_row);
- varset_row_i.swap(*this_varset_row);
+ matrix_row_i.swapBoth(*this_matrix_row);
}
#ifdef DEBUG_GAUSS
assert(m.matrix[i].popcnt(j) == m.matrix[i].popcnt());
//Now A[i,j] will contain the old value of A[maxi,j];
++this_matrix_row;
- ++this_varset_row;
- for (; this_matrix_row != end; ++this_matrix_row, ++this_varset_row) if ((*this_matrix_row)[j]) {
+ for (; this_matrix_row != end; ++this_matrix_row) if ((*this_matrix_row)[j]) {
//subtract row i from row u;
//Now A[u,j] will be 0, since A[u,j] - A[i,j] = A[u,j] -1 = 0.
#ifdef VERBOSE_DEBUG
number_of_row_additions++;
#endif
- *this_matrix_row ^= matrix_row_i;
- *this_varset_row ^= varset_row_i;
+ (*this_matrix_row).xorBoth(matrix_row_i);
//Would early abort, but would not find the best conflict (and would be expensive)
- //if (!it->get_xor_clause_inverted() &&it->isZero()) {
+ //if (it->is_true() &&it->isZero()) {
// conflict_row = i2;
// return 0;
//}
{
assert(best_row != UINT_MAX);
- m.varset[best_row].fill(tmp_clause, solver.assigns, col_to_var_original);
+ m.matrix.getVarsetAt(best_row).fill(tmp_clause, solver.assigns, col_to_var_original);
confl = Clause_new(tmp_clause, solver.learnt_clause_group++, false);
Clause& cla = *confl;
+ #ifdef STATS_NEEDED
if (solver.dynamic_behaviour_analysis)
solver.logger.set_group_name(confl->group, "learnt gauss clause");
+ #endif
if (cla.size() <= 1)
return unit_conflict;
assert(cla.size() >= 2);
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")Found conflict:";
- solver.printClause(cla);
+ cla.plainPrint();
#endif
if (maxlevel != solver.decisionLevel()) {
+ #ifdef STATS_NEEDED
if (solver.dynamic_behaviour_analysis)
solver.logger.conflict(Logger::gauss_confl_type, maxlevel, confl->group, *confl);
+ #endif
solver.cancelUntil(maxlevel);
}
const uint curr_dec_level = solver.decisionLevel();
uint maxsublevel = 0;
uint maxsublevel_at = UINT_MAX;
- for (uint i = 0, size = cla.size(); i < size; i++) if (solver.level[cla[i].var()] == curr_dec_level) {
+ for (uint i = 0, size = cla.size(); i != size; i++) if (solver.level[cla[i].var()] == curr_dec_level) {
uint tmp = find_sublevel(cla[i].var());
if (tmp >= maxsublevel) {
maxsublevel = tmp;
#ifdef DEBUG_GAUSS
assert(m.matrix[row].isZero());
#endif
- if (!m.matrix[row].get_xor_clause_inverted())
+ if (m.matrix.getMatrixAt(row).is_true())
analyse_confl(m, row, maxlevel, size, best_row);
}
#endif
m.num_rows = last_row;
m.matrix.resizeNumRows(m.num_rows);
- m.varset.resizeNumRows(m.num_rows);
gaussian_ret ret = nothing;
unsigned long int var = 0;
uint this_size = 0;
while (true) {
- var = m.varset[row].scan(var);
+ var = m.matrix.getVarsetAt(row).scan(var);
if (var == ULONG_MAX) break;
const Var real_var = col_to_var_original[var];
cout << endl;
#endif
- m.varset[row].fill(tmp_clause, solver.assigns, col_to_var_original);
+ m.matrix.getVarsetAt(row).fill(tmp_clause, solver.assigns, col_to_var_original);
Clause& cla = *Clause_new(tmp_clause, solver.learnt_clause_group++, false);
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")matrix prop clause: ";
- solver.printClause(cla);
+ cla.plainPrint();
cout << endl;
#endif
- assert(!m.matrix[row].get_xor_clause_inverted() == !cla[0].sign());
+ assert(m.matrix.getMatrixAt(row).is_true() == !cla[0].sign());
assert(solver.assigns[cla[0].var()].isUndef());
if (cla.size() == 1) {
const Lit lit = cla[0];
- if (solver.dynamic_behaviour_analysis) {
- solver.logger.set_group_name(cla.group, "unitary learnt clause");
- solver.logger.conflict(Logger::gauss_confl_type, 0, cla.group, cla);
- }
solver.cancelUntil(0);
solver.uncheckedEnqueue(lit);
- if (solver.dynamic_behaviour_analysis)
- solver.logger.propagation(cla[0], Logger::gauss_propagation_type, cla.group);
free(&cla);
return unit_propagation;
}
clauses_toclear.push_back(std::make_pair(&cla, solver.trail.size()-1));
- solver.uncheckedEnqueue(cla[0], &cla);
- if (solver.dynamic_behaviour_analysis) {
+ #ifdef STATS_NEEDED
+ if (solver.dynamic_behaviour_analysis)
solver.logger.set_group_name(cla.group, "gauss prop clause");
- solver.logger.propagation(cla[0], Logger::gauss_propagation_type, cla.group);
- }
+ #endif
+ solver.uncheckedEnqueue(cla[0], &cla);
return propagation;
}
}
Lit lit = (*confl)[0];
+ #ifdef STATS_NEEDED
if (solver.dynamic_behaviour_analysis)
solver.logger.conflict(Logger::gauss_confl_type, 0, confl->group, *confl);
+ #endif
solver.cancelUntil(0);
if (solver.assigns[lit.var()].isDef()) {
- if (solver.dynamic_behaviour_analysis)
- solver.logger.empty_clause(confl->group);
-
free(confl);
return l_False;
}
solver.uncheckedEnqueue(lit);
- if (solver.dynamic_behaviour_analysis)
- solver.logger.propagation(lit, Logger::gauss_propagation_type, confl->group);
free(confl);
return l_Continue;
else cout << col_to_var_original[var]+1 << ", ";
var++;
}
- if (row.get_xor_clause_inverted()) cout << "xor_clause_inverted";
+ if (!row.is_true()) cout << "xor_clause_inverted";
}
template<class T>
}
col++;
}
- if (row.get_xor_clause_inverted()) cout << "xor_clause_inverted";
+ if (!row.is_true()) cout << "xor_clause_inverted";
}
const string Gaussian::lbool_to_string(const lbool toprint)
bool Gaussian::check_no_conflict(matrixset& m) const
{
uint row = 0;
- for(PackedMatrix::iterator r = m.matrix.begin(), end = m.matrix.end(); r != end; ++r, ++row) {
- if (!(*r).get_xor_clause_inverted() && (*r).isZero()) {
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r, ++row) {
+ if ((*r).is_true() && (*r).isZero()) {
cout << "Conflict at row " << row << endl;
return false;
}
void Gaussian::print_matrix(matrixset& m) const
{
uint row = 0;
- for (PackedMatrix::iterator it = m.matrix.begin(); it != m.matrix.end(); ++it, row++) {
+ for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, row++) {
cout << *it << " -- row:" << row;
if (row >= m.num_rows)
cout << " (considered past the end)";
const bool Gaussian::nothing_to_propagate(matrixset& m) const
{
- for(PackedMatrix::iterator r = m.matrix.begin(), end = m.matrix.end(); r != end; ++r) {
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) {
if ((*r).popcnt_is_one()
&& solver.assigns[m.col_to_var[(*r).scan(0)]].isUndef())
return false;
}
- for(PackedMatrix::iterator r = m.matrix.begin(), end = m.matrix.end(); r != end; ++r) {
- if ((*r).isZero() && !(*r).get_xor_clause_inverted())
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) {
+ if ((*r).isZero() && (*r).is_true())
return false;
}
return true;
const uint last = std::min(m.last_one_in_col[i] - 1, (int)m.num_rows);
uint real_last = 0;
uint i2 = 0;
- for (PackedMatrix::iterator it = m.matrix.begin(); it != m.matrix.end(); ++it, i2++) {
+ for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, i2++) {
if ((*it)[i])
real_last = i2;
}
assert(matrix.getSize() == varset.getSize());
for (uint i = 0; i < matrix.getSize(); i++) {
- const PackedRow mat_row = matrix[i];
- const PackedRow var_row = varset[i];
+ const PackedRow mat_row = matrix.getMatrixAt(i);
+ const PackedRow var_row = matrix.getVarsetAt(i);
unsigned long int col = 0;
bool final = false;
col++;
}
- if ((final^mat_row.get_xor_clause_inverted()) != var_row.get_xor_clause_inverted()) {
+ if ((final^!mat_row.is_true()) != !var_row.is_true()) {
cout << "problem with row:"; print_matrix_row_with_assigns(var_row); cout << endl;
assert(false);
}
for(uint i = 0, until = std::min(m.num_rows, m.last_one_in_col[last_col]+1); i < until; i++, this_row++) {
mpz_class& r = *this_row;
mpz_and(tmp.get_mp(), tocount.get_mp(), r.get_mp());
- r.invert_xor_clause_inverted(tmp.popcnt() % 2);
+ r.invert_is_true(tmp.popcnt() % 2);
r &= toclear;
}
void set_disabled(const bool toset);
//functions used throughout the Solver
- void canceling(const int sublevel);
+ void canceling(const uint sublevel);
protected:
Solver& solver;
{
public:
PackedMatrix matrix; // The matrix, updated to reflect variable assignements
- PackedMatrix varset; // The matrix, without variable assignements. The xor-clause is read from here. This matrix only follows the 'matrix' with its row-swap, row-xor, and row-delete operations.
BitArray var_is_set;
vector<Var> col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives unassigned_var if the COL has been zeroed (i.e. the variable assigned)
uint16_t num_rows; // number of active rows in the matrix. Unactive rows are rows that contain only zeros (and if they are conflicting, then the conflict has been treated)
&& decisionlevel < config.decision_until);
}
-inline void Gaussian::canceling(const int sublevel)
+inline void Gaussian::canceling(const uint sublevel)
{
if (disabled)
return;
if (messed_matrix_vars_since_reversal)
return;
- int c = std::min(gauss_last_level, solver.trail.size()-1);
+ int c = std::min((int)gauss_last_level, (int)(solver.trail.size())-1);
for (; c >= sublevel; c--) {
Var var = solver.trail[c].var();
if (var < var_is_in.getSize()
GaussianConfig() :
only_nth_gauss_save(2)
, decision_until(0)
- , starts_from(3)
- {
- }
-
- ~GaussianConfig()
+ , starts_from(2)
{
}
, verbosity(_verbosity)
, begin_called(false)
+ , proofStarts(0)
{
runid /= 10;
runid = time(NULL) % 10000;
if (begin_called)
return;
- begin_called = true;
begin();
}
begin_called = true;
if (proof_graph_on) {
std::stringstream filename;
- filename << "proofs/" << runid << "-proof" << S->starts << ".dot";
+ filename << "proofs/" << runid << "-proof" << proofStarts++ << "-" << S->starts << ".dot";
if (S->starts == 0)
history.push_back(uniqueid);
fprintf(proof,"node%d [shape=polygon,sides=5,label=\"",uniqueid);
if (!mini_proof) {
- for (int i = 0; i < learnt_clause.size(); i++) {
+ for (uint32_t i = 0; i != learnt_clause.size(); i++) {
if (learnt_clause[i].sign()) fprintf(proof,"-");
int myvar = learnt_clause[i].var();
- fprintf(proof,"%s\\n",varnames[myvar].c_str());
+ if (varnames[myvar] != "Noname")
+ fprintf(proof,"%s\\n",varnames[myvar].c_str());
+ else
+ fprintf(proof,"Var: %d\\n",myvar);
}
}
fprintf(proof,"\"];\n");
template void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const vec<Lit>& learnt_clause);
-// For the really strange event that the solver is given an empty clause
-void Logger::empty_clause(const uint group)
-{
- first_begin();
- assert(!(proof == NULL && proof_graph_on));
-
- if (proof_graph_on) {
- uniqueid++;
- fprintf(proof,"node%d -> node%d [label=\"emtpy clause:",history[history.size()-1],uniqueid);
- fprintf(proof,"%s\"];\n", groupnames[group].c_str());
- history.push_back(uniqueid);
- }
-}
-
// Propagating a literal. Type of literal and the (learned clause's)/(propagating clause's)/(etc) group must be given. Updates the proof graph and the statistics. note: the meaning of the variable 'group' depends on the type
-void Logger::propagation(const Lit lit, const prop_type type, const uint group)
+void Logger::propagation(const Lit lit, Clause* c)
{
first_begin();
assert(!(proof == NULL && proof_graph_on));
+
+ uint group;
+ prop_type type;
+ if (c == NULL) {
+ if (S->decisionLevel() == 0)
+ type = add_clause_type;
+ else
+ type = guess_type;
+ group = UINT_MAX;
+ } else {
+ type = simple_propagation_type;
+ group = c->group;
+ }
//graph
- if (proof_graph_on && (!mini_proof || type == guess_type || type == assumption_type)) {
+ if (proof_graph_on && (!mini_proof || type == guess_type)) {
uniqueid++;
fprintf(proof,"node%d [shape=box, label=\"",uniqueid);;
if (lit.sign())
fprintf(proof,"-");
- fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str());
+ if (varnames[lit.var()] != "Noname")
+ fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str());
+ else
+ fprintf(proof,"Var: %d\"];\n",lit.var());
fprintf(proof,"node%d -> node%d [label=\"",history[history.size()-1],uniqueid);
fprintf(proof,"%s\"];\n", groupnames[group].c_str());
break;
- case gauss_propagation_type:
- fprintf(proof,"Gauss propagation\",style=bold];\n");
- break;
-
case add_clause_type:
- fprintf(proof,"red. from %s\"];\n",groupnames[group].c_str());
- break;
-
- case unit_clause_type:
- fprintf(proof,"unit clause %s,style=bold\"];\n",groupnames[group].c_str());
- break;
-
- case assumption_type:
- fprintf(proof,"assumption\"];\n");
+ fprintf(proof,"red. from clause\"];\n");
break;
case guess_type:
if (statistics_on) {
switch (type) {
- case unit_clause_type:
- learnt_unitary_clauses++;
- case add_clause_type:
- case gauss_propagation_type:
case simple_propagation_type:
- no_propagations++;
- times_var_propagated[lit.var()]++;
-
depths_of_propagations_for_group[group].push_back(S->decisionLevel());
times_group_caused_propagation[group]++;
+ case add_clause_type:
+ no_propagations++;
+ times_var_propagated[lit.var()]++;
depths_of_assigns_for_var[lit.var()].push_back(S->decisionLevel());
break;
-
- case assumption_type:
case guess_type:
no_decisions++;
times_var_guessed[lit.var()]++;
// Ending of a restart iteration
void Logger::end(const finish_type finish)
{
+ first_begin();
assert(!(proof == NULL && proof_graph_on));
if (proof_graph_on) {
case unsat_model_found:
fprintf(proof,"node%d [shape=doublecircle, label=\"UNSAT\"];\n",uniqueid);
break;
- case done_adding_clauses:
- fprintf(proof,"node%d [shape=doublecircle, label=\"Done adding\\nclauses\"];\n",uniqueid);
- break;
case restarting:
fprintf(proof,"node%d [shape=doublecircle, label=\"Re-starting\\nsearch\"];\n",uniqueid);
break;
if (finish == restarting)
reset_statistics();
}
+
+ if (model_found || unsat_model_found)
+ begin_called = false;
}
void Logger::print_footer() const
void Logger::print_times_var_guessed() const
{
vector<pair<uint, uint> > times_var_ordered;
- for (int i = 0; i < varnames.size(); i++) if (times_var_guessed[i] > 0)
+ for (uint32_t i = 0; i != varnames.size(); i++) if (times_var_guessed[i] > 0)
times_var_ordered.push_back(std::make_pair(times_var_guessed[i], i));
if (!times_var_ordered.empty()) {
cout << yaxis[height-1-i-middle] << " ";
else
cout << " ";
- for (uint i2 = 0; i2 < no_slices; i2++) {
- if (slices[i2]/hslice >= i) cout << "+";
+ for (uint i2 = 0; i2 != no_slices; i2++) {
+ if (slices[i2]/hslice >= (uint)i) cout << "+";
else cout << " ";
}
cout << "|" << endl;
print_footer();
print_simple_line(" Advanced statistics - for only this restart");
print_footer();
- print_line("Unitary learnts", learnt_unitary_clauses);
+ print_line("Unitary learnts", S->get_unitary_learnts_num() - last_unitary_learnt_clauses);
print_line("No. branches visited", no_conflicts);
print_line("Avg. branch depth", (double)sum_conflict_depths/(double)no_conflicts);
print_line("No. decisions", no_decisions);
sum_decisions_on_branches = 0;
sum_propagations_on_branches = 0;
branch_depth_distrib.clear();
- learnt_unitary_clauses = 0;
+ last_unitary_learnt_clauses = S->get_unitary_learnts_num();
}
};
void setSolver(const Solver* S);
//types of props, confl, and finish
- enum prop_type { unit_clause_type, add_clause_type, assumption_type, guess_type, simple_propagation_type, gauss_propagation_type };
+ enum prop_type { add_clause_type, guess_type, simple_propagation_type};
enum confl_type { simple_confl_type, gauss_confl_type };
- enum finish_type { model_found, unsat_model_found, restarting, done_adding_clauses };
+ enum finish_type { model_found, unsat_model_found, restarting};
//Conflict and propagation(guess is also a proapgation...)
template<class T>
void conflict(const confl_type type, const uint goback_level, const uint group, const T& learnt_clause);
- void propagation(const Lit lit, const prop_type type, const uint group = UINT_MAX);
- void empty_clause(const uint group);
+ void propagation(const Lit lit, Clause* c);
//functions to add/name variables
void new_var(const Var var);
uint no_propagations;
uint sum_decisions_on_branches;
uint sum_propagations_on_branches;
- uint learnt_unitary_clauses;
+ uint last_unitary_learnt_clauses;
//message display properties
const int& verbosity;
void first_begin();
bool begin_called;
+ uint proofStarts;
};
};
assert(b.numRows > 0 && b.numCols > 0);
#endif
- mp = new uint64_t[numRows*(numCols+1)];
- memcpy(mp, b.mp, sizeof(uint64_t)*numRows*(numCols+1));
+ mp = new uint64_t[numRows*2*(numCols+1)];
+ memcpy(mp, b.mp, sizeof(uint64_t)*numRows*2*(numCols+1));
}
~PackedMatrix()
void resize(const uint num_rows, uint num_cols)
{
num_cols = num_cols / 64 + (bool)(num_cols % 64);
- if (numRows*(numCols+1) < num_rows*(num_cols+1)) {
+ if (numRows*2*(numCols+1) < num_rows*2*(num_cols+1)) {
delete[] mp;
- mp = new uint64_t[num_rows*(num_cols+1)];
+ mp = new uint64_t[num_rows*2*(num_cols+1)];
}
numRows = num_rows;
numCols = num_cols;
//assert(b.numRows > 0 && b.numCols > 0);
#endif
- if (numRows*(numCols+1) < b.numRows*(b.numCols+1)) {
+ if (numRows*2*(numCols+1) < b.numRows*2*(b.numCols+1)) {
delete[] mp;
- mp = new uint64_t[b.numRows*(b.numCols+1)];
+ mp = new uint64_t[b.numRows*2*(b.numCols+1)];
}
numRows = b.numRows;
numCols = b.numCols;
- memcpy(mp, b.mp, sizeof(uint64_t)*numRows*(numCols+1));
+ memcpy(mp, b.mp, sizeof(uint64_t)*numRows*2*(numCols+1));
return *this;
}
- inline PackedRow operator[](const uint i)
+ inline PackedRow getMatrixAt(const uint i)
{
#ifdef DEBUG_MATRIX
assert(i <= numRows);
#endif
- return PackedRow(numCols, *(mp+i*(numCols+1)), mp+i*(numCols+1)+1);
+ return PackedRow(numCols, mp+i*2*(numCols+1));
+ }
+ inline PackedRow getVarsetAt(const uint i)
+ {
+ #ifdef DEBUG_MATRIX
+ assert(i <= numRows);
+ #endif
+
+ return PackedRow(numCols, mp+i*2*(numCols+1)+(numCols+1));
}
- inline const PackedRow operator[](const uint i) const
+ inline const PackedRow getMatrixAt(const uint i) const
{
#ifdef DEBUG_MATRIX
assert(i <= numRows);
#endif
- return PackedRow(numCols, *(mp+i*(numCols+1)), mp+i*(numCols+1)+1);
+ return PackedRow(numCols, mp+i*2*(numCols+1));
+ }
+
+ inline const PackedRow getVarsetAt(const uint i) const
+ {
+ #ifdef DEBUG_MATRIX
+ assert(i <= numRows);
+ #endif
+
+ return PackedRow(numCols, mp+i*2*(numCols+1)+(numCols+1));
}
class iterator
public:
PackedRow operator*()
{
- return PackedRow(numCols, *mp, mp+1);
+ return PackedRow(numCols, mp);
}
iterator& operator++()
{
- mp += numCols+1;
+ mp += 2*(numCols+1);
return *this;
}
iterator operator+(const uint num) const
{
iterator ret(*this);
- ret.mp += (numCols+1)*num;
+ ret.mp += 2*(numCols+1)*num;
return ret;
}
const uint operator-(const iterator& b) const
{
- return (mp - b.mp)/(numCols+1);
+ return (mp - b.mp)/(2*(numCols+1));
}
void operator+=(const uint num)
{
- mp += (numCols+1)*num;
+ mp += 2*(numCols+1)*num;
}
const bool operator!=(const iterator& it) const
const uint numCols;
};
- inline iterator begin()
+ inline iterator beginMatrix()
{
return iterator(mp, numCols);
}
- inline iterator end()
+ inline iterator endMatrix()
{
- return iterator(mp+numRows*(numCols+1), numCols);
+ return iterator(mp+numRows*2*(numCols+1), numCols);
}
- /*class const_iterator
- {
- public:
- const PackedRow operator*()
- {
- return PackedRow(numCols, *mp, mp+1);
- }
-
- const_iterator& operator++()
- {
- mp += numCols+1;
- return *this;
- }
-
- const_iterator operator+(const uint num) const
- {
- const_iterator ret(*this);
- ret.mp += (numCols+1)*num;
- return ret;
- }
-
- void operator+=(const uint num)
- {
- mp += (numCols+1)*num;
- }
-
- const bool operator!=(const const_iterator& it) const
- {
- return mp != it.mp;
- }
-
- const bool operator==(const const_iterator& it) const
- {
- return mp == it.mp;
- }
-
- private:
- friend class PackedMatrix;
-
- const_iterator(uint64_t* _mp, const uint _numCols) :
- mp(_mp)
- , numCols(_numCols)
- {}
-
- const uint64_t* mp;
- const uint numCols;
- };
- inline const_iterator begin() const
+ inline iterator beginVarset()
{
- return const_iterator(mp, numCols);
+ return iterator(mp+(numCols+1), numCols);
}
-
- inline const_iterator end() const
+
+ inline iterator endVarset()
{
- return const_iterator(mp+numRows*(numCols+1), numCols);
- }*/
+ return iterator(mp+(numCols+1)+numRows*2*(numCols+1), numCols);
+ }
inline const uint getSize() const
{
for(uint i = 0; i < m.size*64; i++) {
os << m[i];
}
- os << " -- xor: " << m.get_xor_clause_inverted();
+ os << " -- xor: " << !m.is_true();
return os;
}
void PackedRow::fill(vec<Lit>& tmp_clause, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const
{
- bool final = xor_clause_inverted;
+ bool final = !is_true_internal;
tmp_clause.clear();
uint col = 0;
assert(b.size == size);
#endif
- uint64_t * __restrict mp1 = mp;
- uint64_t * __restrict mp2 = b.mp;
-
for (uint i = 0; i != size; i++) {
- *(mp1 + i) ^= *(mp2 + i);
+ *(mp + i) ^= *(b.mp + i);
}
- xor_clause_inverted ^= !b.xor_clause_inverted;
+
+ is_true_internal ^= b.is_true_internal;
return *this;
}
+ void xorBoth(const PackedRow& b)
+ {
+ #ifdef DEBUG_ROW
+ assert(size > 0);
+ assert(b.size > 0);
+ assert(b.size == size);
+ #endif
+
+ for (uint i = 0; i != 2*size+1; i++) {
+ *(mp + i) ^= *(b.mp + i);
+ }
+
+ is_true_internal ^= b.is_true_internal;
+ }
+
uint popcnt() const;
uint popcnt(uint from) const;
bool popcnt_is_one() const
{
char popcount = 0;
- for (uint i = 0; i != size; i++) if (mp[i]) {
+ for (uint i = 0; i != size; i++) {
uint64_t tmp = mp[i];
- for (uint i2 = 0; i2 != 64; i2 += 4) {
+ while(tmp) {
popcount += tmp & 1;
popcount += tmp & 2;
popcount += tmp & 4;
uint64_t tmp = mp[from/64];
tmp >>= from%64;
- for (uint i2 = from%64; i2 < 64; i2 += 4) {
- if (tmp & 1) return false;
- if (tmp & 2) return false;
- if (tmp & 4) return false;
- if (tmp & 8) return false;
- tmp >>= 4;
- }
+ if (tmp) return false;
- for (uint i = from/64+1; i != size; i++) if (mp[i]) {
- tmp = mp[i];
- for (uint i2 = 0; i2 != 64; i2 += 4) {
- if (tmp & 1) return false;
- if (tmp & 2) return false;
- if (tmp & 4) return false;
- if (tmp & 8) return false;
- tmp >>= 4;
- }
- }
+ for (uint i = from/64+1; i != size; i++)
+ if (mp[i]) return false;
return true;
}
- inline const uint64_t& get_xor_clause_inverted() const
+ inline const uint64_t& is_true() const
{
- return xor_clause_inverted;
+ return is_true_internal;
}
inline const bool isZero() const
mp[i/64] &= ~((uint64_t)1 << (i%64));
}
- inline void invert_xor_clause_inverted(const bool b = true)
+ inline void invert_is_true(const bool b = true)
{
- xor_clause_inverted ^= b;
+ is_true_internal ^= b;
}
inline void setBit(const uint i)
assert(b.size == size);
#endif
- uint64_t * __restrict mp1 = mp;
- uint64_t * __restrict mp2 = b.mp;
+ uint64_t * __restrict mp1 = mp-1;
+ uint64_t * __restrict mp2 = b.mp-1;
+
+ uint i = size+1;
+
+ while(i != 0) {
+ uint64_t tmp(*mp2);
+ *mp2 = *mp1;
+ *mp1 = tmp;
+ mp1++;
+ mp2++;
+ i--;
+ }
+ }
+
+ void swapBoth(PackedRow b)
+ {
+ #ifdef DEBUG_ROW
+ assert(size > 0);
+ assert(b.size > 0);
+ assert(b.size == size);
+ #endif
+
+ uint64_t * __restrict mp1 = mp-1;
+ uint64_t * __restrict mp2 = b.mp-1;
+
+ uint i = 2*(size+1);
- for (int i = -1; i != size; i++) {
- uint64_t tmp(*(mp2 + i));
- *(mp2 + i) = *(mp + i);
- *(mp + i) = tmp;
+ while(i != 0) {
+ uint64_t tmp(*mp2);
+ *mp2 = *mp1;
+ *mp1 = tmp;
+ mp1++;
+ mp2++;
+ i--;
}
}
setBit(toset_var);
}
- xor_clause_inverted = v.xor_clause_inverted();
+ is_true_internal = !v.xor_clause_inverted();
}
void fill(vec<Lit>& tmp_clause, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const;
friend std::ostream& operator << (std::ostream& os, const PackedRow& m);
- PackedRow(const uint _size, uint64_t& _xor_clause_inverted, uint64_t* const _mp) :
+ PackedRow(const uint _size, uint64_t* const _mp) :
size(_size)
- , mp(_mp)
- , xor_clause_inverted(_xor_clause_inverted)
+ , mp(_mp+1)
+ , is_true_internal(*_mp)
{}
private:
friend class PackedMatrix;
const uint size;
- uint64_t* const mp;
- uint64_t& xor_clause_inverted;
+ uint64_t* __restrict const mp;
+ uint64_t& is_true_internal;
};
std::ostream& operator << (std::ostream& os, const PackedRow& m);
RestartTypeChooser::RestartTypeChooser(const Solver* const _S) :
S(_S)
, topX(100)
- , limit(40)
+ , limit(30)
{
}
calcHeap();
uint sameIn = 0;
if (!firstVarsOld.empty()) {
- for (uint i = 0; i < 100; i++) {
+ uint thisTopX = std::min(firstVarsOld.size(), (size_t)topX);
+ for (uint i = 0; i != thisTopX; i++) {
if (std::find(firstVars.begin(), firstVars.end(), firstVarsOld[i]) != firstVars.end())
sameIn++;
}
void RestartTypeChooser::calcHeap()
{
- firstVars.resize(100);
+ firstVars.resize(topX);
#ifdef VERBOSE_DEBUG
std::cout << "First vars:" << std::endl;
#endif
Heap<Solver::VarOrderLt> tmp(S->order_heap);
- for (uint i = 0; i != 100; i++) {
+ uint thisTopX = std::min(S->order_heap.size(), (int)topX);
+ for (uint i = 0; i != thisTopX; i++) {
#ifdef VERBOSE_DEBUG
std::cout << tmp.removeMin()+1 << ", ";
#endif
**************************************************************************************************/
#include "Solver.h"
-#include "Sort.h"
#include <cmath>
#include <string.h>
#include <algorithm>
// Statistics: (formerly in 'SolverStats')
//
- , nbDL2(0), nbBin(0), nbReduceDB(0)
, starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
, clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+ , nbDL2(0), nbBin(0), lastNbBin(0), nbReduceDB(0)
, ok (true)
, progress_estimate(0)
, remove_satisfied (true)
, mtrand((unsigned long int)0)
+ #ifdef STATS_NEEDED
, logger(verbosity)
, dynamic_behaviour_analysis(false) //do not document the proof as default
+ #endif
, maxRestarts(UINT_MAX)
, MYFLAG (0)
, learnt_clause_group(0)
varReplacer = new VarReplacer(this);
conglomerate = new Conglomerate(this);
clauseCleaner = new ClauseCleaner(*this);
+
+ #ifdef STATS_NEEDED
logger.setSolver(this);
+ #endif
}
Solver::~Solver()
{
- for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
- for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
- for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]);
+ for (uint32_t i = 0; i != learnts.size(); i++) free(learnts[i]);
+ for (uint32_t i = 0; i != clauses.size(); i++) free(clauses[i]);
+ for (uint32_t i = 0; i != xorclauses.size(); i++) free(xorclauses[i]);
clearGaussMatrixes();
- for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]);
+ for (uint32_t i = 0; i != freeLater.size(); i++) free(freeLater[i]);
delete varReplacer;
delete conglomerate;
delete clauseCleaner;
conglomerate->newVar();
insertVarOrder(v);
+
+ #ifdef STATS_NEEDED
if (dynamic_behaviour_analysis)
logger.new_var(v);
+ #endif
if (libraryCNFFile)
fprintf(libraryCNFFile, "c Solver::newVar() called\n");
}
fprintf(libraryCNFFile, "0\n");
}
-
- if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name);
+
+ #ifdef STATS_NEEDED
+ if (dynamic_behaviour_analysis)
+ logger.set_group_name(group, group_name);
+ #endif
if (!ok)
return false;
// Check if clause is satisfied and remove false/duplicate literals:
if (varReplacer->getNumLastReplacedVars()) {
- for (int i = 0; i != ps.size(); i++) {
+ for (uint32_t i = 0; i != ps.size(); i++) {
ps[i] = varReplacer->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
}
}
- sort(ps);
+ std::sort(ps.getData(), ps.getData()+ps.size());
Lit p;
- int i, j;
- for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+ uint32_t i, j;
+ for (i = j = 0, p = lit_Undef; i != ps.size(); i++) {
xor_clause_inverted ^= ps[i].sign();
ps[i] ^= ps[i].sign();
else //modify xor_clause_inverted instead of adding
xor_clause_inverted ^= (assigns[ps[i].var()].getBool());
}
- ps.shrink(i - j);
+ ps.shrink_(i - j);
switch(ps.size()) {
case 0: {
if (xor_clause_inverted)
return true;
-
- if (dynamic_behaviour_analysis) logger.empty_clause(group);
return ok = false;
}
case 1: {
assert(assigns[ps[0].var()].isUndef());
uncheckedEnqueue(ps[0] ^ xor_clause_inverted);
- if (dynamic_behaviour_analysis)
- logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::add_clause_type, group);
return ok = (propagate() == NULL);
}
case 2: {
assert(decisionLevel() == 0);
if (libraryCNFFile) {
- for (int i = 0; i < ps.size(); i++) {
+ for (uint32_t i = 0; i != ps.size(); i++) {
fprintf(libraryCNFFile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1);
}
fprintf(libraryCNFFile, "0\n");
}
-
+
+ #ifdef STATS_NEEDED
if (dynamic_behaviour_analysis)
logger.set_group_name(group, group_name);
+ #endif
if (!ok)
return false;
// Check if clause is satisfied and remove false/duplicate literals:
if (varReplacer->getNumLastReplacedVars()) {
- for (int i = 0; i != ps.size(); i++) {
+ for (uint32_t i = 0; i != ps.size(); i++) {
ps[i] = varReplacer->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
}
}
- sort(ps);
+ std::sort(ps.getData(), ps.getData()+ps.size());
Lit p;
- int i, j;
- for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+ uint32_t i, j;
+ for (i = j = 0, p = lit_Undef; i != ps.size(); i++) {
if (value(ps[i]).getBool() || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps.shrink(i - j);
if (ps.size() == 0) {
- if (dynamic_behaviour_analysis)
- logger.empty_clause(group);
return ok = false;
} else if (ps.size() == 1) {
assert(value(ps[0]) == l_Undef);
uncheckedEnqueue(ps[0]);
- if (dynamic_behaviour_analysis)
- logger.propagation(ps[0], Logger::add_clause_type, group);
return ok = (propagate() == NULL);
} else {
learnt_clause_group = std::max(group+1, learnt_clause_group);
xorwatches[c[0].var()].push(&c);
xorwatches[c[1].var()].push(&c);
- if (c.learnt()) learnts_literals += c.size();
- else clauses_literals += c.size();
+ clauses_literals += c.size();
}
void Solver::attachClause(Clause& c)
binwatches[index0].push(WatchedBin(&c, c[1]));
binwatches[index1].push(WatchedBin(&c, c[0]));
} else {
- watches[index0].push(&c);
- watches[index1].push(&c);
+ watches[index0].push(Watched(&c, c[c.size()/2]));
+ watches[index1].push(Watched(&c, c[c.size()/2]));
}
if (c.learnt()) learnts_literals += c.size();
remove(xorwatches[c[0].var()], &c);
remove(xorwatches[c[1].var()], &c);
- if (c.learnt()) learnts_literals -= c.size();
- else clauses_literals -= c.size();
+ clauses_literals -= c.size();
}
void Solver::detachClause(const Clause& c)
removeWatchedBinCl(binwatches[(~lit1).toInt()], address);
removeWatchedBinCl(binwatches[(~lit2).toInt()], address);
} else {
- assert(find(watches[(~lit1).toInt()], address));
- assert(find(watches[(~lit2).toInt()], address));
- remove(watches[(~lit1).toInt()], address);
- remove(watches[(~lit2).toInt()], address);
+ assert(findW(watches[(~lit1).toInt()], address));
+ assert(findW(watches[(~lit2).toInt()], address));
+ removeW(watches[(~lit1).toInt()], address);
+ removeW(watches[(~lit2).toInt()], address);
}
if (address->learnt()) learnts_literals -= origSize;
else clauses_literals -= origSize;
assert(find(xorwatches[var2], address));
remove(xorwatches[var1], address);
remove(xorwatches[var2], address);
- if (address->learnt()) learnts_literals -= origSize;
- else clauses_literals -= origSize;
+
+ clauses_literals -= origSize;
}
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
}
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
- trail_lim.shrink(trail_lim.size() - level);
+ trail_lim.shrink_(trail_lim.size() - level);
}
#ifdef VERBOSE_DEBUG
// Simplify conflict clause:
//
- int i, j;
+ uint32_t i, j;
if (expensive_ccmin) {
uint32_t abstract_level = 0;
for (i = 1; i < out_learnt.size(); i++)
if (out_learnt.size() == 1)
out_btlevel = 0;
else {
- int max_i = 1;
- for (int i = 2; i < out_learnt.size(); i++)
+ uint32_t max_i = 1;
+ for (uint32_t i = 2; i < out_learnt.size(); i++)
if (level[out_learnt[i].var()] > level[out_learnt[max_i].var()])
max_i = i;
Lit p = out_learnt[max_i];
nbLevels = 0;
MYFLAG++;
- for(int i = 0; i < out_learnt.size(); i++) {
+ for(uint32_t i = 0; i != out_learnt.size(); i++) {
int lev = level[out_learnt[i].var()];
if (permDiff[lev] != MYFLAG) {
permDiff[lev] = MYFLAG;
#ifdef UPDATEVARACTIVITY
if (lastDecisionLevel.size() > 0) {
- for(int i = 0; i<lastDecisionLevel.size(); i++) {
+ for(uint32_t i = 0; i != lastDecisionLevel.size(); i++) {
if (reason[lastDecisionLevel[i].var()]->activity() < nbLevels)
varBumpActivity(lastDecisionLevel[i].var());
}
}
#endif
- for (int j = 0; j < analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared)
+ for (uint32_t j = 0; j != analyze_toclear.size(); j++)
+ seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared)
}
analyze_stack.push(p);
analyze_toclear.push(p);
} else {
- for (int j = top; j < analyze_toclear.size(); j++)
+ for (uint32_t j = top; j != analyze_toclear.size(); j++)
seen[analyze_toclear[j].var()] = 0;
analyze_toclear.shrink(analyze_toclear.size() - top);
return false;
reason [v] = from;
polarity[p.var()] = p.sign();
trail.push(p);
+
+ #ifdef STATS_NEEDED
+ if (dynamic_behaviour_analysis)
+ logger.propagation(p, from);
+ #endif
}
while (qhead < trail.size()) {
Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
- vec<Clause*>& ws = watches[p.toInt()];
- Clause **i, **j, **end;
+ vec<Watched>& ws = watches[p.toInt()];
+ Watched *i, *j, *end;
num_props++;
//First propagate binary clauses
lbool val = value(imp);
if (val.isUndef()) {
uncheckedEnqueue(imp, k->clause);
- if (dynamic_behaviour_analysis)
- logger.propagation(imp, Logger::simple_propagation_type, k->clause->group);
} else if (val == l_False)
return k->clause;
}
#endif
for (i = j = ws.getData(), end = i + ws.size(); i != end;) {
- Clause& c = **i++;
+ if(value(i->blockedLit).getBool()) { // Clause is sat
+ *j++ = *i++;
+ continue;
+ }
+ Lit bl = i->blockedLit;
+ Clause& c = *(i->clause);
+ i++;
// Make sure the false literal is data[1]:
const Lit false_lit(~p);
// If 0th watch is true, then clause is already satisfied.
const Lit& first = c[0];
- if (value(first) == l_True) {
- *j++ = &c;
+ if (value(first).getBool()) {
+ j->clause = &c;
+ j->blockedLit = first;
+ j++;
} else {
// Look for new watch:
- for (int k = 2; k != c.size(); k++)
+ for (uint32_t k = 2; k != c.size(); k++)
if (value(c[k]) != l_False) {
c[1] = c[k];
c[k] = false_lit;
- watches[(~c[1]).toInt()].push(&c);
+ watches[(~c[1]).toInt()].push(Watched(&c, c[0]));
goto FoundWatch;
}
// Did not find watch -- clause is unit under assignment:
- *j++ = &c;
+ j->clause = &c;
+ j->blockedLit = bl;
+ j++;
if (value(first) == l_False) {
confl = &c;
qhead = trail.size();
*j++ = *i++;
} else {
uncheckedEnqueue(first, &c);
- if (dynamic_behaviour_analysis)
- logger.propagation(first,Logger::simple_propagation_type,c.group);
#ifdef DYNAMICNBLEVEL
if (c.learnt() && c.activity() > 2) { // GA
MYFLAG++;
FoundWatch:
;
}
- ws.shrink(i - j);
+ ws.shrink_(i - j);
//Finally, propagate XOR-clauses
if (xor_as_well && !confl) confl = propagate_xors(p);
#endif
uncheckedEnqueue(c[0], (Clause*)&c);
- if (dynamic_behaviour_analysis)
- logger.propagation(c[0], Logger::simple_propagation_type, c.group);
} else if (!final) {
#ifdef VERBOSE_DEBUG_XOR
void Solver::reduceDB()
{
- int i, j;
+ uint32_t i, j;
nbReduceDB++;
- sort(learnts, reduceDB_lt());
- for (i = j = 0; i < learnts.size() / RATIOREMOVECLAUSES; i++){
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
+ for (i = j = 0; i != learnts.size() / RATIOREMOVECLAUSES; i++){
if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() > 2)
removeClause(*learnts[i]);
else
for (; i < learnts.size(); i++) {
learnts[j++] = learnts[i];
}
- learnts.shrink(i - j);
+ learnts.shrink_(i - j);
}
const vec<Clause*>& Solver::get_learnts() const
const vec<Clause*>& Solver::get_sorted_learnts()
{
- sort(learnts, reduceDB_lt());
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
return learnts;
}
{
vector<Lit> unitaries;
if (decisionLevel() > 0) {
- for (uint i = 0; i < trail_lim[0]; i++)
+ for (uint32_t i = 0; i != trail_lim[0]; i++)
unitaries.push_back(trail[i]);
}
}
if (decisionLevel() > 0) {
- for (uint i = 0; i < trail_lim[0]; i++)
+ for (uint32_t i = 0; i != trail_lim[0]; i++)
printf("%s%d 0\n", trail[i].sign() ? "-" : "", trail[i].var());
}
- sort(learnts, reduceDB_lt());
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
for (int i = learnts.size()-1; i >= 0 ; i--) {
learnts[i]->plainPrint(outfile);
}
assert(decisionLevel() == 0);
if (!ok || propagate() != NULL) {
- if (dynamic_behaviour_analysis) {
- logger.end(Logger::unsat_model_found);
- }
ok = false;
return l_False;
}
}
// Remove satisfied clauses:
- clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts);
- if (remove_satisfied) { // Can be turned off.
- clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses);
- clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses);
+ clauseCleaner->removeAndCleanAll();
+ if (((double)(nbBin - lastNbBin)/BINARY_TO_XOR_APPROX) > (double)order_heap.size() * PERCENTAGEPERFORMREPLACE) {
+ XorFinder xorFinder(this, learnts, ClauseCleaner::learnts);
+ xorFinder.doNoPart(2, 2);
+ if (!ok) return l_False;
+
+ lastNbBin = nbBin;
+ }
+ if (performReplace
+ && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) {
+ varReplacer->performReplace();
+ if (!ok) return l_False;
}
// 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)
- //clauseCleaner->cleanClauses(clauses);
- //clauseCleaner->cleanClauses(xorclauses);
- //clauseCleaner->cleanClauses(learnts);
-
return l_Undef;
}
nbDecisionLevelHistory.fastclear();
progress_estimate = progressEstimate();
cancelUntil(0);
- if (dynamic_behaviour_analysis) {
- logger.end(Logger::restarting);
- }
return l_Undef;
}
break;
if (nof_conflicts >= 0 && conflictC >= nof_conflicts) {
progress_estimate = progressEstimate();
cancelUntil(0);
- if (dynamic_behaviour_analysis)
- logger.end(Logger::restarting);
return l_Undef;
}
break;
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && simplify() == l_False) {
- if (dynamic_behaviour_analysis) {
- logger.end(Logger::unsat_model_found);
- }
return l_False;
}
if (value(p) == l_True) {
// Dummy decision level:
newDecisionLevel();
- if (dynamic_behaviour_analysis) logger.propagation(p, Logger::assumption_type);
} else if (value(p) == l_False) {
analyzeFinal(~p, conflict);
- if (dynamic_behaviour_analysis) {
- logger.end(Logger::unsat_model_found);
- }
return l_False;
} else {
next = p;
decisions++;
next = pickBranchLit(polarity_mode);
- if (next == lit_Undef) {
- // Model found:
- if (dynamic_behaviour_analysis) {
- logger.end(Logger::model_found);
- }
+ if (next == lit_Undef)
return l_True;
- }
}
// Increase decision level and enqueue 'next'
assert(value(next) == l_Undef);
newDecisionLevel();
uncheckedEnqueue(next);
- if (dynamic_behaviour_analysis)
- logger.propagation(next, Logger::guess_type);
return l_Nothing;
}
conflicts++;
conflictC++;
- if (decisionLevel() == 0) {
- if (dynamic_behaviour_analysis) {
- logger.end(Logger::unsat_model_found);
- }
+ if (decisionLevel() == 0)
return l_False;
- }
learnt_clause.clear();
analyze(confl, learnt_clause, backtrack_level, nbLevels);
conf4Stats++;
totalSumOfDecisionLevel += nbLevels;
}
+ #ifdef STATS_NEEDED
if (dynamic_behaviour_analysis)
logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause);
+ #endif
cancelUntil(backtrack_level);
#ifdef VERBOSE_DEBUG
//Unitary learnt
if (learnt_clause.size() == 1) {
uncheckedEnqueue(learnt_clause[0]);
- if (dynamic_behaviour_analysis) {
- logger.set_group_name(learnt_clause_group, "unitary learnt clause");
- logger.propagation(learnt_clause[0], Logger::unit_clause_type, learnt_clause_group);
- learnt_clause_group++;
- }
assert(backtrack_level == 0 && "Unit clause learnt, so must cancel until level 0, right?");
#ifdef VERBOSE_DEBUG
//Normal learnt
} else {
Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true);
+ #ifdef STATS_NEEDED
+ if (dynamic_behaviour_analysis)
+ logger.set_group_name(c->group, "learnt clause");
+ #endif
learnts.push(c);
c->setActivity(nbLevels); // LS
if (nbLevels <= 2) nbDL2++;
if (c->size() == 2) nbBin++;
attachClause(*c);
uncheckedEnqueue(learnt_clause[0], c);
-
- if (dynamic_behaviour_analysis) {
- logger.set_group_name(c->group, "learnt clause");
- logger.propagation(learnt_clause[0], Logger::simple_propagation_type, c->group);
- }
}
varDecayActivity();
double progress = 0;
double F = 1.0 / nVars();
- for (int i = 0; i <= decisionLevel(); i++) {
+ for (uint32_t i = 0; i <= decisionLevel(); i++) {
int beg = i == 0 ? 0 : trail_lim[i - 1];
int end = i == decisionLevel() ? trail.size() : trail_lim[i];
progress += pow(F, i) * (end - beg);
if (xorFinder) {
double time;
- if (clauses.size() < 400000) {
- time = cpuTime();
- uint sumLengths = 0;
- XorFinder xorFinder(this, clauses);
- uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10);
+ if (clauses.size() < MAX_CLAUSENUM_XORFIND) {
+ XorFinder xorFinder(this, clauses, ClauseCleaner::clauses);
+ xorFinder.doNoPart(2, 10);
if (!ok) return;
- if (verbosity >=1)
- printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
-
if (performReplace
&& ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) {
varReplacer->performReplace();
performStepsBeforeSolve();
if (!ok) return l_False;
-
- if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
- printf("============================[ Search Statistics ]========================================\n");
- printf("| Conflicts | ORIGINAL | LEARNT | GAUSS |\n");
- printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | Prop Confl On |\n");
- printf("=========================================================================================\n");
- }
-
- if (dynamic_behaviour_analysis)
- logger.end(Logger::done_adding_clauses);
+ printStatHeader();
RestartTypeChooser restartTypeChooser(this);
// Search:
while (status == l_Undef && starts < maxRestarts) {
- clauseCleaner->removeAndCleanAll();
-
- 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());
- print_gauss_sum_stats();
+ printRestartStat();
+ #ifdef STATS_NEEDED
+ if (dynamic_behaviour_analysis) {
+ logger.end(Logger::restarting);
+ logger.begin();
}
+ #endif
- if (dynamic_behaviour_analysis)
- logger.begin();
status = search((int)nof_conflicts);
nof_conflicts *= restart_inc;
chooseRestartType(status, restartTypeChooser);
}
-
- if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
- printf("====================================================================");
- print_gauss_sum_stats();
- }
+ printEndSearchStat();
for (uint i = 0; i < gauss_matrixes.size(); i++)
delete gauss_matrixes[i];
varReplacer->extendModel();
// Extend & copy model:
model.growTo(nVars());
- for (int i = 0; i < nVars(); i++) model[i] = value(i);
+ for (uint32_t i = 0; i != nVars(); i++) model[i] = value(i);
#ifndef NDEBUG
verifyModel();
#endif
double time = cpuTime();
FindUndef finder(*this);
const uint unbounded = finder.unRoll();
- printf("Greedy unbounding :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded);
+ if (verbosity >= 1)
+ printf("Greedy unbounding :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded);
}
} if (status == l_False) {
if (conflict.size() == 0)
ok = false;
}
+ #ifdef STATS_NEEDED
+ if (dynamic_behaviour_analysis) {
+ if (status == l_True)
+ logger.end(Logger::model_found);
+ else if (status == l_False)
+ logger.end(Logger::unsat_model_found);
+ else if (status == l_Undef)
+ logger.end(Logger::restarting);
+ }
+ #endif
+
#ifdef LS_STATS_NBBUMP
for(int i=0;i<learnts.size();i++)
printf("## %d %d %d\n", learnts[i]->size(),learnts[i]->activity(),
bool failed = false;
- for (int i = 0; i < xorclauses.size(); i++) {
+ for (uint32_t i = 0; i != xorclauses.size(); i++) {
XorClause& c = *xorclauses[i];
bool final = c.xor_clause_inverted();
#ifdef VERBOSE_DEBUG
XorClause* c2 = XorClause_new(c, c.xor_clause_inverted(), c.group);
std::sort(c2->getData(), c2->getData()+ c2->size());
- c2->plain_print();
+ c2->plainPrint();
free(c2);
#endif
void Solver::verifyModel()
{
bool failed = false;
- for (int i = 0; i < clauses.size(); i++) {
+ for (uint32_t i = 0; i != clauses.size(); i++) {
Clause& c = *clauses[i];
for (uint j = 0; j < c.size(); j++)
if (modelValue(c[j]) == l_True)
{
// Check that sizes are calculated correctly:
int cnt = 0;
- for (int i = 0; i < clauses.size(); i++)
+ for (uint32_t i = 0; i != clauses.size(); i++)
cnt += clauses[i]->size();
- for (int i = 0; i < xorclauses.size(); i++)
+ for (uint32_t i = 0; i != xorclauses.size(); i++)
cnt += xorclauses[i]->size();
if ((int)clauses_literals != cnt) {
}
}
+void Solver::printStatHeader() const
+{
+ #ifdef STATS_NEEDED
+ if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
+ #else
+ if (verbosity >= 1) {
+ #endif
+ printf("============================[ Search Statistics ]========================================\n");
+ printf("| Conflicts | ORIGINAL | LEARNT | GAUSS |\n");
+ printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | Prop Confl On |\n");
+ printf("=========================================================================================\n");
+ }
+}
+
+void Solver::printRestartStat() const
+{
+ #ifdef STATS_NEEDED
+ if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
+ #else
+ if (verbosity >= 1) {
+ #endif
+ printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart), (int)nLearnts(), (double)learnts_literals/nLearnts());
+ print_gauss_sum_stats();
+ }
+}
+
+void Solver::printEndSearchStat() const
+{
+ #ifdef STATS_NEEDED
+ if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
+ #else
+ if (verbosity >= 1) {
+ #endif
+ printf("====================================================================");
+ print_gauss_sum_stats();
+ }
+}
+
};
class FindUndef;
class ClauseCleaner;
-//#define VERBOSE_DEBUG_XOR
-//#define VERBOSE_DEBUG
-
#ifdef VERBOSE_DEBUG
using std::cout;
using std::endl;
lbool value (const Var& x) const; // The current value of a variable.
lbool value (const Lit& p) const; // The current value of a literal.
lbool modelValue (const Lit& p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
- int nAssigns () const; // The current number of assigned literals.
- int nClauses () const; // The current number of original clauses.
- int nLearnts () const; // The current number of learnt clauses.
- int nVars () const; // The current number of variables.
+ uint32_t nAssigns () const; // The current number of assigned literals.
+ uint32_t nClauses () const; // The current number of original clauses.
+ uint32_t nLearnts () const; // The current number of learnt clauses.
+ uint32_t nVars () const; // The current number of variables.
// Extra results: (read-only member variable)
//
//
uint64_t starts, decisions, rnd_decisions, propagations, conflicts;
uint64_t clauses_literals, learnts_literals, max_literals, tot_literals;
- uint64_t nbDL2, nbBin, nbReduceDB;
+ uint64_t nbDL2, nbBin, lastNbBin, nbReduceDB;
//Logging
void needStats(); // Prepares the solver to output statistics
void needProofGraph(); // Prepares the solver to output proof graphs during solving
- void setVariableName(int var, char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger')
+ void setVariableName(Var var, char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger')
const vec<Clause*>& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses
const vec<Clause*>& get_learnts() const; //Get all learnt clauses that are >1 long
const vector<Lit> get_unitary_learnts() const; //return the set of unitary learnt clauses
vec<XorClause*> freeLater; // List of xorclauses to free at the end (due to matrixes, they cannot be freed immediately)
vec<double> activity; // A heuristic measurement of the activity of a variable.
double var_inc; // Amount to bump next variable with.
- vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+ vec<vec<Watched> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<vec<XorClause*> > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses.
vec<vec<WatchedBin> > binwatches;
vec<lbool> assigns; // The current assignments
#endif
int64_t curRestart;
int64_t conf4Stats;
- int nbclausesbeforereduce;
- int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
- int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
+ uint32_t nbclausesbeforereduce;
+ uint32_t qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+ uint32_t simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
bqueue<unsigned int> nbDecisionLevelHistory; // Set of last decision level in conflict clauses
float totalSumOfDecisionLevel;
- MTRand mtrand; // random number generator
- Logger logger; // dynamic logging, statistics
+ MTRand mtrand; // random number generaton
friend class Logger;
- bool dynamic_behaviour_analysis; //should 'logger' be called whenever a propagation/conflict/decision is made?
+ #ifdef STATS_NEEDED
+ Logger logger; // dynamic logging, statistics
+ bool dynamic_behaviour_analysis; // Is logger running?
+ #endif
uint maxRestarts; // More than this number of restarts will not be performed
// Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
// Misc:
//
- int decisionLevel () const; // Gives the current decisionlevel.
+ uint32_t decisionLevel () const; // Gives the current decisionlevel.
uint32_t abstractLevel (const Var& x) const; // Used to represent an abstraction of sets of decision levels.
- double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
//Xor-finding related stuff
friend class XorFinder;
void chooseRestartType(const lbool& status, RestartTypeChooser& restartTypeChooser);
void performStepsBeforeSolve();
- // Debug:
+ // Debug & etc:
void printLit (const Lit l) const;
void verifyModel ();
bool verifyXorClauses (const vec<XorClause*>& cs) const;
void checkLiteralCount();
+ void printStatHeader () const;
+ void printRestartStat () const;
+ void printEndSearchStat() const;
+ double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
};
{
if ( (activity[v] += var_inc) > 1e100 ) {
// Rescale:
- for (int i = 0; i < nVars(); i++)
+ for (uint32_t i = 0; i != nVars(); i++)
activity[i] *= 1e-100;
var_inc *= 1e-100;
}
return trail.size() - trail_lim[level-1] - 1;
return trail_lim[level] - trail_lim[level-1] - 1;
}*/
-inline int Solver::decisionLevel () const
+inline uint32_t Solver::decisionLevel () const
{
return trail_lim.size();
}
{
return model[p.var()] ^ p.sign();
}
-inline int Solver::nAssigns () const
+inline uint32_t Solver::nAssigns () const
{
return trail.size();
}
-inline int Solver::nClauses () const
+inline uint32_t Solver::nClauses () const
{
return clauses.size() + xorclauses.size();
}
-inline int Solver::nLearnts () const
+inline uint32_t Solver::nLearnts () const
{
return learnts.size();
}
-inline int Solver::nVars () const
+inline uint32_t Solver::nVars () const
{
return assigns.size();
}
{
mtrand.seed(seed); // Set seed of the variable-selection and clause-permutation(if applicable)
}
+#ifdef STATS_NEEDED
inline void Solver::needStats()
{
dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate statistics
dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate proof graphs during solving
logger.proof_graph_on = true;
}
-inline void Solver::setVariableName(int var, char* name)
+inline void Solver::setVariableName(Var var, char* name)
{
while (var >= nVars()) newVar();
if (dynamic_behaviour_analysis)
logger.set_variable_name(var, name);
} // Sets the varible 'var'-s name to 'name' in the logger
+#else
+inline void Solver::setVariableName(Var var, char* name)
+{}
+#endif
inline const uint Solver::get_unitary_learnts_num() const
{
if (decisionLevel() > 0)
}
template <class T>
inline void Solver::removeWatchedCl(vec<T> &ws, const Clause *c) {
- int j = 0;
- for (; j < ws.size() && ws[j] != c; j++);
+ uint32_t j = 0;
+ for (; j < ws.size() && ws[j].clause != c; j++);
assert(j < ws.size());
for (; j < ws.size()-1; j++) ws[j] = ws[j+1];
ws.pop();
}
template <class T>
inline void Solver::removeWatchedBinCl(vec<T> &ws, const Clause *c) {
- int j = 0;
+ uint32_t j = 0;
for (; j < ws.size() && ws[j].clause != c; j++);
assert(j < ws.size());
for (; j < ws.size()-1; j++) ws[j] = ws[j+1];
template<class T>
inline bool Solver::findWatchedCl(vec<T>& ws, const Clause *c)
{
- int j = 0;
- for (; j < ws.size() && ws[j] != c; j++);
+ uint32_t j = 0;
+ for (; j < ws.size() && ws[j].clause != c; j++);
return j < ws.size();
}
template<class T>
inline bool Solver::findWatchedBinCl(vec<T>& ws, const Clause *c)
{
- int j = 0;
+ uint32_t j = 0;
for (; j < ws.size() && ws[j].clause != c; j++);
return j < ws.size();
}
fprintf(f, "[ ");
if (ls.size() > 0) {
logLit(f, ls[0]);
- for (int i = 1; i < ls.size(); i++) {
+ for (uint32_t i = 1; i < ls.size(); i++) {
fprintf(f, ", ");
logLit(f, ls[i]);
}
CryptoMiniSat
-SVN revision: 614
-GIT revision: 7c6e2b5d2a1d4da60a0d70a3f0745c69f12d8ed2
+SVN revision: 656
+GIT revision: 87b9139cb43d296de0bd680226607ee7f3e3e755
VarReplacer::VarReplacer(Solver *_S) :
replacedLits(0)
+ , lastReplacedLits(0)
, replacedVars(0)
, lastReplacedVars(0)
, addedNewClause(false)
VarReplacer::~VarReplacer()
{
- for (uint i = 0; i < clauses.size(); i++)
+ for (uint i = 0; i != clauses.size(); i++)
free(clauses[i]);
}
replace_set(S->xorclauses, true);
replace_set(S->conglomerate->getCalcAtFinish(), false);
- for (uint i = 0; i < clauses.size(); i++)
+ for (uint i = 0; i != clauses.size(); i++)
S->removeClause(*clauses[i]);
clauses.clear();
if (S->verbosity >=1)
- printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits);
+ printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars-lastReplacedVars, replacedLits-lastReplacedLits);
addedNewClause = false;
lastReplacedVars = replacedVars;
+ lastReplacedLits = replacedLits;
if (S->ok)
S->ok = (S->propagate() == NULL);
uint origSize = c.size();
std::sort(c.getData(), c.getData() + c.size());
Lit p;
- int i, j;
- for (i = j = 0, p = lit_Undef; i < c.size(); i++) {
+ uint32_t i, j;
+ for (i = j = 0, p = lit_Undef; i != c.size(); i++) {
c[i] = c[i].unsign();
if (c[i] == p) {
//added, but easily removed
#ifdef VERBOSE_DEBUG
cout << "xor-clause after replacing: ";
- c.plain_print();
+ c.plainPrint();
#endif
switch (c.size()) {
bool satisfied = false;
std::sort(c.getData(), c.getData() + c.size());
Lit p;
- int i, j;
+ uint32_t i, j;
const uint origSize = c.size();
- for (i = j = 0, p = lit_Undef; i < origSize; i++) {
+ for (i = j = 0, p = lit_Undef; i != origSize; i++) {
if (S->value(c[i]) == l_True || c[i] == ~p) {
satisfied = true;
break;
bool val = (S->assigns[it->var()] == l_False);
S->uncheckedEnqueue(Lit(i, val ^ it->sign()));
} else {
- assert(S->assigns[i].getBool() == S->assigns[it->var()].getBool() ^ it->sign());
+ assert(S->assigns[i].getBool() == (S->assigns[it->var()].getBool() ^ it->sign()));
}
}
}
vec<Clause*> clauses;
uint replacedLits;
+ uint lastReplacedLits;
uint replacedVars;
uint lastReplacedVars;
bool addedNewClause;
#include "Solver.h"
#include "VarReplacer.h"
#include "ClauseCleaner.h"
+#include "time_mem.h"
namespace MINISAT
{
using std::make_pair;
-XorFinder::XorFinder(Solver* _S, vec<Clause*>& _cls) :
+XorFinder::XorFinder(Solver* _S, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
cls(_cls)
+ , type(_type)
, S(_S)
{
}
-uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSize)
+uint XorFinder::doNoPart(const uint minSize, const uint maxSize)
{
- S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses);
+ uint sumLengths = 0;
+ double time = cpuTime();
+
+ S->clauseCleaner->cleanClauses(cls, type);
toRemove.clear();
toRemove.resize(cls.size(), false);
}
uint found = findXors(sumLengths);
+
+ if (S->verbosity >=1)
+ printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, found, (double)sumLengths/(double)found);
+
if (found > 0) {
clearToRemove();
for (ClauseTable::iterator it = begin; it != end; it++)
if (impairSigns(*it->first) == impair){
#ifdef VERBOSE_DEBUG
- it->first->plain_print();
+ it->first->plainPrint();
#endif
toRemove[it->second] = true;
S->removeClause(*it->first);
#ifdef VERBOSE_DEBUG
XorClause* x = XorClause_new(lits, impair, old_group);
cout << "- Final 2-long xor-clause: ";
- x->plain_print();
+ x->plainPrint();
free(x);
#endif
break;
#ifdef VERBOSE_DEBUG
cout << "- Final xor-clause: ";
- x->plain_print();
+ x->plainPrint();
#endif
}
}
#include "Clause.h"
#include <sys/types.h>
#include "VarReplacer.h"
+#include "ClauseCleaner.h"
namespace MINISAT
{
{
public:
- XorFinder(Solver* S, vec<Clause*>& cls);
- uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize);
+ XorFinder(Solver* S, vec<Clause*>& cls, ClauseCleaner::ClauseSetType _type);
+ uint doNoPart(const uint minSize, const uint maxSize);
private:
typedef vector<pair<Clause*, uint> > ClauseTable;
void clearToRemove();
vec<Clause*>& cls;
+ ClauseCleaner::ClauseSetType type;
bool clauseEqual(const Clause& c1, const Clause& c2) const;
bool impairSigns(const Clause& c) const;
#define DYNAMICNBLEVEL
#define UPDATEVARACTIVITY
#define PERCENTAGEPERFORMREPLACE 0.03
+#define STATS_NEEDED
+#define PERCENTAGECLEANCLAUSES 0.005
+#define MAX_CLAUSENUM_XORFIND 1000000
+#define BINARY_TO_XOR_APPROX 10.0
+//#define VERBOSE_DEBUG_XOR
+//#define VERBOSE_DEBUG
#ifndef Alg_h
#define Alg_h
-
-namespace MINISAT
-{
+#include "stdint.h"
//=================================================================================================
// Useful functions on vectors
+namespace MINISAT
+{
-#if 1
template<class V, class T>
static inline void remove(V& ts, const T& t)
{
- int j = 0;
+ uint32_t j = 0;
for (; j < ts.size() && ts[j] != t; j++);
assert(j < ts.size());
for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
ts.pop();
}
-#else
+
template<class V, class T>
-static inline void remove(V& ts, const T& t)
+static inline void removeW(V& ts, const T& t)
{
- int j = 0;
- for (; j < ts.size() && ts[j] != t; j++);
+ uint32_t j = 0;
+ for (; j < ts.size() && ts[j].clause != t; j++);
assert(j < ts.size());
- ts[j] = ts.last();
+ for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
ts.pop();
}
-#endif
template<class V, class T>
static inline bool find(V& ts, const T& t)
{
- int j = 0;
+ uint32_t j = 0;
for (; j < ts.size() && ts[j] != t; j++);
return j < ts.size();
}
+template<class V, class T>
+static inline bool findW(V& ts, const T& t)
+{
+ uint32_t j = 0;
+ for (; j < ts.size() && ts[j].clause != t; j++);
+ return j < ts.size();
+}
+
};
#endif
#include "Vec.h"
#include "string.h"
+#include <stdint.h>
+#define UINT32_MAX ((uint32_t)-1)
namespace MINISAT
{
template<class Comp>
class Heap {
Comp lt;
- vec<int> heap; // heap of ints
- vec<int> indices; // int -> index in heap
+ vec<uint32_t> heap; // heap of ints
+ vec<uint32_t> indices; // int -> index in heap
// Index "traversal" functions
- static inline int left (int i) { return i*2+1; }
- static inline int right (int i) { return (i+1)*2; }
- static inline int parent(int i) { return (i-1) >> 1; }
+ static inline uint32_t left (uint32_t i) { return i*2+1; }
+ static inline uint32_t right (uint32_t i) { return (i+1)*2; }
+ static inline uint32_t parent(uint32_t i) { return (i-1) >> 1; }
inline void percolateUp(int i)
{
- int x = heap[i];
+ uint32_t x = heap[i];
while (i != 0 && lt(x, heap[parent(i)])){
heap[i] = heap[parent(i)];
indices[heap[i]] = i;
}
- inline void percolateDown(int i)
+ inline void percolateDown(uint32_t i)
{
- int x = heap[i];
+ uint32_t x = heap[i];
while (left(i) < heap.size()){
int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
if (!lt(heap[child], x)) break;
}
- bool heapProperty (int i) const {
+ bool heapProperty (uint32_t i) const {
return i >= heap.size()
|| ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
int size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
- bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
- int operator[](int index) const { assert(index < heap.size()); return heap[index]; }
+ bool inHeap (uint32_t n) const { return n < indices.size() && indices[n] != UINT32_MAX; }
+ int operator[](uint32_t index) const { assert(index < heap.size()); return heap[index]; }
- void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); }
+ void decrease (uint32_t n) { assert(inHeap(n)); percolateUp(indices[n]); }
// RENAME WHEN THE DEPRECATED INCREASE IS REMOVED.
- void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+ void increase_ (uint32_t n) { assert(inHeap(n)); percolateDown(indices[n]); }
- void insert(int n)
+ void insert(uint32_t n)
{
- indices.growTo(n+1, -1);
+ indices.growTo(n+1, UINT32_MAX);
assert(!inHeap(n));
indices[n] = heap.size();
int x = heap[0];
heap[0] = heap.last();
indices[heap[0]] = 0;
- indices[x] = -1;
+ indices[x] = UINT32_MAX;
heap.pop();
if (heap.size() > 1) percolateDown(0);
return x;
void clear(bool dealloc = false)
{
- for (int i = 0; i < heap.size(); i++)
- indices[heap[i]] = -1;
-#ifdef NDEBUG
- for (int i = 0; i < indices.size(); i++)
- assert(indices[i] == -1);
+ for (uint32_t i = 0; i != heap.size(); i++)
+ indices[heap[i]] = UINT32_MAX;
+#ifndef NDEBUG
+ for (uint32_t i = 0; i != indices.size(); i++)
+ assert(indices[i] == UINT32_MAX);
#endif
heap.clear(dealloc);
}
// Fool proof variant of insert/decrease/increase
- void update (int n)
+ void update (uint32_t n)
{
if (!inHeap(n))
insert(n);
// *** this could probaly be replaced with a more general "buildHeap(vec<int>&)" method ***
template <class F>
void filter(const F& filt) {
- int i,j;
- for (i = j = 0; i < heap.size(); i++)
+ uint32_t i,j;
+ for (i = j = 0; i != heap.size(); i++)
if (filt(heap[i])){
heap[j] = heap[i];
indices[heap[i]] = j++;
}else
- indices[heap[i]] = -1;
+ indices[heap[i]] = UINT32_MAX;
heap.shrink(i - j);
for (int i = heap.size() / 2 - 1; i >= 0; i--)
// COMPAT: should be removed
- void setBounds (int n) { }
- void increase (int n) { decrease(n); }
+ void setBounds (uint32_t n) { }
+ void increase (uint32_t n) { decrease(n); }
int getmin () { return removeMin(); }
};
+++ /dev/null
-/******************************************************************************************[Sort.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-
-#ifndef Sort_h
-#define Sort_h
-#include "Vec.h"
-
-namespace MINISAT
-{
-//=================================================================================================
-// Some sorting algorithms for vec's
-
-
-template<class T>
-struct LessThan_default {
- bool operator () (T x, T y) { return x < y; }
-};
-
-
-template <class T, class LessThan>
-void selectionSort(T* array, int size, LessThan lt)
-{
- int i, j, best_i;
- T tmp;
-
- for (i = 0; i < size-1; i++){
- best_i = i;
- for (j = i+1; j < size; j++){
- if (lt(array[j], array[best_i]))
- best_i = j;
- }
- tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
- }
-}
-template <class T> static inline void selectionSort(T* array, int size) {
- selectionSort(array, size, LessThan_default<T>()); }
-
-template <class T, class LessThan>
-void sort(T* array, int size, LessThan lt)
-{
- if (size <= 15)
- selectionSort(array, size, lt);
-
- else{
- T pivot = array[size / 2];
- T tmp;
- int i = -1;
- int j = size;
-
- for(;;){
- do i++; while(lt(array[i], pivot));
- do j--; while(lt(pivot, array[j]));
-
- if (i >= j) break;
-
- tmp = array[i]; array[i] = array[j]; array[j] = tmp;
- }
-
- sort(array , i , lt);
- sort(&array[i], size-i, lt);
- }
-}
-template <class T> static inline void sort(T* array, int size) {
- sort(array, size, LessThan_default<T>()); }
-
-
-//=================================================================================================
-// For 'vec's:
-
-
-template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
- sort(v.getData(), v.size(), lt); }
-template <class T> void sort(vec<T>& v) {
- sort(v, LessThan_default<T>()); }
-
-};
-//=================================================================================================
-#endif
#include <cstdlib>
#include <cassert>
#include <new>
+#include <stdint.h>
namespace MINISAT
{
template<class T>
class vec {
T* data;
- int sz;
- int cap;
+ uint32_t sz;
+ uint32_t cap;
- void init(int size, const T& pad);
- void grow(int min_cap);
+ void init(uint32_t size, const T& pad);
+ void grow(uint32_t min_cap);
// Don't allow copying (error prone):
vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
vec (vec<T>& other) { assert(0); }
- static inline int imin(int x, int y) {
- int mask = (x-y) >> (sizeof(int)*8-1);
- return (x&mask) + (y&(~mask)); }
-
- static inline int imax(int x, int y) {
+ static inline uint32_t imax(int x, int y) {
int mask = (y-x) >> (sizeof(int)*8-1);
return (x&mask) + (y&(~mask)); }
public:
// Types:
- typedef int Key;
+ typedef uint32_t Key;
typedef T Datum;
// Constructors:
- vec(void) : data(NULL) , sz(0) , cap(0) { }
- vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
- vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
- vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()')
+ vec(void) : data(NULL) , sz(0) , cap(0) { }
+ vec(uint32_t size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
+ vec(uint32_t size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
+ vec(T* array, uint32_t size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()')
~vec(void) { clear(true); }
// Ownership of underlying array:
T* getData() {return data; }
// Size operations:
- int size (void) const { return sz; }
- void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
- void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; }
+ uint32_t size (void) const { return sz; }
+ void shrink (uint32_t nelems) { assert(nelems <= sz); for (uint32_t i = 0; i != nelems; i++) sz--, data[sz].~T(); }
+ void shrink_(uint32_t nelems) { assert(nelems <= sz); sz -= nelems; }
void pop (void) { sz--, data[sz].~T(); }
- void growTo (int size);
- void growTo (int size, const T& pad);
+ void growTo (uint32_t size);
+ void growTo (uint32_t size, const T& pad);
void clear (bool dealloc = false);
- void capacity (int size) { grow(size); }
+ void capacity (uint32_t size) { grow(size); }
// Stack interface:
-#if 1
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)); } new (&data[sz]) T(elem); 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; }
-#else
- void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; }
- void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
-#endif
const T& last (void) const { return data[sz-1]; }
T& last (void) { return data[sz-1]; }
// Vector interface:
- const T& operator [] (int index) const { return data[index]; }
- T& operator [] (int index) { return data[index]; }
+ const T& operator [] (uint32_t index) const { return data[index]; }
+ T& operator [] (uint32_t index) { return data[index]; }
// Duplicatation (preferred instead):
- void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); }
+ void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (uint32_t i = 0; i != sz; i++) new (©[i]) T(data[i]); }
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
};
template<class T>
-void vec<T>::grow(int min_cap) {
+void vec<T>::grow(uint32_t min_cap) {
if (min_cap <= cap) return;
if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
else do cap = (cap*3+1) >> 1; while (cap < min_cap);
data = (T*)realloc(data, cap * sizeof(T)); }
template<class T>
-void vec<T>::growTo(int size, const T& pad) {
+void vec<T>::growTo(uint32_t size, const T& pad) {
if (sz >= size) return;
grow(size);
- for (int i = sz; i < size; i++) new (&data[i]) T(pad);
+ for (uint32_t i = sz; i != size; i++) new (&data[i]) T(pad);
sz = size; }
template<class T>
-void vec<T>::growTo(int size) {
+void vec<T>::growTo(uint32_t size) {
if (sz >= size) return;
grow(size);
- for (int i = sz; i < size; i++) new (&data[i]) T();
+ for (uint32_t i = sz; i != size; i++) new (&data[i]) T();
sz = size; }
template<class T>
void vec<T>::clear(bool dealloc) {
if (data != NULL){
- for (int i = 0; i < sz; i++) data[i].~T();
+ for (uint32_t i = 0; i != sz; i++) data[i].~T();
sz = 0;
if (dealloc) free(data), data = NULL, cap = 0; } }
projects / francis / stp.git / commitdiff