mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 06:16:09 +00:00
Code Activity

Remove regex_bisim m_node_of mapping

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-10 22:23:49 +00:00 • committed by GitHub
parent 513b81253b
commit 51b2a84ec8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_regex_bisim.cpp
View file

@ -34,7 +34,6 @@ namespace seq {
void regex_bisim::reset() { void regex_bisim::reset() {
m_uf.reset(); m_uf.reset();
m_node_of.reset();
m_pinned.reset(); m_pinned.reset();
m_worklist.reset(); m_worklist.reset();
m_steps = 0; m_steps = 0;
@ -45,13 +44,10 @@ namespace seq {
first encounter. first encounter.
*/ */
unsigned regex_bisim::node_of(expr* r) { unsigned regex_bisim::node_of(expr* r) {
unsigned id = 0; while (r->get_id() >= m_uf.get_num_vars())
if (m_node_of.find(r, id)) m_uf.mk_var();
return id;
id = m_uf.mk_var();
m_node_of.insert(r, id);
m_pinned.push_back(r); m_pinned.push_back(r);
return id; return r->get_id();
} }
/* /*

1
src/ast/rewriter/seq_regex_bisim.h
View file

@ -65,7 +65,6 @@ namespace seq {
seq_rewriter& m_rw; seq_rewriter& m_rw;
seq_util m_util; seq_util m_util;
basic_union_find m_uf; basic_union_find m_uf;
obj_map<expr, unsigned> m_node_of;
expr_ref_vector m_pinned; expr_ref_vector m_pinned;
expr_ref_vector m_worklist; expr_ref_vector m_worklist;
unsigned m_step_bound { 50000 }; unsigned m_step_bound { 50000 };