From d0fb3cba1574a4ce561b962fa07b19f104c59178 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Jan 2022 17:45:43 -0800 Subject: [PATCH] #5641 - projection that skips interpreted functions can violate model evaluation. --- src/qe/mbp/mbp_arith.cpp | 47 +++++++++++++++++++---------------- src/qe/mbp/mbp_arith.h | 4 +-- src/qe/mbp/mbp_arrays.cpp | 4 +-- src/qe/mbp/mbp_arrays.h | 2 +- src/qe/mbp/mbp_datatypes.cpp | 4 +-- src/qe/mbp/mbp_datatypes.h | 2 +- src/qe/mbp/mbp_plugin.h | 4 +-- src/qe/qe_mbi.cpp | 5 +++- src/sat/smt/q_mbi.cpp | 8 +++--- src/sat/smt/q_model_fixer.cpp | 2 +- 10 files changed, 46 insertions(+), 36 deletions(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 120931536..377b62ac0 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -249,8 +249,8 @@ namespace mbp { bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) { app_ref_vector vs(m); vs.push_back(v); - project(model, vs, lits, false); - return vs.empty(); + vector defs; + return project(model, vs, lits, defs, false) && vs.empty(); } typedef opt::model_based_opt::var var; @@ -265,12 +265,12 @@ namespace mbp { return t; } - vector project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, bool compute_def) { + bool project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, vector& result, bool compute_def) { bool has_arith = false; for (expr* v : vars) has_arith |= is_arith(v); if (!has_arith) - return vector(); + return true; model_evaluator eval(model); TRACE("qe", tout << model;); eval.set_model_completion(true); @@ -294,7 +294,7 @@ namespace mbp { } fmls.shrink(j); TRACE("qe", tout << "formulas\n" << fmls << "\n"; - for (auto [e, id] : tids) + for (auto const& [e, id] : tids) tout << mk_pp(e, m) << " -> " << id << "\n";); // fmls holds residue, @@ -312,7 +312,7 @@ namespace mbp { rational r; expr_ref val = eval(v); if (!m.inc()) - return vector(); + return false; if (!a.is_numeral(val, r)) throw default_exception("evaluation did not produce a numeral"); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); @@ -326,15 +326,13 @@ namespace mbp { if (is_arith(e) && !var_mark.is_marked(e)) mark_rec(fmls_mark, e); } - if (m_check_purified) { for (expr* fml : fmls) mark_rec(fmls_mark, fml); for (auto& kv : tids) { expr* e = kv.m_key; - if (!var_mark.is_marked(e)) { - mark_rec(fmls_mark, e); - } + if (!var_mark.is_marked(e)) + mark_rec(fmls_mark, e); } } @@ -364,16 +362,18 @@ namespace mbp { for (auto const& d : defs) tout << "def: " << d << "\n"; tout << fmls << "\n";); - vector result; if (compute_def) optdefs2mbpdef(defs, index2expr, real_vars, result); - if (m_apply_projection) - apply_projection(result, fmls); + if (m_apply_projection && !apply_projection(eval, result, fmls)) + return false; + TRACE("qe", - for (auto [v, t] : result) + for (auto const& [v, t] : result) tout << v << " := " << t << "\n"; + for (auto* f : fmls) + tout << mk_pp(f, m) << " := " << eval(f) << "\n"; tout << "fmls:" << fmls << "\n";); - return result; + return true; } void optdefs2mbpdef(vector const& defs, ptr_vector const& index2expr, unsigned_vector const& real_vars, vector& result) { @@ -548,10 +548,11 @@ namespace mbp { } } - void apply_projection(vector& defs, expr_ref_vector& fmls) { + bool apply_projection(model_evaluator& eval, vector const& defs, expr_ref_vector& fmls) { if (fmls.empty() || defs.empty()) - return; + return true; expr_safe_replace subst(m); + expr_ref_vector fmls_tmp(m); expr_ref tmp(m); for (unsigned i = defs.size(); i-- > 0; ) { auto const& d = defs[i]; @@ -561,8 +562,11 @@ namespace mbp { unsigned j = 0; for (expr* fml : fmls) { subst(fml, tmp); + if (m.is_false(eval(tmp))) + return false; fmls[j++] = tmp; } + return true; } }; @@ -579,12 +583,13 @@ namespace mbp { return (*m_imp)(model, var, vars, lits); } - void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - m_imp->project(model, vars, lits, false); + bool arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + vector defs; + return m_imp->project(model, vars, lits, defs, false); } - vector arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return m_imp->project(model, vars, lits, true); + bool arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + return m_imp->project(model, vars, lits, defs, true); } void arith_project_plugin::set_check_purified(bool check_purified) { diff --git a/src/qe/mbp/mbp_arith.h b/src/qe/mbp/mbp_arith.h index 51d80a870..ca4cccb74 100644 --- a/src/qe/mbp/mbp_arith.h +++ b/src/qe/mbp/mbp_arith.h @@ -29,8 +29,8 @@ namespace mbp { bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; } family_id get_family_id() override; - void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); } opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt); diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 149d11987..0f4c805b7 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -1624,8 +1624,8 @@ namespace mbp { ); } - vector array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return vector(); + bool array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + return true; } void array_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) { diff --git a/src/qe/mbp/mbp_arrays.h b/src/qe/mbp/mbp_arrays.h index bb18cde11..7dd904108 100644 --- a/src/qe/mbp/mbp_arrays.h +++ b/src/qe/mbp/mbp_arrays.h @@ -35,7 +35,7 @@ namespace mbp { bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; void operator()(model& model, app_ref_vector& vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects); family_id get_family_id() override; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override; }; diff --git a/src/qe/mbp/mbp_datatypes.cpp b/src/qe/mbp/mbp_datatypes.cpp index 798258599..e40a19546 100644 --- a/src/qe/mbp/mbp_datatypes.cpp +++ b/src/qe/mbp/mbp_datatypes.cpp @@ -300,8 +300,8 @@ namespace mbp { return m_imp->solve(model, vars, lits); } - vector datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return vector(); + bool datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + return true; } void datatype_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) { diff --git a/src/qe/mbp/mbp_datatypes.h b/src/qe/mbp/mbp_datatypes.h index 345260970..f30aaaa9f 100644 --- a/src/qe/mbp/mbp_datatypes.h +++ b/src/qe/mbp/mbp_datatypes.h @@ -34,7 +34,7 @@ namespace mbp { bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; family_id get_family_id() override; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override; }; diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 741639aaa..12b592960 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -67,7 +67,7 @@ namespace mbp { virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; } virtual family_id get_family_id() { return null_family_id; } - virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { }; + virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; /** \brief project vars modulo model, return set of definitions for eliminated variables. @@ -76,7 +76,7 @@ namespace mbp { - returns set of definitions (TBD: in triangular form, the last definition can be substituted into definitions that come before) */ - virtual vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return vector(); } + virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { return true; } /** \brief model based saturation. Saturates theory axioms to equi-satisfiable literals over EUF, diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 1dcbb178f..5d00d8a6b 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -266,7 +266,10 @@ namespace qe { vector uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) { mbp::arith_project_plugin ap(m); ap.set_check_purified(false); - return ap.project(*mdl.get(), avars, lits); + vector defs; + bool ok = ap.project(*mdl.get(), avars, lits, defs); + CTRACE("qe", !ok, tout << "projection failure ignored!!!!\n"); + return defs; } mbi_result uflia_mbi::operator()(expr_ref_vector& lits, model_ref& mdl) { diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 000937700..38e8ff45e 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -67,7 +67,7 @@ namespace q { } } m_max_cex += ctx.get_config().m_mbqi_max_cexs; - for (auto [qlit, fml, generation] : m_instantiations) { + for (auto const& [qlit, fml, generation] : m_instantiations) { euf::solver::scoped_generation sg(ctx, generation + 1); sat::literal lit = ctx.mk_literal(fml); m_qs.add_clause(~qlit, ~lit); @@ -308,8 +308,10 @@ namespace q { proj.extract_literals(*m_model, vars, fmls); fmls_extracted = true; } - if (p) - (*p)(*m_model, vars, fmls); + if (!p) + continue; + if (!(*p)(*m_model, vars, fmls)) + return expr_ref(nullptr, m); } for (app* v : vars) { expr_ref term(m); diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index a87bf3397..456525c42 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -256,7 +256,7 @@ namespace q { 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 (v2r.find(value, r)) return r->get_expr();