mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 15:40:37 +00:00
Code Activity

euf_sgraph: make drop_left/drop_right depth-linear and simplify string classification (#9771)

Browse source 
ZIPT review identified two hot-path inefficiencies in `euf_sgraph`:
`drop_left`/`drop_right` were implemented as repeated single-token drops
(`O(count × depth)`), and `classify` performed redundant string checks.
This change aligns behavior with the intended tree-navigation approach
while keeping semantics unchanged.

- **Algorithmic update: `drop_left` / `drop_right`**
- Replaced iterative `drop_first`/`drop_last` loops with direct
recursion over concat children.
- New logic drops across subtree boundaries using child lengths,
reducing work to tree depth (`O(depth)`).

- **Classification cleanup: `classify`**
- Collapsed double `is_string` probing into a single `is_string(e, s)`
call.
- Preserves existing kind mapping (`empty` vs non-empty string constant
handling).

- **Focused test coverage extension**
- Added boundary checks in `test_sgraph_drop` for `drop_left(..., 1)`
and `drop_right(..., 1)` on a 4-token concat tree.

```cpp
snode* sgraph::drop_left(snode* n, unsigned count) {
    if (count == 0 || n->is_empty()) return n;
    if (count >= n->length()) return mk_empty_seq(n->get_sort());
    SASSERT(n->is_concat());
    unsigned left_len = n->arg(0)->length();
    if (count < left_len)
        return mk_concat(drop_left(n->arg(0), count), n->arg(1));
    return drop_left(n->arg(1), count - left_len);
}
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-06-10 14:46:03 +02:00 • committed by GitHub
parent 294ee984b8
commit 03a76c0309
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 26 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/test/euf_sgraph.cpp
View file

@ -564,11 +564,23 @@ static void test_sgraph_drop() {
SASSERT(cd2->length() == 2);
SASSERT(cd2->first() == c);
// drop_left(1): [A, B, C, D] => [B, C, D]
euf::snode* bcd2 = sg.drop_left(abcd, 1);
SASSERT(bcd2->length() == 3);
SASSERT(bcd2->first() == b);
SASSERT(bcd2->last() == d);
// drop_right(2): [A, B, C, D] => [A, B]
euf::snode* ab2 = sg.drop_right(abcd, 2);
SASSERT(ab2->length() == 2);
SASSERT(ab2->last() == b);
// drop_right(1): [A, B, C, D] => [A, B, C]
euf::snode* abc2 = sg.drop_right(abcd, 1);
SASSERT(abc2->length() == 3);
SASSERT(abc2->first() == a);
SASSERT(abc2->last() == c);
// drop all: [A, B, C, D] => empty
euf::snode* empty = sg.drop_left(abcd, 4);
SASSERT(empty->is_empty());