From aa2721517ba17938f257e678debda78f87d3d456 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Mar 2018 16:24:22 -0700 Subject: [PATCH] model conversion and acce tracking Signed-off-by: Nikolaj Bjorner --- .../ackermannize_bv_tactic.cpp | 2 +- src/sat/sat_asymm_branch.cpp | 22 +++++++--- src/sat/sat_model_converter.cpp | 10 ++--- src/sat/sat_simplifier.cpp | 43 +++++++++++++++---- src/sat/sat_solver.cpp | 8 ++++ src/tactic/goal.cpp | 3 ++ 6 files changed, 67 insertions(+), 21 deletions(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index f0e960644..df230a7e2 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -52,7 +52,7 @@ public: result.push_back(resg.get()); // report model if (g->models_enabled()) { - g->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); + resg->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); } resg->inc_depth(); diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 971e86d95..65003a6e4 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -333,13 +333,18 @@ namespace sat { if (!m_to_delete.empty()) { unsigned j = 0; for (unsigned i = 0; i < c.size(); ++i) { - if (!m_to_delete.contains(c[i])) { - c[j] = c[i]; - ++j; - } - else { - m_pos.erase(c[i]); - m_neg.erase(~c[i]); + literal lit = c[i]; + switch (s.value(lit)) { + case l_true: + scoped_d.del_clause(); + return false; + case l_false: + break; + default: + if (!m_to_delete.contains(lit)) { + c[j++] = lit; + } + break; } } return re_attach(scoped_d, c, j); @@ -359,6 +364,7 @@ namespace sat { } bool asymm_branch::flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz) { + VERIFY(s.m_trail.size() == s.m_qhead); bool found_conflict = false; unsigned i = 0, sz = c.size(); s.push(); @@ -399,6 +405,7 @@ namespace sat { } bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) { + VERIFY(s.m_trail.size() == s.m_qhead); m_elim_literals += c.size() - new_sz; if (c.is_learned()) { m_elim_learned_literals += c.size() - new_sz; @@ -415,6 +422,7 @@ namespace sat { return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); + VERIFY(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], c.is_learned()); if (s.m_trail.size() > s.m_qhead) s.propagate_core(false); scoped_d.del_clause(); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 9bda5cf3d..6b0eb1a7c 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,7 +75,7 @@ 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 = true; + bool first = false; // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; @@ -99,8 +99,8 @@ namespace sat { process_stack(m, clause, st->stack()); } sat = false; - if (false && first && m_solver && !m_solver->check_clauses(m)) { - display(std::cout, *it) << "\n"; + if (first && m_solver && !m_solver->check_clauses(m)) { + IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n"); first = false; } ++index; @@ -125,8 +125,8 @@ namespace sat { m[v] = sign ? l_false : l_true; // if (first) std::cout << "set: " << l << "\n"; sat = true; - if (false && first && m_solver && !m_solver->check_clauses(m)) { - display(std::cout, *it) << "\n";; + if (first && m_solver && !m_solver->check_clauses(m)) { + IF_VERBOSE(0, display(verbose_stream() << "after flipping undef\n", *it) << "\n"); first = false; } } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index be0222d3b..6ef0be83a 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -939,6 +939,19 @@ 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 { + if (cls()) { + out << *cls() << " "; + } + if (lit1() != null_literal) { + out << lit1() << " "; + } + if (lit2() != null_literal) { + out << lit2() << " "; + } + out << "\n"; + return out; + } }; class queue { @@ -1154,10 +1167,14 @@ namespace sat { \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. + + It has a bug: literals that are used to prune tautologies during resolution intersection should be included + in the dependencies. */ void minimize_covered_clause(unsigned idx) { // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause // << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";); + literal _blocked = m_covered_clause[idx]; 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); @@ -1167,8 +1184,18 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } + if (_blocked.var() == 16774 && 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] << ":"); + }); + } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; + s.mark_visited(lit); + continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { @@ -1205,6 +1232,9 @@ namespace sat { // unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); VERIFY(j >= m_clause.size()); + if (_blocked.var() == 16774 && false) { + IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"); + } // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";); } @@ -1282,7 +1312,7 @@ namespace sat { for (unsigned i = 0; i < m_covered_clause.size(); ++i) { literal lit = m_covered_clause[i]; if (resolution_intersection(lit, false)) { - blocked = m_covered_clause[i]; + blocked = m_covered_clause[i]; minimize_covered_clause(i); return true; } @@ -1531,13 +1561,10 @@ namespace sat { return; } for (literal l2 : m_intersection) { - l2.neg(); - watched* w = find_binary_watch(s.get_wlist(~l), l2); + watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { - IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";); - s.get_wlist(~l).push_back(watched(l2, true)); - VERIFY(!find_binary_watch(s.get_wlist(~l2), l)); - s.get_wlist(~l2).push_back(watched(l, true)); + IF_VERBOSE(10, verbose_stream() << "bca " << l << " " << ~l2 << "\n";); + s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } } @@ -1997,7 +2024,7 @@ namespace sat { sat_simplifier_params p(_p); m_cce = p.cce(); m_acce = p.acce(); - m_bca = p.bca(); + m_bca = false && p.bca(); // disabled m_abce = p.abce(); m_ate = p.ate(); m_bce_delay = p.bce_delay(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 10b813fc9..1617b487b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -333,6 +333,13 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { +#if 0 + if ((l1 == literal(5981, false) && l2 == literal(16764, false)) || + (l2 == literal(5981, false) && l1 == literal(16764, false))) { + IF_VERBOSE(0, display(verbose_stream())); + //VERIFY(false); + } +#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; @@ -1656,6 +1663,7 @@ 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())); throw solver_exception("check model failed"); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index c7b730099..5252a410d 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -85,6 +85,9 @@ goal::goal(goal const & src, bool): m_core_enabled(src.unsat_core_enabled()), m_inconsistent(false), m_precision(src.m_precision) { + m_mc = src.m_mc.get(); + m_pc = src.m_pc.get(); + m_dc = src.m_dc.get(); } goal::~goal() {