From 21738d9750aa5902173ad47df61f5f4c7dcaf9d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Apr 2018 15:59:55 -0700 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 3 ++- src/sat/sat_simplifier.cpp | 14 ++++---------- 2 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index bebb3e384..b097b3462 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; // false; // true; // false; // true; + bool first = false; // true; // false; // // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; @@ -101,6 +101,7 @@ namespace sat { if (!sat && it->get_kind() != ATE && v0 != null_bool_var) { VERIFY(legal_to_flip(v0)); m[v0] = var_sign ? l_false : l_true; + //IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n"); } elim_stack* st = it->m_elim_stack[index]; if (st) { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 52c7236a0..3f6c2d6ca 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1174,7 +1174,8 @@ namespace sat { 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. + in the dependencies. They may get used in some RI prunings and then they have to be included to avoid flipping + RI literals. */ void minimize_covered_clause(unsigned idx) { // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause @@ -1199,8 +1200,8 @@ namespace sat { } 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()) { @@ -1617,13 +1618,6 @@ 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; }