{
using namespace MINISAT;
-Conglomerate::Conglomerate(Solver *_S) :
- S(_S)
+Conglomerate::Conglomerate(Solver *_s) :
+ S(_s)
{}
Conglomerate::~Conglomerate()
namespace MINISAT
{
-FindUndef::FindUndef(Solver& _S) :
- S(_S)
+FindUndef::FindUndef(Solver& _s) :
+ S(_s)
, isPotentialSum(0)
{
dontLookAtClause.resize(S.clauses.size(), false);
uint num_xorclauses = 0;
for (uint32_t i = 0; i != xorclauses.size(); i++) {
#ifdef DEBUG_GAUSS
- assert(xorclauses[i]->mark() || !solver.satisfied(*xorclauses[i]));
+ assert(xorclauses[i]->mark() || !Solver.cpplauseCleaner->satisfied(*xorclauses[i]));
#endif
if (!xorclauses[i]->mark()) {
num_xorclauses++;
origMat.var_is_set.setZero();
origMat.col_to_var.clear();
- for (int i = solver.order_heap.size()-1; i >= 0 ; i--)
- //for inverse order:
- //for (int i = 0; i < order_heap.size() ; i++)
+ Heap<Solver::VarOrderLt> order_heap(solver.order_heap);
+ while (!order_heap.empty())
{
- Var v = solver.order_heap[i];
+ Var v = order_heap.removeMin();
if (var_to_col[v] == 1) {
#ifdef DEBUG_GAUSS
origMat.num_cols = origMat.col_to_var.size();
col_to_var_original = origMat.col_to_var;
changed_rows.resize(origMat.num_rows);
- changed_rows.setZero();
+ memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size());
origMat.last_one_in_col.resize(origMat.num_cols);
std::fill(origMat.last_one_in_col.begin(), origMat.last_one_in_col.end(), origMat.num_rows);
- origMat.past_the_end_last_one_in_col = origMat.num_cols;
+ origMat.first_one_in_row.resize(origMat.num_rows);
origMat.removeable_cols = 0;
origMat.least_column_changed = -1;
uint row_num = 0;
if (solver.assigns[var].getBool()) {
- for (uint end = m.last_one_in_col[col]; row_num != end && row_num != m.num_rows; ++this_row, row_num++) {
+ for (uint end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) {
if ((*this_row)[col]) {
- changed_rows.setBit(row_num);
+ changed_rows[row_num] = true;
(*this_row).invert_is_true();
(*this_row).clearBit(col);
}
}
} else {
- for (uint end = m.last_one_in_col[col]; row_num != end && row_num != m.num_rows; ++this_row, row_num++) {
+ for (uint end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) {
if ((*this_row)[col]) {
- changed_rows.setBit(row_num);
+ changed_rows[row_num] = true;
(*this_row).clearBit(col);
}
}
#ifdef DEBUG_GAUSS
bool c = false;
- for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.getSize(); r != end; ++r)
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = r + m.matrix.getSize(); r != end; ++r)
c |= (*r)[col];
assert(!c);
#endif
assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m));
#endif
- changed_rows.setZero();
+ memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size());
uint last = 0;
uint col = 0;
last = 0;
}
m.num_cols -= last;
- m.past_the_end_last_one_in_col = std::min(m.past_the_end_last_one_in_col, (uint16_t)m.num_cols);
#ifdef DEBUG_GAUSS
- check_matrix_against_varset(m.matrix, m.varset, m);
+ check_matrix_against_varset(m.matrix, m);
#endif
#ifdef VERBOSE_DEBUG
cout << "removeable cols:" << m.removeable_cols << endl;*/
}
+inline void Gaussian::update_last_one_in_col(matrixset& m)
+{
+ for (uint16_t* i = &m.last_one_in_col[0]+m.last_one_in_col.size()-1, *end = &m.last_one_in_col[0]-1; i != end && *i >= m.num_rows; i--)
+ *i = m.num_rows;
+}
+
Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
{
if (solver.decisionLevel() >= badlevel)
assert(level < matrix_sets.size());
cur_matrixset = matrix_sets[level];
}
+ update_last_one_in_col(cur_matrixset);
update_matrix_by_col_all(cur_matrixset);
messed_matrix_vars_since_reversal = false;
uint conflict_row = UINT_MAX;
uint last_row = eliminate(cur_matrixset, conflict_row);
#ifdef DEBUG_GAUSS
- check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset.varset, cur_matrixset);
+ check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset);
#endif
gaussian_ret ret;
} else {*/
ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl);
//}
+ #ifdef DEBUG_GAUSS
+ assert(ret == conflict || nothing_to_propagate(cur_matrixset));
+ #endif
if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) {
badlevel = solver.decisionLevel();
uint i = 0;
uint j = m.least_column_changed + 1;
+ PackedMatrix::iterator beginIt = m.matrix.beginMatrix();
+ PackedMatrix::iterator rowIt = m.matrix.beginMatrix();
+ #ifdef DEBUG_GAUSS
+ check_first_one_in_row(m, j);
+ #endif
+
if (j) {
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)
+ if (j-1 > m.first_one_in_row[m.num_rows-1])
until = m.num_rows;
- for (;i != until; i++) if (changed_rows[i] && m.matrix.getMatrixAt(i).popcnt_is_one())
+ for (;i != until; i++, ++rowIt) if (changed_rows[i] && (*rowIt).popcnt_is_one(m.first_one_in_row[i]))
propagatable_rows.push(i);
}
- if (j > m.past_the_end_last_one_in_col) {
+ #ifdef VERBOSE_DEBUG
+ cout << "At while() start: i,j = " << i << ", " << j << endl;
+ cout << "num_rows:" << m.num_rows << " num_cols:" << m.num_cols << endl;
+ #endif
+
+ if (j > m.num_cols) {
#ifdef VERBOSE_DEBUG
cout << "Going straight to finish" << endl;
#endif
goto finish;
}
- #ifdef VERBOSE_DEBUG
- cout << "At while() start: i,j = " << i << ", " << j << endl;
- #endif
-
#ifdef DEBUG_GAUSS
assert(i <= m.num_rows && j <= m.num_cols);
#endif
continue;
}
- 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);
+ PackedMatrix::iterator this_matrix_row = rowIt;
+ PackedMatrix::iterator end = beginIt + m.last_one_in_col[j];
for (; this_matrix_row != end; ++this_matrix_row) {
if ((*this_matrix_row)[j])
break;
}
- uint best_row = this_matrix_row - m.matrix.beginMatrix();
if (this_matrix_row != end) {
- 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) {
+ if (this_matrix_row != rowIt) {
#ifdef VERBOSE_DEBUG
no_exchanged++;
#endif
// conflict_row = i;
// return 0;
//}
- matrix_row_i.swapBoth(*this_matrix_row);
+ (*rowIt).swapBoth(*this_matrix_row);
}
#ifdef DEBUG_GAUSS
- assert(m.matrix[i].popcnt(j) == m.matrix[i].popcnt());
- assert(m.matrix[i][j]);
+ assert(m.matrix.getMatrixAt(i).popcnt(j) == m.matrix.getMatrixAt(i).popcnt());
+ assert(m.matrix.getMatrixAt(i)[j]);
#endif
- if (matrix_row_i.popcnt_is_one(j))
+ if ((*rowIt).popcnt_is_one(j))
propagatable_rows.push(i);
//Now A[i,j] will contain the old value of A[maxi,j];
number_of_row_additions++;
#endif
- (*this_matrix_row).xorBoth(matrix_row_i);
+ (*this_matrix_row).xorBoth(*rowIt);
//Would early abort, but would not find the best conflict (and would be expensive)
//if (it->is_true() &&it->isZero()) {
// conflict_row = i2;
// return 0;
//}
}
+ m.first_one_in_row[i] = j;
i++;
+ ++rowIt;
m.last_one_in_col[j] = i;
- } else
+ } else {
+ m.first_one_in_row[i] = j;
m.last_one_in_col[j] = i + 1;
+ }
j++;
}
-
- m.past_the_end_last_one_in_col = j;
finish:
assert(check_last_one_in_cols(m));
uint row = 0;
uint col = 0;
- for (; col < m.num_cols && row < m.num_rows && row < i && col < m.past_the_end_last_one_in_col; col++) {
- assert(m.matrix[row].popcnt() == m.matrix[row].popcnt(col));
- assert(!(m.col_to_var[col] == unassigned_var && m.matrix[row][col]));
- if (m.col_to_var[col] == unassigned_var || !m.matrix[row][col]) {
+ for (; col < m.num_cols && row < m.num_rows && row < i ; col++) {
+ assert(m.matrix.getMatrixAt(row).popcnt() == m.matrix.getMatrixAt(row).popcnt(col));
+ assert(!(m.col_to_var[col] == unassigned_var && m.matrix.getMatrixAt(row)[col]));
+ if (m.col_to_var[col] == unassigned_var || !m.matrix.getMatrixAt(row)[col]) {
#ifdef VERBOSE_DEBUG
cout << "row:" << row << " col:" << col << " m.last_one_in_col[col]-1: " << m.last_one_in_col[col]-1 << endl;
#endif
- assert(m.col_to_var[col] == unassigned_var || std::min(m.last_one_in_col[col]-1, (int)m.num_rows) == row);
+ assert(m.col_to_var[col] == unassigned_var || std::min((uint16_t)(m.last_one_in_col[col]-1), m.num_rows) == row);
continue;
}
row++;
for (uint row = last_row; row != m.num_rows; row++) {
#ifdef DEBUG_GAUSS
- assert(m.matrix[row].isZero());
+ assert(m.matrix.getMatrixAt(row).isZero());
#endif
if (m.matrix.getMatrixAt(row).is_true())
analyse_confl(m, row, maxlevel, size, best_row);
#ifdef DEBUG_GAUSS
assert(check_no_conflict(m));
+ assert(last_row == 0 || !m.matrix.getMatrixAt(last_row-1).isZero());
+ #endif
+
+ #ifdef VERBOSE_DEBUG
+ cout << "Resizing matrix to num_rows = " << last_row << endl;
#endif
m.num_rows = last_row;
m.matrix.resizeNumRows(m.num_rows);
for (Gaussian **gauss = &(solver.gauss_matrixes[0]), **end= gauss + solver.gauss_matrixes.size(); gauss != end; gauss++)
if (*gauss != this) (*gauss)->canceling(sublevel);
- for (int level = solver.trail.size()-1; level >= sublevel; level--) {
+ for (int level = solver.trail.size()-1; level >= (int)sublevel; level--) {
Var var = solver.trail[level].var();
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")Canceling var " << var+1 << endl;
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")matrix conflict found!" << endl;
cout << "(" << matrix_no << ")conflict clause's vars: ";
- print_matrix_row_with_assigns(m.varset[row]);
+ print_matrix_row_with_assigns(m.matrix.getVarsetAt(row));
cout << endl;
cout << "(" << matrix_no << ")corresponding matrix's row (should be empty): ";
- print_matrix_row(m.matrix[row]);
+ print_matrix_row(m.matrix.getMatrixAt(row));
cout << endl;
#endif
{
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")matrix prop found!" << endl;
- cout << m.matrix[row] << endl;
+ cout << m.matrix.getMatrixAt(row) << endl;
cout << "(" << matrix_no << ")matrix row:";
- print_matrix_row(m.matrix[row]);
+ print_matrix_row(m.matrix.getMatrixAt(row));
cout << endl;
#endif
else cout << col_to_var_original[var]+1 << ", ";
var++;
}
- if (!row.is_true()) cout << "xor_clause_inverted";
+ cout << "final:" << row.is_true() << endl;;
}
template<class T>
for (uint i = 0; i < m.num_cols; i++) {
cout << "last_one_in_col[" << i << "]-1 = " << m.last_one_in_col[i]-1 << endl;
}
- cout << "m.past_the_end_last_one_in_col:" << m.past_the_end_last_one_in_col << endl;
}
const bool Gaussian::nothing_to_propagate(matrixset& m) const
return true;
}
-const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) const
+const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, const matrixset& m) const
{
- assert(matrix.getSize() == varset.getSize());
-
for (uint i = 0; i < matrix.getSize(); i++) {
const PackedRow mat_row = matrix.getMatrixAt(i);
const PackedRow var_row = matrix.getVarsetAt(i);
}
}
+const void Gaussian::check_first_one_in_row(matrixset& m, const uint j)
+{
+ if (j) {
+ uint16_t until2 = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows);
+ if (j-1 > m.first_one_in_row[m.num_rows-1]) {
+ until2 = m.num_rows;
+ #ifdef VERBOSE_DEBUG
+ cout << "j-1 > m.first_one_in_row[m.num_rows-1]" << "j:" << j << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl;
+ #endif
+ }
+ for (uint i2 = 0; i2 != until2; i2++) {
+ #ifdef VERBOSE_DEBUG
+ cout << endl << "row " << i2 << " (num rows:" << m.num_rows << ")" << endl;
+ cout << m.matrix.getMatrixAt(i2) << endl;
+ cout << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl;
+ cout << "first_one_in_row:" << m.first_one_in_row[i2] << endl;
+ cout << "num_cols:" << m.num_cols << endl;
+ cout << "popcnt:" << m.matrix.getMatrixAt(i2).popcnt() << endl;
+ cout << "popcnt_is_one():" << m.matrix.getMatrixAt(i2).popcnt_is_one() << endl;
+ cout << "popcnt_is_one("<< m.first_one_in_row[i2] <<"): " << m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]) << endl;
+ #endif
+
+ for (uint i3 = 0; i3 < m.first_one_in_row[i2]; i3++) {
+ assert(m.matrix.getMatrixAt(i2)[i3] == 0);
+ }
+ assert(m.matrix.getMatrixAt(i2)[m.first_one_in_row[i2]]);
+ assert(m.matrix.getMatrixAt(i2).popcnt_is_one() ==
+ m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]));
+ }
+ }
+}
+
const uint Gaussian::get_called() const
{
return called;
{
using namespace MINISAT;
+//#define VERBOSE_DEBUG
+//#define DEBUG_GAUSS
+
#ifdef VERBOSE_DEBUG
using std::vector;
using std::cout;
static const uint16_t unassigned_col = -1;
static const Var unassigned_var = -1;
-//#define VERBOSE_DEBUG
-//#define DEBUG_GAUSS
class Gaussian
{
public:
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)
uint num_cols; // number of active columns in the matrix. The columns at the end that have all be zeroed are no longer active
int least_column_changed; // when updating the matrix, this value contains the smallest column number that has been updated (Gauss elim. can start from here instead of from column 0)
- uint16_t past_the_end_last_one_in_col;
vector<uint16_t> last_one_in_col; //last_one_in_col[COL] tells the last row+1 that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row)
+ vector<uint16_t> first_one_in_row;
uint removeable_cols; // the number of columns that have been zeroed out (i.e. assigned)
};
//State of current elimnation
vec<uint> propagatable_rows; //used to store which rows were deemed propagatable during elimination
- BitArray changed_rows; //used to store which rows were deemed propagatable during elimination
+ vector<unsigned char> changed_rows; //used to store which rows were deemed propagatable during elimination
//Statistics
uint useful_prop; //how many times Gauss gave propagation as a result
bool should_check_gauss(const uint decisionlevel, const uint starts) const;
void disable_if_necessary();
void reset_stats();
+ void update_last_one_in_col(matrixset& m);
private:
void print_matrix_row(const T& row) const; // Print matrix row 'row'
template<class T>
void print_matrix_row_with_assigns(const T& row) const;
- const bool check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) const;
+ const bool check_matrix_against_varset(PackedMatrix& matrix,const matrixset& m) const;
const bool check_last_one_in_cols(matrixset& m) const;
+ const void check_first_one_in_row(matrixset& m, const uint j);
void print_matrix(matrixset& m) const;
void print_last_one_in_cols(matrixset& m) const;
static const string lbool_to_string(const lbool toprint);
{
runid /= 10;
runid = time(NULL) % 10000;
- if (verbosity >= 1) printf("RunID is: #%d\n",runid);
+ if (verbosity >= 1) printf("c RunID is: #%d\n",runid);
}
-void Logger::setSolver(const Solver* _S)
+void Logger::setSolver(const Solver* _s)
{
- S = _S;
+ S = _s;
}
// Adds a new variable to the knowledge of the logger
void Logger::cut_name_to_size(string& name) const
{
uint len = name.length();
- if (len > 0 && name[len-1] == '\r') {
+ while(len > 0 && (name[len-1] == ' ' || name[len-1] == 0x0A || name[len-1] == 0x0D)) {
name[len-1] = '\0';
+ name.resize(len-1);
len--;
}
print_line("Avg. literals per learnt clause",(double)S->learnts_literals/(double)S->nLearnts());
print_line("Progress estimate (%):", S->progress_estimate*100.0);
print_line("All unitary learnts until now", S->get_unitary_learnts_num());
-
+ print_footer();
+}
+
+void Logger::print_learnt_unitaries(const uint from, const string display) const
+{
+ print_footer();
+ print_simple_line(display);
+ print_header("var", "name", "value");
+ for (uint i = from; i < S->trail.size(); i++) {
+ Var var = S->trail[i].var();
+ bool sign = S->trail[i].sign();
+ std::stringstream ss;
+ print_line(var+1, varnames[var], sign);
+ }
print_footer();
}
print_branch_depth_distrib();
print_learnt_clause_distrib();
print_matrix_stats();
+ print_learnt_unitaries(0," Unitary clauses learnt until now");
+ print_learnt_unitaries(last_unitary_learnt_clauses, " Unitary clauses during this restart");
print_advanced_stats();
print_general_stats();
}
void print_statistics_note() const;
void print_matrix_stats() const;
void print_general_stats() const;
+ void print_learnt_unitaries(const uint from, const string display) const;
uint max_print_lines;
template<class T>
//#define PART_FINDING
-MatrixFinder::MatrixFinder(Solver *_S) :
- unAssigned(_S->nVars() + 1)
- , S(_S)
+MatrixFinder::MatrixFinder(Solver *_s) :
+ unAssigned(_s->nVars() + 1)
+ , S(_s)
{
}
&& realMatrixNum < 3)
{
if (S->verbosity >=1)
- cout << "| Matrix no " << std::setw(4) << realMatrixNum;
+ cout << "c | Matrix no " << std::setw(4) << realMatrixNum;
S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, realMatrixNum, xorsInMatrix[i]));
realMatrixNum++;
} else {
if (S->verbosity >=1 && numXorInMatrix[a].second >= 20)
- cout << "| Unused Matrix ";
+ cout << "c | Unused Matrix ";
}
if (S->verbosity >=1 && numXorInMatrix[a].second >= 20) {
cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size();
for(uint i = 0; i < m.size*64; i++) {
os << m[i];
}
- os << " -- xor: " << !m.is_true();
+ os << " -- xor: " << m.is_true();
return os;
}
uint64_t tmp = mp[i];
while(tmp) {
popcount += tmp & 1;
- popcount += tmp & 2;
- popcount += tmp & 4;
- popcount += tmp & 8;
- if (popcount > 1) return false;
- tmp >>= 4;
+ tmp >>= 1;
}
}
- return popcount;
+ return popcount == 1;
}
bool popcnt_is_one(uint from) const
inline const bool isZero() const
{
- const uint64_t* mp2 = (const uint64_t*)mp;
-
for (uint i = 0; i != size; i++) {
- if (mp2[i]) return false;
+ if (mp[i]) return false;
}
return true;
}
mp[i/64] |= ((uint64_t)1 << (i%64));
}
- void swap(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 = size+1;
-
- while(i != 0) {
- uint64_t tmp(*mp2);
- *mp2 = *mp1;
- *mp1 = tmp;
- mp1++;
- mp2++;
- i--;
- }
- }
-
void swapBoth(PackedRow b)
{
#ifdef DEBUG_ROW
uint i = 2*(size+1);
while(i != 0) {
- uint64_t tmp(*mp2);
- *mp2 = *mp1;
- *mp1 = tmp;
+ std::swap(*mp1, *mp2);
mp1++;
mp2++;
i--;
{
using namespace MINISAT;
-RestartTypeChooser::RestartTypeChooser(const Solver* const _S) :
- S(_S)
+RestartTypeChooser::RestartTypeChooser(const Solver* const _s) :
+ S(_s)
, topX(100)
, limit(30)
{
std::cout << "First vars:" << std::endl;
#endif
Heap<Solver::VarOrderLt> tmp(S->order_heap);
- uint thisTopX = std::min(S->order_heap.size(), (int)topX);
+ uint thisTopX = std::min(S->order_heap.size(), topX);
for (uint i = 0; i != thisTopX; i++) {
#ifdef VERBOSE_DEBUG
std::cout << tmp.removeMin()+1 << ", ";
, xorFinder (true)
, performReplace (true)
, greedyUnbound (false)
- , restartType (static_restart)
+ , fixRestartType (auto_restart)
// Statistics: (formerly in 'SolverStats')
//
, progress_estimate(0)
, remove_satisfied (true)
, mtrand((unsigned long int)0)
+ , restartType (static_restart)
#ifdef STATS_NEEDED
, logger(verbosity)
, dynamic_behaviour_analysis(false) //do not document the proof as default
{
if (status.isUndef() && starts > 2 && starts < 8) {
RestartType tmp = restartTypeChooser.choose();
+ if (fixRestartType != auto_restart)
+ tmp = fixRestartType;
if (starts == 7) {
if (tmp == dynamic_restart) {
nbDecisionLevelHistory.fastclear();
totalSumOfDecisionLevel = 0;
clearGaussMatrixes();
if (verbosity >= 1)
- printf("| Decided on dynamic restart strategy |\n");
+ printf("c | Decided on dynamic restart strategy |\n");
} else {
if (verbosity >= 1)
- printf("| Decided on static restart strategy |\n");
+ printf("c | Decided on static restart strategy |\n");
}
restartType = tmp;
}
time = cpuTime();
uint foundCong = conglomerate->conglomerateXors();
if (verbosity >=1)
- printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong);
+ printf("c | Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong);
if (!ok) return;
uint new_total = 0;
new_total += xorclauses[i]->size();
}
if (verbosity >=1) {
- printf("| Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls);
- printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total);
+ printf("c | Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls);
+ printf("c | Sum xlits before: %11d, after: %12d |\n", orig_total, new_total);
}
if (performReplace
MatrixFinder m(this);
const uint numMatrixes = m.findMatrixes();
if (verbosity >=1)
- printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes);
+ printf("c | Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes);
}
}
FindUndef finder(*this);
const uint unbounded = finder.unRoll();
if (verbosity >= 1)
- printf("Greedy unbounding :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded);
+ printf("c Greedy unbounding :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded);
}
} if (status == l_False) {
if (conflict.size() == 0)
assert(!failed);
if (verbosity >=1)
- printf("Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size());
+ printf("c Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size());
}
#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");
+ printf("c ============================[ Search Statistics ]========================================\n");
+ printf("c | Conflicts | ORIGINAL | LEARNT | GAUSS |\n");
+ printf("c | | Vars Clauses Literals | Limit Clauses Lit/Cl | Prop Confl On |\n");
+ printf("c =========================================================================================\n");
}
}
#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());
+ printf("c | %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();
}
}
#else
if (verbosity >= 1) {
#endif
- printf("====================================================================");
+ printf("c ====================================================================");
print_gauss_sum_stats();
}
}
bool performReplace; // Should var-replacing be performed?
friend class FindUndef;
bool greedyUnbound; //If set, then variables will be greedily unbounded (set to l_Undef)
- RestartType restartType; // If set to true, the restart strategy will be dynamic
+ RestartType fixRestartType; // If set, the solver will always choose the given restart strategy
enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 };
bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
bqueue<unsigned int> nbDecisionLevelHistory; // Set of last decision level in conflict clauses
float totalSumOfDecisionLevel;
- MTRand mtrand; // random number generaton
- friend class Logger;
+ MTRand mtrand; // random number generaton
+ RestartType restartType; // Used internally to determine which restart strategy to choose
+ friend class Logger;
#ifdef STATS_NEEDED
Logger logger; // dynamic logging, statistics
- bool dynamic_behaviour_analysis; // Is logger running?
+ bool dynamic_behaviour_analysis; // Is logger running?
#endif
uint maxRestarts; // More than this number of restarts will not be performed
typedef uint32_t Var;
#define var_Undef (0xffffffffU >>1)
-enum RestartType {dynamic_restart, static_restart};
+enum RestartType {dynamic_restart, static_restart, auto_restart};
class Lit
{
CryptoMiniSat
-SVN revision: 656
-GIT revision: 87b9139cb43d296de0bd680226607ee7f3e3e755
+SVN revision: 681
+GIT revision: 14117f70a8eaa1c54e813f028252fa4449fdc151
namespace MINISAT
{
-VarReplacer::VarReplacer(Solver *_S) :
+VarReplacer::VarReplacer(Solver *_s) :
replacedLits(0)
, lastReplacedLits(0)
, replacedVars(0)
, lastReplacedVars(0)
, addedNewClause(false)
- , S(_S)
+ , S(_s)
{
}
clauses.clear();
if (S->verbosity >=1)
- printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars-lastReplacedVars, replacedLits-lastReplacedLits);
+ printf("c | Replacing %8d vars, replaced %8d lits |\n", replacedVars-lastReplacedVars, replacedLits-lastReplacedLits);
addedNewClause = false;
lastReplacedVars = replacedVars;
using std::make_pair;
-XorFinder::XorFinder(Solver* _S, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
+XorFinder::XorFinder(Solver* _s, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
cls(_cls)
, type(_type)
- , S(_S)
+ , S(_s)
{
}
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);
+ printf("c | Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, found, (double)sumLengths/(double)found);
if (found > 0) {
clearToRemove();
static inline uint32_t parent(uint32_t i) { return (i-1) >> 1; }
- inline void percolateUp(int i)
+ inline void percolateUp(uint32_t i)
{
uint32_t x = heap[i];
while (i != 0 && lt(x, heap[parent(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);
+ uint32_t child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
if (!lt(heap[child], x)) break;
heap[i] = heap[child];
indices[heap[i]] = i;
Heap(const Comp& c) : lt(c) { }
Heap(const Heap<Comp>& other) : lt(other.lt) {
heap.growTo(other.heap.size());
- memcpy(heap.getData(), other.heap.getData(), sizeof(int)*other.heap.size());
+ memcpy(heap.getData(), other.heap.getData(), sizeof(uint32_t)*other.heap.size());
indices.growTo(other.indices.size());
- memcpy(indices.getData(), other.indices.getData(), sizeof(int)*other.indices.size());
+ memcpy(indices.getData(), other.indices.getData(), sizeof(uint32_t)*other.indices.size());
}
- int size () const { return heap.size(); }
+ uint32_t size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
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]; }
+ uint32_t operator[](uint32_t index) const { assert(index < heap.size()); return heap[index]; }
void decrease (uint32_t n) { assert(inHeap(n)); percolateUp(indices[n]); }
}
- int removeMin()
+ uint32_t removeMin()
{
- int x = heap[0];
+ uint32_t x = heap[0];
heap[0] = heap.last();
indices[heap[0]] = 0;
indices[x] = UINT32_MAX;
// COMPAT: should be removed
void setBounds (uint32_t n) { }
void increase (uint32_t n) { decrease(n); }
- int getmin () { return removeMin(); }
+ uint32_t getmin () { return removeMin(); }
};
projects / francis / stp.git / commitdiff