From ac39ddb43fd6a7126cdae85585ee94d7f5d81626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jul 2020 14:30:48 -0700 Subject: [PATCH] flush gmc for sat-preprocessor model bug #4532 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.h | 2 +- src/sat/sat_solver.cpp | 6 ++++-- src/sat/tactic/goal2sat.cpp | 12 +++++++----- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index e453bcaa182..8a3891797d3 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -81,7 +81,7 @@ namespace sat { private: vector m_entries; // entries accumulated during SAT search unsigned m_exposed_lim; // last entry that was exposed to model converter. - bool_vector m_mark; // literals that are used in asserted clauses. + bool_vector m_mark; // literals that are used in asserted clauses. solver const* m_solver; elim_stackv m_elim_stack; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0197feb9508..0a036e849db 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -91,9 +91,9 @@ namespace sat { solver::~solver() { m_ext = nullptr; SASSERT(m_config.m_num_threads > 1 || check_invariant()); - TRACE("sat", tout << "Delete clauses\n";); + CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";); del_clauses(m_clauses); - TRACE("sat", tout << "Delete learned\n";); + CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";); del_clauses(m_learned); dealloc(m_cuber); m_cuber = nullptr; @@ -1207,6 +1207,7 @@ namespace sat { propagate(false); if (check_inconsistent()) return l_false; if (m_config.m_force_cleanup) do_cleanup(true); + TRACE("sat", display(tout);); if (m_config.m_gc_burst) { // force gc @@ -1221,6 +1222,7 @@ namespace sat { if (m_config.m_max_conflicts == 0) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";); + TRACE("sat", display(tout); m_mc.display(tout);); return l_undef; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 0255fcf501c..47ac5a35507 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -965,8 +965,10 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) { s.flush(m_smc); m_var2expr.resize(s.num_vars()); map.mk_var_inv(m_var2expr); + flush_gmc(); } + void sat2goal::mc::flush_gmc() { sat::literal_vector updates; m_smc.expand(updates); @@ -1072,14 +1074,15 @@ 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())) { + sat::bool_var v = l.var(); + if (!m_var2expr.get(v)) { app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - m_var2expr.set(l.var(), aux); + m_var2expr.set(v, aux); if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); m_gmc->hide(aux->get_decl()); } - VERIFY(m_var2expr.get(l.var())); - expr_ref result(m_var2expr.get(l.var()), m); + VERIFY(m_var2expr.get(v)); + expr_ref result(m_var2expr.get(v), m); if (l.sign()) { result = m.mk_not(result); } @@ -1210,7 +1213,6 @@ struct sat2goal::imp { checkpoint(); r.assert_expr(lit2expr(mc, s.trail_literal(i))); } - // collect binary clauses svector bin_clauses; s.collect_bin_clauses(bin_clauses, m_learned, false);