From 180614330a4dc08b0a9143b159b248c4bd319d9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Oct 2024 20:33:53 -0700 Subject: [PATCH] Refactor context management, improve datatype handling, and enhance logging in sls plugins. --- src/ast/sls/sls_context.cpp | 8 ++++-- src/ast/sls/sls_context.h | 4 ++- src/ast/sls/sls_datatype_plugin.cpp | 40 ++++++++++++++++++----------- src/ast/sls/sls_datatype_plugin.h | 3 +++ src/ast/sls/sls_euf_plugin.cpp | 2 ++ 5 files changed, 39 insertions(+), 18 deletions(-) diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 590298e2a..9ec317c5c 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -72,14 +72,18 @@ namespace sls { verbose_stream() << "did not find plugin for " << fid << "\n"; } - scoped_ptr& context::ensure_euf() { + scoped_ptr& context::egraph() { + return euf().egraph(); + } + + euf_plugin& context::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(); + return *dynamic_cast(p); } void context::ensure_plugin(expr* e) { diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index 74eba4682..efff6da68 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -29,6 +29,7 @@ Author: namespace sls { class context; + class euf_plugin; class plugin { protected: @@ -196,7 +197,8 @@ 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(); + scoped_ptr& egraph(); + euf_plugin& 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 8d4216397..babe33169 100644 --- a/src/ast/sls/sls_datatype_plugin.cpp +++ b/src/ast/sls/sls_datatype_plugin.cpp @@ -62,19 +62,26 @@ Model-repair based: violated x != y: x <- fresh, y <- fresh violated x != t: x <- fresh, subterm y of t: y <- fresh - model::get_fresh_value(s) - model::get_some_value(s) + acc(x) = t: eval(x) = c(u, v) acc(c(u,v)) = u -> repair(u = t) + acc(x) = t: eval(x) does not match acc -> acc(x) + has a fixed interpretation, so repair over t instead, or update interpretation of x + + uses: + model::get_fresh_value(s) + model::get_some_value(s) --*/ #include "ast/sls/sls_datatype_plugin.h" +#include "ast/sls/sls_euf_plugin.h" #include "ast/ast_pp.h" namespace sls { datatype_plugin::datatype_plugin(context& c): plugin(c), - g(c.ensure_euf()), + euf(c.euf()), + g(c.egraph()), dt(m), m_axioms(m), m_values(m) { @@ -205,6 +212,10 @@ namespace sls { auto c = dt.get_recognizer_constructor(f); m_axioms.push_back(m.mk_iff(t, m.mk_app(dt.get_constructor_is(c), u))); } + + if (dt.is_update_field(t)) { + NOT_IMPLEMENTED_YET(); + } if (dt.is_datatype(s)) { auto& cns = *dt.get_datatype_constructors(s); @@ -309,13 +320,12 @@ namespace sls { // assign fresh values to uninterpeted nodes for (euf::enode* n : deps.top_sorted()) { SASSERT(n->is_root()); + expr* e = n->get_expr(); + if (!dt.is_datatype(e)) + continue; 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; auto con = get_constructor(n); if (con) continue; @@ -327,13 +337,10 @@ namespace sls { 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; - if (m_values.get(id, nullptr)) + if (m_values.get(id)) continue; euf::enode* con = get_constructor(n); if (!con) @@ -432,9 +439,10 @@ namespace sls { break; } } - verbose_stream() << "cycle\n"; - for (auto e : diseqs) - verbose_stream() << mk_pp(e, m) << "\n"; + IF_VERBOSE(1, + verbose_stream() << "cycle\n"; + for (auto e : diseqs) + verbose_stream() << mk_pp(e, m) << "\n";); ctx.add_constraint(m.mk_or(diseqs)); return true; } @@ -463,7 +471,9 @@ namespace sls { return out; } - void datatype_plugin::propagate_literal(sat::literal lit) {} + void datatype_plugin::propagate_literal(sat::literal lit) { + euf.propagate_literal(lit); + } bool datatype_plugin::is_sat() { return true; } void datatype_plugin::register_term(expr* e) {} diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h index 0399dd6e8..55b04e612 100644 --- a/src/ast/sls/sls_datatype_plugin.h +++ b/src/ast/sls/sls_datatype_plugin.h @@ -21,6 +21,8 @@ Author: #include "util/top_sort.h" namespace sls { + + class euf_plugin; class datatype_plugin : public plugin { struct stats { @@ -31,6 +33,7 @@ namespace sls { expr* parent; sat::literal lit; }; + euf_plugin& euf; scoped_ptr& g; obj_map> m_dts; obj_map> m_parents; diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index 0fe0d8670..f4393bd01 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -216,6 +216,7 @@ namespace sls { return; auto block = [&](euf::enode* a, euf::enode* b) { + TRACE("euf", tout << "block " << m_g->bpp(a) << " != " << m_g->bpp(b) << "\n"); if (a->get_root() != b->get_root()) return; ptr_vector explain; @@ -281,6 +282,7 @@ namespace sls { // merge all equalities // check for conflict with disequalities during propagation if (merge_eqs) { + TRACE("euf", tout << "root literals " << ctx.root_literals() << "\n"); for (auto lit : ctx.root_literals()) { if (!ctx.is_true(lit)) lit.neg();