From: msoos Date: Wed, 16 Dec 2009 16:11:49 +0000 (+0000) Subject: Updating CryptoMiniSat2 to r656 X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cf8ac7c9e79266c699d689646039f2092627123a;p=francis%2Fstp.git Updating CryptoMiniSat2 to r656 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@520 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index a95ffad..6983b96 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -57,8 +57,7 @@ protected: 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; @@ -83,11 +82,11 @@ public: 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); @@ -127,8 +126,8 @@ public: 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; } @@ -151,7 +150,7 @@ public: } 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; @@ -181,11 +180,6 @@ public: { 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()); @@ -205,10 +199,6 @@ public: 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); @@ -253,9 +243,9 @@ inline Lit Clause::subsumes(const Clause& other) const 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]){ @@ -278,6 +268,14 @@ class WatchedBin { Lit impliedLit; Clause *clause; }; + +class Watched { + public: + Watched(Clause *_clause, Lit _blockedLit) : blockedLit(_blockedLit), clause(_clause) {}; + Lit blockedLit; + Clause *clause; +}; + }; #endif //CLAUSE_H diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index 5a376a7..1a9abcc 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -48,7 +48,7 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, con else cs[j++] = cs[i]; } - cs.shrink(i - j); + cs.shrink_(i - j); lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); } @@ -69,7 +69,7 @@ void ClauseCleaner::removeSatisfied(vec& cs, ClauseSetType type, const else cs[j++] = cs[i]; } - cs.shrink(i - j); + cs.shrink_(i - j); lastNumUnitarySat[type] = solver.get_unitary_learnts_num(); } @@ -97,8 +97,13 @@ inline const bool ClauseCleaner::cleanClause(Clause& c) 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; } @@ -187,13 +192,14 @@ inline const bool ClauseCleaner::cleanClause(XorClause& c) 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; @@ -202,7 +208,7 @@ bool ClauseCleaner::satisfied(const Clause& c) const 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(); diff --git a/src/sat/cryptominisat2/ClauseCleaner.h b/src/sat/cryptominisat2/ClauseCleaner.h index d59948e..de05c74 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.h +++ b/src/sat/cryptominisat2/ClauseCleaner.h @@ -50,7 +50,7 @@ class ClauseCleaner 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); diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index 0694463..f3040a1 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -158,7 +158,7 @@ uint Conglomerate::conglomerateXors() #ifdef VERBOSE_DEBUG cout << "- Removing: "; - x.plain_print(); + x.plainPrint(); cout << "Adding var " << var+1 << " to calcAtFinish" << endl; #endif @@ -176,7 +176,7 @@ uint Conglomerate::conglomerateXors() #ifdef VERBOSE_DEBUG cout << "- Removing: "; - x.plain_print(); + x.plainPrint(); #endif const uint old_group = x.group; @@ -239,7 +239,7 @@ bool Conglomerate::dealWithNewClause(vec& ps, const bool inverted, const ui #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 @@ -254,7 +254,7 @@ bool Conglomerate::dealWithNewClause(vec& ps, const bool inverted, const ui #ifdef VERBOSE_DEBUG cout << "- Adding: "; - newX->plain_print(); + newX->plainPrint(); #endif S->xorclauses.push(newX); @@ -347,7 +347,7 @@ void Conglomerate::doCalcAtFinish() #ifdef VERBOSE_DEBUG cout << "doCalcFinish for xor-clause:"; - S->printClause(c); cout << endl; + c.plainPrint(); #endif bool final = c.xor_clause_inverted(); @@ -396,7 +396,7 @@ void Conglomerate::addRemovedClauses() XorClause& c = *calcAtFinish[i]; #ifdef VERBOSE_DEBUG cout << "readding already removed (conglomerated) clause: "; - c.plain_print(); + c.plainPrint(); #endif ps.clear(); diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index bfbd7a5..9dc5748 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -37,7 +37,7 @@ using namespace MINISAT; ostream& operator << (ostream& os, const vec& 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 << " "; } @@ -132,7 +132,7 @@ uint Gaussian::select_columnorder(vector& var_to_col, matrixset& origM 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 @@ -215,19 +215,18 @@ void Gaussian::fill_matrix(matrixset& origMat) 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++; } } @@ -246,24 +245,22 @@ void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint col) #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); } } } @@ -418,7 +415,7 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) 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); } @@ -445,18 +442,16 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) 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) { @@ -465,12 +460,11 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_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()); @@ -482,18 +476,16 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row) //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; //} @@ -544,11 +536,13 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matri { 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; @@ -556,12 +550,14 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matri 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(); @@ -569,7 +565,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matri 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; @@ -599,7 +595,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint #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); } @@ -611,7 +607,6 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint #endif m.num_rows = last_row; m.matrix.resizeNumRows(m.num_rows); - m.varset.resizeNumRows(m.num_rows); gaussian_ret ret = nothing; @@ -692,7 +687,7 @@ void Gaussian::analyse_confl(const matrixset& m, const uint row, uint& maxlevel, 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]; @@ -748,37 +743,31 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row 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; } @@ -823,22 +812,19 @@ llbool Gaussian::find_truths(vec& learnt_clause, int& conflictC) } 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; @@ -862,7 +848,7 @@ void Gaussian::print_matrix_row(const T& row) const 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 @@ -880,7 +866,7 @@ void Gaussian::print_matrix_row_with_assigns(const T& row) const } 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) @@ -926,8 +912,8 @@ void Gaussian::reset_stats() 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; } @@ -938,7 +924,7 @@ bool Gaussian::check_no_conflict(matrixset& m) const 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)"; @@ -956,13 +942,13 @@ void Gaussian::print_last_one_in_cols(matrixset& m) const 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; @@ -974,7 +960,7 @@ const bool Gaussian::check_last_one_in_cols(matrixset& m) const 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; } @@ -990,8 +976,8 @@ const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMat 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; @@ -1019,7 +1005,7 @@ const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMat 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); } @@ -1094,7 +1080,7 @@ void Gaussian::set_disabled(const bool toset) 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; } diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h index a6f5eb6..309345d 100644 --- a/src/sat/cryptominisat2/Gaussian.h +++ b/src/sat/cryptominisat2/Gaussian.h @@ -61,7 +61,7 @@ public: void set_disabled(const bool toset); //functions used throughout the Solver - void canceling(const int sublevel); + void canceling(const uint sublevel); protected: Solver& solver; @@ -82,7 +82,6 @@ protected: { 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 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) @@ -173,7 +172,7 @@ inline bool Gaussian::should_check_gauss(const uint decisionlevel, const uint st && decisionlevel < config.decision_until); } -inline void Gaussian::canceling(const int sublevel) +inline void Gaussian::canceling(const uint sublevel) { if (disabled) return; @@ -186,7 +185,7 @@ inline void Gaussian::canceling(const int sublevel) 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() diff --git a/src/sat/cryptominisat2/GaussianConfig.h b/src/sat/cryptominisat2/GaussianConfig.h index 1994f1a..595dff4 100644 --- a/src/sat/cryptominisat2/GaussianConfig.h +++ b/src/sat/cryptominisat2/GaussianConfig.h @@ -32,11 +32,7 @@ class GaussianConfig GaussianConfig() : only_nth_gauss_save(2) , decision_until(0) - , starts_from(3) - { - } - - ~GaussianConfig() + , starts_from(2) { } diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index 46e30e1..857a481 100644 --- a/src/sat/cryptominisat2/Logger.cpp +++ b/src/sat/cryptominisat2/Logger.cpp @@ -60,6 +60,7 @@ Logger::Logger(int& _verbosity) : , verbosity(_verbosity) , begin_called(false) + , proofStarts(0) { runid /= 10; runid = time(NULL) % 10000; @@ -155,7 +156,6 @@ void Logger::first_begin() if (begin_called) return; - begin_called = true; begin(); } @@ -164,7 +164,7 @@ void Logger::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); @@ -199,10 +199,13 @@ void Logger::conflict(const confl_type type, const uint goback_level, const uint 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"); @@ -242,34 +245,36 @@ template void Logger::conflict(const confl_type type, const uint goback_level, c template void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const vec& 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); @@ -278,20 +283,8 @@ void Logger::propagation(const Lit lit, const prop_type type, const uint group) 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: @@ -303,20 +296,14 @@ void Logger::propagation(const Lit lit, const prop_type type, const uint group) 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()]++; @@ -330,6 +317,7 @@ void Logger::propagation(const Lit lit, const prop_type type, const uint group) // Ending of a restart iteration void Logger::end(const finish_type finish) { + first_begin(); assert(!(proof == NULL && proof_graph_on)); if (proof_graph_on) { @@ -341,9 +329,6 @@ void Logger::end(const finish_type finish) 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; @@ -362,6 +347,9 @@ void Logger::end(const finish_type finish) if (finish == restarting) reset_statistics(); } + + if (model_found || unsat_model_found) + begin_called = false; } void Logger::print_footer() const @@ -447,7 +435,7 @@ void Logger::print_confl_order() const void Logger::print_times_var_guessed() const { vector > 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()) { @@ -692,8 +680,8 @@ void Logger::print_leearnt_clause_graph_distrib(const uint maximum, const map= i) cout << "+"; + for (uint i2 = 0; i2 != no_slices; i2++) { + if (slices[i2]/hslice >= (uint)i) cout << "+"; else cout << " "; } cout << "|" << endl; @@ -789,7 +777,7 @@ void Logger::print_advanced_stats() const 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); @@ -864,7 +852,7 @@ void Logger::reset_statistics() 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(); } }; diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h index 19bac10..b7d5ad9 100644 --- a/src/sat/cryptominisat2/Logger.h +++ b/src/sat/cryptominisat2/Logger.h @@ -55,15 +55,14 @@ public: 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 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); @@ -156,7 +155,7 @@ private: 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; @@ -165,6 +164,7 @@ private: void first_begin(); bool begin_called; + uint proofStarts; }; }; diff --git a/src/sat/cryptominisat2/PackedMatrix.h b/src/sat/cryptominisat2/PackedMatrix.h index 854f30b..0edf1e0 100644 --- a/src/sat/cryptominisat2/PackedMatrix.h +++ b/src/sat/cryptominisat2/PackedMatrix.h @@ -48,8 +48,8 @@ public: 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() @@ -60,9 +60,9 @@ public: 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; @@ -83,34 +83,51 @@ public: //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 @@ -118,30 +135,30 @@ public: 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 @@ -166,72 +183,25 @@ public: 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 { diff --git a/src/sat/cryptominisat2/PackedRow.cpp b/src/sat/cryptominisat2/PackedRow.cpp index 9f09e7a..22c88ca 100644 --- a/src/sat/cryptominisat2/PackedRow.cpp +++ b/src/sat/cryptominisat2/PackedRow.cpp @@ -24,7 +24,7 @@ std::ostream& operator << (std::ostream& os, const PackedRow& m) 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; } @@ -84,7 +84,7 @@ uint PackedRow::popcnt(const uint from) const void PackedRow::fill(vec& tmp_clause, const vec& assigns, const vector& col_to_var_original) const { - bool final = xor_clause_inverted; + bool final = !is_true_internal; tmp_clause.clear(); uint col = 0; diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h index f794a04..0fa9905 100644 --- a/src/sat/cryptominisat2/PackedRow.h +++ b/src/sat/cryptominisat2/PackedRow.h @@ -66,16 +66,29 @@ public: 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; @@ -83,9 +96,9 @@ public: 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; @@ -103,30 +116,16 @@ public: 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 @@ -149,9 +148,9 @@ public: 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) @@ -167,13 +166,41 @@ public: 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--; } } @@ -199,7 +226,7 @@ public: setBit(toset_var); } - xor_clause_inverted = v.xor_clause_inverted(); + is_true_internal = !v.xor_clause_inverted(); } void fill(vec& tmp_clause, const vec& assigns, const vector& col_to_var_original) const; @@ -217,17 +244,17 @@ public: 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); diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp index afeb9c5..960c3e7 100644 --- a/src/sat/cryptominisat2/RestartTypeChooser.cpp +++ b/src/sat/cryptominisat2/RestartTypeChooser.cpp @@ -27,7 +27,7 @@ using namespace MINISAT; RestartTypeChooser::RestartTypeChooser(const Solver* const _S) : S(_S) , topX(100) - , limit(40) + , limit(30) { } @@ -37,7 +37,8 @@ const RestartType RestartTypeChooser::choose() 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++; } @@ -68,12 +69,13 @@ const double RestartTypeChooser::avg() const void RestartTypeChooser::calcHeap() { - firstVars.resize(100); + firstVars.resize(topX); #ifdef VERBOSE_DEBUG std::cout << "First vars:" << std::endl; #endif Heap 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 diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index e3fc0bf..acae0cb 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -20,7 +20,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA **************************************************************************************************/ #include "Solver.h" -#include "Sort.h" #include #include #include @@ -65,9 +64,9 @@ Solver::Solver() : // 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) @@ -84,8 +83,10 @@ Solver::Solver() : , 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) @@ -94,16 +95,19 @@ Solver::Solver() : 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; @@ -139,8 +143,11 @@ Var Solver::newVar(bool sign, bool dvar) 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"); @@ -158,23 +165,26 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro } 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(); @@ -189,21 +199,17 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro 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: { @@ -234,29 +240,31 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) 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) @@ -265,14 +273,10 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) 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); @@ -293,8 +297,7 @@ void Solver::attachClause(XorClause& c) 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) @@ -307,8 +310,8 @@ 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(); @@ -324,8 +327,7 @@ void Solver::detachClause(const XorClause& c) 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) @@ -359,10 +361,10 @@ void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint ori 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; @@ -376,8 +378,8 @@ void Solver::detachModifiedClause(const Var var1, const Var var2, const uint ori 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). @@ -405,7 +407,7 @@ void Solver::cancelUntil(int level) } 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 @@ -572,7 +574,7 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int // 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++) @@ -604,8 +606,8 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int 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]; @@ -616,7 +618,7 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int 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; @@ -627,7 +629,7 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int #ifdef UPDATEVARACTIVITY if (lastDecisionLevel.size() > 0) { - for(int i = 0; iactivity() < nbLevels) varBumpActivity(lastDecisionLevel[i].var()); } @@ -635,7 +637,8 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int } #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) } @@ -661,7 +664,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) 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; @@ -726,6 +729,11 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) reason [v] = from; polarity[p.var()] = p.sign(); trail.push(p); + + #ifdef STATS_NEEDED + if (dynamic_behaviour_analysis) + logger.propagation(p, from); + #endif } @@ -751,8 +759,8 @@ Clause* Solver::propagate(const bool xor_as_well) while (qhead < trail.size()) { Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. - vec& ws = watches[p.toInt()]; - Clause **i, **j, **end; + vec& ws = watches[p.toInt()]; + Watched *i, *j, *end; num_props++; //First propagate binary clauses @@ -762,8 +770,6 @@ Clause* Solver::propagate(const bool xor_as_well) 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; } @@ -775,7 +781,13 @@ Clause* Solver::propagate(const bool xor_as_well) #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); @@ -786,20 +798,24 @@ Clause* Solver::propagate(const bool xor_as_well) // 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(); @@ -808,8 +824,6 @@ Clause* Solver::propagate(const bool xor_as_well) *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++; @@ -831,7 +845,7 @@ Clause* Solver::propagate(const bool xor_as_well) FoundWatch: ; } - ws.shrink(i - j); + ws.shrink_(i - j); //Finally, propagate XOR-clauses if (xor_as_well && !confl) confl = propagate_xors(p); @@ -911,8 +925,6 @@ Clause* Solver::propagate_xors(const Lit& 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 @@ -974,11 +986,11 @@ struct reduceDB_lt { 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 @@ -987,7 +999,7 @@ void Solver::reduceDB() for (; i < learnts.size(); i++) { learnts[j++] = learnts[i]; } - learnts.shrink(i - j); + learnts.shrink_(i - j); } const vec& Solver::get_learnts() const @@ -997,7 +1009,7 @@ const vec& Solver::get_learnts() const const vec& Solver::get_sorted_learnts() { - sort(learnts, reduceDB_lt()); + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt()); return learnts; } @@ -1005,7 +1017,7 @@ const vector Solver::get_unitary_learnts() const { vector 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]); } @@ -1021,11 +1033,11 @@ void Solver::dump_sorted_learnts(const char* file) } 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); } @@ -1050,9 +1062,6 @@ lbool Solver::simplify() assert(decisionLevel() == 0); if (!ok || propagate() != NULL) { - if (dynamic_behaviour_analysis) { - logger.end(Logger::unsat_model_found); - } ok = false; return l_False; } @@ -1062,10 +1071,18 @@ lbool Solver::simplify() } // 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: @@ -1074,10 +1091,6 @@ lbool Solver::simplify() 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; } @@ -1140,9 +1153,6 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) nbDecisionLevelHistory.fastclear(); progress_estimate = progressEstimate(); cancelUntil(0); - if (dynamic_behaviour_analysis) { - logger.end(Logger::restarting); - } return l_Undef; } break; @@ -1150,8 +1160,6 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { progress_estimate = progressEstimate(); cancelUntil(0); - if (dynamic_behaviour_analysis) - logger.end(Logger::restarting); return l_Undef; } break; @@ -1159,9 +1167,6 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) // 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; } @@ -1179,12 +1184,8 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) 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; @@ -1197,21 +1198,14 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC) 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; } @@ -1230,12 +1224,8 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf 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++; @@ -1244,8 +1234,10 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf 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 @@ -1259,11 +1251,6 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf //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 @@ -1272,17 +1259,16 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf //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(); @@ -1295,7 +1281,7 @@ double Solver::progressEstimate() const 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); @@ -1368,16 +1354,11 @@ inline void Solver::performStepsBeforeSolve() 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(); @@ -1454,40 +1435,26 @@ lbool Solver::solve(const vec& assumps) 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]; @@ -1501,7 +1468,7 @@ lbool Solver::solve(const vec& assumps) 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 @@ -1509,13 +1476,25 @@ lbool Solver::solve(const vec& assumps) 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;isize(),learnts[i]->activity(), @@ -1537,14 +1516,14 @@ bool Solver::verifyXorClauses(const vec& cs) const 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 @@ -1565,7 +1544,7 @@ bool Solver::verifyXorClauses(const vec& cs) const 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) @@ -1592,10 +1571,10 @@ void Solver::checkLiteralCount() { // 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) { @@ -1604,5 +1583,43 @@ void Solver::checkLiteralCount() } } +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(); + } +} + }; diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 4ab8561..ec75bce 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -59,9 +59,6 @@ class XorFinder; class FindUndef; class ClauseCleaner; -//#define VERBOSE_DEBUG_XOR -//#define VERBOSE_DEBUG - #ifdef VERBOSE_DEBUG using std::cout; using std::endl; @@ -113,10 +110,10 @@ public: 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) // @@ -149,12 +146,12 @@ public: // 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& 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& get_learnts() const; //Get all learnt clauses that are >1 long const vector get_unitary_learnts() const; //return the set of unitary learnt clauses @@ -198,7 +195,7 @@ protected: vec freeLater; // List of xorclauses to free at the end (due to matrixes, they cannot be freed immediately) vec activity; // A heuristic measurement of the activity of a variable. double var_inc; // Amount to bump next variable with. - vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. vec > binwatches; vec assigns; // The current assignments @@ -214,9 +211,9 @@ protected: #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 assumptions; // Current set of assumptions provided to solve by the user. Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. @@ -224,10 +221,12 @@ protected: bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. bqueue 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 @@ -284,9 +283,8 @@ protected: // 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; @@ -301,11 +299,15 @@ protected: void chooseRestartType(const lbool& status, RestartTypeChooser& restartTypeChooser); void performStepsBeforeSolve(); - // Debug: + // Debug & etc: void printLit (const Lit l) const; void verifyModel (); bool verifyXorClauses (const vec& cs) const; void checkLiteralCount(); + void printStatHeader () const; + void printRestartStat () const; + void printEndSearchStat() const; + double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... }; @@ -326,7 +328,7 @@ inline void Solver::varBumpActivity(Var v) { 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; } @@ -356,7 +358,7 @@ inline void Solver::newDecisionLevel() 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(); } @@ -376,19 +378,19 @@ inline lbool Solver::modelValue (const Lit& p) const { 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(); } @@ -416,6 +418,7 @@ inline void Solver::setSeed (const uint32_t seed) { 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 @@ -426,12 +429,16 @@ inline void Solver::needProofGraph() 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) @@ -441,15 +448,15 @@ inline const uint Solver::get_unitary_learnts_num() const } template inline void Solver::removeWatchedCl(vec &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 inline void Solver::removeWatchedBinCl(vec &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]; @@ -458,14 +465,14 @@ inline void Solver::removeWatchedBinCl(vec &ws, const Clause *c) { template inline bool Solver::findWatchedCl(vec& 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 inline bool Solver::findWatchedBinCl(vec& ws, const Clause *c) { - int j = 0; + uint32_t j = 0; for (; j < ws.size() && ws[j].clause != c; j++); return j < ws.size(); } @@ -502,7 +509,7 @@ static inline void logLits(FILE* f, const vec& ls) 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]); } diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index ab0c398..6d08e9c 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,3 @@ CryptoMiniSat -SVN revision: 614 -GIT revision: 7c6e2b5d2a1d4da60a0d70a3f0745c69f12d8ed2 +SVN revision: 656 +GIT revision: 87b9139cb43d296de0bd680226607ee7f3e3e755 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index ba12931..731d702 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -35,6 +35,7 @@ namespace MINISAT VarReplacer::VarReplacer(Solver *_S) : replacedLits(0) + , lastReplacedLits(0) , replacedVars(0) , lastReplacedVars(0) , addedNewClause(false) @@ -44,7 +45,7 @@ VarReplacer::VarReplacer(Solver *_S) : VarReplacer::~VarReplacer() { - for (uint i = 0; i < clauses.size(); i++) + for (uint i = 0; i != clauses.size(); i++) free(clauses[i]); } @@ -88,15 +89,16 @@ void VarReplacer::performReplace() 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); @@ -140,8 +142,8 @@ const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, co 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 @@ -157,7 +159,7 @@ const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, co #ifdef VERBOSE_DEBUG cout << "xor-clause after replacing: "; - c.plain_print(); + c.plainPrint(); #endif switch (c.size()) { @@ -222,9 +224,9 @@ const bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const 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; @@ -322,7 +324,7 @@ void VarReplacer::extendModel() const 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())); } } } diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index c13f9ec..36f38fd 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -67,6 +67,7 @@ class VarReplacer vec clauses; uint replacedLits; + uint lastReplacedLits; uint replacedVars; uint lastReplacedVars; bool addedNewClause; diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index ba263fe..02ba026 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -23,6 +23,7 @@ along with this program. If not, see . #include "Solver.h" #include "VarReplacer.h" #include "ClauseCleaner.h" +#include "time_mem.h" namespace MINISAT { @@ -38,15 +39,19 @@ using std::endl; using std::make_pair; -XorFinder::XorFinder(Solver* _S, vec& _cls) : +XorFinder::XorFinder(Solver* _S, vec& _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); @@ -61,6 +66,10 @@ uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSiz } 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(); @@ -100,7 +109,7 @@ uint XorFinder::findXors(uint& sumLengths) 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); @@ -113,7 +122,7 @@ uint XorFinder::findXors(uint& sumLengths) #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; @@ -125,7 +134,7 @@ uint XorFinder::findXors(uint& sumLengths) #ifdef VERBOSE_DEBUG cout << "- Final xor-clause: "; - x->plain_print(); + x->plainPrint(); #endif } } diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h index 9ba3104..bee1e81 100644 --- a/src/sat/cryptominisat2/XorFinder.h +++ b/src/sat/cryptominisat2/XorFinder.h @@ -21,6 +21,7 @@ along with this program. If not, see . #include "Clause.h" #include #include "VarReplacer.h" +#include "ClauseCleaner.h" namespace MINISAT { @@ -33,8 +34,8 @@ class XorFinder { public: - XorFinder(Solver* S, vec& cls); - uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize); + XorFinder(Solver* S, vec& cls, ClauseCleaner::ClauseSetType _type); + uint doNoPart(const uint minSize, const uint maxSize); private: typedef vector > ClauseTable; @@ -105,6 +106,7 @@ class XorFinder void clearToRemove(); vec& cls; + ClauseCleaner::ClauseSetType type; bool clauseEqual(const Clause& c1, const Clause& c2) const; bool impairSigns(const Clause& c) const; diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index 7936493..d063651 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -23,3 +23,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #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 diff --git a/src/sat/cryptominisat2/mtl/Alg.h b/src/sat/cryptominisat2/mtl/Alg.h index 58fc50a..0e4d000 100644 --- a/src/sat/cryptominisat2/mtl/Alg.h +++ b/src/sat/cryptominisat2/mtl/Alg.h @@ -19,44 +19,50 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Alg_h #define Alg_h - -namespace MINISAT -{ +#include "stdint.h" //================================================================================================= // Useful functions on vectors +namespace MINISAT +{ -#if 1 template 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 -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 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 +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 diff --git a/src/sat/cryptominisat2/mtl/Heap.h b/src/sat/cryptominisat2/mtl/Heap.h index dcea08f..4857b13 100644 --- a/src/sat/cryptominisat2/mtl/Heap.h +++ b/src/sat/cryptominisat2/mtl/Heap.h @@ -22,6 +22,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" #include "string.h" +#include +#define UINT32_MAX ((uint32_t)-1) namespace MINISAT { @@ -33,18 +35,18 @@ namespace MINISAT template class Heap { Comp lt; - vec heap; // heap of ints - vec indices; // int -> index in heap + vec heap; // heap of ints + vec 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; @@ -55,9 +57,9 @@ class Heap { } - 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; @@ -70,7 +72,7 @@ class Heap { } - 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))); } @@ -86,18 +88,18 @@ class Heap { 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(); @@ -111,7 +113,7 @@ class Heap { 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; @@ -120,18 +122,18 @@ class Heap { 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); @@ -146,13 +148,13 @@ class Heap { // *** this could probaly be replaced with a more general "buildHeap(vec&)" method *** template 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--) @@ -168,8 +170,8 @@ class Heap { // 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(); } }; diff --git a/src/sat/cryptominisat2/mtl/Sort.h b/src/sat/cryptominisat2/mtl/Sort.h deleted file mode 100644 index 76f168f..0000000 --- a/src/sat/cryptominisat2/mtl/Sort.h +++ /dev/null @@ -1,94 +0,0 @@ -/******************************************************************************************[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 -struct LessThan_default { - bool operator () (T x, T y) { return x < y; } -}; - - -template -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 static inline void selectionSort(T* array, int size) { - selectionSort(array, size, LessThan_default()); } - -template -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 static inline void sort(T* array, int size) { - sort(array, size, LessThan_default()); } - - -//================================================================================================= -// For 'vec's: - - -template void sort(vec& v, LessThan lt) { - sort(v.getData(), v.size(), lt); } -template void sort(vec& v) { - sort(v, LessThan_default()); } - -}; -//================================================================================================= -#endif diff --git a/src/sat/cryptominisat2/mtl/Vec.h b/src/sat/cryptominisat2/mtl/Vec.h index a3c5fca..3e84bca 100644 --- a/src/sat/cryptominisat2/mtl/Vec.h +++ b/src/sat/cryptominisat2/mtl/Vec.h @@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include #include +#include namespace MINISAT { @@ -33,34 +34,30 @@ namespace MINISAT template 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& operator = (vec& other) { assert(0); return *this; } vec (vec& 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: @@ -69,64 +66,58 @@ public: 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& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } + void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (uint32_t i = 0; i != sz; i++) new (©[i]) T(data[i]); } void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } }; template -void vec::grow(int min_cap) { +void vec::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 -void vec::growTo(int size, const T& pad) { +void vec::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 -void vec::growTo(int size) { +void vec::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 void vec::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; } }