#include "sat/sat_cleaner.h"
#include "sat/sat_solver.h"
#include "util/trace.h"
#include "util/stopwatch.h"
namespace sat {
cleaner::cleaner(solver & _s):
s(_s),
m_last_num_units(0),
m_cleanup_counter(0) {
reset_statistics();
}
void cleaner::cleanup_watches() {
vector<watch_list>::iterator it = s.m_watches.begin();
vector<watch_list>::iterator end = s.m_watches.end();
unsigned l_idx = 0;
for (; it != end; ++it, ++l_idx) {
if (s.value(to_literal(l_idx)) != l_undef) {
it->finalize();
SASSERT(it->empty());
continue;
}
TRACE(cleanup_bug, tout << "processing wlist of " << to_literal(l_idx) << "\n";);
watch_list & wlist = *it;
watch_list::iterator it2 = wlist.begin();
watch_list::iterator it_prev = it2;
watch_list::iterator end2 = wlist.end();
for (; it2 != end2; ++it2) {
switch (it2->get_kind()) {
case watched::BINARY:
TRACE(cleanup_bug,
tout << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";
tout << s.value(~to_literal(l_idx)) << " " << s.value(it2->get_literal()) << "\n";
tout << s.was_eliminated(it2->get_literal()) << " " << s.inconsistent() << "\n";);
SASSERT(s.value(it2->get_literal()) == l_true || s.value(it2->get_literal()) == l_undef);
if (s.value(it2->get_literal()) == l_undef) {
*it_prev = *it2;
++it_prev;
}
TRACE(cleanup_bug, tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";);
break;
case watched::CLAUSE:
break;
case watched::EXT_CONSTRAINT:
*it_prev = *it2;
++it_prev;
break;
}
}
wlist.set_end(it_prev);
}
}
void cleaner::cleanup_clauses(clause_vector & cs) {
clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it;
clause_vector::iterator end = cs.end();
for (; it != end; ++it) {
clause & c = *(*it);
TRACE(sat_cleaner_bug, tout << "cleaning: " << c << "\n";
for (unsigned i = 0; i < c.size(); ++i) tout << c[i] << ": " << s.value(c[i]) << "\n";);
CTRACE(sat_cleaner_frozen, c.frozen(), tout << c << "\n";);
unsigned sz = c.size();
unsigned i = 0, j = 0;
m_cleanup_counter += sz;
for (; i < sz; ++i) {
switch (s.value(c[i])) {
case l_true:
goto end_loop;
case l_false:
m_elim_literals++;
break;
case l_undef:
if (i != j) {
std::swap(c[j], c[i]);
}
j++;
break;
}
}
end_loop:
CTRACE(sat_cleaner_frozen, c.frozen(),
tout << "sat: " << (i < sz) << ", new_size: " << j << "\n";
tout << mk_lits_pp(j, c.begin()) << "\n";);
if (i < sz) {
m_elim_clauses++;
s.del_clause(c);
}
else {
unsigned new_sz = j;
CTRACE(sat_cleaner_bug, new_sz < 2, tout << "new_sz: " << new_sz << "\n";
if (c.size() > 0) tout << "unit: " << c[0] << "\n";
s.display_watches(tout););
switch (new_sz) {
case 0:
s.set_conflict();
s.del_clause(c);
break;
case 1:
s.assign_unit(c[0]);
s.del_clause(c);
break;
case 2:
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
TRACE(cleanup_bug, tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
s.mk_bin_clause(c[0], c[1], c.is_learned());
s.del_clause(c);
break;
default:
s.shrink(c, sz, new_sz);
*it2 = *it;
it2++;
if (!c.frozen()) {
s.attach_clause(c);
}
break;
}
}
}
cs.set_end(it2);
}
struct cleaner::report {
cleaner & m_cleaner;
stopwatch m_watch;
unsigned m_elim_clauses;
unsigned m_elim_literals;
report(cleaner & c):
m_cleaner(c),
m_elim_clauses(c.m_elim_clauses),
m_elim_literals(c.m_elim_literals) {
m_watch.start();
}
~report() {
m_watch.stop();
IF_VERBOSE(2,
verbose_stream() << " (sat-cleaner";
verbose_stream() << " :elim-literals " << (m_cleaner.m_elim_literals - m_elim_literals);
verbose_stream() << " :elim-clauses " << (m_cleaner.m_elim_clauses - m_elim_clauses);
verbose_stream() << " :cost " << m_cleaner.m_cleanup_counter << m_watch << ")\n";);
}
};
bool cleaner::is_clean() const {
for (clause* cp : s.m_clauses) {
for (literal lit : *cp) {
if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false;
}
}
for (clause* cp : s.m_learned) {
for (literal lit : *cp) {
if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false;
}
}
unsigned idx = 0;
for (auto& wlist : s.m_watches) {
literal lit = to_literal(idx);
if (s.value(lit) != l_undef && s.lvl(lit) == 0 && !wlist.empty()) return false;
++idx;
}
return true;
}
bool cleaner::operator()(bool force) {
CASSERT("cleaner_bug", s.check_invariant());
unsigned trail_sz = s.m_trail.size();
s.propagate(false); TRACE(sat_cleaner_bug, s.display(tout); s.display_watches(tout););
if (s.m_inconsistent)
return false;
if (m_last_num_units == trail_sz)
return false; if (!force && m_cleanup_counter > 0)
return false; report rpt(*this);
m_last_num_units = trail_sz;
m_cleanup_counter = 0;
do {
trail_sz = s.m_trail.size();
cleanup_watches();
cleanup_clauses(s.m_clauses);
cleanup_clauses(s.m_learned);
s.propagate(false);
}
while (trail_sz < s.m_trail.size() && !s.inconsistent());
CASSERT("cleaner_bug", s.check_invariant());
return true;
}
void cleaner::reset_statistics() {
m_elim_clauses = 0;
m_elim_literals = 0;
}
void cleaner::collect_statistics(statistics & st) const {
st.update("sat elim clauses", m_elim_clauses);
st.update("sat elim literals", m_elim_literals);
}
}