From ad07e0e18d9806c4461beac7670faf4431727af7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Dec 2023 10:27:54 -0800 Subject: [PATCH] add sub and super-slice functionality directory to euf-bv-plugin --- src/ast/euf/euf_bv_plugin.cpp | 134 ++++++++++++++++++++++++++++++++++ src/ast/euf/euf_bv_plugin.h | 13 ++++ 2 files changed, 147 insertions(+) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index f640b3ed074..89b5ade160a 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -352,6 +352,140 @@ namespace euf { push_merge(mk_concat(lo, hi), n); } + void bv_plugin::sub_slices(enode* n, std::function& consumer) { + m_todo.push_back({ n, 0 }); + unsigned lo, hi; + expr* e; + + for (unsigned i = 0; i < m_todo.size(); ++i) { + auto [n, offset] = m_todo[i]; + m_offsets.reserve(n->get_root_id() + 1); + auto& offsets = m_offsets[n->get_root_id()]; + if (offsets.contains(offset)) + continue; + offsets.push_back(offset); + if (!consumer(n, offset)) + continue; + for (auto sib : euf::enode_class(n)) { + if (bv.is_concat(sib->get_expr())) { + unsigned delta = 0; + for (unsigned j = sib->num_args(); j-- > 0; ) { + auto arg = sib->get_arg(j); + m_todo.push_back({ arg, offset + delta }); + delta += width(arg); + } + } + } + for (auto p : euf::enode_parents(n->get_root())) { + if (bv.is_extract(p->get_expr(), lo, hi, e)) { + SASSERT(g.find(e)->get_root() == n->get_root()); + m_todo.push_back({ p, offset + lo }); + } + } + } + clear_offsets(); + } + + void bv_plugin::super_slices(enode* n, std::function& consumer) { + m_todo.push_back({ n, 0 }); + unsigned lo, hi; + expr* e; + + for (unsigned i = 0; i < m_todo.size(); ++i) { + auto [n, offset] = m_todo[i]; + m_offsets.reserve(n->get_root_id() + 1); + auto& offsets = m_offsets[n->get_root_id()]; + if (offsets.contains(offset)) + continue; + offsets.push_back(offset); + if (!consumer(n, offset)) + continue; + for (auto sib : euf::enode_class(n)) { + if (bv.is_extract(sib->get_expr(), lo, hi, e)) { + auto child = g.find(e); + m_todo.push_back({ child, offset + lo }); + } + } + for (auto p : euf::enode_parents(n->get_root())) { + if (bv.is_concat(p->get_expr())) { + unsigned delta = 0; + for (unsigned j = p->num_args(); j-- > 0; ) { + auto arg = p->get_arg(j); + if (arg->get_root() == n->get_root()) + m_todo.push_back({ p, offset + delta }); + delta += width(arg); + } + } + } + } + clear_offsets(); + } + + // + // Explain that a is a subslice of b at offset + // or that b is a subslice of a at offset + // + void bv_plugin::explain_slice(enode* a, unsigned offset, enode* b, std::function& consumer) { + if (width(a) < width(b)) + std::swap(a, b); + SASSERT(width(a) >= width(b)); + svector> just; + m_jtodo.push_back({ a, 0, UINT_MAX }); + unsigned lo, hi; + expr* e; + + for (unsigned i = 0; i < m_jtodo.size(); ++i) { + auto [n, offs, j] = m_jtodo[i]; + m_offsets.reserve(n->get_root_id() + 1); + auto& offsets = m_offsets[n->get_root_id()]; + if (offsets.contains(offs)) + continue; + offsets.push_back(offs); + if (n->get_root() == b->get_root() && offs == offset) { + while (j != UINT_MAX) { + auto [x, y, j2] = just[j]; + consumer(x, y); + j = j2; + } + for (auto const& [n, offset, j] : m_jtodo) { + m_offsets.reserve(n->get_root_id() + 1); + m_offsets[n->get_root_id()].reset(); + } + m_jtodo.reset(); + return; + } + for (auto sib : euf::enode_class(n)) { + if (bv.is_concat(sib->get_expr())) { + unsigned delta = 0; + unsigned j2 = just.size(); + just.push_back({ n, sib, j }); + for (unsigned j = sib->num_args(); j-- > 0; ) { + auto arg = sib->get_arg(j); + m_jtodo.push_back({ arg, offset + delta, j2 }); + delta += width(arg); + } + } + } + for (auto p : euf::enode_parents(n->get_root())) { + if (bv.is_extract(p->get_expr(), lo, hi, e)) { + SASSERT(g.find(e)->get_root() == n->get_root()); + unsigned j2 = just.size(); + just.push_back({ g.find(e), n, j}); + m_jtodo.push_back({ p, offset + lo, j2}); + } + } + } + UNREACHABLE(); + } + + void bv_plugin::clear_offsets() { + for (auto const& [n, offset] : m_todo) { + m_offsets.reserve(n->get_root_id() + 1); + m_offsets[n->get_root_id()].reset(); + } + m_todo.reset(); + } + std::ostream& bv_plugin::display(std::ostream& out) const { out << "bv\n"; for (auto const& i : m_info) diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h index b8d62051e29..199aed4e787 100644 --- a/src/ast/euf/euf_bv_plugin.h +++ b/src/ast/euf/euf_bv_plugin.h @@ -41,6 +41,8 @@ namespace euf { bv_util bv; slice_info_vector m_info; // indexed by enode::get_id() + + enode_vector m_xs, m_ys; bool is_concat(enode* n) const { return bv.is_concat(n->get_expr()); } @@ -74,6 +76,11 @@ namespace euf { void propagate_extract(enode* n); void propagate_values(enode* n); + vector m_offsets; + svector> m_todo; + svector> m_jtodo; + void clear_offsets(); + enode_vector m_undo_split; void push_undo_split(enode* n); @@ -95,6 +102,12 @@ namespace euf { void undo() override; std::ostream& display(std::ostream& out) const override; + + void sub_slices(enode* n, std::function& consumer); + + void super_slices(enode* n, std::function& consumer); + + void explain_slice(enode* a, unsigned offset, enode* b, std::function& consumer); }; }