mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix updates to cce

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-30 23:41:04 -08:00
parent 2d0f80f78e
commit 2739342aba
16 changed files with 248 additions and 254 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/ba_solver.cpp
View file

@ -2798,7 +2798,7 @@ namespace sat {
}
unsigned ba_solver::get_num_unblocked_bin(literal l) {
return s().m_simplifier.get_num_unblocked_bin(l);
return s().m_simplifier.num_nonlearned_bin(l);
}
/*

13
src/sat/sat_asymm_branch.cpp
View file

@ -60,7 +60,7 @@ namespace sat {
verbose_stream()
<< " (sat-asymm-branch :elim-literals " << (num_total - num_learned)
<< " :elim-learned-literals " << num_learned
<< " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies)
<< " :hte " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies)
<< " :cost " << m_asymm_branch.m_counter
<< mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
@ -124,13 +124,13 @@ namespace sat {
break;
}
SASSERT(s.m_qhead == s.m_trail.size());
if (m_counter < limit || s.inconsistent()) {
clause & c = *(*it);
if (m_counter < limit || s.inconsistent() || c.was_removed()) {
*it2 = *it;
++it2;
continue;
}
s.checkpoint();
clause & c = *(*it);
s.checkpoint();
if (big ? !process_sampled(*big, c) : !process(c)) {
continue; // clause was removed
}
@ -431,7 +431,8 @@ namespace sat {
bool asymm_branch::process_sampled(big& big, clause & c) {
scoped_detach scoped_d(s, c);
sort(big, c);
if ((c.is_learned() || !big.learned()) && uhte(big, c)) {
if (!big.learned() && !c.is_learned() && uhte(big, c)) {
// TBD: mark clause as learned.
++m_hidden_tautologies;
scoped_d.del_clause();
return false;
@ -501,7 +502,7 @@ namespace sat {
void asymm_branch::collect_statistics(statistics & st) const {
st.update("elim literals", m_elim_literals);
st.update("hidden tautologies", m_hidden_tautologies);
st.update("hte", m_hidden_tautologies);
}
void asymm_branch::reset_statistics() {

9
src/sat/sat_clause.cpp
View file

@ -87,6 +87,15 @@ namespace sat {
mark_strengthened();
}
void clause::shrink(unsigned num_lits) {
SASSERT(num_lits <= m_size);
if (num_lits < m_size) {
m_size = num_lits;
mark_strengthened();
}
}
bool clause::satisfied_by(model const & m) const {
for (literal l : *this) {
if (l.sign()) {

2
src/sat/sat_clause.h
View file

@ -66,7 +66,7 @@ namespace sat {
literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; }
bool is_learned() const { return m_learned; }
void set_learned(bool l) { SASSERT(is_learned() != l); m_learned = l; }
void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } }
void shrink(unsigned num_lits);
bool strengthened() const { return m_strengthened; }
void mark_strengthened() { m_strengthened = true; update_approx(); }
void unmark_strengthened() { m_strengthened = false; }

5
src/sat/sat_cleaner.cpp
View file

@ -145,10 +145,7 @@ namespace sat {
*it2 = *it;
it2++;
if (!c.frozen()) {
if (new_sz == 3)
s.attach_ter_clause(c);
else
s.attach_nary_clause(c);
s.attach_clause(c);
}
if (s.m_config.m_drat) {
// for optimization, could also report deletion

4
src/sat/sat_elim_eqs.cpp
View file

@ -95,10 +95,10 @@ namespace sat {
m_solver.detach_clause(c);
// apply substitution
for (i = 0; i < sz; i++) {
literal lit = c[i];
literal lit = c[i];
c[i] = norm(roots, lit);
VERIFY(c[i] == norm(roots, c[i]));
VERIFY(!m_solver.was_eliminated(c[i].var()) || lit == c[i]);
VERIFY(!m_solver.was_eliminated(c[i].var()) || lit == c[i]);
}
std::sort(c.begin(), c.end());
for (literal l : c) VERIFY(l == norm(roots, l));

4
src/sat/sat_elim_vars.cpp
View file

@ -37,9 +37,9 @@ namespace sat{
literal pos_l(v, false);
literal neg_l(v, true);
unsigned num_bin_pos = simp.get_num_unblocked_bin(pos_l);
unsigned num_bin_pos = simp.num_nonlearned_bin(pos_l);
if (num_bin_pos > m_max_literals) return false;
unsigned num_bin_neg = simp.get_num_unblocked_bin(neg_l);
unsigned num_bin_neg = simp.num_nonlearned_bin(neg_l);
if (num_bin_neg > m_max_literals) return false;
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_l);

2
src/sat/sat_iff3_finder.cpp
View file

@ -73,7 +73,7 @@ namespace sat {
It assumes wlist have been sorted using iff3_lt
*/
static bool contains(watch_list const & wlist, literal l1, literal l2) {
watched k(l1, l2, false);
watched k(l1, l2);
if (wlist.size() < SMALL_WLIST)
return wlist.contains(k);
iff3_lt lt;

10
src/sat/sat_integrity_checker.cpp
View file

@ -28,8 +28,8 @@ namespace sat {
}
// for ternary clauses
static bool contains_watched(watch_list const & wlist, literal l1, literal l2, bool learned) {
return wlist.contains(watched(l1, l2, learned));
static bool contains_watched(watch_list const & wlist, literal l1, literal l2) {
return wlist.contains(watched(l1, l2));
}
// for nary clauses
@ -68,9 +68,9 @@ namespace sat {
tout << "watch_list:\n";
sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
tout << "\n";);
VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.is_learned()));
VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2], c.is_learned()));
VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1], c.is_learned()));
VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
}
else {
if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {

1
src/sat/sat_lookahead.cpp
View file

@ -2306,6 +2306,7 @@ namespace sat {
roots[v] = p;
VERIFY(get_parent(p) == p);
VERIFY(get_parent(~p) == ~p);
IF_VERBOSE(0, verbose_stream() << p << " " << q << "\n";);
}
}
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";);

371
src/sat/sat_simplifier.cpp
View file

@ -148,27 +148,17 @@ namespace sat {
m_use_list.erase(c, l);
}
inline void simplifier::block_clause(clause & c) {
if (m_retain_blocked_clauses) {
m_need_cleanup = true;
s.set_learned(c, true);
m_use_list.block(c);
}
else {
remove_clause(c);
}
inline void simplifier::set_learned(clause & c) {
m_need_cleanup = true;
s.set_learned(c, true);
m_use_list.block(c);
}
inline void simplifier::unblock_clause(clause & c) {
s.set_learned(c, false);
m_use_list.unblock(c);
}
inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
get_wlist(~l1).erase(watched(l2, learned));
m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
m_sub_bin_todo.erase(bin_clause(l2, l1, learned));
inline void simplifier::set_learned(literal l1, literal l2) {
m_sub_bin_todo.erase(bin_clause(l1, l2, false));
m_sub_bin_todo.erase(bin_clause(l2, l1, false));
m_sub_bin_todo.push_back(bin_clause(l1, l2, true));
m_sub_bin_todo.push_back(bin_clause(l2, l1, true));
}
void simplifier::init_visited() {
@ -308,13 +298,16 @@ namespace sat {
clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it;
clause_vector::iterator end = cs.end();
unsigned nm = 0;
for (; it != end; ++it) {
clause & c = *(*it);
if (learned && !c.is_learned()) {
s.m_clauses.push_back(&c);
++nm;
}
else if (!learned && c.is_learned()) {
s.m_learned.push_back(&c);
++nm;
}
else {
*it2 = *it;
@ -322,6 +315,7 @@ namespace sat {
}
}
cs.set_end(it2);
IF_VERBOSE(0, verbose_stream() << "num moved: " << nm << "\n";);
}
void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
@ -373,19 +367,10 @@ namespace sat {
s.del_clause(c);
continue;
}
// clause became a learned clause
if (!learned && c.is_learned()) {
SASSERT(!c.frozen());
s.m_learned.push_back(&c);
continue;
}
*it2 = *it;
it2++;
if (!c.frozen()) {
if (sz == 3)
s.attach_ter_clause(c);
else
s.attach_nary_clause(c);
s.attach_clause(c);
if (s.m_config.m_drat) {
s.m_drat.add(c, true);
}
@ -895,6 +880,10 @@ namespace sat {
break;
clause & c = m_sub_todo.erase();
if (c.id() == 60127) {
IF_VERBOSE(0, verbose_stream() << "subsume " << c << "\n";);
}
c.unmark_strengthened();
m_sub_counter--;
TRACE("subsumption", tout << "next: " << c << "\n";);
@ -904,6 +893,9 @@ namespace sat {
continue;
}
unsigned sz = c.size();
if (c.id() == 60127) {
IF_VERBOSE(0, verbose_stream() << "subsume " << c << "\n";);
}
if (sz == 0) {
s.set_conflict(justification());
return;
@ -990,11 +982,11 @@ namespace sat {
int m_counter;
model_converter & mc;
queue m_queue;
clause_vector m_to_remove;
literal_vector m_covered_clause;
svector<clause_ante> m_covered_antecedent;
literal_vector m_intersection;
literal_vector m_tautology;
literal_vector m_new_intersection;
literal_vector m_blocked_binary;
svector<bool> m_in_intersection;
@ -1084,39 +1076,25 @@ namespace sat {
model_converter::entry* new_entry = 0;
watch_list & wlist = s.get_wlist(~l);
m_counter -= wlist.size();
watch_list::iterator it = wlist.begin();
watch_list::iterator it2 = it;
watch_list::iterator end = wlist.end();
for (; it != end; ++it) {
if (!it->is_binary_non_learned_clause()) {
*it2 = *it; it2++;
for (watched& w : wlist) {
if (!w.is_binary_non_learned_clause()) {
continue;
}
literal l2 = it->get_literal();
literal l2 = w.get_literal();
s.mark_visited(l2);
if (all_tautology(l)) {
block_binary(it, l, new_entry);
s.m_num_blocked_clauses++;
block_binary(w, l, new_entry);
w.set_learned(true);
s.s.set_learned1(l2, l, true);
s.m_num_bce++;
m_blocked_binary.push_back(l2);
}
else {
*it2 = *it; it2++;
}
s.unmark_visited(l2);
}
wlist.set_end(it2);
if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) {
IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";);
for (literal lit2 : m_blocked_binary) {
s.s.mk_bin_clause(l, lit2, true);
}
}
}
void process_clauses(literal l) {
model_converter::entry* new_entry = 0;
m_to_remove.reset();
clause_use_list & occs = s.m_use_list.get(l);
clause_use_list::iterator it = occs.mk_iterator();
for (; !it.at_end(); it.next()) {
@ -1127,12 +1105,11 @@ namespace sat {
s.mark_all_but(c, l);
if (all_tautology(l)) {
block_clause(c, l, new_entry);
s.m_num_blocked_clauses++;
s.m_num_bce++;
s.set_learned(c);
}
s.unmark_all(c);
}
for (clause* c : m_to_remove)
s.block_clause(*c);
}
}
void reset_intersection() {
@ -1155,6 +1132,7 @@ namespace sat {
if (!process_var(l.var())) return false;
bool first = true;
reset_intersection();
m_tautology.reset();
for (watched & w : s.get_wlist(l)) {
// when adding a blocked clause, then all non-learned clauses have to be considered for the
// resolution intersection.
@ -1162,6 +1140,7 @@ namespace sat {
if (process_bin) {
literal lit = w.get_literal();
if (s.is_marked(~lit) && lit != ~l) {
m_tautology.push_back(~lit);
continue; // tautology
}
if (!first || s.is_marked(lit)) {
@ -1178,8 +1157,10 @@ namespace sat {
bool tautology = false;
clause & c = it.curr();
if (c.is_learned() && !adding) continue;
if (c.was_removed()) continue;
for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) {
m_tautology.push_back(~lit);
tautology = true;
break;
}
@ -1204,25 +1185,30 @@ namespace sat {
return false;
}
}
// if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";);
return first;
}
bool check_abce_tautology(literal l) {
m_tautology.reset();
if (!process_var(l.var())) return false;
for (watched & w : s.get_wlist(l)) {
if (w.is_binary_non_learned_clause()) {
literal lit = w.get_literal();
if (!s.is_marked(~lit) || lit == ~l) return false;
VERIFY(lit != ~l);
if (!s.is_marked(~lit)) return false;
m_tautology.push_back(~lit);
}
}
clause_use_list & neg_occs = s.m_use_list.get(~l);
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
clause & c = it.curr();
if (c.is_learned()) continue;
if (c.is_learned() || c.was_removed()) continue;
bool tautology = false;
for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) {
tautology = true;
m_tautology.push_back(~lit);
break;
}
}
@ -1251,26 +1237,36 @@ namespace sat {
return !m_clause.is_binary() && (m_clause.get_clause() == &c);
}
/**
\brief idx is the index of the blocked literal.
m_tautology contains literals that were used to establish that the current members of m_covered_clause is blocked.
This routine removes literals that were not relevant to establishing it was blocked.
*/
void minimize_covered_clause(unsigned idx) {
IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause << " @ " << idx << "\n";);
// IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";);
for (literal l : m_tautology) VERIFY(s.is_marked(l));
for (literal l : m_covered_clause) s.unmark_visited(l);
for (literal l : m_tautology) s.mark_visited(l);
s.mark_visited(m_covered_clause[idx]);
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
if (s.is_marked(m_covered_clause[i])) idx = i;
}
for (unsigned i = idx; i > 0; --i) {
literal lit = m_covered_clause[i];
if (!s.is_marked(lit)) continue;
clause_ante const& ante = m_covered_antecedent[i];
if (ante.cls()) {
//IF_VERBOSE(0, verbose_stream() << "clause ante: " << lit << ": " << *ante.cls() << "\n";);
for (literal l : *ante.cls()) {
IF_VERBOSE(0, verbose_stream() << "clause ante: " << l << "\n";);
if (l != ~lit) s.mark_visited(l);
}
}
if (ante.lit1() != null_literal) {
IF_VERBOSE(0, verbose_stream() << "ante1: " << ante.lit1() << "\n";);
//IF_VERBOSE(0, verbose_stream() << "ante1: " << lit << ": " << ante.lit1() << "\n";);
s.mark_visited(ante.lit1());
}
if (ante.lit2() != null_literal) {
IF_VERBOSE(0, verbose_stream() << "ante2: " << ante.lit2() << "\n";);
//IF_VERBOSE(0, verbose_stream() << "ante2: " << lit << ": " << ante.lit2() << "\n";);
s.mark_visited(ante.lit2());
}
}
@ -1282,8 +1278,16 @@ namespace sat {
s.unmark_visited(lit);
}
}
// ensure that rest of literals from original clause are included
for (unsigned i = idx + 1; i < m_covered_clause.size() && m_covered_antecedent[i] == clause_ante(); ++i) {
literal lit = m_covered_clause[i];
m_covered_clause[j++] = lit;
}
for (literal l : m_covered_clause) VERIFY(!s.is_marked(l));
unsigned sz0 = m_covered_clause.size();
m_covered_clause.resize(j);
IF_VERBOSE(0, verbose_stream() << "reduced: " << m_covered_clause << "\n";);
VERIFY(j >= m_clause.size());
// IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";);
}
/*
@ -1303,71 +1307,51 @@ namespace sat {
bool add_ala() {
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
literal l = m_covered_clause[m_ala_qhead];
for (watched & w : s.get_wlist(~l)) {
if (w.is_binary_non_learned_clause()) {
literal lit = w.get_literal();
if (revisit_binary(l, lit)) continue;
if (s.is_marked(lit)) {
IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";);
//IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";);
return true;
}
if (!s.is_marked(~lit)) {
IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";);
//IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";);
m_covered_clause.push_back(~lit);
m_covered_antecedent.push_back(clause_ante(l));
s.mark_visited(~lit);
}
}
else if (w.is_ternary_clause() && !w.is_learned()) {
literal lit1 = w.get_literal1();
literal lit2 = w.get_literal2();
if (revisit_ternary(l, lit1, lit2)) continue;
if (s.is_marked(lit1) && s.is_marked(lit2)) {
IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " ternary: " << l << " " << lit1 << " " << lit2 << "\n";);
return true;
}
clause_use_list & pos_occs = s.m_use_list.get(l);
clause_use_list::iterator it = pos_occs.mk_iterator();
for (; !it.at_end(); it.next()) {
clause & c = it.curr();
if (c.is_learned() || c.was_removed()) continue;
if (revisit_clause(c)) continue;
literal lit1 = null_literal;
bool ok = true;
for (literal lit : c) {
if (lit == l) continue;
if (s.is_marked(lit)) continue;
if (!s.is_marked(~lit) && lit1 == null_literal) {
lit1 = lit;
}
if (s.is_marked(lit1) && !s.is_marked(~lit2)) {
IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternary " << l << " " << lit1 << " " << lit2 << " " << (~lit2) << "\n";);
m_covered_clause.push_back(~lit2);
m_covered_antecedent.push_back(clause_ante(l, lit1));
s.mark_visited(~lit2);
continue;
}
if (s.is_marked(lit2) && !s.is_marked(~lit1)) {
IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternay " << l << " " << lit1 << " " << lit2 << " " << (~lit1) << "\n";);
m_covered_clause.push_back(~lit1);
m_covered_antecedent.push_back(clause_ante(l, lit2));
s.mark_visited(~lit1);
continue;
else {
ok = false;
break;
}
}
else if (w.is_clause()) {
clause & c = s.s.get_clause(w.get_clause_offset());
if (c.is_learned()) continue;
if (revisit_clause(c)) continue;
literal lit1 = null_literal;
bool ok = true;
for (literal lit : c) {
if (lit == l) continue;
if (s.is_marked(lit)) continue;
if (!s.is_marked(~lit) && lit1 == null_literal) {
lit1 = lit;
}
else {
ok = false;
break;
}
}
if (!ok) continue;
if (lit1 == null_literal) {
IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " clause " << c << "\n";);
return true;
}
IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " clause " << c << " " << (~lit1) << "\n";);
m_covered_clause.push_back(~lit1);
m_covered_antecedent.push_back(clause_ante(c));
s.mark_visited(~lit1);
if (!ok) continue;
if (lit1 == null_literal) {
//IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " clause " << c << "\n";);
return true;
}
// IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " clause " << c << " " << (~lit1) << "\n";);
m_covered_clause.push_back(~lit1);
m_covered_antecedent.push_back(clause_ante(c));
s.mark_visited(~lit1);
}
}
return false;
@ -1430,10 +1414,9 @@ namespace sat {
for (literal l : m_covered_clause) s.unmark_visited(l);
return at_t;
}
for (unsigned i = 0; !is_tautology && i < sz0; ++i) {
for (unsigned i = 0; i < sz0; ++i) {
if (check_abce_tautology(m_covered_clause[i])) {
blocked = m_covered_clause[i];
minimize_covered_clause(i);
is_tautology = true;
break;
}
@ -1456,7 +1439,6 @@ namespace sat {
is_tautology = add_cla(blocked);
}
while (m_covered_clause.size() > sz && !is_tautology);
if (above_threshold(sz0)) break;
if (et == acce_t && !is_tautology) {
sz = m_covered_clause.size();
if (add_ala()) {
@ -1465,9 +1447,9 @@ namespace sat {
}
k = model_converter::ACCE;
}
if (above_threshold(sz0)) break;
}
while (m_covered_clause.size() > sz && !is_tautology);
// if (is_tautology) std::cout << num_iterations << " " << m_covered_clause.size() << " " << sz0 << " " << is_tautology << " " << m_elim_stack.size() << "\n";
for (literal l : m_covered_clause) s.unmark_visited(l);
return (is_tautology && !above_threshold(sz0)) ? bc_t : no_t;
}
@ -1484,6 +1466,7 @@ namespace sat {
m_covered_clause.push_back(l);
m_covered_antecedent.push_back(clause_ante());
}
// shuffle<literal>(s.s.m_rand, m_covered_clause);
return cla<et>(blocked, k);
}
@ -1516,81 +1499,68 @@ namespace sat {
template<elim_type et>
void process_cce_binary(literal l) {
m_blocked_binary.reset();
literal blocked = null_literal;
watch_list & wlist = s.get_wlist(~l);
m_counter -= wlist.size();
watch_list::iterator it = wlist.begin();
watch_list::iterator it2 = it;
watch_list::iterator end = wlist.end();
model_converter::kind k;
for (; it != end; ++it) {
if (!it->is_binary_non_learned_clause()) {
*it2 = *it;
it2++;
continue;
}
literal l2 = it->get_literal();
for (watched & w : wlist) {
if (!w.is_binary_non_learned_clause()) continue;
literal l2 = w.get_literal();
switch (cce<et>(l, l2, blocked, k)) {
case bc_t:
block_covered_binary(it, l, blocked, k);
s.m_num_covered_clauses++;
m_blocked_binary.push_back(l2);
inc_bc<et>();
block_covered_binary(w, l, blocked, k);
w.set_learned(true);
s.s.set_learned1(l2, l, true);
break;
case at_t:
s.m_num_ate++;
m_blocked_binary.push_back(l2);
w.set_learned(true);
s.s.set_learned1(l2, l, true);
break;
case no_t:
*it2 = *it;
it2++;
break;
}
}
wlist.set_end(it2);
if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) {
IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";);
for (literal lit2 : m_blocked_binary) {
s.s.mk_bin_clause(l, lit2, true);
}
}
}
template<elim_type et>
void cce_clauses() {
m_to_remove.reset();
literal blocked;
model_converter::kind k;
for (clause* cp : s.s.m_clauses) {
clause& c = *cp;
if (!c.was_removed() && !c.is_learned()) {
switch (cce<et>(c, blocked, k)) {
case bc_t:
block_covered_clause(c, blocked, k);
s.m_num_covered_clauses++;
break;
case at_t:
m_to_remove.push_back(&c);
break;
case no_t:
break;
}
if (c.was_removed() || c.is_learned()) continue;
switch (cce<et>(c, blocked, k)) {
case bc_t:
inc_bc<et>();
block_covered_clause(c, blocked, k);
s.set_learned(c);
break;
case at_t:
s.m_num_ate++;
s.set_learned(c);
break;
case no_t:
break;
}
}
for (clause* c : m_to_remove) {
s.block_clause(*c);
}
m_to_remove.reset();
}
template<elim_type et>
void inc_bc() {
switch (et) {
case cce_t: s.m_num_cce++; break;
case acce_t: s.m_num_acce++; break;
case abce_t: s.m_num_abce++; break;
}
}
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
VERIFY(!s.is_external(l));
if (new_entry == 0)
new_entry = &(mc.mk(k, l.var()));
m_to_remove.push_back(&c);
for (literal lit : c) {
if (lit != l && process_var(lit.var())) {
m_queue.decreased(~lit);
@ -1611,25 +1581,25 @@ namespace sat {
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
void prepare_block_binary(watched const& w, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
SASSERT(!s.is_external(blocked));
if (new_entry == 0)
new_entry = &(mc.mk(k, blocked.var()));
literal l2 = it->get_literal();
literal l2 = w.get_literal();
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
s.remove_bin_clause_half(l2, l1, it->is_learned());
s.set_learned(l1, l2);
m_queue.decreased(~l2);
}
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
literal l2 = it->get_literal();
prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT);
void block_binary(watched const& w, literal l, model_converter::entry *& new_entry) {
literal l2 = w.get_literal();
prepare_block_binary(w, l, l, new_entry, model_converter::BLOCK_LIT);
mc.insert(*new_entry, l, l2);
}
void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) {
void block_covered_binary(watched const& w, literal l, literal blocked, model_converter::kind k) {
model_converter::entry * new_entry = 0;
prepare_block_binary(it, l, blocked, new_entry, k);
prepare_block_binary(w, l, blocked, new_entry, k);
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
@ -1681,6 +1651,7 @@ namespace sat {
for (; !it.at_end(); it.next()) {
clause & c = it.curr();
if (c.is_learned()) continue;
if (c.was_removed()) continue;
m_counter -= c.size();
unsigned sz = c.size();
unsigned i;
@ -1707,33 +1678,40 @@ namespace sat {
struct simplifier::blocked_cls_report {
simplifier & m_simplifier;
stopwatch m_watch;
unsigned m_num_blocked_clauses;
unsigned m_num_covered_clauses;
unsigned m_num_bce;
unsigned m_num_cce;
unsigned m_num_acce;
unsigned m_num_abce;
unsigned m_num_ate;
unsigned m_num_added_clauses;
unsigned m_num_bca;
blocked_cls_report(simplifier & s):
m_simplifier(s),
m_num_blocked_clauses(s.m_num_blocked_clauses),
m_num_covered_clauses(s.m_num_covered_clauses),
m_num_bce(s.m_num_bce),
m_num_cce(s.m_num_cce),
m_num_acce(s.m_num_acce),
m_num_abce(s.m_num_abce),
m_num_ate(s.m_num_ate),
m_num_added_clauses(s.m_num_bca) {
m_num_bca(s.m_num_bca) {
m_watch.start();
}
~blocked_cls_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
<< " :elim-covered-clauses "
<< (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
<< " :added-clauses "
<< (m_simplifier.m_num_bca - m_num_added_clauses)
<< " :ate "
<< (m_simplifier.m_num_ate - m_num_ate)
<< mem_stat()
verbose_stream() << " (sat-blocked-clauses";
report(m_simplifier.m_num_ate, m_num_ate, " :ate ");
report(m_simplifier.m_num_bce, m_num_bce, " :bce ");
report(m_simplifier.m_num_abce, m_num_abce, " :abce ");
report(m_simplifier.m_num_cce, m_num_cce, " :cce ");
report(m_simplifier.m_num_bca, m_num_bca, " :bca ");
report(m_simplifier.m_num_acce, m_num_acce, " :acce ");
verbose_stream() << mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
void report(unsigned n, unsigned m, char const* s) {
if (n > m) verbose_stream() << s << (n - m);
}
};
void simplifier::elim_blocked_clauses() {
@ -1743,7 +1721,7 @@ namespace sat {
elim();
}
unsigned simplifier::get_num_unblocked_bin(literal l) const {
unsigned simplifier::num_nonlearned_bin(literal l) const {
unsigned r = 0;
watch_list const & wlist = get_wlist(~l);
for (auto & w : wlist) {
@ -1758,8 +1736,8 @@ namespace sat {
literal neg_l(v, true);
unsigned num_pos = m_use_list.get(pos_l).size();
unsigned num_neg = m_use_list.get(neg_l).size();
unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
unsigned num_bin_pos = num_nonlearned_bin(pos_l);
unsigned num_bin_neg = num_nonlearned_bin(neg_l);
unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
<< " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
@ -1799,9 +1777,10 @@ namespace sat {
void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
clause_use_list const & cs = m_use_list.get(l);
for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
if (!it.curr().is_learned()) {
r.push_back(clause_wrapper(it.curr()));
SASSERT(r.back().size() == it.curr().size());
clause& c = it.curr();
if (!c.is_learned() && !c.was_removed()) {
r.push_back(clause_wrapper(c));
SASSERT(r.back().size() == c.size());
}
}
@ -1939,8 +1918,8 @@ namespace sat {
literal pos_l(v, false);
literal neg_l(v, true);
unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
unsigned num_bin_pos = num_nonlearned_bin(pos_l);
unsigned num_bin_neg = num_nonlearned_bin(neg_l);
clause_use_list & pos_occs = m_use_list.get(pos_l);
clause_use_list & neg_occs = m_use_list.get(neg_l);
unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos;
@ -2146,15 +2125,19 @@ namespace sat {
st.update("subsumed", m_num_subsumed);
st.update("subsumption resolution", m_num_sub_res);
st.update("elim literals", m_num_elim_lits);
st.update("elim blocked clauses", m_num_blocked_clauses);
st.update("elim covered clauses", m_num_covered_clauses);
st.update("blocked clauses added", m_num_bca);
st.update("asymmetric tautologies eliminated", m_num_ate);
st.update("bce", m_num_bce);
st.update("cce", m_num_cce);
st.update("acce", m_num_acce);
st.update("abce", m_num_abce);
st.update("bca", m_num_bca);
st.update("ate", m_num_ate);
}
void simplifier::reset_statistics() {
m_num_blocked_clauses = 0;
m_num_covered_clauses = 0;
m_num_bce = 0;
m_num_cce = 0;
m_num_acce = 0;
m_num_abce = 0;
m_num_subsumed = 0;
m_num_sub_res = 0;
m_num_elim_lits = 0;

17
src/sat/sat_simplifier.h
View file

@ -100,14 +100,16 @@ namespace sat {
unsigned m_elim_vars_bdd_delay;
// stats
unsigned m_num_blocked_clauses;
unsigned m_num_covered_clauses;
unsigned m_num_bce;
unsigned m_num_cce;
unsigned m_num_acce;
unsigned m_num_abce;
unsigned m_num_bca;
unsigned m_num_ate;
unsigned m_num_subsumed;
unsigned m_num_elim_vars;
unsigned m_num_sub_res;
unsigned m_num_elim_lits;
unsigned m_num_bca;
unsigned m_num_ate;
bool m_learned_in_use_lists;
unsigned m_old_num_elim_vars;
@ -132,9 +134,8 @@ namespace sat {
void remove_clause_core(clause & c);
void remove_clause(clause & c);
void remove_clause(clause & c, literal l);
void block_clause(clause & c);
void unblock_clause(clause & c);
void remove_bin_clause_half(literal l1, literal l2, bool learned);
void set_learned(clause & c);
void set_learned(literal l1, literal l2);
bool_var get_min_occ_var(clause const & c) const;
bool subsumes1(clause const & c1, clause const & c2, literal & l);
@ -183,7 +184,7 @@ namespace sat {
bool elim_vars_bdd_enabled() const;
bool elim_vars_enabled() const;
unsigned get_num_unblocked_bin(literal l) const;
unsigned num_nonlearned_bin(literal l) const;
unsigned get_to_elim_cost(bool_var v) const;
void order_vars_for_elim(bool_var_vector & r);
void collect_clauses(literal l, clause_wrapper_vector & r);

32
src/sat/sat_solver.cpp
View file

@ -396,9 +396,9 @@ namespace sat {
bool solver::attach_ter_clause(clause & c) {
bool reinit = false;
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2], c.is_learned()));
m_watches[(~c[1]).index()].push_back(watched(c[0], c[2], c.is_learned()));
m_watches[(~c[2]).index()].push_back(watched(c[0], c[1], c.is_learned()));
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
if (!at_base_lvl()) {
if (value(c[1]) == l_false && value(c[2]) == l_false) {
m_stats.m_ter_propagate++;
@ -482,17 +482,23 @@ namespace sat {
}
void solver::set_learned(clause& c, bool learned) {
if (c.is_learned() == learned)
return;
if (c.size() == 3) {
set_ternary_learned(get_wlist(~c[0]), c[1], c[2], learned);
set_ternary_learned(get_wlist(~c[1]), c[0], c[2], learned);
set_ternary_learned(get_wlist(~c[2]), c[0], c[1], learned);
}
c.set_learned(learned);
if (c.is_learned() != learned)
c.set_learned(learned);
}
void solver::set_learned1(literal l1, literal l2, bool learned) {
for (watched& w : get_wlist(~l1)) {
if (w.is_binary_clause() && l2 == w.get_literal() && !w.is_learned()) {
w.set_learned(learned);
break;
}
}
}
void solver::set_learned(literal l1, literal l2, bool learned) {
set_learned1(l1, l2, learned);
set_learned1(l2, l1, learned);
}
/**
\brief Select a watch literal starting the search at the given position.
@ -1523,7 +1529,7 @@ namespace sat {
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
si.check_watches();
si.check_watches();
if (!m_learned.empty()) {
m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation());

2
src/sat/sat_solver.h
View file

@ -234,6 +234,8 @@ namespace sat {
void attach_clause(clause & c, bool & reinit);
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
void set_learned(clause& c, bool learned);
void set_learned(literal l1, literal l2, bool learned);
void set_learned1(literal l1, literal l2, bool learned);
class scoped_disable_checkpoint {
solver& s;
public:

18
src/sat/sat_watched.cpp
View file

@ -71,29 +71,23 @@ namespace sat {
}
void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) {
watched w(l1, l2);
watch_list::iterator it = wlist.begin(), end = wlist.end();
watch_list::iterator it2 = it;
bool found = false;
for (; it != end; ++it) {
if (it->is_ternary_clause() && it->get_literal1() == l1 && it->get_literal2() == l2) {
if (!found && w == *it) {
found = true;
continue;
}
*it2 = *it;
++it2;
else {
*it2 = *it;
++it2;
}
}
wlist.set_end(it2);
VERIFY(found);
}
void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned) {
for (watched& w : wlist) {
if (w.is_ternary_clause() && w.get_literal1() == l1 && w.get_literal2() == l2) {
w.set_learned(learned);
}
}
}
void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
watch_list::iterator end = wlist.end();
for (; it != end; ++it, ++it2)

10
src/sat/sat_watched.h
View file

@ -53,12 +53,12 @@ namespace sat {
SASSERT(learned || is_binary_non_learned_clause());
}
watched(literal l1, literal l2, bool learned) {
watched(literal l1, literal l2) {
SASSERT(l1 != l2);
if (l1.index() > l2.index())
std::swap(l1, l2);
m_val1 = l1.to_uint();
m_val2 = static_cast<unsigned>(TERNARY) + (static_cast<unsigned>(learned) << 2) + (l2.to_uint() << 3);
m_val2 = static_cast<unsigned>(TERNARY) + (l2.to_uint() << 2);
SASSERT(is_ternary_clause());
SASSERT(get_literal1() == l1);
SASSERT(get_literal2() == l2);
@ -87,16 +87,16 @@ namespace sat {
bool is_binary_clause() const { return get_kind() == BINARY; }
literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); }
bool is_learned() const { SASSERT(is_binary_clause() || is_ternary_clause()); return ((m_val2 >> 2) & 1) == 1; }
bool is_learned() const { SASSERT(is_binary_clause()); return ((m_val2 >> 2) & 1) == 1; }
bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); }
bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); }
void set_learned(bool l) { SASSERT(is_learned() != l); if (l) m_val2 |= 4; else m_val2 &= 3; SASSERT(is_learned() == l); }
void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); }
bool is_ternary_clause() const { return get_kind() == TERNARY; }
literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); }
literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); }
bool is_clause() const { return get_kind() == CLAUSE; }
clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); }