mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

put ensure concat on a list

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 13:44:59 -08:00
parent 477db7d8bd
commit 01c5a09575
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/euf/euf_bv_plugin.cpp
View file

@ -205,7 +205,9 @@ namespace euf {
enode* arg_r = arg->get_root(); enode* arg_r = arg->get_root();
enode* n_r = n->get_root(); enode* n_r = n->get_root();
m_ensure_concat.reset();
auto ensure_concat = [&](unsigned lo, unsigned mid, unsigned hi) { auto ensure_concat = [&](unsigned lo, unsigned mid, unsigned hi) {
// verbose_stream() << lo << " " << mid << " " << hi << "\n";
TRACE("bv", tout << "ensure-concat " << lo << " " << mid << " " << hi << "\n"); TRACE("bv", tout << "ensure-concat " << lo << " " << mid << " " << hi << "\n");
unsigned lo_, hi_; unsigned lo_, hi_;
for (enode* p1 : enode_parents(n)) for (enode* p1 : enode_parents(n))
@ -219,14 +221,14 @@ namespace euf {
TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n"); TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n");
for (enode* sib : enode_class(b)) for (enode* sib : enode_class(b))
if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2) if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2)
ensure_concat(lo1, hi1, hi2); m_ensure_concat.push_back({lo1, hi1, hi2});
}; };
auto propagate_below = [&](enode* a) { auto propagate_below = [&](enode* a) {
TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n"); TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n");
for (enode* sib : enode_class(a)) for (enode* sib : enode_class(a))
if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1) if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1)
ensure_concat(lo2, hi2, hi1); m_ensure_concat.push_back({lo2, hi2, hi1});
}; };
for (enode* p : enode_parents(n)) { for (enode* p : enode_parents(n)) {
@ -237,6 +239,10 @@ namespace euf {
propagate_above(a); propagate_above(a);
} }
} }
for (auto [lo, mid, hi] : m_ensure_concat)
ensure_concat(lo, mid, hi);
} }
class bv_plugin::undo_split : public trail { class bv_plugin::undo_split : public trail {

1
src/ast/euf/euf_bv_plugin.h
View file

@ -72,6 +72,7 @@ namespace euf {
bool unfold_width(enode* x, enode_vector& xs, enode* y, enode_vector& ys); bool unfold_width(enode* x, enode_vector& xs, enode* y, enode_vector& ys);
bool unfold_sub(enode* x, enode_vector& xs); bool unfold_sub(enode* x, enode_vector& xs);
void merge(enode_vector& xs, enode_vector& ys, justification j); void merge(enode_vector& xs, enode_vector& ys, justification j);
svector<std::tuple<unsigned, unsigned, unsigned>> m_ensure_concat;
void propagate_extract(enode* n); void propagate_extract(enode* n);
void propagate_values(enode* n); void propagate_values(enode* n);