mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-12 20:05:36 +00:00
Code Activity

Address code review: fix const-correctness, improve child registration, add comments

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-01 20:25:18 +00:00
parent 2e17bb8767
commit e4f9a517e4
2 changed files with 26 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -142,6 +142,8 @@ namespace euf {
} }
case snode_kind::s_power: { case snode_kind::s_power: {
// s^n: nullable follows base, consistent with ZIPT's PowerToken
// the exponent n is assumed to be a symbolic integer, may or may not be zero
SASSERT(n->num_args() >= 1); SASSERT(n->num_args() >= 1);
snode* base = n->arg(0); snode* base = n->arg(0);
n->m_ground = base->is_ground(); n->m_ground = base->is_ground();
@ -278,14 +280,14 @@ namespace euf {
app* a = to_app(e); app* a = to_app(e);
unsigned arity = a->get_num_args(); unsigned arity = a->get_num_args();
// recursively register children that are sequences or regexes // recursively register children
// for seq/re children, create classified snodes
// for other children (e.g. integer exponents), create s_other snodes
snode_vector child_nodes; snode_vector child_nodes;
for (unsigned i = 0; i < arity; ++i) { for (unsigned i = 0; i < arity; ++i) {
expr* ch = a->get_arg(i); expr* ch = a->get_arg(i);
if (m_seq.is_seq(ch) || m_seq.is_re(ch)) { snode* cn = mk(ch);
snode* cn = mk(ch); child_nodes.push_back(cn);
child_nodes.push_back(cn);
}
} }
return mk_snode(e, k, child_nodes.size(), child_nodes.data()); return mk_snode(e, k, child_nodes.size(), child_nodes.data());

24
src/ast/euf/euf_snode.h
View file

@ -67,7 +67,7 @@ namespace euf {
unsigned m_level = 0; // tree depth/level (0 for empty, 1 for singletons) unsigned m_level = 0; // tree depth/level (0 for empty, 1 for singletons)
unsigned m_length = 0; // token count, number of leaf tokens in the tree unsigned m_length = 0; // token count, number of leaf tokens in the tree
snode* m_args[0]; snode* m_args[0]; // variable-length array, allocated via get_snode_size(num_args)
friend class sgraph; friend class sgraph;
@ -129,18 +129,32 @@ namespace euf {
} }
// analogous to ZIPT's Str.First / Str.Last // analogous to ZIPT's Str.First / Str.Last
snode* first() const { snode const* first() const {
snode const* s = this; snode const* s = this;
while (s->is_concat()) while (s->is_concat())
s = s->arg(0); s = s->arg(0);
return const_cast<snode*>(s); return s;
} }
snode* last() const { snode const* last() const {
snode const* s = this; snode const* s = this;
while (s->is_concat()) while (s->is_concat())
s = s->arg(1); s = s->arg(1);
return const_cast<snode*>(s); return s;
}
snode* first() {
snode* s = this;
while (s->is_concat())
s = s->arg(0);
return s;
}
snode* last() {
snode* s = this;
while (s->is_concat())
s = s->arg(1);
return s;
} }
}; };