From 3b1810d8933cc35f903fa2a358673f53a1b0ccec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jan 2018 23:18:41 -0800 Subject: [PATCH] fix hidden tautology bug on non-learned clauses Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 4 +--- src/sat/sat_elim_vars.cpp | 3 ++- src/sat/sat_model_converter.cpp | 9 +-------- src/sat/sat_model_converter.h | 10 ++++++++++ src/sat/sat_simplifier.cpp | 2 ++ src/sat/sat_solver.cpp | 4 +++- src/sat/tactic/goal2sat.cpp | 3 +++ 7 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index ee8e9db88..dfe94c5f4 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -399,13 +399,11 @@ namespace sat { bool asymm_branch::process_sampled(big& big, clause & c) { scoped_detach scoped_d(s, c); sort(big, c); -#if 1 - if (uhte(big, c)) { + if (c.is_learned() && uhte(big, c)) { ++m_hidden_tautologies; scoped_d.del_clause(); return false; } -#endif return uhle(scoped_d, big, c); } diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index f04318a5d..a2e6b445b 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -88,6 +88,7 @@ namespace sat{ simp.collect_clauses(pos_l, simp.m_pos_cls); simp.collect_clauses(neg_l, simp.m_neg_cls); VERIFY(!simp.is_external(v)); + model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); simp.save_clauses(mc_entry, simp.m_pos_cls); simp.save_clauses(mc_entry, simp.m_neg_cls); @@ -100,7 +101,7 @@ namespace sat{ pos_occs.reset(); neg_occs.reset(); literal_vector lits; - add_clauses(b, lits); + add_clauses(b, lits); return true; } diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 7a2b4f5f4..9bda5cf3d 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -275,14 +275,7 @@ namespace sat { } std::ostream& model_converter::display(std::ostream& out, entry const& entry) const { - out << " ("; - switch (entry.get_kind()) { - case ELIM_VAR: out << "elim"; break; - case BLOCK_LIT: out << "blocked"; break; - case CCE: out << "cce"; break; - case ACCE: out << "acce"; break; - } - out << " " << entry.var(); + out << " (" << entry.get_kind() << " " << entry.var(); bool start = true; unsigned index = 0; for (literal l : entry.m_clauses) { diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index be7d03188..bc60844ca 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -134,6 +134,16 @@ namespace sat { void expand(literal_vector& update_stack); }; + 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::CCE: out << "cce"; break; + case model_converter::ACCE: out << "acce"; break; + } + return out; + } + }; #endif diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 66e0baa89..de59966e6 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1818,6 +1818,7 @@ namespace sat { if (s.m_config.m_drat) s.m_drat.add(*new_c, true); s.m_clauses.push_back(new_c); + m_use_list.insert(*new_c); if (m_sub_counter > 0) back_subsumption1(*new_c); @@ -1829,6 +1830,7 @@ namespace sat { return true; } } + return true; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 61e05b3ed..2dd459372 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3225,7 +3225,9 @@ namespace sat { literal l2 = w.get_literal(); if (l.index() > l2.index()) continue; - out << "(" << l << " " << l2 << ")\n"; + out << "(" << l << " " << l2 << ")"; + if (w.is_learned()) out << "*"; + out << "\n"; } } } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 9dbfaea57..a7b2eb582 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -142,6 +142,7 @@ struct goal2sat::imp { sat::bool_var v = m_solver.mk_var(ext); m_map.insert(t, v); l = sat::literal(v, sign); + // if (to_app(t)->get_decl()->get_name() == "XX") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(t, m) << ": " << "v" << v << "\n";); TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); if (ext && !is_uninterp_const(t)) { m_interpreted_atoms.push_back(t); @@ -1025,6 +1026,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { expr_ref sat2goal::mc::lit2expr(sat::literal l) { if (!m_var2expr.get(l.var())) { app* aux = m.mk_fresh_const(0, m.mk_bool_sort()); + // if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";); m_var2expr.set(l.var(), aux); } VERIFY(m_var2expr.get(l.var())); @@ -1067,6 +1069,7 @@ struct sat2goal::imp { app* aux = mc ? mc->var2expr(l.var()) : nullptr; if (!aux) { aux = m.mk_fresh_const(0, m.mk_bool_sort()); + // if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";); if (mc) mc->insert(l.var(), aux, true); }