From 505133a4b3eebca15d3a93125ab24283de5fc3e8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2017 17:06:15 -0800 Subject: [PATCH] debugging card Signed-off-by: Nikolaj Bjorner --- src/sat/card_extension.cpp | 23 ++++++++++++++++------- src/sat/sat_solver.cpp | 16 +++++++++++++--- 2 files changed, 29 insertions(+), 10 deletions(-) diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index afa768863..712162e44 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -234,9 +234,8 @@ namespace sat { } bool card_extension::resolve_conflict(card& c, literal alit) { - bool_var v; - m_conflict_lvl = 0; + m_conflict_lvl = lvl(~alit); for (unsigned i = c.k(); i < c.size(); ++i) { literal lit = c[i]; SASSERT(value(lit) == l_false); @@ -245,6 +244,7 @@ namespace sat { if (m_conflict_lvl < lvl(c.lit()) || m_conflict_lvl == 0) { return false; } + std::cout << "conflict level: " << m_conflict_lvl << " " << lvl(~alit) << "\n"; reset_coeffs(); m_num_marks = 0; @@ -351,10 +351,11 @@ namespace sat { --m_num_marks; } + DEBUG_CODE(for (bool_var i = 0; i < static_cast(s().num_vars()); ++i) SASSERT(!s().is_marked(i));); SASSERT(validate_lemma()); normalize_active_coeffs(); - + if (m_bound > 0 && m_active_vars.empty()) { return false; } @@ -367,11 +368,13 @@ namespace sat { ++idx; alit = null_literal; -#if 0 +#if 1 + std::cout << c.size() << " >= " << c.k() << "\n"; + std::cout << m_active_vars.size() << ": " << slack + m_bound << " >= " << m_bound << "\n"; while (0 <= slack) { literal lit = lits[idx]; bool_var v = lit.var(); - if (m_active_vars.contains(v)) { + if (m_active_var_set.contains(v)) { int coeff = get_coeff(v); bool append = false; if (coeff < 0 && !lit.sign()) { @@ -394,6 +397,9 @@ namespace sat { SASSERT(idx > 0 || slack < 0); --idx; } + if (alit == null_literal) { + return false; + } if (alit != null_literal) { m_conflict.push_back(alit); } @@ -402,7 +408,7 @@ namespace sat { SASSERT(i <= idx); literal lit = lits[i]; bool_var v = lit.var(); - if (m_active_vars.contains(v)) { + if (m_active_var_set.contains(v)) { int coeff = get_coeff(v); if (coeff < 0 && !lit.sign()) { @@ -514,6 +520,7 @@ namespace sat { void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) { if (idx == 0) { + std::cout << "antecedents0: " << l << " " << m_conflict.size() << "\n"; SASSERT(m_conflict.back() == l); for (unsigned i = 0; i + 1 < m_conflict.size(); ++i) { SASSERT(value(m_conflict[i]) == l_false); @@ -529,7 +536,8 @@ namespace sat { found = c[i] == l; } SASSERT(found);); - + + std::cout << "antecedents: " << idx << ": " << l << " " << c.size() - c.k() + 1 << "\n"; r.push_back(c.lit()); SASSERT(value(c.lit()) == l_true); for (unsigned i = c.k(); i < c.size(); ++i) { @@ -834,6 +842,7 @@ namespace sat { // validate that m_A & m_B implies m_C bool card_extension::validate_resolvent() { + std::cout << "validate resolvent\n"; u_map coeffs; unsigned k = m_A.m_k + m_B.m_k; for (unsigned i = 0; i < m_A.m_lits.size(); ++i) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f7f8bfa54..6eafd8906 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1726,12 +1726,13 @@ namespace sat { m_lemma.push_back(null_literal); unsigned num_marks = 0; + literal consequent = null_literal; if (m_not_l != null_literal) { TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";); process_antecedent(m_not_l, num_marks); + consequent = ~m_not_l; } - literal consequent = m_not_l; justification js = m_conflict; do { @@ -1900,11 +1901,12 @@ namespace sat { } m_lemma.reset(); m_lemma.push_back(null_literal); // asserted literal + literal consequent = null_literal; if (m_not_l != null_literal) { TRACE("sat", tout << "not_l: " << m_not_l << "\n";); process_antecedent_for_init(m_not_l); + consequent = ~m_not_l; } - literal consequent = m_not_l; justification js = m_conflict; SASSERT(m_trail.size() > 0); @@ -2008,6 +2010,7 @@ namespace sat { } + static int count = 0; void solver::resolve_conflict_for_unsat_core() { TRACE("sat", display(tout); unsigned level = 0; @@ -2039,6 +2042,7 @@ namespace sat { unsigned old_size = m_unmark.size(); int idx = skip_literals_above_conflict_level(); + literal consequent = m_not_l; if (m_not_l != null_literal) { justification js = m_justification[m_not_l.var()]; TRACE("sat", tout << "not_l: " << m_not_l << "\n"; @@ -2052,9 +2056,9 @@ namespace sat { else { process_consequent_for_unsat_core(m_not_l, js); } + consequent = ~m_not_l; } - literal consequent = m_not_l; justification js = m_conflict; while (true) { @@ -2093,6 +2097,9 @@ namespace sat { set_model(m_mus.get_model()); IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";); } + + ++count; + SASSERT(count == 1); } @@ -2116,6 +2123,9 @@ namespace sat { literal_vector::iterator end = m_ext_antecedents.end(); for (; it != end; ++it) r = std::max(r, lvl(*it)); + if (true || r != scope_lvl() || r != lvl(not_l)) { + std::cout << "get max level " << r << " scope level " << scope_lvl() << " lvl(l): " << lvl(not_l) << "\n"; + } return r; } default: