mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 03:53:10 +00:00
Code Activity

Change ownership: sgraph owns egraph with seq_plugin, add assoc hash table, add unit tests

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-01 23:23:12 +00:00
parent 12b7a4dae3
commit 5c14edf030
7 changed files with 391 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/euf/euf_seq_plugin.cpp
View file

@ -21,15 +21,16 @@ Author:
--*/
#include "ast/euf/euf_seq_plugin.h"
#include "ast/euf/euf_sgraph.h"
#include "ast/euf/euf_egraph.h"
#include "ast/ast_pp.h"
namespace euf {
seq_plugin::seq_plugin(egraph& g):
seq_plugin::seq_plugin(egraph& g, sgraph& sg):
plugin(g),
m_seq(g.get_manager()),
m_sg(g.get_manager()) {
m_sg(sg) {
}
void seq_plugin::register_node(enode* n) {
@ -232,25 +233,15 @@ namespace euf {
if (m_qhead > m_queue.size())
m_qhead = m_queue.size();
break;
case undo_kind::undo_push_scope:
m_sg.pop(1);
break;
}
}
void seq_plugin::push_scope_eh() {
m_sg.push();
m_undo.push_back(undo_kind::undo_push_scope);
push_plugin_undo(get_id());
}
std::ostream& seq_plugin::display(std::ostream& out) const {
out << "seq\n";
m_sg.display(out);
out << "seq-plugin\n";
return out;
}
void seq_plugin::collect_statistics(statistics& st) const {
m_sg.collect_statistics(st);
// statistics are collected by sgraph which owns us
}
}

9
src/ast/euf/euf_seq_plugin.h
View file

@ -40,21 +40,20 @@ Author:
#include "ast/seq_decl_plugin.h"
#include "ast/euf/euf_plugin.h"
#include "ast/euf/euf_sgraph.h"
namespace euf {
class egraph;
class sgraph;
class seq_plugin : public plugin {
enum class undo_kind {
undo_add_concat,
undo_push_scope
};
seq_util m_seq;
sgraph m_sg;
sgraph& m_sg;
svector<undo_kind> m_undo;
// queue of merges and registrations to process
@ -101,7 +100,7 @@ namespace euf {
bool same_loop_body(enode* a, enode* b, unsigned& lo1, unsigned& hi1, unsigned& lo2, unsigned& hi2);
public:
seq_plugin(egraph& g);
seq_plugin(egraph& g, sgraph& sg);
theory_id get_id() const override { return m_seq.get_family_id(); }
@ -115,8 +114,6 @@ namespace euf {
void undo() override;
void push_scope_eh() override;
std::ostream& display(std::ostream& out) const override;
void collect_statistics(statistics& st) const override;

75
src/ast/euf/euf_sgraph.cpp
View file

@ -17,15 +17,58 @@ Author:
--*/
#include "ast/euf/euf_sgraph.h"
#include "ast/euf/euf_seq_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
namespace euf {
// Associativity-respecting hash: flattens concat into leaf sequence
// concat(concat(a, b), c) and concat(a, concat(b, c)) hash identically
static void collect_leaves(snode const* n, ptr_vector<snode const>& leaves) {
if (n->is_concat()) {
collect_leaves(n->arg(0), leaves);
collect_leaves(n->arg(1), leaves);
}
else {
leaves.push_back(n);
}
}
unsigned concat_hash::operator()(snode const* n) const {
if (!n->is_concat())
return n->id();
ptr_vector<snode const> leaves;
collect_leaves(n, leaves);
unsigned h = 0;
for (snode const* l : leaves)
h = combine_hash(h, l->id());
return h;
}
bool concat_eq::operator()(snode const* a, snode const* b) const {
if (a == b) return true;
if (!a->is_concat() && !b->is_concat())
return a->id() == b->id();
ptr_vector<snode const> la, lb;
collect_leaves(a, la);
collect_leaves(b, lb);
if (la.size() != lb.size())
return false;
for (unsigned i = 0; i < la.size(); ++i)
if (la[i]->id() != lb[i]->id())
return false;
return true;
}
sgraph::sgraph(ast_manager& m):
m(m),
m_seq(m),
m_egraph(m),
m_exprs(m) {
// create seq_plugin and register it with the egraph
// the seq_plugin gets a reference back to this sgraph
m_egraph.add_plugin(alloc(seq_plugin, m_egraph, *this));
}
sgraph::~sgraph() {
@ -263,6 +306,9 @@ namespace euf {
m_expr2snode.reserve(eid + 1, nullptr);
m_expr2snode[eid] = n;
}
// insert concats into the associativity-respecting hash table
if (k == snode_kind::s_concat)
m_concat_table.insert(n);
++m_stats.m_num_nodes;
return n;
}
@ -303,6 +349,16 @@ namespace euf {
return nullptr;
}
snode* sgraph::find_assoc_equal(snode* n) const {
if (!n || !n->is_concat())
return nullptr;
snode* existing = nullptr;
if (m_concat_table.find(n, existing) && existing != n) {
return existing;
}
return nullptr;
}
snode* sgraph::mk_empty(sort* s) {
expr_ref e(m_seq.str.mk_empty(s), m);
return mk(e);
@ -328,9 +384,23 @@ namespace euf {
return mk_snode(e, snode_kind::s_power, 2, args);
}
enode* sgraph::mk_enode(expr* e) {
enode* n = m_egraph.find(e);
if (n) return n;
enode_vector args;
if (is_app(e)) {
for (expr* arg : *to_app(e)) {
enode* a = mk_enode(arg);
args.push_back(a);
}
}
return m_egraph.mk(e, 0, args.size(), args.data());
}
void sgraph::push() {
m_scopes.push_back(m_nodes.size());
++m_num_scopes;
m_egraph.push();
}
void sgraph::pop(unsigned num_scopes) {
@ -341,6 +411,8 @@ namespace euf {
unsigned old_sz = m_scopes[new_lvl];
for (unsigned i = m_nodes.size(); i-- > old_sz; ) {
snode* n = m_nodes[i];
if (n->is_concat())
m_concat_table.remove(n);
if (n->get_expr()) {
unsigned eid = n->get_expr()->get_id();
if (eid < m_expr2snode.size())
@ -351,6 +423,7 @@ namespace euf {
m_exprs.shrink(old_sz);
m_scopes.shrink(new_lvl);
m_num_scopes = new_lvl;
m_egraph.pop(num_scopes);
}
std::ostream& sgraph::display(std::ostream& out) const {
@ -403,6 +476,8 @@ namespace euf {
st.update("seq-graph-nodes", m_stats.m_num_nodes);
st.update("seq-graph-concat", m_stats.m_num_concat);
st.update("seq-graph-power", m_stats.m_num_power);
st.update("seq-graph-hash-hits", m_stats.m_num_hash_hits);
m_egraph.collect_statistics(st);
}
}

30
src/ast/euf/euf_sgraph.h
View file

@ -69,24 +69,43 @@ Author:
#include "util/region.h"
#include "util/statistics.h"
#include "util/hashtable.h"
#include "ast/ast.h"
#include "ast/seq_decl_plugin.h"
#include "ast/euf/euf_snode.h"
#include "ast/euf/euf_egraph.h"
namespace euf {
class seq_plugin;
// Associativity-respecting hash for concatenations.
// The hash function flattens concat trees so that
// concat(concat(a, b), c) and concat(a, concat(b, c))
// hash to the same value. This is how ZIPT ensures
// finding equal concatenations efficiently.
struct concat_hash {
unsigned operator()(snode const* n) const;
};
struct concat_eq {
bool operator()(snode const* a, snode const* b) const;
};
class sgraph {
struct stats {
unsigned m_num_nodes;
unsigned m_num_concat;
unsigned m_num_power;
unsigned m_num_hash_hits;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
ast_manager& m;
seq_util m_seq;
egraph m_egraph;
region m_region;
snode_vector m_nodes;
expr_ref_vector m_exprs; // pin expressions
@ -97,6 +116,9 @@ namespace euf {
// maps expression id to snode
ptr_vector<snode> m_expr2snode;
// hash table for finding equal concatenations modulo associativity
hashtable<snode*, concat_hash, concat_eq> m_concat_table;
snode* mk_snode(expr* e, snode_kind k, unsigned num_args, snode* const* args);
snode_kind classify(expr* e) const;
void compute_metadata(snode* n);
@ -107,6 +129,8 @@ namespace euf {
ast_manager& get_manager() const { return m; }
seq_util& get_seq_util() { return m_seq; }
egraph& get_egraph() { return m_egraph; }
egraph const& get_egraph() const { return m_egraph; }
// register an expression and return its snode
snode* mk(expr* e);
@ -114,11 +138,17 @@ namespace euf {
// lookup an already-registered expression
snode* find(expr* e) const;
// find an existing concat that is equal modulo associativity
snode* find_assoc_equal(snode* n) const;
// build compound snodes
snode* mk_empty(sort* s);
snode* mk_concat(snode* a, snode* b);
snode* mk_power(snode* base, snode* exp);
// register expression in both sgraph and egraph
enode* mk_enode(expr* e);
// scope management for backtracking
void push();
void pop(unsigned num_scopes);