From a4275dfb158d4adf6999e04603e7e1d0f8c473af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Oct 2024 09:36:07 -0700 Subject: [PATCH] dt updates Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.h | 2 + src/ast/sls/sls_context.cpp | 10 ++ src/ast/sls/sls_context.h | 2 + src/ast/sls/sls_datatype_plugin.cpp | 143 ++++++++++++++++++++++++---- src/ast/sls/sls_datatype_plugin.h | 8 +- src/ast/sls/sls_euf_plugin.h | 2 + 6 files changed, 147 insertions(+), 20 deletions(-) diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index dcca78970..48033d129 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -341,8 +341,10 @@ namespace datatype { ast_manager & get_manager() const { return m; } // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); } + bool is_datatype(expr* e) const { return is_datatype(e->get_sort()); } bool is_enum_sort(sort* s); bool is_recursive(sort * ty); + bool is_recursive(expr* e) { return is_recursive(e->get_sort()); } bool is_recursive_nested(sort * ty); bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); } bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); } diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index bafbd247d..df2a5f29a 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -69,6 +69,16 @@ namespace sls { verbose_stream() << "did not find plugin for " << fid << "\n"; } + scoped_ptr& context::ensure_euf() { + auto fid = user_sort_family_id; + auto p = m_plugins.get(fid, nullptr); + if (!p) { + p = alloc(euf_plugin, *this); + register_plugin(p); + } + return dynamic_cast(p)->egraph(); + } + void context::ensure_plugin(expr* e) { auto fid = get_fid(e); ensure_plugin(fid); diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index a83946a77..74eba4682 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -20,6 +20,7 @@ Author: #include "util/sat_sls.h" #include "util/statistics.h" #include "ast/ast.h" +#include "ast/euf/euf_egraph.h" #include "model/model.h" #include "util/scoped_ptr_vector.h" #include "util/obj_hashtable.h" @@ -195,6 +196,7 @@ namespace sls { ast_manager& get_manager() { return m; } std::ostream& display(std::ostream& out) const; std::ostream& display_all(std::ostream& out) const { return s.display(out); } + scoped_ptr& ensure_euf(); void collect_statistics(statistics& st) const; void reset_statistics(); diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp index ed38967a1..3a30c6a19 100644 --- a/src/ast/sls/sls_datatype_plugin.cpp +++ b/src/ast/sls/sls_datatype_plugin.cpp @@ -33,13 +33,21 @@ Axioms: a := s = acc(t), a in Atoms => (a => s < t) in P s << t if there is a path P with conditions L. - L => s != t + L => s != t This disregards if acc is applied to non-matching constructor. In this case we rely on that the interpretation of acc can be forced. If this is incorrect, include is-c(t) assumptions in path axioms. + Is P sufficient? Should we just consider all possible paths of depth at most k to be safe? + Example: + C(acc(t)) == C(s) + triggers equation acc(t) = s, but the equation is implicit, so acc(t) and s are not directly + connected. + Even, the axioms extracted from P don't consider transitivity of =. + So the can-be-equal alias approximation is currently too strong. + --*/ #include "ast/sls/sls_datatype_plugin.h" @@ -48,7 +56,10 @@ namespace sls { datatype_plugin::datatype_plugin(context& c): plugin(c), - dt(m) { + g(c.ensure_euf()), + dt(m), + m_axioms(m), + m_values(m) { m_fid = dt.get_family_id(); } @@ -56,9 +67,14 @@ namespace sls { void datatype_plugin::collect_path_axioms() { expr* t = nullptr, *z = nullptr; - for (auto s : ctx.subterms()) - if (dt.is_accessor(s, t) && dt.is_recursive(t->get_sort())) + for (auto s : ctx.subterms()) { + if (dt.is_accessor(s, t) && dt.is_recursive(t) && dt.is_recursive(s)) add_edge(s, t, sat::null_literal); + if (dt.is_constructor(s) && dt.is_recursive(s)) { + for (auto arg : *to_app(s)) + add_edge(arg, s, sat::null_literal); + } + } expr* x = nullptr, *y = nullptr; for (sat::bool_var v = 0; v < ctx.num_bool_vars(); ++v) { expr* e = ctx.atom(v); @@ -66,8 +82,10 @@ namespace sls { continue; if (!m.is_eq(e, x, y)) continue; + if (!dt.is_recursive(x)) + continue; sat::literal lp(v, false), ln(v, true); - if (dt.is_accessor(x, z) && dt.is_recursive(z->get_sort())) { + if (dt.is_accessor(x, z) && dt.is_recursive(z)) { if (ctx.is_unit(lp)) add_edge(y, z, sat::null_literal); else if (ctx.is_unit(ln)) @@ -75,7 +93,7 @@ namespace sls { else add_edge(y, z, lp); } - if (dt.is_accessor(y, z) && dt.is_recursive(z->get_sort())) { + if (dt.is_accessor(y, z) && dt.is_recursive(z)) { if (ctx.is_unit(lp)) add_edge(x, z, sat::null_literal); else if (ctx.is_unit(ln)) @@ -107,7 +125,9 @@ namespace sls { if (lit != sat::null_literal) lits.push_back(~lit); if (children.contains(parent)) { - ctx.add_clause(lits); + // only assert loop clauses for proper loops + if (parent == children[0]) + ctx.add_clause(lits); if (lit != sat::null_literal) lits.pop_back(); continue; @@ -144,17 +164,17 @@ namespace sls { if (dt.is_constructor(t)) { auto r = dt.get_constructor_recognizer(f); - axioms.push_back(m.mk_app(r, t)); + m_axioms.push_back(m.mk_app(r, t)); auto& acc = *dt.get_constructor_accessors(f); for (unsigned i = 0; i < ta->get_num_args(); ++i) { auto ti = ta->get_arg(i); - axioms.push_back(m.mk_eq(ti, m.mk_app(acc[i], t))); + m_axioms.push_back(m.mk_eq(ti, m.mk_app(acc[i], t))); } auto& cns = *dt.get_datatype_constructors(s); for (auto c : cns) { if (c != f) { auto r2 = dt.get_constructor_recognizer(c); - axioms.push_back(m.mk_not(m.mk_app(r2, t))); + m_axioms.push_back(m.mk_not(m.mk_app(r2, t))); } } continue; @@ -166,7 +186,7 @@ namespace sls { expr_ref_vector args(m); for (auto a : acc) args.push_back(m.mk_app(a, u)); - axioms.push_back(m.mk_implies(m.mk_app(r, u), m.mk_eq(u, m.mk_app(c, args)))); + m_axioms.push_back(m.mk_implies(m.mk_app(r, u), m.mk_eq(u, m.mk_app(c, args)))); } if (dt.is_datatype(s)) { @@ -176,18 +196,18 @@ namespace sls { auto r = dt.get_constructor_recognizer(c); ors.push_back(m.mk_app(r, t)); } - axioms.push_back(m.mk_or(ors)); + m_axioms.push_back(m.mk_or(ors)); for (unsigned i = 0; i < cns.size(); ++i) { auto r1 = dt.get_constructor_recognizer(cns[i]); for (unsigned j = i + 1; j < cns.size(); ++j) { auto r2 = dt.get_constructor_recognizer(cns[j]); - axioms.push_back(m.mk_or(m.mk_not(m.mk_app(r1, t)), m.mk_not(m.mk_app(r2, t)))); + m_axioms.push_back(m.mk_or(m.mk_not(m.mk_app(r1, t)), m.mk_not(m.mk_app(r2, t)))); } } for (auto c : cns) { if (c->get_arity() == 0) { auto r = dt.get_constructor_recognizer(c); - axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_const(c)))); + m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_const(c)))); } } @@ -203,19 +223,104 @@ namespace sls { collect_path_axioms(); } - expr_ref datatype_plugin::get_value(expr* e) { return expr_ref(m); } - void datatype_plugin::initialize() {} - void datatype_plugin::start_propagation() {} + void datatype_plugin::initialize() { + add_axioms(); + } + + expr_ref datatype_plugin::get_value(expr* e) { + if (!dt.is_datatype(e)) + return expr_ref(m); + init_values(); + return expr_ref(m_values.get(g->find(e)->get_root_id()), m); + } + + void datatype_plugin::init_values() { + if (!m_values.empty()) + return; + // retrieve e-graph from sls_euf_solver: add bridge in sls_context to share e-graph + SASSERT(g); + // build top_sort similar to dt_solver.cpp + top_sort deps; + for (auto* n : g->nodes()) + if (n->is_root()) + add_dep(n, deps); + + deps.topological_sort(); + expr_ref_vector args(m); + // walk topological sort in order of leaves to roots, attaching values to nodes. + for (euf::enode* n : deps.top_sorted()) { + SASSERT(n->is_root()); + unsigned id = n->get_id(); + if (m_values.get(id, nullptr)) + continue; + expr* e = n->get_expr(); + m_values.reserve(id + 1); + if (!dt.is_datatype(e)) + continue; + euf::enode* con = nullptr; + for (auto sib : euf::enode_class(n)) { + if (dt.is_constructor(sib->get_expr())) { + con = sib; + break; + } + } + if (con) { + auto f = con->get_decl(); + args.reset(); + for (auto arg : euf::enode_args(con)) { + if (dt.is_datatype(arg->get_sort())) + args.push_back(m_values.get(arg->get_root_id())); + else + args.push_back(ctx.get_value(arg->get_expr())); + } + m_values.setx(n->get_id(), m.mk_app(f, args)); + } + else { + NOT_IMPLEMENTED_YET(); + } + } + } + + void datatype_plugin::add_dep(euf::enode* n, top_sort& dep) { + if (!dt.is_datatype(n->get_expr())) + return; + euf::enode* con = nullptr; + for (auto sib : euf::enode_class(n)) { + if (dt.is_constructor(sib->get_expr())) { + con = sib; + break; + } + } + TRACE("dt", display(tout) << g->bpp(n) << " con: " << g->bpp(con) << "\n";); + if (!con) + dep.insert(n, nullptr); + else if (con->num_args() == 0) + dep.insert(n, nullptr); + for (euf::enode* arg : euf::enode_args(con)) + dep.add(n, arg->get_root()); + } + + + void datatype_plugin::start_propagation() { + m_values.reset(); + } + void datatype_plugin::propagate_literal(sat::literal lit) {} bool datatype_plugin::propagate() { return false; } bool datatype_plugin::is_sat() { return true; } void datatype_plugin::register_term(expr* e) {} std::ostream& datatype_plugin::display(std::ostream& out) const { + for (auto a : m_axioms) + out << mk_bounded_pp(a, m, 3) << "\n"; return out; } - void datatype_plugin::mk_model(model& mdl) {} + void datatype_plugin::mk_model(model& mdl) { + } - void datatype_plugin::collect_statistics(statistics& st) const {} + void datatype_plugin::collect_statistics(statistics& st) const { + st.update("sls-dt-axioms", m_axioms.size()); + } + void datatype_plugin::reset_statistics() {} } diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h index 71c8b6df7..61cc2b938 100644 --- a/src/ast/sls/sls_datatype_plugin.h +++ b/src/ast/sls/sls_datatype_plugin.h @@ -18,6 +18,7 @@ Author: #include "ast/sls/sls_context.h" #include "ast/datatype_decl_plugin.h" +#include "util/top_sort.h" namespace sls { @@ -30,10 +31,12 @@ namespace sls { expr* parent; sat::literal lit; }; + scoped_ptr& g; obj_map> m_dts; obj_map> m_parents; - + datatype_util dt; + expr_ref_vector m_axioms, m_values; stats m_stats; void collect_path_axioms(); @@ -41,6 +44,9 @@ namespace sls { void add_path_axioms(); void add_path_axioms(ptr_vector& children, sat::literal_vector& lits, svector const& parents); void add_axioms(); + + void init_values(); + void add_dep(euf::enode* n, top_sort& dep); public: datatype_plugin(context& c); diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h index d4dfe0f56..32d3849bd 100644 --- a/src/ast/sls/sls_euf_plugin.h +++ b/src/ast/sls/sls_euf_plugin.h @@ -87,6 +87,8 @@ namespace sls { void collect_statistics(statistics& st) const override; void reset_statistics() override; + + scoped_ptr& egraph() { return m_g; } }; }