From 1f150ecd5230808d660949d665ba49aee696890e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Sep 2022 22:22:34 -0500 Subject: [PATCH] #6319 #6319 - fix incompleteness in propagation of default to all array terms in the equivalence class. Fix bug with q_mbi where domain restrictions are not using values because the current model does not evaluate certain bound variables to values. Set model completion when adding these bound variables to the model to ensure their values are not missed. Add better propagation of diagnostics when tactics and the new solver return unknown. The reason for unknown can now be traced to what theory was culprit (currently no additional information) --- src/CMakeLists.txt | 2 +- src/sat/sat_extension.h | 2 ++ src/sat/sat_solver.cpp | 2 +- src/sat/smt/arith_solver.cpp | 1 - src/sat/smt/array_internalize.cpp | 2 +- src/sat/smt/array_model.cpp | 13 ++++++++++--- src/sat/smt/array_solver.cpp | 9 +++++++-- src/sat/smt/array_solver.h | 5 +++-- src/sat/smt/euf_model.cpp | 12 +++++++++++- src/sat/smt/euf_solver.cpp | 9 ++++++--- src/sat/smt/euf_solver.h | 2 ++ src/sat/smt/q_mbi.cpp | 20 ++++++++++++++------ src/sat/tactic/sat_tactic.cpp | 2 ++ src/solver/solver2tactic.cpp | 1 + src/tactic/goal.h | 5 +++++ src/tactic/tactic.cpp | 7 ++++--- 16 files changed, 70 insertions(+), 24 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 56c1d65cd..b96638944 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -135,7 +135,7 @@ if (MSVC AND Z3_BUILD_LIBZ3_MSVC_STATIC) set(${CompilerFlag} "${${CompilerFlag}}" CACHE STRING "msvc compiler flags" FORCE) message("MSVC flags: ${CompilerFlag}:${${CompilerFlag}}") endforeach() -endif(MSVC) +endif() add_library(libz3 ${lib_type} ${object_files}) target_include_directories(libz3 INTERFACE $ diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index ffcb95587..8730a2c2e 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -132,6 +132,8 @@ namespace sat { return false; } virtual bool is_pb() { return false; } + + virtual std::string reason_unknown() { return "unknown"; } }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5222201c9..59503fb00 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1357,7 +1357,6 @@ namespace sat { return is_sat; } catch (const abort_solver &) { - m_reason_unknown = "sat.giveup"; IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort giveup\")\n";); return l_undef; } @@ -1778,6 +1777,7 @@ namespace sat { case check_result::CR_CONTINUE: break; case check_result::CR_GIVEUP: + m_reason_unknown = m_ext->reason_unknown(); throw abort_solver(); } return l_undef; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 883773988..87e159b87 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -686,7 +686,6 @@ namespace arith { if (m_nla) m_nla->push(); th_euf_solver::push_core(); - } void solver::pop_core(unsigned num_scopes) { diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index bd01f52da..4df4f3a50 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -122,7 +122,7 @@ namespace array { ctx.push(push_back_vector(m_minmaxdiffs)); break; case OP_ARRAY_DEFAULT: - add_parent_default(find(n->get_arg(0)), n); + add_parent_default(find(n->get_arg(0))); break; case OP_ARRAY_MAP: case OP_SET_UNION: diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index 8b56ff3ae..aa986d87f 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -69,14 +69,21 @@ namespace array { values.set(n->get_expr_id(), n->get_expr()); return; } - + theory_var v = get_th_var(n); + euf::enode* d = get_default(v); + + if (a.is_const(n->get_expr())) { + expr* val = values.get(d->get_root_id()); + SASSERT(val); + values.set(n->get_expr_id(), a.mk_const_array(n->get_sort(), val)); + return; + } + unsigned arity = get_array_arity(srt); func_decl * f = mk_aux_decl_for_array_sort(m, srt); func_interp * fi = alloc(func_interp, m, arity); mdl.register_decl(f, fi); - theory_var v = get_th_var(n); - euf::enode* d = get_default(v); if (d && !fi->get_else()) fi->set_else(values.get(d->get_root_id())); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 2481e337a..1c4b95abe 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -172,6 +172,10 @@ namespace array { add_parent_select(v1, select); if (is_lambda(e1) || is_lambda(e2)) push_axiom(congruence_axiom(n1, n2)); + if (d1.m_has_default && !d2.m_has_default) + add_parent_default(v2); + if (!d1.m_has_default && d2.m_has_default) + add_parent_default(v1); } void solver::add_parent_select(theory_var v_child, euf::enode* select) { @@ -206,9 +210,10 @@ namespace array { propagate_select_axioms(d, lambda); } - void solver::add_parent_default(theory_var v, euf::enode* def) { - SASSERT(a.is_default(def->get_expr())); + void solver::add_parent_default(theory_var v) { auto& d = get_var_data(find(v)); + ctx.push(value_trail(d.m_has_default)); + d.m_has_default = true; for (euf::enode* lambda : d.m_lambdas) push_axiom(default_axiom(lambda)); if (should_prop_upward(d)) diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index fbff2afb6..5c2708842 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -50,7 +50,8 @@ namespace array { // void log_drat(array_justification const& c); struct var_data { - bool m_prop_upward{ false }; + bool m_prop_upward = false ; + bool m_has_default = false; euf::enode_vector m_lambdas; // equivalent nodes that have beta reduction properties euf::enode_vector m_parent_lambdas; // parents that have beta reduction properties euf::enode_vector m_parent_selects; // parents that use array in select position @@ -202,7 +203,7 @@ namespace array { // solving void add_parent_select(theory_var v_child, euf::enode* select); - void add_parent_default(theory_var v_child, euf::enode* def); + void add_parent_default(theory_var v_child); void add_lambda(theory_var v, euf::enode* lambda); void add_parent_lambda(theory_var v_child, euf::enode* lambda); diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 4b7745dd7..c22c46322 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -296,7 +296,17 @@ namespace euf { expr_ref sval(m); th_rewriter rw(m); rw(val, sval); - out << bpp(r) << " := " << sval << " " << mdl(r->get_root()->get_expr()) << "\n"; + expr_ref mval = mdl(r->get_root()->get_expr()); + if (mval != sval) { + out << bpp(r) << " :=\neval: " << sval << "\nmval: " << mval << "\n"; + continue; + } + if (!m.is_bool(val)) + continue; + auto bval = s().value(r->bool_var()); + bool tt = l_true == bval; + if (tt != m.is_true(sval)) + out << bpp(r) << " :=\neval: " << sval << "\nmval: " << bval << "\n"; } for (euf::enode* r : nodes) r->unmark1(); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 806509e4a..c30fdbf89 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -166,8 +166,9 @@ namespace euf { IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n"); } - void solver::init_search() { + void solver::init_search() { TRACE("before_search", s().display(tout);); + m_reason_unknown.clear(); for (auto* s : m_solvers) s->init_search(); } @@ -482,7 +483,7 @@ namespace euf { auto apply_solver = [&](th_solver* e) { switch (e->check()) { case sat::check_result::CR_CONTINUE: cont = true; break; - case sat::check_result::CR_GIVEUP: give_up = true; break; + case sat::check_result::CR_GIVEUP: m_reason_unknown = "incomplete theory " + e->name().str(); TRACE("euf", tout << "give up " << e->name() << "\n"); give_up = true; break; default: break; } }; @@ -490,8 +491,10 @@ namespace euf { cont = true; for (unsigned i = 0; i < m_solvers.size(); ++i) { auto* e = m_solvers[i]; - if (!m.inc()) + if (!m.inc()) { + m_reason_unknown = "canceled"; return sat::check_result::CR_GIVEUP; + } if (e == m_qsolver) continue; apply_solver(e); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 089c896cb..d19e0acac 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -105,6 +105,7 @@ namespace euf { user_solver::solver* m_user_propagator = nullptr; th_solver* m_qsolver = nullptr; unsigned m_generation = 0; + std::string m_reason_unknown; mutable ptr_vector m_todo; ptr_vector m_bool_var2expr; @@ -290,6 +291,7 @@ namespace euf { bool should_research(sat::literal_vector const& core) override; void add_assumptions(sat::literal_set& assumptions) override; bool tracking_assumptions() override; + std::string reason_unknown() override { return m_reason_unknown; } void propagate(literal lit, ext_justification_idx idx); bool propagate(enode* a, enode* b, ext_justification_idx idx); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index f2caa2a3e..a87be2dee 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -198,6 +198,7 @@ namespace q { expr_ref_vector eqs(m); add_domain_bounds(mdl, qb); auto proj = solver_project(mdl, qb, eqs, false); + CTRACE("q", !proj, tout << "could not project " << qb.mbody << " " << eqs << "\n" << mdl); if (!proj) return false; add_instantiation(q, proj); @@ -339,8 +340,10 @@ namespace q { fmls.append(qb.domain_eqs); eliminate_nested_vars(fmls, qb); for (expr* e : fmls) - if (!m_model->is_true(e)) + if (!m_model->is_true(e)) { + TRACE("q", tout << "not true: " << mk_pp(e, m) << " := " << (*m_model)(e) << "\n"); return expr_ref(nullptr, m); + } mbp::project_plugin proj(m); proj.extract_literals(*m_model, vars, fmls); fmls_extracted = true; @@ -348,8 +351,9 @@ namespace q { if (!p) continue; if (ctx.use_drat()) { - if (!p->project(*m_model, vars, fmls, m_defs)) - return expr_ref(m); + if (!p->project(*m_model, vars, fmls, m_defs)) + return expr_ref(m); + } else if (!(*p)(*m_model, vars, fmls)) return expr_ref(m); @@ -430,8 +434,11 @@ namespace q { void mbqi::add_domain_bounds(model& mdl, q_body& qb) { qb.domain_eqs.reset(); m_model->reset_eval_cache(); - for (app* v : qb.vars) - m_model->register_decl(v->get_decl(), mdl(v)); + { + model::scoped_model_completion _sc(mdl, true); + 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; @@ -440,7 +447,8 @@ namespace q { expr_ref _term = subst(t, qb.vars); app_ref term(to_app(_term), m); expr_ref value = (*m_model)(term->get_arg(idx)); - m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs); + if (m.is_value(value)) + m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs); } } diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 892a88f89..562fa431e 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -74,6 +74,8 @@ class sat_tactic : public tactic { TRACE("sat", tout << "result of checking: " << r << " "; if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n"; if (m_goal2sat.has_interpreted_funs()) tout << "has interpreted\n";); + if (r == l_undef) + g->set_reason_unknown(m_solver->get_reason_unknown()); if (r == l_false) { expr_dependency * lcore = nullptr; if (produce_core) { diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 389ee124b..81d21f959 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -164,6 +164,7 @@ public: in->assert_expr(local_solver->get_assertion(i)); } } + in->set_reason_unknown(local_solver->reason_unknown()); result.push_back(in.get()); break; } diff --git a/src/tactic/goal.h b/src/tactic/goal.h index f32e4a66b..5e7e0b2fe 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -55,6 +55,7 @@ protected: proof_converter_ref m_pc; dependency_converter_ref m_dc; unsigned m_ref_count; + std::string m_reason_unknown; expr_array m_forms; expr_array m_proofs; expr_dependency_array m_dependencies; @@ -159,6 +160,8 @@ public: void set(model_converter* m) { m_mc = m; } void set(proof_converter* p) { m_pc = p; } + void set_reason_unknown(std::string const& reason_unknown) { m_reason_unknown = reason_unknown; } + std::string const& get_reason_unknown() { return m_reason_unknown; } bool is_cnf() const; goal * translate(ast_translation & translator) const; @@ -176,6 +179,8 @@ template inline bool is_decided_sat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_sat(); } template inline bool is_decided_unsat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_unsat(); } +template +inline std::string get_reason_unknown(GoalCollection const & c) { return c.size() == 1 ? c[0]->get_reason_unknown() : std::string("unknown"); } template void for_each_expr_at(ForEachProc& proc, goal const & s) { diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index cc0ab8f5e..b1609ed85 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -184,8 +184,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p if (r.size() > 0) { pr = r[0]->pr(0); CTRACE("tactic", pr, tout << pr << "\n";); - } - + } if (is_decided_sat(r)) { model_converter_ref mc = r[0]->mc(); @@ -217,7 +216,9 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p if (mc) (*mc)(labels); } - reason_unknown = "incomplete"; + reason_unknown = get_reason_unknown(r); + if (reason_unknown.empty()) + reason_unknown = "unknown"; return l_undef; } }