From fe1622b592be4420a08234206f777b084fd5415f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Jan 2025 15:16:04 -0800 Subject: [PATCH] sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_array_plugin.cpp | 87 +++++++++++++++++++++++--------- src/ast/sls/sls_array_plugin.h | 53 +++++++++++++++---- src/ast/sls/sls_context.cpp | 8 ++- src/ast/sls/sls_euf_plugin.cpp | 2 +- 4 files changed, 110 insertions(+), 40 deletions(-) diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp index bf7dc1fc5..9c7bfd88a 100644 --- a/src/ast/sls/sls_array_plugin.cpp +++ b/src/ast/sls/sls_array_plugin.cpp @@ -24,6 +24,7 @@ namespace sls { array_plugin::array_plugin(context& ctx): plugin(ctx), + euf(ctx.euf()), a(m) { m_fid = a.get_family_id(); @@ -36,36 +37,67 @@ namespace sls { m_kv = nullptr; init_egraph(*m_g); saturate(*m_g); -#if 0 if (m_g->inconsistent()) { resolve_conflict(); return false; } -#endif return !m_g->inconsistent(); } void array_plugin::resolve_conflict() { + ++m_stats.m_num_conflicts; auto& g = *m_g; SASSERT(g.inconsistent()); - unsigned n = 0; - sat::literal_vector lits; ptr_vector explain; g.begin_explain(); g.explain(explain, nullptr); g.end_explain(); - verbose_stream() << "conflict\n"; + IF_VERBOSE(3, verbose_stream() << "array conflict\n"); + bool has_missing_axiom = false; for (auto p : explain) { - if (is_literal(p)) { - sat::literal l = to_literal(p); - verbose_stream() << l << " " << mk_bounded_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n"; - } - else { - verbose_stream() << mk_bounded_pp(to_expr(p), m) << " == " << mk_bounded_pp(ctx.get_value(to_expr(p)), m) << "\n"; + if (is_index(p)) { + has_missing_axiom = true; + unsigned idx = to_index(p); + auto [t, sto, sel] = m_delayed_axioms[idx]; + switch (t) { + case store_axiom1: + add_store_axiom1(sto->get_app()); + break; + case store_axiom2_down: + case store_axiom2_up: + add_store_axiom2(sto->get_app(), sel->get_app()); + break; + case map_axiom: + case const_axiom: + add_eq_axiom(sto, sel); + break; + default: + UNREACHABLE(); + break; + } } } + if (has_missing_axiom) + return; + + sat::literal_vector lits; + for (auto p : explain) { + if (is_enode(p)) { + auto n = to_enode(p); + auto v = ctx.get_value(n->get_expr()); + lits.push_back(~ctx.mk_literal(m.mk_eq(n->get_expr(), v))); + if (a.is_store(n->get_expr())) + add_store_axiom1(n->get_app()); + } + else if (is_literal(p)) { + sat::literal l = to_literal(p); + lits.push_back(~l); + } + } + IF_VERBOSE(3, verbose_stream() << "add conflict clause\n"); + ctx.add_clause(lits); } // b ~ a[i -> v] @@ -141,13 +173,12 @@ namespace sls { if (nmap->get_root() == nsel->get_root()) return; if (!are_distinct(nsel, nmap)) { - g.merge(nmap, nsel, nullptr); + g.merge(nmap, nsel, to_ptr(map_axiom_index(nmap, nsel))); g.propagate(); if (!g.inconsistent()) return; } - expr_ref eq(m.mk_eq(nmap->get_expr(), nsel->get_expr()), m); - ctx.add_theory_axiom(eq); + add_eq_axiom(nmap, nsel); } euf::enode* array_plugin::mk_select(euf::egraph& g, euf::enode* b, euf::enode* sel) { @@ -175,10 +206,10 @@ namespace sls { auto nsel = mk_select(g, n, n); VERIFY(!g.inconsistent()); if (!are_distinct(nsel, val)) { - g.merge(nsel, val, nullptr); + g.merge(nsel, val, to_ptr(store_axiom1_index(n))); g.propagate(); if (!g.inconsistent()) - return; + return; } add_store_axiom1(n->get_app()); } @@ -195,7 +226,7 @@ namespace sls { return; auto nsel = mk_select(g, sto->get_arg(0), sel); if (!are_distinct(nsel, sel)) { - g.merge(nsel, sel, nullptr); + g.merge(nsel, sel, to_ptr(store_axiom2_down_index(sto, sel))); g.propagate(); if (!g.inconsistent()) return; @@ -215,7 +246,7 @@ namespace sls { return; auto nsel = mk_select(g, sto, sel); if (!are_distinct(nsel, sel)) { - g.merge(nsel, sel, nullptr); + g.merge(nsel, sel, to_ptr(store_axiom2_up_index(sto, sel))); g.propagate(); if (!g.inconsistent()) return; @@ -234,13 +265,13 @@ namespace sls { auto val = cn->get_arg(0); auto nsel = mk_select(g, cn, sel); if (!are_distinct(nsel, sel)) { - g.merge(nsel, sel, nullptr); + g.merge(nsel, sel, to_ptr(const_axiom_index(val, nsel))); g.propagate(); if (!g.inconsistent()) return; } - expr_ref eq(m.mk_eq(val->get_expr(), nsel->get_expr()), m); - ctx.add_theory_axiom(eq); + ++m_stats.m_num_axioms; + add_eq_axiom(val, nsel); } bool array_plugin::are_distinct(euf::enode* a, euf::enode* b) { @@ -270,6 +301,7 @@ namespace sls { expr_ref sel(a.mk_select(args), m); expr_ref eq(m.mk_eq(sel, to_app(sto)->get_arg(sto->get_num_args() - 1)), m); IF_VERBOSE(3, verbose_stream() << "add store axiom 1 " << mk_bounded_pp(sto, m) << "\n"); + ++m_stats.m_num_axioms; ctx.add_theory_axiom(eq); } @@ -291,6 +323,7 @@ namespace sls { for (unsigned i = 1; i < sel->get_num_args() - 1; ++i) ors.push_back(m.mk_eq(sel->get_arg(i), sto->get_arg(i))); IF_VERBOSE(3, verbose_stream() << "add store axiom 2 " << mk_bounded_pp(sto, m) << " " << mk_bounded_pp(sel, m) << "\n"); + ++m_stats.m_num_axioms; ctx.add_theory_axiom(m.mk_or(ors)); } @@ -307,11 +340,13 @@ namespace sls { n1 = n1 ? n1 : g.mk(t, 0, args.size(), args.data()); if (a.is_array(t)) continue; + if (m.is_bool(t)) + continue; auto v = ctx.get_value(t); IF_VERBOSE(3, verbose_stream() << "init " << mk_bounded_pp(t, m) << " := " << mk_bounded_pp(v, m) << " " << g.inconsistent() << "\n"); n2 = g.find(v); n2 = n2 ? n2: g.mk(v, 0, 0, nullptr); - g.merge(n1, n2, to_ptr(t)); + g.merge(n1, n2, to_ptr(n1)); } for (auto lit : ctx.root_literals()) { if (!ctx.is_true(lit) || lit.sign()) @@ -319,9 +354,10 @@ namespace sls { auto e = ctx.atom(lit.var()); expr* x = nullptr, * y = nullptr; if (e && m.is_eq(e, x, y)) - g.merge(g.find(x), g.find(y), to_ptr(lit)); + g.merge(g.find(x), g.find(y), nullptr); } + g.propagate(); IF_VERBOSE(3, display(verbose_stream())); @@ -388,4 +424,9 @@ namespace sls { } return out; } + + void array_plugin::collect_statistics(statistics& st) const { + st.update("sls-array-conflicts", m_stats.m_num_conflicts); + st.update("sls-array-axioms", m_stats.m_num_axioms); + } } diff --git a/src/ast/sls/sls_array_plugin.h b/src/ast/sls/sls_array_plugin.h index 3c76cc4e5..02d2b1865 100644 --- a/src/ast/sls/sls_array_plugin.h +++ b/src/ast/sls/sls_array_plugin.h @@ -22,6 +22,8 @@ Author: namespace sls { + class euf_plugin; + class array_plugin : public plugin { struct select_args { euf::enode* sel = nullptr; @@ -29,15 +31,15 @@ namespace sls { select_args() {} }; struct select_args_hash { - unsigned operator()(select_args const& a) const { + unsigned operator()(select_args const& a) const { unsigned h = 0; for (unsigned i = 1; i < a.sel->num_args(); ++i) - h ^= a.sel->get_arg(i)->get_root()->hash(); + h ^= a.sel->get_arg(i)->get_root()->hash(); return h; }; }; struct select_args_eq { - bool operator()(select_args const& a, select_args const& b) const { + bool operator()(select_args const& a, select_args const& b) const { SASSERT(a.sel->num_args() == b.sel->num_args()); for (unsigned i = 1; i < a.sel->num_args(); ++i) if (a.sel->get_arg(i)->get_root() != b.sel->get_arg(i)->get_root()) @@ -47,12 +49,37 @@ namespace sls { }; typedef map select2value; typedef obj_map kv; + struct stats { + unsigned m_num_conflicts = 0; + unsigned m_num_axioms = 0; + void reset() { memset(this, 0, sizeof(*this)); } + }; + euf_plugin& euf; array_util a; scoped_ptr m_g; - scoped_ptr m_kv; - bool m_add_conflicts = true; - bool m_has_arrays = false; + scoped_ptr m_kv; + bool m_add_conflicts = true; + bool m_has_arrays = false; + stats m_stats; + + enum axiom_t { store_axiom1, store_axiom2_down, store_axiom2_up, map_axiom, const_axiom }; + struct axiom_instance { + axiom_t t; + euf::enode* sto; euf::enode* sel; + }; + svector m_delayed_axioms; + unsigned store_axiom1_index(euf::enode* n) { m_delayed_axioms.push_back({ store_axiom1, n, nullptr }); return m_delayed_axioms.size() - 1; } + unsigned store_axiom2_down_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ store_axiom2_down, sto, sel }); return m_delayed_axioms.size() - 1; } + unsigned store_axiom2_up_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ store_axiom2_up, sto, sel }); return m_delayed_axioms.size() - 1; } + unsigned map_axiom_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ map_axiom, sto, sel }); return m_delayed_axioms.size() - 1; } + unsigned const_axiom_index(euf::enode* val, euf::enode* sel) { m_delayed_axioms.push_back({ const_axiom, val, sel }); return m_delayed_axioms.size() - 1; } + + void add_eq_axiom(euf::enode* x, euf::enode* y) { + ++m_stats.m_num_axioms; + expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m); + ctx.add_theory_axiom(eq); + } void init_egraph(euf::egraph& g); void init_kv(euf::egraph& g, kv& kv); @@ -73,10 +100,14 @@ namespace sls { void resolve_conflict(); size_t* to_ptr(sat::literal l) { return reinterpret_cast((size_t)(l.index() << 4)); }; - size_t* to_ptr(expr* t) { return reinterpret_cast((reinterpret_cast(t) << 4) + 1); } - bool is_literal(size_t* p) { return (reinterpret_cast(p) & 1) == 0; } + size_t* to_ptr(euf::enode* t) { return reinterpret_cast((reinterpret_cast(t) << 4) + 1); } + size_t* to_ptr(unsigned n) { return reinterpret_cast((size_t)(n << 4) + 3); } + bool is_literal(size_t* p) { return (reinterpret_cast(p) & 3) == 0; } + bool is_index(size_t* p) { return (reinterpret_cast(p) & 3) == 3; } + bool is_enode(size_t* p) { return (reinterpret_cast(p) & 3) == 1; } sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast(reinterpret_cast(p) >> 4)); }; - expr* to_expr(size_t* p) { return reinterpret_cast(reinterpret_cast(p) >> 4); } + euf::enode* to_enode(size_t* p) { return reinterpret_cast(reinterpret_cast(p) >> 4); } + unsigned to_index(size_t* p) { return static_cast(reinterpret_cast(p) >> 4); } public: array_plugin(context& ctx); @@ -95,8 +126,8 @@ namespace sls { void on_restart() override {} std::ostream& display(std::ostream& out) const override; bool set_value(expr* e, expr* v) override { return false; } - void collect_statistics(statistics& st) const override {} - void reset_statistics() override {} + void collect_statistics(statistics& st) const override; + void reset_statistics() override { m_stats.reset(); } }; } diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index dc3d5c30f..8ed3619e8 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -315,11 +315,9 @@ namespace sls { auto p = m_plugins.get(fid, nullptr); if (p) return p->get_value(e); - if (m.is_bool(e)) { - sat::bool_var v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var); - if (v != sat::null_bool_var) - return expr_ref(m.mk_bool_val(is_true(v)), m); - } + if (m.is_bool(e)) + return expr_ref(m.mk_bool_val(is_true(e)), m); + verbose_stream() << fid << " " << m.get_family_name(fid) << " " << mk_pp(e, m) << "\n"; UNREACHABLE(); return expr_ref(e, m); diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index d3d120cd0..b7c2195f0 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -90,7 +90,7 @@ namespace sls { g.explain(explain, nullptr); g.end_explain(); double reward = -1; - TRACE("enf", + TRACE("euf", for (auto p : explain) { sat::literal l = to_literal(p); tout << l << " " << mk_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n";