Skip to content

euf_seq_plugin: root-canonical simplification fixes + loop bound overflow guard#9744

Draft
Copilot wants to merge 3 commits into
c3from
copilot/copilotfix-euf-snode-support
Draft

euf_seq_plugin: root-canonical simplification fixes + loop bound overflow guard#9744
Copilot wants to merge 3 commits into
c3from
copilot/copilotfix-euf-snode-support

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented Jun 6, 2026

euf_seq_plugin was applying several regex concat simplifications against raw child enodes instead of canonical e-graph roots, so rules could silently miss after merges. It also merged loop bounds with unchecked unsigned addition, allowing overflowed bounds.

  • Root-canonical checks in simplification rules

    • Use get_root() for nullable/full-seq absorption checks.
    • Update same_star_body to test is_star on roots and compare rooted star bodies.
    • Evaluate extended star rules (v*.v*.c / c.v*.v*) against concat roots, not syntactic children.
  • Safe loop merge arithmetic

    • Gate loop merging on overflow-safe bound addition checks before constructing merged re.loop.
  • Re-simplify concats affected by child merges

    • In propagate_merge, re-run propagate_simplify for tracked concat nodes whose left/right child root is in the merged class, not only concats in the class itself.
  • Regression coverage in src/test/euf_seq_plugin.cpp

    • Added focused tests for:
      • star merge firing after child-to-star merge,
      • extended star rule using root concat shape,
      • nullable absorption via merged roots,
      • loop-merge non-application on overflow.
// before: structural check on non-canonical enode
if (is_concat(b, b1, b2) && same_star_body(a, b1))

// after: structural check on canonical representative
if (is_concat(b->get_root(), b1, b2) && same_star_body(a, b1))

Copilot AI changed the title [WIP] Fix correctness and robustness issues in euf_seq_plugin euf_seq_plugin: root-canonical simplification fixes + loop bound overflow guard Jun 6, 2026
Copilot AI requested a review from NikolajBjorner June 6, 2026 19:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[zipt-review] ZIPT Code Review: 5 correctness/robustness fixes for euf_seq_plugin

2 participants