From 4adb24ede5879995a71e4f12d8e917ee6d4a8157 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jan 2018 16:12:59 -0800 Subject: [PATCH] fix model bugs Signed-off-by: Nikolaj Bjorner --- src/model/model.cpp | 6 ++-- src/opt/maxres.cpp | 22 ++++++++----- src/opt/opt_context.cpp | 36 ++++++++++---------- src/sat/ba_solver.cpp | 3 +- src/sat/sat_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 28 +++++++++------- src/sat/tactic/atom2bool_var.cpp | 6 ++++ src/sat/tactic/atom2bool_var.h | 1 + src/sat/tactic/goal2sat.cpp | 47 ++++++++++----------------- src/sat/tactic/goal2sat.h | 2 +- 10 files changed, 79 insertions(+), 73 deletions(-) diff --git a/src/model/model.cpp b/src/model/model.cpp index 7ac1300de..d02785584 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -42,10 +42,8 @@ model::~model() { void model::copy_const_interps(model const & source) { - decl2expr::iterator it1 = source.m_interp.begin(); - decl2expr::iterator end1 = source.m_interp.end(); - for (; it1 != end1; ++it1) { - register_decl(it1->m_key, it1->m_value); + for (auto const& kv : source.m_interp) { + register_decl(kv.m_key, kv.m_value); } } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 5fa87b3ba..3d638212b 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -52,18 +52,19 @@ Notes: --*/ +#include "ast/ast_pp.h" +#include "ast/pb_decl_plugin.h" +#include "ast/ast_util.h" +#include "model/model_smt2_pp.h" #include "solver/solver.h" +#include "solver/mus.h" +#include "sat/sat_solver/inc_sat_solver.h" +#include "smt/smt_solver.h" +#include "opt/opt_context.h" +#include "opt/opt_params.hpp" #include "opt/maxsmt.h" #include "opt/maxres.h" -#include "ast/ast_pp.h" -#include "solver/mus.h" #include "opt/mss.h" -#include "sat/sat_solver/inc_sat_solver.h" -#include "opt/opt_context.h" -#include "ast/pb_decl_plugin.h" -#include "opt/opt_params.hpp" -#include "ast/ast_util.h" -#include "smt/smt_solver.h" using namespace opt; @@ -737,6 +738,8 @@ public: m_model = mdl; + TRACE("opt", model_smt2_pp(tout << "updated model\n", m, *m_model, 0);); + for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } @@ -780,6 +783,9 @@ public: bool is_true(expr_ref_vector const& es) { unsigned i = 0; for (; i < es.size() && is_true(es[i]); ++i) { } + CTRACE("opt", i < es.size(), tout << mk_pp(es[i], m) << "\n"; + model_smt2_pp(tout, m, *m_model, 0); + ); return i == es.size(); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index dd90963df..7cb2c6034 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -17,11 +17,13 @@ Notes: --*/ -#include "opt/opt_context.h" -#include "ast/ast_pp.h" -#include "opt/opt_solver.h" -#include "opt/opt_params.hpp" #include "ast/for_each_expr.h" +#include "ast/ast_pp.h" +#include "ast/bv_decl_plugin.h" +#include "ast/pb_decl_plugin.h" +#include "ast/ast_smt_pp.h" +#include "ast/ast_pp_util.h" +#include "model/model_smt2_pp.h" #include "tactic/goal.h" #include "tactic/tactic.h" #include "tactic/arith/lia2card_tactic.h" @@ -32,17 +34,16 @@ Notes: #include "tactic/core/solve_eqs_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/tactical.h" -#include "model/model_smt2_pp.h" #include "tactic/arith/card2bv_tactic.h" #include "tactic/arith/eq2bv_tactic.h" #include "tactic/bv/dt2bv_tactic.h" -#include "sat/sat_solver/inc_sat_solver.h" -#include "ast/bv_decl_plugin.h" -#include "ast/pb_decl_plugin.h" -#include "ast/ast_smt_pp.h" #include "tactic/generic_model_converter.h" -#include "ast/ast_pp_util.h" +#include "sat/sat_solver/inc_sat_solver.h" #include "qe/qsat.h" +#include "opt/opt_context.h" +#include "opt/opt_solver.h" +#include "opt/opt_params.hpp" + namespace opt { @@ -995,7 +996,11 @@ namespace opt { } rational v = m_objectives[index].m_adjust_value(_v); expr_ref val(m); - model_ref mdl = md; + // + // we have to clone the model so that maxsat solver can use + // internal variables that are otherwise deleted from the model. + // + model_ref mdl = md->copy(); fix_model(mdl); if (!mdl->eval(term, val)) { @@ -1021,9 +1026,7 @@ namespace opt { generic_model_converter_ref fm; if (m_arith.is_add(term)) { expr_ref_vector args(m); - unsigned sz = term->get_num_args(); - for (unsigned i = 0; i < sz; ++i) { - expr* arg = term->get_arg(i); + for (expr* arg : *term) { if (is_mul_const(arg)) { args.push_back(arg); } @@ -1364,9 +1367,8 @@ namespace opt { if (m_simplify) { m_simplify->collect_statistics(stats); } - map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); - for (; it != end; ++it) { - it->m_value->collect_statistics(stats); + for (auto const& kv : m_maxsmts) { + kv.m_value->collect_statistics(stats); } get_memory_statistics(stats); get_rlimit_statistics(m.limit(), stats); diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index be4498061..20a0a774d 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1640,7 +1640,6 @@ namespace sat { bool ba_solver::propagate(literal l, ext_constraint_idx idx) { SASSERT(value(l) == l_true); constraint& c = index2constraint(idx); - TRACE("ba", tout << l << "\n";); if (c.lit() != null_literal && l.var() == c.lit().var()) { init_watch(c); return true; @@ -1756,7 +1755,7 @@ namespace sat { for (unsigned i = 1; i < x.size(); ++i) { literal lit(value(x[i]) == l_true ? x[i] : ~x[i]); inc_parity(lit.var()); - if (true || lvl(lit) == level) { + if (lvl(lit) == level) { ++num_marks; } else { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index ad1f36c99..651eedee8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -270,6 +270,7 @@ namespace sat { void set_non_external(bool_var v); bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } void set_eliminated(bool_var v, bool f) { m_eliminated[v] = f; } + bool was_eliminated(literal l) const { return was_eliminated(l.var()); } unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 97818e155..9f248c25f 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -533,11 +533,11 @@ private: TRACE("sat", g->display_with_dependencies(tout);); // ensure that if goal is already internalized, then import mc from m_solver. - if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); - m_sat_mc->flush_smc(m_solver); m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma); m_goal2sat.get_interpreted_atoms(atoms); + if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); + m_sat_mc->flush_smc(m_solver, m_map); if (!atoms.empty()) { std::stringstream strm; strm << "interpreted atoms sent to SAT solver " << atoms; @@ -796,18 +796,22 @@ private: if (m_mc0) { (*m_mc0)(m_model); } - SASSERT(m_model); + TRACE("sat", model_smt2_pp(tout, m, *m_model, 0);); - DEBUG_CODE( - for (expr * f : m_fmls) { - expr_ref tmp(m); - if (m_model->eval(f, tmp, true)) { - CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; - model_smt2_pp(tout, m, *(m_model.get()), 0);); - SASSERT(m.is_true(tmp)); + IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";); + for (expr * f : m_fmls) { + expr_ref tmp(m); + if (m_model->eval(f, tmp, true)) { + CTRACE("sat", !m.is_true(tmp), + tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n"; + model_smt2_pp(tout, m, *(m_model.get()), 0);); + if (!m.is_true(tmp)) { + IF_VERBOSE(0, verbose_stream() << "failed to verify: " << tmp << "\n";); + IF_VERBOSE(0, verbose_stream() << m_params << "\n";); } - }); + VERIFY(m.is_true(tmp)); + } + } } }; diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index d8827fe66..e3c9b6767 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -31,6 +31,12 @@ 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.set(kv.m_value, to_app(kv.m_key)); + } +} + sat::bool_var atom2bool_var::to_bool_var(expr * n) const { sat::bool_var v = sat::null_bool_var; m_mapping.find(n, v); diff --git a/src/sat/tactic/atom2bool_var.h b/src/sat/tactic/atom2bool_var.h index d360d3fe0..b7f533537 100644 --- a/src/sat/tactic/atom2bool_var.h +++ b/src/sat/tactic/atom2bool_var.h @@ -31,6 +31,7 @@ public: void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); } sat::bool_var to_bool_var(expr * n) const; void mk_inv(expr_ref_vector & lit2expr) const; + void mk_var_inv(app_ref_vector & var2expr) const; // return true if the mapping contains uninterpreted atoms. bool interpreted_atoms() const { return expr2var::interpreted_vars(); } }; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d810c60b7..0e488c5c1 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -880,8 +880,11 @@ void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) { sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} -void sat2goal::mc::flush_smc(sat::solver& s) { + +void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) { s.flush(m_smc); + m_var2expr.resize(s.num_vars()); + map.mk_var_inv(m_var2expr); } void sat2goal::mc::flush_gmc() { @@ -941,6 +944,7 @@ void sat2goal::mc::operator()(model_ref & md) { // create a SAT model using md sat::model sat_md; expr_ref val(m); + VERIFY(!m_var2expr.empty()); for (expr * atom : m_var2expr) { if (!atom) { sat_md.push_back(l_undef); @@ -1011,7 +1015,6 @@ expr_ref sat2goal::mc::lit2expr(sat::literal l) { struct sat2goal::imp { typedef mc sat_model_converter; - typedef ref sat_model_converter_ref; ast_manager & m; expr_ref_vector m_lit2expr; @@ -1034,23 +1037,7 @@ struct sat2goal::imp { throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } - void init_lit2expr(sat::solver const & s, atom2bool_var const & map, sat_model_converter_ref & mc) { - unsigned num_vars = s.num_vars(); - m_lit2expr.resize(num_vars * 2); - map.mk_inv(m_lit2expr); - if (mc) { - for (sat::bool_var v = 0; v < num_vars; v++) { - checkpoint(); - sat::literal l(v, false); - if (m_lit2expr.get(l.index()) && !mc->var2expr(v)) { - mc->insert(v, to_app(m_lit2expr.get(l.index())), false); - SASSERT(m_lit2expr.get((~l).index())); - } - } - } - } - - expr * lit2expr(sat_model_converter_ref& mc, sat::literal l) { + expr * lit2expr(ref& mc, sat::literal l) { if (!m_lit2expr.get(l.index())) { SASSERT(m_lit2expr.get((~l).index()) == 0); app* aux = mc ? mc->var2expr(l.var()) : nullptr; @@ -1059,13 +1046,14 @@ struct sat2goal::imp { if (mc) mc->insert(l.var(), aux, true); } - m_lit2expr.set(l.index(), aux); - m_lit2expr.set((~l).index(), m.mk_not(aux)); + sat::literal lit(l.var(), false); + m_lit2expr.set(lit.index(), aux); + m_lit2expr.set((~lit).index(), m.mk_not(aux)); } return m_lit2expr.get(l.index()); } - void assert_pb(sat_model_converter_ref& mc, goal& r, sat::ba_solver::pb const& p) { + void assert_pb(ref& mc, goal& r, sat::ba_solver::pb const& p) { pb_util pb(m); ptr_buffer lits; vector coeffs; @@ -1082,7 +1070,7 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_card(sat_model_converter_ref& mc, goal& r, sat::ba_solver::card const& c) { + void assert_card(ref& mc, goal& r, sat::ba_solver::card const& c) { pb_util pb(m); ptr_buffer lits; for (sat::literal l : c) { @@ -1096,7 +1084,7 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_xor(sat_model_converter_ref& mc, goal & r, sat::ba_solver::xor const& x) { + void assert_xor(ref& mc, goal & r, sat::ba_solver::xor const& x) { ptr_buffer lits; for (sat::literal l : x) { lits.push_back(lit2expr(mc, l)); @@ -1109,7 +1097,7 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_clauses(sat_model_converter_ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { + void assert_clauses(ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { ptr_buffer lits; for (sat::clause* cp : clauses) { checkpoint(); @@ -1136,8 +1124,9 @@ struct sat2goal::imp { if (r.models_enabled() && !mc) { mc = alloc(sat_model_converter, m); } - if (mc) mc->flush_smc(s); - init_lit2expr(s, map, mc); + if (mc) mc->flush_smc(s, map); + m_lit2expr.resize(s.num_vars() * 2); + map.mk_inv(m_lit2expr); // collect units unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { @@ -1173,7 +1162,7 @@ struct sat2goal::imp { } } - void add_clause(sat_model_converter_ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { + void add_clause(ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { expr_ref_vector lemma(m); for (sat::literal l : lits) { expr* e = lit2expr(mc, l); @@ -1183,7 +1172,7 @@ struct sat2goal::imp { lemmas.push_back(mk_or(lemma)); } - void add_clause(sat_model_converter_ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { + void add_clause(ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { expr_ref_vector lemma(m); for (sat::literal l : c) { expr* e = lit2expr(mc, l); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 43ee5a835..463a50ff6 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -88,7 +88,7 @@ public: mc(ast_manager& m); virtual ~mc() {} // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver& s); + void flush_smc(sat::solver& s, atom2bool_var const& map); void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; model_converter* translate(ast_translation& translator) override;