mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-01-31 11:10:54 -08:00
commit a639452553
16 changed files with 256 additions and 286 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) { 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);
} }
/* /*

11
src/sat/sat_asymm_branch.cpp
View file

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

9
src/sat/sat_clause.cpp
View file

@ -87,6 +87,15 @@ namespace sat {
mark_strengthened(); 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 { bool clause::satisfied_by(model const & m) const {
for (literal l : *this) { for (literal l : *this) {
if (l.sign()) { 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]; } literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; }
bool is_learned() const { return m_learned; } bool is_learned() const { return m_learned; }
void set_learned(bool l) { SASSERT(is_learned() != l); m_learned = l; } 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; } bool strengthened() const { return m_strengthened; }
void mark_strengthened() { m_strengthened = true; update_approx(); } void mark_strengthened() { m_strengthened = true; update_approx(); }
void unmark_strengthened() { m_strengthened = false; } void unmark_strengthened() { m_strengthened = false; }

5
src/sat/sat_cleaner.cpp
View file

@ -145,10 +145,7 @@ namespace sat {
*it2 = *it; *it2 = *it;
it2++; it2++;
if (!c.frozen()) { if (!c.frozen()) {
if (new_sz == 3) s.attach_clause(c);
s.attach_ter_clause(c);
else
s.attach_nary_clause(c);
} }
if (s.m_config.m_drat) { if (s.m_config.m_drat) {
// for optimization, could also report deletion // 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); m_solver.detach_clause(c);
// apply substitution // apply substitution
for (i = 0; i < sz; i++) { for (i = 0; i < sz; i++) {
literal lit = c[i]; literal lit = c[i];
c[i] = norm(roots, lit); c[i] = norm(roots, lit);
VERIFY(c[i] == norm(roots, c[i])); 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()); std::sort(c.begin(), c.end());
for (literal l : c) VERIFY(l == norm(roots, l)); 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 pos_l(v, false);
literal neg_l(v, true); 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; 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; if (num_bin_neg > m_max_literals) return false;
clause_use_list & pos_occs = simp.m_use_list.get(pos_l); clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_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 It assumes wlist have been sorted using iff3_lt
*/ */
static bool contains(watch_list const & wlist, literal l1, literal l2) { 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) if (wlist.size() < SMALL_WLIST)
return wlist.contains(k); return wlist.contains(k);
iff3_lt lt; iff3_lt lt;

10
src/sat/sat_integrity_checker.cpp
View file

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

405
src/sat/sat_simplifier.cpp
View file

