if (S->assigns[ps[0].var()] == l_Undef) {
assert(S->decisionLevel() == 0);
S->uncheckedEnqueue(Lit(ps[0].var(), inverted));
- ps[0] = Lit(ps[0].var(), inverted);
- Clause* newC = Clause_new(ps, old_group);
- S->unitary_learnts.push(newC);
} else if (S->assigns[ps[0].var()] != boolToLBool(!inverted)) {
#ifdef VERBOSE_DEBUG
cout << "Conflict. Aborting.";
Gaussian::~Gaussian()
{
- clear_clauses();
+ for (uint i = 0; i < clauses_toclear.size(); i++)
+ free(clauses_toclear[i].first);
}
inline void Gaussian::set_matrixset_to_cur()
matrix_sets[level] = cur_matrixset;
}
-void Gaussian::clear_clauses()
-{
- std::for_each(matrix_clauses_toclear.begin(), matrix_clauses_toclear.end(), std::ptr_fun(free));
- matrix_clauses_toclear.clear();
-}
-
llbool Gaussian::full_init()
{
if (!should_init()) return l_Nothing;
continue;
}
- uint best_row = i;
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);
- for (; this_matrix_row != end; ++this_matrix_row, best_row++) {
+ for (; this_matrix_row != end; ++this_matrix_row) {
if ((*this_matrix_row)[j])
break;
}
+ uint best_row = this_matrix_row - m.matrix.begin();
if (this_matrix_row != end) {
PackedRow matrix_row_i = m.matrix[i];
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")Canceling until sublevel " << sublevel << endl;
#endif
+
+ 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--) {
Var var = solver.trail[level].var();
solver.assigns[var] = l_Undef;
solver.insertVarOrder(var);
- for (Gaussian **gauss = &(solver.gauss_matrixes[0]), **end= gauss + solver.gauss_matrixes.size(); gauss != end; gauss++)
- if (*gauss != this) (*gauss)->canceling(level, var);
}
solver.trail.shrink(solver.trail.size() - sublevel);
solver.cancelUntil(0);
solver.uncheckedEnqueue(lit);
- solver.unitary_learnts.push(&cla);
if (solver.dynamic_behaviour_analysis)
solver.logger.propagation(cla[0], Logger::gauss_propagation_type, cla.group);
+ free(&cla);
return unit_propagation;
}
- matrix_clauses_toclear.push_back(&cla);
+ clauses_toclear.push_back(std::make_pair(&cla, solver.trail.size()-1));
solver.uncheckedEnqueue(cla[0], &cla);
if (solver.dynamic_behaviour_analysis) {
solver.logger.set_group_name(cla.group, "gauss prop clause");
void set_disabled(const bool toset);
//functions used throughout the Solver
- void back_to_level(const uint level);
- void canceling(const uint level, const Var var);
- void clear_clauses();
+ void canceling(const int sublevel);
protected:
Solver& solver;
//Varibales to keep Gauss state
bool messed_matrix_vars_since_reversal;
int gauss_last_level;
- vector<Clause*> matrix_clauses_toclear;
+ vector<pair<Clause*, uint> > clauses_toclear;
bool disabled; // Gauss is disabled
//State of current elimnation
&& decisionlevel < config.decision_until);
}
-inline void Gaussian::canceling(const uint level, const Var var)
+inline void Gaussian::canceling(const int sublevel)
{
- if (!messed_matrix_vars_since_reversal
- && level <= gauss_last_level
- && var < var_is_in.getSize()
+ if (disabled)
+ return;
+ uint a = 0;
+ for (int i = clauses_toclear.size()-1; i >= 0 && clauses_toclear[i].second > sublevel; i--) {
+ free(clauses_toclear[i].first);
+ a++;
+ }
+ clauses_toclear.resize(clauses_toclear.size()-a);
+
+ if (messed_matrix_vars_since_reversal)
+ return;
+ int c = std::min(gauss_last_level, solver.trail.size()-1);
+ for (; c >= sublevel; c--) {
+ Var var = solver.trail[c].var();
+ if (var < var_is_in.getSize()
&& var_is_in[var]
- && cur_matrixset.var_is_set[var]
- )
+ && cur_matrixset.var_is_set[var]) {
messed_matrix_vars_since_reversal = true;
+ return;
+ }
+ }
}
inline void Gaussian::print_matrix_stats() const
void Logger::begin()
{
+ begin_called = true;
if (proof_graph_on) {
std::stringstream filename;
filename << "proofs/" << runid << "-proof" << S->starts << ".dot";
it->second++;
}
- learnt_sizes[0] = S->get_unitary_learnts().size();
+ learnt_sizes[0] = S->get_unitary_learnts_num();
uint slice = (maximum+1)/max_print_lines + (bool)((maximum+1)%max_print_lines);
print_line("Number of literals in clauses",S->clauses_literals);
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->unitary_learnts.size());
+ print_line("All unitary learnts until now", S->get_unitary_learnts_num());
print_footer();
}
if (S->xorclauses.size() == 0)
return 0;
+ S->removeSatisfied(S->xorclauses);
+ S->cleanClauses(S->xorclauses);
+
for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) {
set<uint> tomerge;
vector<Var> newSet;
return ret;
}
+ const uint operator-(const iterator& b) const
+ {
+ return (mp - b.mp)/(numCols+1);
+ }
+
void operator+=(const uint num)
{
mp += (numCols+1)*num;
assert(b.size == size);
#endif
- memcpy(tmp_row, b.mp-1, sizeof(uint64_t)*(size+1));
- memcpy(b.mp-1, mp-1, sizeof(uint64_t)*(size+1));
- memcpy(mp-1, tmp_row, sizeof(uint64_t)*(size+1));
+ for (int i = -1; i != size; i++) {
+ uint64_t tmp(*(b.mp + i));
+ *(b.mp + i) = *(mp + i);
+ *(mp + i) = tmp;
+ }
}
PackedRow& operator^=(const PackedRow& b);
#include "Conglomerate.h"
#include "XorFinder.h"
-//#define DEBUG_LIB
+#define DEBUG_LIB
#ifdef DEBUG_LIB
#include <sstream>
Solver::~Solver()
{
for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
- for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_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 (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i];
- gauss_matrixes.clear();
+ for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]);
delete toReplace;
delete conglomerate;
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+ if (toReplace->getNumReplacedLits())
+ ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
xor_clause_inverted ^= ps[i].sign();
ps[i] ^= ps[i].sign();
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+ if (toReplace->getNumReplacedLits())
+ ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
if (value(ps[i]) == l_True || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
#endif
if (decisionLevel() > level) {
+
+ for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
+ (*gauss)->canceling(trail_lim[level]);
+
for (int c = trail.size()-1; c >= trail_lim[level]; c--) {
Var x = trail[c].var();
#ifdef VERBOSE_DEBUG
cout << "Canceling var " << x+1 << " sublevel:" << c << endl;
#endif
- for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
- (*gauss)->canceling(c, x);
assigns[x] = l_Undef;
insertVarOrder(x);
}
return learnts;
}
-const vec<Clause*>& Solver::get_unitary_learnts() const
+const vector<Lit> Solver::get_unitary_learnts() const
{
- return unitary_learnts;
+ vector<Lit> unitaries;
+ if (decisionLevel() > 0) {
+ for (uint i = 0; i < trail_lim[0]; i++)
+ unitaries.push_back(trail[i]);
+ }
+
+ return unitaries;
}
void Solver::dump_sorted_learnts(const char* file)
exit(-1);
}
- for (uint i = 0; i < unitary_learnts.size(); i++)
- unitary_learnts[i]->plain_print(outfile);
+ if (decisionLevel() > 0) {
+ for (uint i = 0; i < trail_lim[0]; i++)
+ printf("%s%d 0\n", trail[i].sign() ? "-" : "", trail[i].var());
+ }
sort(learnts, reduceDB_lt());
for (int i = learnts.size()-1; i >= 0 ; i--) {
if (ret != l_Nothing) return ret;
}
- if (dynamic_behaviour_analysis) logger.begin();
-
for (;;) {
Clause* confl = propagate();
assert(value(learnt_clause[0]) == l_Undef);
//Unitary learnt
if (learnt_clause.size() == 1) {
- Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true);
- unitary_learnts.push(c);
uncheckedEnqueue(learnt_clause[0]);
if (dynamic_behaviour_analysis) {
- logger.set_group_name(c->group, "unitary learnt clause");
- logger.propagation(learnt_clause[0], Logger::unit_clause_type, c->group);
+ 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?");
fprintf(myoutputfile, "c Solver::solve() called\n");
#endif
- if (dynamic_behaviour_analysis)
- logger.end(Logger::done_adding_clauses);
-
model.clear();
conflict.clear();
}
}
+ for (uint i = 0; i < gauss_matrixes.size(); i++)
+ delete gauss_matrixes[i];
+ gauss_matrixes.clear();
+ for (uint i = 0; i < freeLater.size(); i++)
+ free(freeLater[i]);
+ freeLater.clear();
+
if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) {
- removeSatisfied(xorclauses);
- cleanClauses(xorclauses);
double time = cpuTime();
MatrixFinder m(this);
const uint numMatrixes = m.findMatrixes();
printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | Prop Confl On |\n");
printf("=========================================================================================\n");
}
+
+ if (dynamic_behaviour_analysis)
+ logger.end(Logger::done_adding_clauses);
// Search:
while (status == l_Undef && starts < maxRestarts) {
for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
(*gauss)->reset_stats();
+ if (dynamic_behaviour_analysis)
+ logger.begin();
status = search((int)nof_conflicts);
nof_conflicts *= restart_inc;
-
- for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
- (*gauss)->clear_clauses();
}
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
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')
const vec<Clause*>& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses
const vec<Clause*>& get_learnts() const; //Get all learnt clauses
- const vec<Clause*>& get_unitary_learnts() const; //return the set of unitary learned clauses
+ const vector<Lit> get_unitary_learnts() const; //return the set of unitary learnt clauses
+ const uint get_unitary_learnts_num() const; //return the number of unitary learnt clauses
void dump_sorted_learnts(const char* file);
protected:
vec<Clause*> clauses; // List of problem clauses.
vec<XorClause*> xorclauses; // List of problem xor-clauses. Will be freed
vec<Clause*> learnts; // List of learnt clauses.
- vec<Clause*> unitary_learnts; // List of learnt clauses.
+ vec<XorClause*> freeLater; // List of xorclauses to free at the end (due to matrixes, they cannot be freed immediately)
vec<double> activity; // A heuristic measurement of the activity of a variable.
double var_inc; // Amount to bump next variable with.
vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
{
useRealUnknowns = true;
}
+inline const uint Solver::get_unitary_learnts_num() const
+{
+ if (decisionLevel() > 0)
+ return trail_lim[0];
+ return 0;
+}
template<class T>
void Solver::removeSatisfied(vec<T*>& cs)
{
inline void Solver::removeClause(XorClause& c)
{
detachClause(c);
+ freeLater.push(&c);
c.mark(1);
}
CryptoMiniSat
-SVN revision: 519
-GIT revision: 0426e61b02a00a073a87fdffc0282820875fad61
+SVN revision:
+GIT revision: 63f0b6f7e4927759643c97913060c37f8ae4c82a
if (S->verbosity >=1)
printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits);
- replacedLits = 0;
addedNewClause = false;
if (S->ok)
projects / francis / stp.git / commitdiff