From 3d7098ec8509ef1823a440990eca672fcc805d75 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Mar 2020 07:15:06 +0100 Subject: [PATCH] fix #3137 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 23 +++++++++++++---------- src/sat/tactic/atom2bool_var.cpp | 1 + src/sat/tactic/goal2sat.cpp | 4 +++- src/sat/tactic/goal2sat.h | 1 - 4 files changed, 17 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 215fc0d91..5124ca586 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -33,7 +33,6 @@ Notes: #include "tactic/arith/card2bv_tactic.h" #include "tactic/bv/bit_blaster_tactic.h" #include "tactic/core/simplify_tactic.h" -#include "tactic/core/solve_eqs_tactic.h" #include "tactic/bv/bit_blaster_model_converter.h" #include "model/model_smt2_pp.h" #include "model/model_v2_pp.h" @@ -509,6 +508,7 @@ public: m_cached_mc = m_mcs.back(); m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get()); m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get()); + TRACE("sat", m_cached_mc->display(tout);); return m_cached_mc; } else { @@ -556,12 +556,11 @@ public: m_preprocess = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), - //time consuming if done in inner loop: mk_solve_eqs_tactic(m, simp1_p), mk_card2bv_tactic(m, m_params), // updates model converter using_params(mk_simplify_tactic(m), simp1_p), mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m, m_bb_rewriter.get()) - /*TBD remove and check what simplifier does with expansion */ , using_params(mk_simplify_tactic(m), simp2_p) + mk_bit_blaster_tactic(m, m_bb_rewriter.get()), + using_params(mk_simplify_tactic(m), simp2_p) ); while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { m_bb_rewriter->push(); @@ -878,14 +877,18 @@ private: return; } TRACE("sat", m_solver.display_model(tout);); + CTRACE("sat", m_sat_mc, m_sat_mc->display(tout);); sat::model ll_m = m_solver.get_model(); mdl = alloc(model, m); if (m_sat_mc) { (*m_sat_mc)(ll_m); } - for (sat::bool_var v = 0; m_sat_mc && v < m_sat_mc->num_vars(); ++v) { - expr* n = m_sat_mc->var2expr(v); - if (!n || !is_app(n) || to_app(n)->get_num_args() > 0) { + app_ref_vector var2expr(m); + m_map.mk_var_inv(var2expr); + + for (unsigned v = 0; v < var2expr.size(); ++v) { + app * n = var2expr.get(v); + if (!n || !is_uninterp_const(n)) { continue; } switch (sat::value_at(v, ll_m)) { @@ -904,7 +907,8 @@ private: if (m_sat_mc) { (*m_sat_mc)(mdl); } - if (m_mcs.back()) { + if (m_mcs.back()) { + TRACE("sat", m_mcs.back()->display(tout);); (*m_mcs.back())(mdl); } TRACE("sat", model_smt2_pp(tout, m, *mdl, 0);); @@ -916,12 +920,11 @@ private: model_evaluator eval(*mdl); eval.set_model_completion(true); bool all_true = true; - //unsigned i = 0; for (expr * f : m_fmls) { expr_ref tmp(m); eval(f, tmp); CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n"; + tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; model_smt2_pp(tout, m, *(mdl.get()), 0);); if (!m.is_true(tmp)) { IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n"); diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index cd6ab776d..08e1258d9 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -33,6 +33,7 @@ void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const { void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const { for (auto const& kv : m_mapping) { + var2expr.reserve(kv.m_value + 1); var2expr.set(kv.m_value, to_app(kv.m_key)); } } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 896041e16..c4bc4c64d 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1039,8 +1039,9 @@ void sat2goal::mc::operator()(sat::model& md) { void sat2goal::mc::operator()(model_ref & md) { // apply externalized model converter + CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md);); if (m_gmc) (*m_gmc)(md); - TRACE("sat_mc", tout << "after sat_mc\n"; model_v2_pp(tout, *md);); + CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md);); } @@ -1059,6 +1060,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); m_gmc->hide(atom->get_decl()); } + TRACE("sat_mc", tout << "insert " << v << "\n";); } expr_ref sat2goal::mc::lit2expr(sat::literal l) { diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 7ccba173e..31e94bd74 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -96,7 +96,6 @@ public: void set_env(ast_pp_util* visitor) override; void display(std::ostream& out) override; void get_units(obj_map& units) override; - unsigned num_vars() const { return m_var2expr.size(); } app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } expr_ref lit2expr(sat::literal l); void insert(sat::bool_var v, app * atom, bool aux);