From 1c2966f8e97da8cd08b5beb26583dc86772b5f11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jan 2018 11:20:23 -0800 Subject: [PATCH] updates to model generation Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 12 +++++++----- src/sat/tactic/goal2sat.cpp | 16 ++++------------ src/tactic/generic_model_converter.cpp | 7 +++++++ src/tactic/generic_model_converter.h | 6 +----- src/tactic/model_converter.cpp | 1 + 6 files changed, 21 insertions(+), 22 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index bbeb87f83..ad1f36c99 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -279,6 +279,7 @@ namespace sat { unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(literal l) const { return m_level[l.var()]; } unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } + literal trail_literal(unsigned i) const { return m_trail[i]; } void assign(literal l, justification j) { TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";); switch (value(l)) { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 39b58e3a5..97818e155 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -787,21 +787,23 @@ private: } m_model = md; + if (m_sat_mc) { + (*m_sat_mc)(m_model); + } if (m_bb_rewriter.get() && !m_bb_rewriter->const2bits().empty()) { m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits())); } - if (m_mc0) { + if (m_mc0) { (*m_mc0)(m_model); } SASSERT(m_model); DEBUG_CODE( - for (unsigned i = 0; i < m_fmls.size(); ++i) { + for (expr * f : m_fmls) { expr_ref tmp(m); - if (m_model->eval(m_fmls[i].get(), tmp, true)) { + if (m_model->eval(f, tmp, true)) { CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) - << " to " << tmp << "\n"; + tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; model_smt2_pp(tout, m, *(m_model.get()), 0);); SASSERT(m.is_true(tmp)); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 6d78bc331..d810c60b7 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1139,20 +1139,12 @@ struct sat2goal::imp { if (mc) mc->flush_smc(s); init_lit2expr(s, map, mc); // collect units - unsigned num_vars = s.num_vars(); - for (sat::bool_var v = 0; v < num_vars; v++) { + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { checkpoint(); - switch (s.value(v)) { - case l_true: - r.assert_expr(lit2expr(mc, sat::literal(v, false))); - break; - case l_false: - r.assert_expr(lit2expr(mc, sat::literal(v, true))); - break; - case l_undef: - break; - } + r.assert_expr(lit2expr(mc, s.trail_literal(i))); } + // collect binary clauses svector bin_clauses; s.collect_bin_clauses(bin_clauses, m_learned); diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index eb18aa545..47a4b4d48 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -28,6 +28,13 @@ Notes: #include "model/model_evaluator.h" +void generic_model_converter::add(func_decl * d, expr* e) { + struct entry et(d, e, m, ADD); + VERIFY(d->get_range() == m.get_sort(e)); + m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size()); + m_add_entries.push_back(et); +} + void generic_model_converter::operator()(model_ref & md) { TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout);); model_evaluator ev(*(md.get())); diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index a9043d5cf..34e9d8166 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -47,11 +47,7 @@ public: void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); } - void add(func_decl * d, expr* e) { - struct entry et(d, e, m, ADD); - m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size()); - m_add_entries.push_back(et); - } + void add(func_decl * d, expr* e); void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); } diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 2598aa4f1..25829d3ce 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -25,6 +25,7 @@ Notes: */ void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const { VERIFY(m_env); + VERIFY(f->get_range() == m.get_sort(e)); ast_smt2_pp(out, f, e, *m_env, params_ref(), 0, "model-add") << "\n"; }