From a3ba4e136634b0c94806e6508b5f2002d020344a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 11:34:44 -0700 Subject: [PATCH 01/13] #5528 --- src/sat/smt/q_eval.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index 73232fb7c24..600dcd2c5ef 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -181,23 +181,25 @@ namespace q { while (!todo.empty()) { expr* t = todo.back(); SASSERT(!is_ground(t) || ctx.get_egraph().find(t)); + if (m_mark.is_marked(t)) { + todo.pop_back(); + continue; + } if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) { - m_mark.mark(t); m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); if (!m_eval[t->get_id()]) return nullptr; - todo.pop_back(); - continue; - } - if (m_mark.is_marked(t)) { + m_mark.mark(t); todo.pop_back(); continue; } if (is_var(t)) { - m_mark.mark(t); if (to_var(t)->get_idx() >= n) return nullptr; m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr); + if (!m_eval[t->get_id()]) + return nullptr; + m_mark.mark(t); todo.pop_back(); continue; } From 8bdc8d0e1a0ed8ebb34c0217a00cb9cd2da79c29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 11:35:06 -0700 Subject: [PATCH 02/13] Update solver_subsumption_tactic.h use naming convention with - instead of _ for tactics --- src/tactic/portfolio/solver_subsumption_tactic.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/portfolio/solver_subsumption_tactic.h b/src/tactic/portfolio/solver_subsumption_tactic.h index c088aa0b04b..73dfb562c43 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.h +++ b/src/tactic/portfolio/solver_subsumption_tactic.h @@ -19,7 +19,7 @@ class tactic; tactic * mk_solver_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref()); /* - ADD_TACTIC("solver_subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)") + ADD_TACTIC("solver-subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)") */ From a7bc4719c08f300f6c08367ec9175344a8d5df3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 11:45:21 -0700 Subject: [PATCH 03/13] fix #5526 when propagation claims progress, but is a no-op. --- src/solver/assertions/asserted_formulas.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index be931ccd676..9e9b5414058 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -532,14 +532,14 @@ void asserted_formulas::propagate_values() { flush_cache(); unsigned num_prop = 0; - unsigned delta_prop = m_formulas.size(); - while (!inconsistent() && m_formulas.size()/20 < delta_prop) { + unsigned sz = m_formulas.size(); + unsigned delta_prop = sz; + while (!inconsistent() && sz/20 < delta_prop) { m_expr2depth.reset(); m_scoped_substitution.push(); unsigned prop = num_prop; TRACE("propagate_values", display(tout << "before:\n");); unsigned i = m_qhead; - unsigned sz = m_formulas.size(); for (; i < sz; i++) { prop += propagate_values(i); } @@ -558,6 +558,9 @@ void asserted_formulas::propagate_values() { TRACE("propagate_values", tout << "after:\n"; display(tout);); delta_prop = prop - num_prop; num_prop = prop; + if (sz <= m_formulas.size()) + break; + sz = m_formulas.size(); } TRACE("asserted_formulas", tout << num_prop << "\n";); if (num_prop > 0) From 7ce4be8455d52e73c483f2a67358063cfd505de7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 14:01:15 -0700 Subject: [PATCH 04/13] #5528 --- src/sat/smt/euf_internalize.cpp | 4 +++- src/sat/smt/euf_solver.cpp | 21 ++++++++++++++++++++- src/sat/smt/euf_solver.h | 2 ++ 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 020d29baa28..f60c3597dad 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -342,7 +342,9 @@ namespace euf { break; } } - + if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id()) + return true; + for (enode* parent : euf::enode_parents(n)) { app* p = to_app(parent->get_expr()); family_id fid = p->get_family_id(); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 5d9b9695881..1f0523ddeab 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -300,7 +300,7 @@ namespace euf { size_t* c = to_ptr(l); SASSERT(is_literal(c)); SASSERT(l == get_literal(c)); - if (n->value_conflict()) { + if (n->value_conflict()) { euf::enode* nb = sign ? mk_false() : mk_true(); euf::enode* r = n->get_root(); euf::enode* rb = sign ? mk_true() : mk_false(); @@ -458,6 +458,8 @@ namespace euf { give_up = true; unsigned num_nodes = m_egraph.num_nodes(); + if (merge_shared_bools()) + cont = true; for (auto* e : m_solvers) { if (!m.inc()) return sat::check_result::CR_GIVEUP; @@ -485,6 +487,23 @@ namespace euf { return sat::check_result::CR_DONE; } + bool solver::merge_shared_bools() { + bool merged = false; + for (euf::enode* n : m_egraph.nodes()) { + if (!is_shared(n) || !m.is_bool(n->get_expr())) + continue; + if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) { + m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var()))); + merged = true; + } + if (n->value() == l_false && !m.is_false(n->get_root()->get_expr())) { + m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var()))); + merged = true; + } + } + return merged; + } + void solver::push() { si.push(); scope s; diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index d88a832eca2..db928259c9c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -165,6 +165,7 @@ namespace euf { bool is_self_propagated(th_eq const& e); void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing); void new_diseq(enode* a, enode* b, literal lit); + bool merge_shared_bools(); // proofs void log_antecedents(std::ostream& out, literal l, literal_vector const& r); @@ -286,6 +287,7 @@ namespace euf { void propagate(literal lit, th_explain* p) { propagate(lit, p->to_index()); } bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); } + size_t* to_justification(sat::literal l) { return to_ptr(l); } void set_conflict(th_explain* p) { set_conflict(p->to_index()); } bool set_root(literal l, literal r) override; From 0c53c139da18d0804003cbb4b6a841692e50d724 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 15:37:58 -0700 Subject: [PATCH 05/13] add to_string method to make it easier to use without << --- src/api/c++/z3++.h | 1 + src/sat/smt/array_axioms.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 97413ae5436..c11269b1578 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -599,6 +599,7 @@ namespace z3 { iterator begin() const noexcept { return iterator(this, 0); } iterator end() const { return iterator(this, size()); } friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } + std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector); } }; diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index ecb1bc4708a..c34b8ae1715 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -451,6 +451,7 @@ namespace array { expr_ref alpha(a.mk_select(args), m); expr_ref beta(alpha); rewrite(beta); + TRACE("array", tout << alpha << " == " << beta << "\n";); return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom()); } From ba68fba4193569a24263629b2af449e7fac5f6c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 17:10:23 -0700 Subject: [PATCH 06/13] build --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index c11269b1578..fd204a5bf72 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -599,7 +599,7 @@ namespace z3 { iterator begin() const noexcept { return iterator(this, 0); } iterator end() const { return iterator(this, size()); } friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } - std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector); } + std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); } }; From cf9e55fa969692c5cdf8b7a7e19fd426064e3fb6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 17:44:17 -0700 Subject: [PATCH 07/13] #5516 expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes. --- src/ast/rewriter/array_rewriter.cpp | 7 +++---- src/params/array_rewriter_params.pyg | 1 + 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index b464a33f8eb..f941de8f1b1 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -31,7 +31,7 @@ void array_rewriter::updt_params(params_ref const & _p) { m_expand_store_eq = p.expand_store_eq(); m_expand_nested_stores = p.expand_nested_stores(); m_blast_select_store = p.blast_select_store(); - m_expand_select_ite = false; + m_expand_select_ite = p.expand_select_ite(); } void array_rewriter::get_param_descrs(param_descrs & r) { @@ -226,8 +226,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, result = subst(q->get_expr(), _args.size(), _args.data()); inv_var_shifter invsh(m()); invsh(result, _args.size(), result); - return BR_REWRITE_FULL; - + return BR_REWRITE_FULL; } if (m_util.is_map(args[0])) { @@ -698,7 +697,7 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) { unsigned n = to_app(rhs)->get_num_args(); result = m().mk_and(m().mk_eq(lhs, to_app(rhs)->get_arg(0)), - m().mk_eq(v, to_app(rhs)->get_arg(n - 1))); + m().mk_eq(v, to_app(rhs)->get_arg(n - 1))); return BR_REWRITE2; } if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) { diff --git a/src/params/array_rewriter_params.pyg b/src/params/array_rewriter_params.pyg index ba178f40dab..26444440f24 100644 --- a/src/params/array_rewriter_params.pyg +++ b/src/params/array_rewriter_params.pyg @@ -4,5 +4,6 @@ def_module_params(module_name='rewriter', params=(("expand_select_store", BOOL, False, "conservatively replace a (select (store ...) ...) term by an if-then-else term"), ("blast_select_store", BOOL, False, "eagerly replace all (select (store ..) ..) term by an if-then-else term"), ("expand_nested_stores", BOOL, False, "replace nested stores by a lambda expression"), + ("expand_select_ite", BOOL, False, "expand select over ite expressions"), ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"), ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different"))) From a74c01c8b98088ed096e7c046a8baa1906cf5f24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 20:39:54 -0700 Subject: [PATCH 08/13] #5528 --- src/sat/smt/arith_internalize.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index e59d3f4d7fa..d8671c910c5 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -42,6 +42,7 @@ namespace arith { void solver::init_internalize() { force_push(); // initialize 0, 1 variables: + if (!m_internalize_initialized) { get_one(true); get_one(false); @@ -484,10 +485,10 @@ namespace arith { return st.vars()[0]; } else if (is_one(st) && a.is_numeral(term)) { - return get_one(a.is_int(term)); + return lp().local_to_external(get_one(a.is_int(term))); } else if (is_zero(st) && a.is_numeral(term)) { - return get_zero(a.is_int(term)); + return lp().local_to_external(get_zero(a.is_int(term))); } else { init_left_side(st); From 6907d3071796f403ae8c6817905e197c1884fb26 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 20:44:00 -0700 Subject: [PATCH 09/13] #5528 --- src/sat/smt/euf_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 1f0523ddeab..fbe54c8fe1f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -489,7 +489,8 @@ namespace euf { bool solver::merge_shared_bools() { bool merged = false; - for (euf::enode* n : m_egraph.nodes()) { + for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) { + euf::enode* n = m_egraph.nodes()[i]; if (!is_shared(n) || !m.is_bool(n->get_expr())) continue; if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) { From 968717a532baaa6b5bdf56a688a6380bc7791a0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 20:49:39 -0700 Subject: [PATCH 10/13] follow on fix from #5528 the same bug is also undetected in the main solver --- src/smt/theory_lra.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index abe10d0f32a..1244611895f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -807,10 +807,10 @@ class theory_lra::imp { return st.vars()[0]; } else if (is_one(st) && a.is_numeral(term)) { - return get_one(a.is_int(term)); + return lp().local_to_external(get_one(a.is_int(term))); } else if (is_zero(st) && a.is_numeral(term)) { - return get_zero(a.is_int(term)); + return lp().local_to_external(get_zero(a.is_int(term))); } else { init_left_side(st); From 9e306e3b6ecc78b70e2bcc86db1b9bc75c515d6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 20:50:35 -0700 Subject: [PATCH 11/13] more useful diagnostics --- src/smt/smt_context_inv.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index bc994f0b347..f0e8fb59b3a 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -371,7 +371,7 @@ namespace smt { case l_true: if (!m_proto_model->eval(n, res, false)) return true; - CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); + CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); if (m.is_false(res)) { return false; } @@ -379,7 +379,7 @@ namespace smt { case l_false: if (!m_proto_model->eval(n, res, false)) return true; - CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); + CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); if (m.is_true(res)) { return false; } From f4abe3db0237e5439db74fcedcf39f731f642d29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Sep 2021 03:13:46 -0700 Subject: [PATCH 12/13] #5528 --- src/sat/smt/q_mam.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index bd8859575fc..e5922fd8cb7 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -3745,7 +3745,7 @@ namespace q { // However, the simplifier may turn a non-ground pattern into a ground one. // So, we should check it again here. for (expr* arg : *mp) - if (is_ground(arg)) + if (is_ground(arg) || has_quantifiers(arg)) return; // ignore multi-pattern containing ground pattern. update_filters(qa, mp); m_new_patterns.push_back(qp_pair(qa, mp)); From e05ef8ece9c527e1ea6fabb84f7ecbe5287e691f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Sep 2021 04:20:19 -0700 Subject: [PATCH 13/13] account for updating scoped state by goal2sat #5528 --- src/sat/tactic/goal2sat.cpp | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 9be810e9de0..76e11474e5d 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -251,7 +251,7 @@ struct goal2sat::imp : public sat::sat_internalizer { return; } n -= m_num_scopes; - m_num_scopes = 0; + m_num_scopes = 0; m_map.pop(n); unsigned k = m_cache_lim[m_cache_lim.size() - n]; for (unsigned i = m_cache_trail.size(); i-- > k; ) { @@ -284,7 +284,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_cache_trail.push_back(t); } - void convert_atom(expr * t, bool root, bool sign) { + void convert_atom(expr * t, bool root, bool sign) { SASSERT(m.is_bool(t)); sat::literal l; sat::bool_var v = m_map.to_bool_var(t); @@ -954,9 +954,11 @@ struct goal2sat::imp : public sat::sat_internalizer { } void user_push() { + push(); } void user_pop(unsigned n) { + pop(n); } }; @@ -1010,15 +1012,7 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core for (unsigned i = 0; i < m_scopes; ++i) m_imp->user_push(); } - (*m_imp)(g); - - if (!t.get_extension() && m_imp->interpreted_funs().empty()) { - dealloc(m_imp); - m_imp = nullptr; - } - else - m_scopes = 0; - + (*m_imp)(g); } void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) {