From c6f0afa008b2aef5bbe16d11813a6e3ce459726e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Jun 2021 12:29:16 -0700 Subject: [PATCH] #5324 --- src/qe/mbp/mbp_arith.cpp | 6 +++--- src/qe/mbp/mbp_plugin.cpp | 2 ++ src/sat/smt/euf_model.cpp | 16 +++++++++++----- src/sat/smt/euf_solver.h | 3 ++- src/sat/smt/q_mbi.cpp | 12 +++++++++++- src/sat/smt/q_model_fixer.cpp | 9 +++++---- 6 files changed, 34 insertions(+), 14 deletions(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index eb394c59f..fb07ae450 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -281,9 +281,9 @@ namespace mbp { obj_map tids; expr_ref_vector pinned(m); unsigned j = 0; - TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";); - for (unsigned i = 0; i < fmls.size(); ++i) { - expr * fml = fmls.get(i); + TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n"; + for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";); + for (expr* fml : fmls) { if (!linearize(mbo, eval, fml, fmls, tids)) { TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";); fmls[j++] = fml; diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index 2731fc5e2..af1043593 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -102,6 +102,8 @@ namespace mbp { model_evaluator eval(model); eval.set_expand_array_equalities(true); TRACE("qe", tout << fmls << "\n";); + DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); }); + for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3; SASSERT(m.is_bool(fml)); diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index ce0fc29a7..bdf7bee11 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -229,17 +229,23 @@ namespace euf { // TODO } + void solver::model_updated(model_ref& mdl) { + m_values2root.reset(); + for (enode* n : m_egraph.nodes()) + if (n->is_root() && m_values.get(n->get_expr_id())) + m_values[n->get_expr_id()] = (*mdl)(n->get_expr()); + } + obj_map const& solver::values2root() { if (!m_values2root.empty()) return m_values2root; for (enode* n : m_egraph.nodes()) if (n->is_root() && m_values.get(n->get_expr_id())) m_values2root.insert(m_values.get(n->get_expr_id()), n); -#if 0 - for (auto kv : m_values2root) { - std::cout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n"; - } -#endif + TRACE("model", + for (auto kv : m_values2root) + tout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";); + return m_values2root; } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index b0bfcd4ff..ac8c41d59 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -149,7 +149,7 @@ namespace euf { // model building expr_ref_vector m_values; - obj_map m_values2root; + obj_map m_values2root; bool include_func_interp(func_decl* f); void register_macros(model& mdl); void dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl); @@ -370,6 +370,7 @@ namespace euf { // model construction void update_model(model_ref& mdl); obj_map const& values2root(); + void model_updated(model_ref& mdl); expr* node2value(enode* n) const; // diagnostics diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 39218d612..0cdf56cf9 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -377,6 +377,7 @@ namespace q { m_model->reset_eval_cache(); for (app* v : qb.vars) m_model->register_decl(v->get_decl(), mdl(v)); + ctx.model_updated(m_model); if (qb.var_args.empty()) return; var_subst subst(m); @@ -416,7 +417,16 @@ namespace q { expr_ref value = (*m_model)(term); expr* s = m_model_fixer.invert_app(term, value); rep.insert(term, s); - eqs.push_back(m.mk_eq(term, s)); + expr_ref eq(m.mk_eq(term, s), m); + if (m_model->is_false(eq)) { + IF_VERBOSE(0, + verbose_stream() << mk_pp(s, m) << " := " << (*m_model)(s) << "\n"; + verbose_stream() << mk_pp(term, m) << " := " << (*m_model)(term) << "\n"; + verbose_stream() << value << " -> " << (*m_model)(ctx.values2root()[value]->get_expr()) << "\n"; + verbose_stream() << (*m_model)(s) << " -> " << (*m_model)(ctx.values2root()[(*m_model)(s)]->get_expr()) << "\n"; + verbose_stream() << *m_model << "\n";); + } + eqs.push_back(eq); } rep(fmls); fmls.append(eqs); diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 512a21179..86c502932 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -218,13 +218,14 @@ namespace q { expr* model_fixer::invert_app(app* t, expr* value) { euf::enode* r = nullptr; + auto& v2r = ctx.values2root(); TRACE("q", - tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n"; - if (ctx.values2root().find(value, r)) + tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n"; + if (v2r.find(value, r)) tout << "inverse " << mk_pp(r->get_expr(), m) << "\n"; - ctx.display(tout); + ctx.display(tout); ); - if (ctx.values2root().find(value, r)) + if (v2r.find(value, r)) return r->get_expr(); return value; }