@ -148,27 +148,17 @@ namespace sat {
m_use_list.erase(c, l); m_use_list.erase(c, l);
} }
inline void simplifier::block_clause(clause & c) { inline void simplifier::set_learned(clause & c) {
if (m_retain_blocked_clauses) { m_need_cleanup = true;
m_need_cleanup = true; s.set_learned(c, true);
s.set_learned(c, true); m_use_list.block(c);
m_use_list.block(c);
}
else {
remove_clause(c);
}
} }
inline void simplifier::unblock_clause(clause & c) { inline void simplifier::set_learned(literal l1, literal l2) {
s.set_learned(c, false); m_sub_bin_todo.erase(bin_clause(l1, l2, false));
m_use_list.unblock(c); 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));
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));
} }
void simplifier::init_visited() { void simplifier::init_visited() {
@ -308,13 +298,16 @@ namespace sat {
clause_vector::iterator it = cs.begin(); clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it; clause_vector::iterator it2 = it;
clause_vector::iterator end = cs.end(); clause_vector::iterator end = cs.end();
unsigned nm = 0;
for (; it != end; ++it) { for (; it != end; ++it) {
clause & c = *(*it); clause & c = *(*it);
if (learned && !c.is_learned()) { if (learned && !c.is_learned()) {
s.m_clauses.push_back(&c); s.m_clauses.push_back(&c);
++nm;
} }
else if (!learned && c.is_learned()) { else if (!learned && c.is_learned()) {
s.m_learned.push_back(&c); s.m_learned.push_back(&c);
++nm;
} }
else { else {
*it2 = *it; *it2 = *it;
@ -373,19 +366,10 @@ namespace sat {
s.del_clause(c); s.del_clause(c);
continue; continue;
} }
// clause became a learned clause
if (!learned && c.is_learned()) {
SASSERT(!c.frozen());
s.m_learned.push_back(&c);
continue;
}
*it2 = *it; *it2 = *it;
it2++; it2++;
if (!c.frozen()) { if (!c.frozen()) {
if (sz == 3) s.attach_clause(c);
s.attach_ter_clause(c);
else
s.attach_nary_clause(c);
if (s.m_config.m_drat) { if (s.m_config.m_drat) {
s.m_drat.add(c, true); s.m_drat.add(c, true);
} }
@ -895,6 +879,7 @@ namespace sat {
break; break;
clause & c = m_sub_todo.erase(); clause & c = m_sub_todo.erase();
c.unmark_strengthened(); c.unmark_strengthened();
m_sub_counter--; m_sub_counter--;
TRACE("subsumption", tout << "next: " << c << "\n";); TRACE("subsumption", tout << "next: " << c << "\n";);
@ -944,21 +929,23 @@ namespace sat {
}; };
class clause_ante { class clause_ante {
bool m_from_ri;
literal m_lit1; literal m_lit1;
literal m_lit2; literal m_lit2;
clause* m_clause; clause* m_clause;
public: public:
clause_ante(): clause_ante():
m_lit1(null_literal), m_lit2(null_literal), m_clause(nullptr) {} m_from_ri(false), m_lit1(null_literal), m_lit2(null_literal), m_clause(nullptr) {}
clause_ante(literal l1): clause_ante(literal l1, bool from_ri):
m_lit1(l1), m_lit2(null_literal), m_clause(nullptr) {} m_from_ri(from_ri), m_lit1(l1), m_lit2(null_literal), m_clause(nullptr) {}
clause_ante(literal l1, literal l2): clause_ante(literal l1, literal l2):
m_lit1(l1), m_lit2(l2), m_clause(nullptr) {} m_from_ri(false), m_lit1(l1), m_lit2(l2), m_clause(nullptr) {}
clause_ante(clause& c): clause_ante(clause& c):
m_lit1(null_literal), m_lit2(null_literal), m_clause(&c) {} m_from_ri(false), m_lit1(null_literal), m_lit2(null_literal), m_clause(&c) {}
literal lit1() const { return m_lit1; } literal lit1() const { return m_lit1; }
literal lit2() const { return m_lit2; } literal lit2() const { return m_lit2; }
clause* cls() const { return m_clause; } clause* cls() const { return m_clause; }
bool from_ri() const { return m_from_ri; }
bool operator==(clause_ante const& a) const { bool operator==(clause_ante const& a) const {
return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause; return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause;
} }
@ -990,13 +977,12 @@ namespace sat {
int m_counter; int m_counter;
model_converter & mc; model_converter & mc;
queue m_queue; queue m_queue;
clause_vector m_to_remove;
literal_vector m_covered_clause; literal_vector m_covered_clause; // covered clause
svector<clause_ante> m_covered_antecedent; svector<clause_ante> m_covered_antecedent; // explainations for literals in covered clause
literal_vector m_intersection; literal_vector m_intersection; // current resolution intersection
literal_vector m_tautology; // literals that are used in blocking tautology
literal_vector m_new_intersection; literal_vector m_new_intersection;
literal_vector m_blocked_binary;
svector<bool> m_in_intersection; svector<bool> m_in_intersection;
sat::model_converter::elim_stackv m_elim_stack; sat::model_converter::elim_stackv m_elim_stack;
unsigned m_ala_qhead; unsigned m_ala_qhead;
@ -1080,43 +1066,27 @@ namespace sat {
} }
void process_binary(literal l) { void process_binary(literal l) {
m_blocked_binary.reset();
model_converter::entry* new_entry = 0; model_converter::entry* new_entry = 0;
watch_list & wlist = s.get_wlist(~l); watch_list & wlist = s.get_wlist(~l);
m_counter -= wlist.size(); m_counter -= wlist.size();
watch_list::iterator it = wlist.begin(); for (watched& w : wlist) {
watch_list::iterator it2 = it; if (!w.is_binary_non_learned_clause()) {
watch_list::iterator end = wlist.end();
for (; it != end; ++it) {
if (!it->is_binary_non_learned_clause()) {
*it2 = *it; it2++;
continue; continue;
} }
literal l2 = it->get_literal(); literal l2 = w.get_literal();
s.mark_visited(l2); s.mark_visited(l2);
if (all_tautology(l)) { if (all_tautology(l)) {
block_binary(it, l, new_entry); block_binary(w, l, new_entry);
s.m_num_blocked_clauses++; w.set_learned(true);
m_blocked_binary.push_back(l2); s.s.set_learned1(l2, l, true);
} s.m_num_bce++;
else {
*it2 = *it; it2++;
} }
s.unmark_visited(l2); 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) { void process_clauses(literal l) {
model_converter::entry* new_entry = 0; model_converter::entry* new_entry = 0;
m_to_remove.reset();
clause_use_list & occs = s.m_use_list.get(l); clause_use_list & occs = s.m_use_list.get(l);
clause_use_list::iterator it = occs.mk_iterator(); clause_use_list::iterator it = occs.mk_iterator();
for (; !it.at_end(); it.next()) { for (; !it.at_end(); it.next()) {
@ -1127,12 +1097,11 @@ namespace sat {
s.mark_all_but(c, l); s.mark_all_but(c, l);
if (all_tautology(l)) { if (all_tautology(l)) {
block_clause(c, l, new_entry); block_clause(c, l, new_entry);
s.m_num_blocked_clauses++; s.m_num_bce++;
s.set_learned(c);
} }
s.unmark_all(c); s.unmark_all(c);
} }
for (clause* c : m_to_remove)
s.block_clause(*c);
} }
void reset_intersection() { void reset_intersection() {
@ -1145,8 +1114,6 @@ namespace sat {
m_in_intersection[lit.index()] = true; m_in_intersection[lit.index()] = true;
} }
// //
// Resolve intersection // Resolve intersection
// Find literals that are in the intersection of all resolvents with l. // Find literals that are in the intersection of all resolvents with l.
@ -1155,6 +1122,7 @@ namespace sat {
if (!process_var(l.var())) return false; if (!process_var(l.var())) return false;
bool first = true; bool first = true;
reset_intersection(); reset_intersection();
m_tautology.reset();
for (watched & w : s.get_wlist(l)) { for (watched & w : s.get_wlist(l)) {
// when adding a blocked clause, then all non-learned clauses have to be considered for the // when adding a blocked clause, then all non-learned clauses have to be considered for the
// resolution intersection. // resolution intersection.
@ -1162,6 +1130,7 @@ namespace sat {
if (process_bin) { if (process_bin) {
literal lit = w.get_literal(); literal lit = w.get_literal();
if (s.is_marked(~lit) && lit != ~l) { if (s.is_marked(~lit) && lit != ~l) {
m_tautology.push_back(~lit);
continue; // tautology continue; // tautology
} }
if (!first || s.is_marked(lit)) { if (!first || s.is_marked(lit)) {
@ -1178,8 +1147,10 @@ namespace sat {
bool tautology = false; bool tautology = false;
clause & c = it.curr(); clause & c = it.curr();
if (c.is_learned() && !adding) continue; if (c.is_learned() && !adding) continue;
if (c.was_removed()) continue;
for (literal lit : c) { for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) { if (s.is_marked(~lit) && lit != ~l) {
m_tautology.push_back(~lit);
tautology = true; tautology = true;
break; break;
} }
@ -1204,25 +1175,30 @@ namespace sat {
return false; return false;
} }
} }
// if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";);
return first; return first;
} }
bool check_abce_tautology(literal l) { bool check_abce_tautology(literal l) {
m_tautology.reset();
if (!process_var(l.var())) return false; if (!process_var(l.var())) return false;
for (watched & w : s.get_wlist(l)) { for (watched & w : s.get_wlist(l)) {
if (w.is_binary_non_learned_clause()) { if (w.is_binary_non_learned_clause()) {
literal lit = w.get_literal(); 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); clause_use_list & neg_occs = s.m_use_list.get(~l);
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
clause & c = it.curr(); clause & c = it.curr();
if (c.is_learned()) continue; if (c.is_learned() || c.was_removed()) continue;
bool tautology = false; bool tautology = false;
for (literal lit : c) { for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) { if (s.is_marked(~lit) && lit != ~l) {
tautology = true; tautology = true;
m_tautology.push_back(~lit);
break; break;
} }
} }
@ -1237,53 +1213,65 @@ namespace sat {
(m_clause[0] == l2 && m_clause[1] == l1)); (m_clause[0] == l2 && m_clause[1] == l1));
} }
bool revisit_ternary(literal l1, literal l2, literal l3) const {
return m_clause.size() == 3 &&
((m_clause[0] == l1 && m_clause[1] == l2 && m_clause[2] == l3) ||
(m_clause[0] == l2 && m_clause[1] == l1 && m_clause[2] == l3) ||
(m_clause[0] == l2 && m_clause[1] == l3 && m_clause[2] == l1) ||
(m_clause[0] == l1 && m_clause[1] == l3 && m_clause[2] == l2) ||
(m_clause[0] == l3 && m_clause[1] == l1 && m_clause[2] == l2) ||
(m_clause[0] == l3 && m_clause[1] == l2 && m_clause[2] == l1));
}
bool revisit_clause(clause const& c) const { bool revisit_clause(clause const& c) const {
return !m_clause.is_binary() && (m_clause.get_clause() == &c); 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) { 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_covered_clause) s.unmark_visited(l);
for (literal l : m_tautology) s.mark_visited(l);
s.mark_visited(m_covered_clause[idx]); s.mark_visited(m_covered_clause[idx]);
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
literal lit = m_covered_clause[i];
if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
if (s.is_marked(lit)) idx = i;
}
for (unsigned i = idx; i > 0; --i) { for (unsigned i = idx; i > 0; --i) {
literal lit = m_covered_clause[i]; literal lit = m_covered_clause[i];
if (!s.is_marked(lit)) continue; if (!s.is_marked(lit)) continue;
clause_ante const& ante = m_covered_antecedent[i]; clause_ante const& ante = m_covered_antecedent[i];
if (ante.cls()) { if (ante.cls()) {
for (literal l : *ante.cls()) { for (literal l : *ante.cls()) {
IF_VERBOSE(0, verbose_stream() << "clause ante: " << l << "\n";);
if (l != ~lit) s.mark_visited(l); if (l != ~lit) s.mark_visited(l);
} }
} }
if (ante.lit1() != null_literal) { if (ante.lit1() != null_literal) {
IF_VERBOSE(0, verbose_stream() << "ante1: " << ante.lit1() << "\n";);
s.mark_visited(ante.lit1()); s.mark_visited(ante.lit1());
} }
if (ante.lit2() != null_literal) { if (ante.lit2() != null_literal) {
IF_VERBOSE(0, verbose_stream() << "ante2: " << ante.lit2() << "\n";);
s.mark_visited(ante.lit2()); s.mark_visited(ante.lit2());
} }
} }
unsigned j = 0; unsigned j = 0;
literal blocked = null_literal;
for (unsigned i = 0; i <= idx; ++i) { for (unsigned i = 0; i <= idx; ++i) {
literal lit = m_covered_clause[i]; literal lit = m_covered_clause[i];
if (s.is_marked(lit) || m_covered_antecedent[i] == clause_ante()) { if (s.is_marked(lit)) {
//
// Record that the resolving literal for
// resolution intersection can be flipped.
//
clause_ante const& ante = m_covered_antecedent[i];
if (ante.from_ri() && blocked != ante.lit1()) {
blocked = ante.lit1();
m_elim_stack.push_back(std::make_pair(j, blocked));
}
m_covered_clause[j++] = lit; m_covered_clause[j++] = lit;
s.unmark_visited(lit); s.unmark_visited(lit);
} }
} }
for (literal l : m_covered_clause) VERIFY(!s.is_marked(l));
// unsigned sz0 = m_covered_clause.size();
m_covered_clause.resize(j); 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";);
} }
/* /*
@ -1308,66 +1296,41 @@ namespace sat {
literal lit = w.get_literal(); literal lit = w.get_literal();
if (revisit_binary(l, lit)) continue; if (revisit_binary(l, lit)) continue;
if (s.is_marked(lit)) { if (s.is_marked(lit)) {
IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";);
return true; return true;
} }
if (!s.is_marked(~lit)) { if (!s.is_marked(~lit)) {
IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";);
m_covered_clause.push_back(~lit); m_covered_clause.push_back(~lit);
m_covered_antecedent.push_back(clause_ante(l)); m_covered_antecedent.push_back(clause_ante(l, false));
s.mark_visited(~lit); s.mark_visited(~lit);
} }
} }
else if (w.is_ternary_clause() && !w.is_learned()) { }
literal lit1 = w.get_literal1(); clause_use_list & pos_occs = s.m_use_list.get(l);
literal lit2 = w.get_literal2(); clause_use_list::iterator it = pos_occs.mk_iterator();
if (revisit_ternary(l, lit1, lit2)) continue; for (; !it.at_end(); it.next()) {
if (s.is_marked(lit1) && s.is_marked(lit2)) { clause & c = it.curr();
IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " ternary: " << l << " " << lit1 << " " << lit2 << "\n";); if (c.is_learned() || c.was_removed()) continue;
return true; 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)) { else {
IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternary " << l << " " << lit1 << " " << lit2 << " " << (~lit2) << "\n";); ok = false;
m_covered_clause.push_back(~lit2); break;
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 if (w.is_clause()) { if (!ok) continue;
clause & c = s.s.get_clause(w.get_clause_offset()); if (lit1 == null_literal) {
if (c.is_learned()) continue; return true;
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);
} }
m_covered_clause.push_back(~lit1);
m_covered_antecedent.push_back(clause_ante(c));
s.mark_visited(~lit1);
} }
} }
return false; return false;
@ -1389,14 +1352,11 @@ namespace sat {
minimize_covered_clause(i); minimize_covered_clause(i);
return true; return true;
} }
if (!m_intersection.empty()) {
m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
}
for (literal l : m_intersection) { for (literal l : m_intersection) {
if (!s.is_marked(l)) { if (!s.is_marked(l)) {
s.mark_visited(l); s.mark_visited(l);
m_covered_clause.push_back(l); m_covered_clause.push_back(l);
m_covered_antecedent.push_back(clause_ante(lit)); m_covered_antecedent.push_back(clause_ante(lit, true));
} }
} }
} }
@ -1430,10 +1390,9 @@ namespace sat {
for (literal l : m_covered_clause) s.unmark_visited(l); for (literal l : m_covered_clause) s.unmark_visited(l);
return at_t; 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])) { if (check_abce_tautology(m_covered_clause[i])) {
blocked = m_covered_clause[i]; blocked = m_covered_clause[i];
minimize_covered_clause(i);
is_tautology = true; is_tautology = true;
break; break;
} }
@ -1456,7 +1415,6 @@ namespace sat {
is_tautology = add_cla(blocked); is_tautology = add_cla(blocked);
} }
while (m_covered_clause.size() > sz && !is_tautology); while (m_covered_clause.size() > sz && !is_tautology);
if (above_threshold(sz0)) break;
if (et == acce_t && !is_tautology) { if (et == acce_t && !is_tautology) {
sz = m_covered_clause.size(); sz = m_covered_clause.size();
if (add_ala()) { if (add_ala()) {
@ -1465,11 +1423,11 @@ namespace sat {
} }
k = model_converter::ACCE; k = model_converter::ACCE;
} }
if (above_threshold(sz0)) break;
} }
while (m_covered_clause.size() > sz && !is_tautology); 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); for (literal l : m_covered_clause) s.unmark_visited(l);
return (is_tautology && !above_threshold(sz0)) ? bc_t : no_t; return is_tautology ? bc_t : no_t;
} }
// perform covered clause elimination. // perform covered clause elimination.
@ -1484,6 +1442,7 @@ namespace sat {
m_covered_clause.push_back(l); m_covered_clause.push_back(l);
m_covered_antecedent.push_back(clause_ante()); m_covered_antecedent.push_back(clause_ante());
} }
// shuffle<literal>(s.s.m_rand, m_covered_clause);
return cla<et>(blocked, k); return cla<et>(blocked, k);
} }
@ -1516,81 +1475,68 @@ namespace sat {
template<elim_type et> template<elim_type et>
void process_cce_binary(literal l) { void process_cce_binary(literal l) {
m_blocked_binary.reset();
literal blocked = null_literal; literal blocked = null_literal;
watch_list & wlist = s.get_wlist(~l); watch_list & wlist = s.get_wlist(~l);
m_counter -= wlist.size(); 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; model_converter::kind k;
for (; it != end; ++it) { for (watched & w : wlist) {
if (!it->is_binary_non_learned_clause()) { if (!w.is_binary_non_learned_clause()) continue;
*it2 = *it; literal l2 = w.get_literal();
it2++;
continue;
}
literal l2 = it->get_literal();
switch (cce<et>(l, l2, blocked, k)) { switch (cce<et>(l, l2, blocked, k)) {
case bc_t: case bc_t:
block_covered_binary(it, l, blocked, k); inc_bc<et>();
s.m_num_covered_clauses++; block_covered_binary(w, l, blocked, k);
m_blocked_binary.push_back(l2); w.set_learned(true);
s.s.set_learned1(l2, l, true);
break; break;
case at_t: case at_t:
s.m_num_ate++; s.m_num_ate++;
m_blocked_binary.push_back(l2); w.set_learned(true);
s.s.set_learned1(l2, l, true);
break; break;
case no_t: case no_t:
*it2 = *it;
it2++;
break; 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> template<elim_type et>
void cce_clauses() { void cce_clauses() {
m_to_remove.reset();
literal blocked; literal blocked;
model_converter::kind k; model_converter::kind k;
for (clause* cp : s.s.m_clauses) { for (clause* cp : s.s.m_clauses) {
clause& c = *cp; clause& c = *cp;
if (!c.was_removed() && !c.is_learned()) { if (c.was_removed() || c.is_learned()) continue;
switch (cce<et>(c, blocked, k)) { switch (cce<et>(c, blocked, k)) {
case bc_t: case bc_t:
block_covered_clause(c, blocked, k); inc_bc<et>();
s.m_num_covered_clauses++; block_covered_clause(c, blocked, k);
break; s.set_learned(c);
case at_t: break;
m_to_remove.push_back(&c); case at_t:
break; s.m_num_ate++;
case no_t: s.set_learned(c);
break; 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) { 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";); TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
VERIFY(!s.is_external(l)); VERIFY(!s.is_external(l));
if (new_entry == 0) if (new_entry == 0)
new_entry = &(mc.mk(k, l.var())); new_entry = &(mc.mk(k, l.var()));
m_to_remove.push_back(&c);
for (literal lit : c) { for (literal lit : c) {
if (lit != l && process_var(lit.var())) { if (lit != l && process_var(lit.var())) {
m_queue.decreased(~lit); m_queue.decreased(~lit);
@ -1611,25 +1557,25 @@ namespace sat {
mc.insert(*new_entry, m_covered_clause, m_elim_stack); 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)); SASSERT(!s.is_external(blocked));
if (new_entry == 0) if (new_entry == 0)
new_entry = &(mc.mk(k, blocked.var())); 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";); 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); m_queue.decreased(~l2);
} }
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { void block_binary(watched const& w, literal l, model_converter::entry *& new_entry) {
literal l2 = it->get_literal(); literal l2 = w.get_literal();
prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT); prepare_block_binary(w, l, l, new_entry, model_converter::BLOCK_LIT);
mc.insert(*new_entry, l, l2); 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; 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); mc.insert(*new_entry, m_covered_clause, m_elim_stack);
} }
@ -1681,6 +1627,7 @@ namespace sat {
for (; !it.at_end(); it.next()) { for (; !it.at_end(); it.next()) {
clause & c = it.curr(); clause & c = it.curr();
if (c.is_learned()) continue; if (c.is_learned()) continue;
if (c.was_removed()) continue;
m_counter -= c.size(); m_counter -= c.size();
unsigned sz = c.size(); unsigned sz = c.size();
unsigned i; unsigned i;
@ -1707,33 +1654,40 @@ namespace sat {
struct simplifier::blocked_cls_report { struct simplifier::blocked_cls_report {
simplifier & m_simplifier; simplifier & m_simplifier;
stopwatch m_watch; stopwatch m_watch;
unsigned m_num_blocked_clauses; unsigned m_num_bce;
unsigned m_num_covered_clauses; unsigned m_num_cce;
unsigned m_num_acce;
unsigned m_num_abce;
unsigned m_num_ate; unsigned m_num_ate;
unsigned m_num_added_clauses; unsigned m_num_bca;
blocked_cls_report(simplifier & s): blocked_cls_report(simplifier & s):
m_simplifier(s), m_simplifier(s),
m_num_blocked_clauses(s.m_num_blocked_clauses), m_num_bce(s.m_num_bce),
m_num_covered_clauses(s.m_num_covered_clauses), 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_ate(s.m_num_ate),
m_num_added_clauses(s.m_num_bca) { m_num_bca(s.m_num_bca) {
m_watch.start(); m_watch.start();
} }
~blocked_cls_report() { ~blocked_cls_report() {
m_watch.stop(); m_watch.stop();
IF_VERBOSE(SAT_VB_LVL, IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses " verbose_stream() << " (sat-blocked-clauses";
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) report(m_simplifier.m_num_ate, m_num_ate, " :ate ");
<< " :elim-covered-clauses " report(m_simplifier.m_num_bce, m_num_bce, " :bce ");
<< (m_simplifier.m_num_covered_clauses - m_num_covered_clauses) report(m_simplifier.m_num_abce, m_num_abce, " :abce ");
<< " :added-clauses " report(m_simplifier.m_num_cce, m_num_cce, " :cce ");
<< (m_simplifier.m_num_bca - m_num_added_clauses) report(m_simplifier.m_num_bca, m_num_bca, " :bca ");
<< " :ate " report(m_simplifier.m_num_acce, m_num_acce, " :acce ");
<< (m_simplifier.m_num_ate - m_num_ate) verbose_stream() << mem_stat()
<< mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); << " :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() { void simplifier::elim_blocked_clauses() {
@ -1743,7 +1697,7 @@ namespace sat {
elim(); elim();
} }
unsigned simplifier::get_num_unblocked_bin(literal l) const { unsigned simplifier::num_nonlearned_bin(literal l) const {
unsigned r = 0; unsigned r = 0;
watch_list const & wlist = get_wlist(~l); watch_list const & wlist = get_wlist(~l);
for (auto & w : wlist) { for (auto & w : wlist) {
@ -1758,8 +1712,8 @@ namespace sat {
literal neg_l(v, true); literal neg_l(v, true);
unsigned num_pos = m_use_list.get(pos_l).size(); unsigned num_pos = m_use_list.get(pos_l).size();
unsigned num_neg = m_use_list.get(neg_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_pos = num_nonlearned_bin(pos_l);
unsigned num_bin_neg = get_num_unblocked_bin(neg_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; 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 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";); << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
@ -1799,9 +1753,10 @@ namespace sat {
void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) { void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
clause_use_list const & cs = m_use_list.get(l); clause_use_list const & cs = m_use_list.get(l);
for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
if (!it.curr().is_learned()) { clause& c = it.curr();
r.push_back(clause_wrapper(it.curr())); if (!c.is_learned() && !c.was_removed()) {
SASSERT(r.back().size() == it.curr().size()); r.push_back(clause_wrapper(c));
SASSERT(r.back().size() == c.size());
} }
} }
@ -1939,8 +1894,8 @@ namespace sat {
literal pos_l(v, false); literal pos_l(v, false);
literal neg_l(v, true); literal neg_l(v, true);
unsigned num_bin_pos = get_num_unblocked_bin(pos_l); unsigned num_bin_pos = num_nonlearned_bin(pos_l);
unsigned num_bin_neg = get_num_unblocked_bin(neg_l); unsigned num_bin_neg = num_nonlearned_bin(neg_l);
clause_use_list & pos_occs = m_use_list.get(pos_l); clause_use_list & pos_occs = m_use_list.get(pos_l);
clause_use_list & neg_occs = m_use_list.get(neg_l); clause_use_list & neg_occs = m_use_list.get(neg_l);
unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos; unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos;
@ -2146,15 +2101,19 @@ namespace sat {
st.update("subsumed", m_num_subsumed); st.update("subsumed", m_num_subsumed);
st.update("subsumption resolution", m_num_sub_res); st.update("subsumption resolution", m_num_sub_res);
st.update("elim literals", m_num_elim_lits); st.update("elim literals", m_num_elim_lits);
st.update("elim blocked clauses", m_num_blocked_clauses); st.update("bce", m_num_bce);
st.update("elim covered clauses", m_num_covered_clauses); st.update("cce", m_num_cce);
st.update("blocked clauses added", m_num_bca); st.update("acce", m_num_acce);
st.update("asymmetric tautologies eliminated", m_num_ate); st.update("abce", m_num_abce);
st.update("bca", m_num_bca);
st.update("ate", m_num_ate);
} }
void simplifier::reset_statistics() { void simplifier::reset_statistics() {
m_num_blocked_clauses = 0; m_num_bce = 0;
m_num_covered_clauses = 0; m_num_cce = 0;
m_num_acce = 0;
m_num_abce = 0;
m_num_subsumed = 0; m_num_subsumed = 0;
m_num_sub_res = 0; m_num_sub_res = 0;
m_num_elim_lits = 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; unsigned m_elim_vars_bdd_delay;
// stats // stats
unsigned m_num_blocked_clauses; unsigned m_num_bce;
unsigned m_num_covered_clauses; 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_subsumed;
unsigned m_num_elim_vars; unsigned m_num_elim_vars;
unsigned m_num_sub_res; unsigned m_num_sub_res;
unsigned m_num_elim_lits; unsigned m_num_elim_lits;
unsigned m_num_bca;
unsigned m_num_ate;
bool m_learned_in_use_lists; bool m_learned_in_use_lists;
unsigned m_old_num_elim_vars; unsigned m_old_num_elim_vars;
@ -132,9 +134,8 @@ namespace sat {
void remove_clause_core(clause & c); void remove_clause_core(clause & c);
void remove_clause(clause & c); void remove_clause(clause & c);
void remove_clause(clause & c, literal l); void remove_clause(clause & c, literal l);
void block_clause(clause & c); void set_learned(clause & c);
void unblock_clause(clause & c); void set_learned(literal l1, literal l2);
void remove_bin_clause_half(literal l1, literal l2, bool learned);
bool_var get_min_occ_var(clause const & c) const; bool_var get_min_occ_var(clause const & c) const;
bool subsumes1(clause const & c1, clause const & c2, literal & l); 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_bdd_enabled() const;
bool elim_vars_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; unsigned get_to_elim_cost(bool_var v) const;
void order_vars_for_elim(bool_var_vector & r); void order_vars_for_elim(bool_var_vector & r);
void collect_clauses(literal l, clause_wrapper_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 solver::attach_ter_clause(clause & c) {
bool reinit = false; bool reinit = false;
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2], 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], c.is_learned())); m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
m_watches[(~c[2]).index()].push_back(watched(c[0], c[1], c.is_learned())); m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
if (!at_base_lvl()) { if (!at_base_lvl()) {
if (value(c[1]) == l_false && value(c[2]) == l_false) { if (value(c[1]) == l_false && value(c[2]) == l_false) {
m_stats.m_ter_propagate++; m_stats.m_ter_propagate++;
@ -482,17 +482,23 @@ namespace sat {
} }
void solver::set_learned(clause& c, bool learned) { void solver::set_learned(clause& c, bool learned) {
if (c.is_learned() == learned) if (c.is_learned() != learned)
return; c.set_learned(learned);
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);
} }
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. \brief Select a watch literal starting the search at the given position.
@ -1523,7 +1529,7 @@ namespace sat {
m_simplifier(false); m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_missed_prop", check_missed_propagation());
si.check_watches(); si.check_watches();
if (!m_learned.empty()) { if (!m_learned.empty()) {
m_simplifier(true); m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation()); 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);
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); } void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
void set_learned(clause& c, bool learned); 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 { class scoped_disable_checkpoint {
solver& s; solver& s;
public: 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) { 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 it = wlist.begin(), end = wlist.end();
watch_list::iterator it2 = it; watch_list::iterator it2 = it;
bool found = false; bool found = false;
for (; it != end; ++it) { for (; it != end; ++it) {
if (it->is_ternary_clause() && it->get_literal1() == l1 && it->get_literal2() == l2) { if (!found && w == *it) {
found = true; found = true;
continue;
} }
*it2 = *it; else {
++it2; *it2 = *it;
++it2;
}
} }
wlist.set_end(it2); wlist.set_end(it2);
VERIFY(found); 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) { void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
watch_list::iterator end = wlist.end(); watch_list::iterator end = wlist.end();
for (; it != end; ++it, ++it2) 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()); SASSERT(learned || is_binary_non_learned_clause());
} }
watched(literal l1, literal l2, bool learned) { watched(literal l1, literal l2) {
SASSERT(l1 != l2); SASSERT(l1 != l2);
if (l1.index() > l2.index()) if (l1.index() > l2.index())
std::swap(l1, l2); std::swap(l1, l2);
m_val1 = l1.to_uint(); 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(is_ternary_clause());
SASSERT(get_literal1() == l1); SASSERT(get_literal1() == l1);
SASSERT(get_literal2() == l2); SASSERT(get_literal2() == l2);
@ -87,16 +87,16 @@ namespace sat {
bool is_binary_clause() const { return get_kind() == BINARY; } 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)); } 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(); } 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_learned_clause() const { return is_binary_clause() && is_learned(); }
bool is_binary_non_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; } 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_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; } bool is_clause() const { return get_kind() == CLAUSE; }
clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); } clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); }