From a954ab7d8db1c62a6bcb295da21e63a821b69248 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Apr 2018 08:38:01 -0700 Subject: [PATCH] flip literals in ATEs produced using RI Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 1 + src/sat/sat_big.cpp | 4 +- src/sat/sat_model_converter.cpp | 76 ++++++++++---- src/sat/sat_model_converter.h | 23 +++-- src/sat/sat_simplifier.cpp | 172 +++++++++++++++++++++++--------- src/sat/sat_solver.cpp | 29 ++++-- src/sat/sat_solver.h | 4 + 7 files changed, 224 insertions(+), 85 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 65003a6e4..b2053c68f 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -410,6 +410,7 @@ namespace sat { if (c.is_learned()) { m_elim_learned_literals += c.size() - new_sz; } + switch(new_sz) { case 0: s.set_conflict(justification()); diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 2f1a3727f..27b87d4c9 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -194,7 +194,9 @@ namespace sat { if (u != get_parent(v) && safe_reach(u, v)) { ++elim; add_del(~u, v); - // IF_VERBOSE(1, verbose_stream() << "remove " << u << " -> " << v << "\n"); + if (s.get_config().m_drat) s.m_drat.del(~u, v); + s.m_mc.stackv().reset(); // TBD: brittle code + s.add_ate(~u, v); if (find_binary_watch(wlist, ~v)) { IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n"); s.assign(~u, justification()); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c2a4858f7..bebb3e384 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,33 +75,41 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = false; // true; + bool first = true; // false; // true; // false; // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; bool_var v0 = it->var(); - SASSERT(it->get_kind() != ELIM_VAR || m[v0] == l_undef); - // if it->get_kind() == BLOCK_LIT, then it might be the case that m[v] != l_undef, + SASSERT(it->get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef); + // if it->get_kind() == BCE, then it might be the case that m[v] != l_undef, // and the following procedure flips its value. bool sat = false; bool var_sign = false; unsigned index = 0; literal_vector clause; - VERIFY(legal_to_flip(v0)); + VERIFY(v0 == null_bool_var || legal_to_flip(v0)); for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause - elim_stack* st = it->m_elim_stack[index]; - if (!sat) { + if (!sat && it->get_kind() == ATE) { + IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n"); + IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";); + IF_VERBOSE(0, display(verbose_stream())); + exit(0); + first = false; + } + if (!sat && it->get_kind() != ATE && v0 != null_bool_var) { VERIFY(legal_to_flip(v0)); m[v0] = var_sign ? l_false : l_true; } + elim_stack* st = it->m_elim_stack[index]; if (st) { process_stack(m, clause, st->stack()); } sat = false; if (first && m_solver && !m_solver->check_clauses(m)) { IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n"); + IF_VERBOSE(0, display(verbose_stream())); first = false; } ++index; @@ -191,17 +199,43 @@ namespace sat { entry & e = m_entries.back(); SASSERT(e.var() == v); SASSERT(e.get_kind() == k); - VERIFY(legal_to_flip(v)); + VERIFY(v == null_bool_var || legal_to_flip(v)); return e; } + void model_converter::add_ate(clause const& c) { + if (stackv().empty()) return; + insert(mk(ATE, null_bool_var), c); + } + + void model_converter::add_ate(literal_vector const& lits) { + if (stackv().empty()) return; + insert(mk(ATE, null_bool_var), lits); + } + + void model_converter::add_ate(literal l1, literal l2) { + if (stackv().empty()) return; + insert(mk(ATE, null_bool_var), l1, l2); + } + + void model_converter::add_elim_stack(entry & e) { + e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv())); +#if 0 + if (!stackv().empty() && e.get_kind() == ATE) { + IF_VERBOSE(0, display(verbose_stream(), e) << "\n"); + } +#endif + for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var())); + stackv().reset(); + } + void model_converter::insert(entry & e, clause const & c) { SASSERT(c.contains(e.var())); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(nullptr); + add_elim_stack(e); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } @@ -212,7 +246,7 @@ namespace sat { e.m_clauses.push_back(l1); e.m_clauses.push_back(l2); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(nullptr); + add_elim_stack(e); TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";); } @@ -224,18 +258,17 @@ namespace sat { for (unsigned i = 0; i < sz; ++i) e.m_clauses.push_back(c[i]); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(nullptr); + add_elim_stack(e); // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } - void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) { + void model_converter::insert(entry & e, literal_vector const& c) { SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true))); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims)); - for (auto const& s : elims) VERIFY(legal_to_flip(s.second.var())); + add_elim_stack(e); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } @@ -246,7 +279,7 @@ namespace sat { vector::const_iterator it = m_entries.begin(); vector::const_iterator end = m_entries.end(); for (; it != end; ++it) { - SASSERT(it->var() < num_vars); + SASSERT(it->var() == null_bool_var || it->var() < num_vars); if (it->get_kind() == ELIM_VAR) { svector::const_iterator it2 = it; it2++; @@ -276,7 +309,8 @@ namespace sat { } std::ostream& model_converter::display(std::ostream& out, entry const& entry) const { - out << " (" << entry.get_kind() << " " << entry.var(); + out << " (" << entry.get_kind() << " "; + if (entry.var() != null_bool_var) out << entry.var(); bool start = true; unsigned index = 0; for (literal l : entry.m_clauses) { @@ -306,7 +340,7 @@ namespace sat { } out << ")"; for (literal l : entry.m_clauses) { - if (l != null_literal) { + if (l != null_literal && l.var() != null_bool_var) { if (false && m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l; } } @@ -333,7 +367,7 @@ namespace sat { for (entry const& e : m_entries) { for (literal l : e.m_clauses) { if (l != null_literal) { - if (l.var() > result) + if (l.var() != null_bool_var && l.var() > result) result = l.var(); } } @@ -372,9 +406,11 @@ namespace sat { update_stack.push_back(null_literal); } } - swap(e.var(), clause.size(), clause); - update_stack.append(clause); - update_stack.push_back(null_literal); + if (e.var() != null_bool_var) { + swap(e.var(), clause.size(), clause); + update_stack.append(clause); + update_stack.push_back(null_literal); + } clause.reset(); } else { diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index bc60844ca..65e132729 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -66,11 +66,11 @@ namespace sat { unsigned ref_count() const { return m_refcount; } }; - enum kind { ELIM_VAR = 0, BLOCK_LIT, CCE, ACCE }; + enum kind { ELIM_VAR = 0, BCE, CCE, ACCE, ABCE, ATE }; class entry { friend class model_converter; - unsigned m_var:30; - unsigned m_kind:2; + bool_var m_var; + kind m_kind; literal_vector m_clauses; // the different clauses are separated by null_literal sref_vector m_elim_stack; entry(kind k, bool_var v): m_var(v), m_kind(k) {} @@ -82,11 +82,12 @@ namespace sat { m_elim_stack.append(src.m_elim_stack); } bool_var var() const { return m_var; } - kind get_kind() const { return static_cast(m_kind); } + kind get_kind() const { return m_kind; } }; private: vector m_entries; solver const* m_solver; + elim_stackv m_elim_stack; void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const; @@ -96,6 +97,8 @@ namespace sat { void swap(bool_var v, unsigned sz, literal_vector& clause); + void add_elim_stack(entry & e); + public: model_converter(); ~model_converter(); @@ -103,11 +106,17 @@ namespace sat { void operator()(model & m) const; model_converter& operator=(model_converter const& other); + elim_stackv& stackv() { return m_elim_stack; } + entry & mk(kind k, bool_var v); void insert(entry & e, clause const & c); void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); - void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack); + void insert(entry & c, literal_vector const& covered_clause); + + void add_ate(literal_vector const& lits); + void add_ate(literal l1, literal l2); + void add_ate(clause const& c); bool empty() const { return m_entries.empty(); } @@ -137,9 +146,11 @@ namespace sat { inline std::ostream& operator<<(std::ostream& out, model_converter::kind k) { switch (k) { case model_converter::ELIM_VAR: out << "elim"; break; - case model_converter::BLOCK_LIT: out << "blocked"; break; + case model_converter::BCE: out << "bce"; break; case model_converter::CCE: out << "cce"; break; case model_converter::ACCE: out << "acce"; break; + case model_converter::ABCE: out << "abce"; break; + case model_converter::ATE: out << "ate"; break; } return out; } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index bac790698..52c7236a0 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -939,16 +939,21 @@ namespace sat { bool operator==(clause_ante const& a) const { return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause; } - std::ostream& display(std::ostream& out) const { + std::ostream& display(std::ostream& out, literal lit) const { if (cls()) { out << *cls() << " "; } + else { + out << "(" << ~lit; + } if (lit1() != null_literal) { - out << lit1() << " "; + out << " " << lit1(); } if (lit2() != null_literal) { - out << lit2() << " "; + out << " " << lit2(); } + if (!cls()) out << ")"; + if (from_ri()) out << "ri"; out << "\n"; return out; } @@ -978,7 +983,7 @@ namespace sat { simplifier & s; int m_counter; - model_converter & mc; + model_converter & m_mc; queue m_queue; literal_vector m_covered_clause; // covered clause @@ -987,7 +992,6 @@ namespace sat { literal_vector m_tautology; // literals that are used in blocking tautology literal_vector m_new_intersection; svector m_in_intersection; - sat::model_converter::elim_stackv m_elim_stack; unsigned m_ala_qhead; clause_wrapper m_clause; @@ -995,7 +999,7 @@ namespace sat { vector & wlist): s(_s), m_counter(limit), - mc(_mc), + m_mc(_mc), m_queue(l, wlist), m_clause(null_literal, null_literal) { m_in_intersection.resize(s.s.num_vars() * 2, false); @@ -1069,6 +1073,7 @@ namespace sat { m_tautology.reset(); if (!process_var(l.var())) return false; bool first = true; + VERIFY(s.value(l) == l_undef); 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. @@ -1184,18 +1189,18 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } - if (false && _blocked.var() == 16774) { + if (false) { IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; verbose_stream() << "tautology: " << m_tautology << "\n"; verbose_stream() << "index: " << idx << "\n"; for (unsigned i = idx; i > 0; --i) { - m_covered_antecedent[i].display(verbose_stream() << "ante " << m_covered_clause[i] << ":"); + m_covered_antecedent[i].display(verbose_stream(), m_covered_clause[i]); }); } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; - s.mark_visited(lit); - continue; + //s.mark_visited(lit); + //continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { @@ -1222,13 +1227,16 @@ namespace sat { 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)); + VERIFY(s.value(blocked) == l_undef); + m_mc.stackv().push_back(std::make_pair(j, blocked)); } m_covered_clause[j++] = lit; s.unmark_visited(lit); } } for (literal l : m_covered_clause) VERIFY(!s.is_marked(l)); + for (bool_var v = 0; v < s.s.num_vars(); ++v) VERIFY(!s.is_marked(literal(v, true)) && !s.is_marked(literal(v, false))); + // unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); VERIFY(j >= m_clause.size()); @@ -1263,6 +1271,7 @@ namespace sat { return true; } if (!s.is_marked(~lit)) { + // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n"); m_covered_clause.push_back(~lit); m_covered_antecedent.push_back(clause_ante(l, false)); s.mark_visited(~lit); @@ -1292,6 +1301,7 @@ namespace sat { if (lit1 == null_literal) { return true; } + // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n"); m_covered_clause.push_back(~lit1); m_covered_antecedent.push_back(clause_ante(c)); s.mark_visited(~lit1); @@ -1332,13 +1342,17 @@ namespace sat { return sz0 * 400 < m_covered_clause.size(); } + void reset_mark() { + for (literal l : m_covered_clause) s.unmark_visited(l); + } + template elim_type cce(literal& blocked, model_converter::kind& k) { - bool is_tautology = false, first = true; + bool first = true; unsigned sz = 0, sz0 = m_covered_clause.size(); for (literal l : m_covered_clause) s.mark_visited(l); shuffle(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand); - m_elim_stack.reset(); + m_mc.stackv().reset(); m_ala_qhead = 0; switch (et) { @@ -1349,7 +1363,7 @@ namespace sat { k = model_converter::ACCE; break; default: - k = model_converter::BLOCK_LIT; + k = model_converter::BCE; break; } @@ -1361,48 +1375,77 @@ namespace sat { * and then check if any of the first sz0 literals are blocked. */ - while (!is_tautology && m_covered_clause.size() > sz && !above_threshold(sz0)) { - SASSERT(!is_tautology); + if (et == ate_t) { + bool ala = add_ala(); + reset_mark(); + m_covered_clause.shrink(sz0); + return ala ? ate_t : no_t; + } - if ((et == abce_t || et == acce_t || et == ate_t) && add_ala()) { - for (literal l : m_covered_clause) s.unmark_visited(l); + while (m_covered_clause.size() > sz && !above_threshold(sz0)) { + + if ((et == abce_t || et == acce_t) && add_ala()) { + reset_mark(); + if (first) { + m_covered_clause.shrink(sz0); + } + else { + /* + * tautology depends on resolution intersection. + * literals used for resolution intersection may have to be flipped. + */ + m_tautology.reset(); + for (literal l : m_covered_clause) { + m_tautology.push_back(l); + s.mark_visited(l); + } + minimize_covered_clause(m_covered_clause.size()-1); + } return ate_t; } - if (et == ate_t) { - for (literal l : m_covered_clause) s.unmark_visited(l); - return no_t; - } - if (first) { for (unsigned i = 0; i < sz0; ++i) { if (check_abce_tautology(m_covered_clause[i])) { blocked = m_covered_clause[i]; - is_tautology = true; - break; + reset_mark(); +#if 0 + if (sz0 == 3 && blocked.var() == 10219) { + IF_VERBOSE(0, verbose_stream() << "abce: " << m_covered_clause << "\n"; + for (literal l : m_covered_clause) verbose_stream() << s.value(l) << "\n"; + ); + literal l = blocked; + 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_VERBOSE(0, verbose_stream() << c << "\n"); + } + } +#endif + m_covered_clause.shrink(sz0); + if (et == bce_t) return bce_t; + k = model_converter::ABCE; + return abce_t; } } - first = false; } + first = false; - if (is_tautology || et == abce_t || et == bce_t) { - for (literal l : m_covered_clause) s.unmark_visited(l); - m_covered_clause.shrink(sz0); - if (!is_tautology) return no_t; - if (et == bce_t) return bce_t; - return abce_t; + if (et == abce_t || et == bce_t) { + break; } /* * Add resolution intersection while checking if the clause becomes a tautology. */ sz = m_covered_clause.size(); - if (et == cce_t || et == acce_t) { - is_tautology = add_cla(blocked); + if ((et == cce_t || et == acce_t) && add_cla(blocked)) { + reset_mark(); + return et; } } - for (literal l : m_covered_clause) s.unmark_visited(l); - return is_tautology ? et : no_t; + reset_mark(); + return no_t; } // perform covered clause elimination. @@ -1463,13 +1506,14 @@ namespace sat { case ate_t: w.set_learned(true); s.s.set_learned1(l2, l, true); + m_mc.add_ate(m_covered_clause); break; case no_t: break; default: - block_covered_binary(w, l, blocked, k); w.set_learned(true); s.s.set_learned1(l2, l, true); + block_covered_binary(w, l, blocked, k); break; } } @@ -1487,7 +1531,8 @@ namespace sat { inc_bc(r); switch (r) { case ate_t: - s.set_learned(c); + m_mc.add_ate(m_covered_clause); + s.set_learned(c); break; case no_t: break; @@ -1518,32 +1563,33 @@ namespace sat { } void block_covered_clause(clause& c, literal l, model_converter::kind k) { - if (false && l.var() == 39021) { + if (false) { IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n"; s.m_use_list.display(verbose_stream() << "use " << l << ":", l); s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l); - /*s.s.display(verbose_stream());*/ + display_watch_list(verbose_stream() << ~l << ": ", s.s.m_cls_allocator, s.get_wlist(l)) << "\n"; + display_watch_list(verbose_stream() << l << ": ", s.s.m_cls_allocator, s.get_wlist(~l)) << "\n"; ); } TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); SASSERT(!s.is_external(l)); - model_converter::entry& new_entry = mc.mk(k, l.var()); + model_converter::entry& new_entry = m_mc.mk(k, l.var()); for (literal lit : c) { if (lit != l && process_var(lit.var())) { m_queue.decreased(~lit); } } - mc.insert(new_entry, m_covered_clause, m_elim_stack); + m_mc.insert(new_entry, m_covered_clause); } void block_covered_binary(watched const& w, literal l1, literal blocked, model_converter::kind k) { SASSERT(!s.is_external(blocked)); - model_converter::entry& new_entry = mc.mk(k, blocked.var()); + model_converter::entry& new_entry = m_mc.mk(k, blocked.var()); literal l2 = w.get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";); s.set_learned(l1, l2); - mc.insert(new_entry, m_covered_clause, m_elim_stack); + m_mc.insert(new_entry, m_covered_clause); m_queue.decreased(~l2); } @@ -1571,6 +1617,13 @@ namespace sat { for (literal l2 : m_intersection) { watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { +#if 0 + IF_VERBOSE(0, verbose_stream() << "bca " << l << " " << ~l2 << "\n"); + if (l.var() == 10219 && l2.var() == 10202) { + IF_VERBOSE(0, s.s.display(verbose_stream())); + exit(0); + } +#endif s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } @@ -1777,13 +1830,19 @@ namespace sat { } void simplifier::save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs) { - model_converter & mc = s.m_mc; for (auto & e : cs) { - mc.insert(mc_entry, e); + s.m_mc.insert(mc_entry, e); } } void simplifier::add_non_learned_binary_clause(literal l1, literal l2) { +#if 0 + if ((l1.var() == 2039 || l2.var() == 2039) && + (l1.var() == 27042 || l2.var() == 27042)) { + IF_VERBOSE(1, verbose_stream() << "add_bin: " << l1 << " " << l2 << "\n"); + } +#endif +#if 0 watched* w; watch_list & wlist1 = get_wlist(~l1); watch_list & wlist2 = get_wlist(~l2); @@ -1804,6 +1863,9 @@ namespace sat { else { wlist2.push_back(watched(l1, false)); } +#else + s.mk_bin_clause(l1, l2, false); +#endif } /** @@ -1820,6 +1882,11 @@ namespace sat { watch_list::iterator end2 = wlist2.end(); for (; it2 != end2; ++it2) { if (it2->is_binary_clause() && it2->get_literal() == l) { + if ((l.var() == 2039 || l2.var() == 2039) && + (l.var() == 27042 || l2.var() == 27042)) { + IF_VERBOSE(1, verbose_stream() << "remove_bin: " << l << " " << l2 << "\n"); + } + TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";); m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned())); continue; @@ -1920,6 +1987,13 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; + if (false) { + literal l(v, false); + IF_VERBOSE(0, + verbose_stream() << "elim: " << l << "\n"; + display_watch_list(verbose_stream() << ~l << ": ", s.m_cls_allocator, get_wlist(l)) << "\n"; + display_watch_list(verbose_stream() << l << ": ", s.m_cls_allocator, get_wlist(~l)) << "\n";); + } // eliminate variable ++s.m_stats.m_elim_var_res; VERIFY(!is_external(v)); @@ -1936,12 +2010,14 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; + + for (auto & c1 : m_pos_cls) { for (auto & c2 : m_neg_cls) { m_new_cls.reset(); if (!resolve(c1, c2, pos_l, m_new_cls)) continue; - // if (v == 39063) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); + if (false && v == 27041) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";); if (cleanup_clause(m_new_cls)) continue; // clause is already satisfied. @@ -2053,7 +2129,7 @@ namespace sat { m_subsumption = p.subsumption(); m_subsumption_limit = p.subsumption_limit(); m_elim_vars = p.elim_vars(); - m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy + m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy? m_elim_vars_bdd_delay = p.elim_vars_bdd_delay(); m_incremental_mode = s.get_config().m_incremental && !p.override_incremental(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 299b1f704..da11ed3a1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -333,6 +333,12 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { +#if 0 + if ((l1.var() == 2039 || l2.var() == 2039) && + (l1.var() == 27042 || l2.var() == 27042)) { + IF_VERBOSE(1, verbose_stream() << "mk_bin: " << l1 << " " << l2 << " " << learned << "\n"); + } +#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; @@ -345,13 +351,13 @@ namespace sat { if (w0) { if (w0->is_learned() && !learned) { w0->set_learned(false); - } - w0 = find_binary_watch(get_wlist(~l2), l1); - } - if (w0) { - if (w0->is_learned() && !learned) { - w0->set_learned(false); - } + } + else { + return; + } + w0 = find_binary_watch(get_wlist(~l2), l1); + VERIFY(w0); + w0->set_learned(false); return; } if (m_config.m_drat) @@ -671,7 +677,6 @@ namespace sat { TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";); if (at_base_lvl()) { if (m_config.m_drat) m_drat.add(l, !j.is_none()); - j = justification(); // erase justification for level 0 } m_assignment[l.index()] = l_true; @@ -1215,7 +1220,7 @@ namespace sat { } } if (num_in > 0 || num_out > 0) { - IF_VERBOSE(1, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";); } } } @@ -1657,7 +1662,11 @@ namespace sat { if (!check_clauses(m_model)) { IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); - // IF_VERBOSE(10, m_mc.display(verbose_stream())); + IF_VERBOSE(10, m_mc.display(verbose_stream())); + //IF_VERBOSE(0, display_units(verbose_stream())); + //IF_VERBOSE(0, display(verbose_stream())); + IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); + throw solver_exception("check model failed"); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c56c033a0..1bf78ab8c 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -236,6 +236,10 @@ namespace sat { 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); + void add_ate(clause& c) { m_mc.add_ate(c); } + void add_ate(literal l1, literal l2) { m_mc.add_ate(l1, l2); } + void add_ate(literal_vector const& lits) { m_mc.add_ate(lits); } + class scoped_disable_checkpoint { solver& s; public: