Skip to content

Conversation

@kroening
Copy link
Collaborator

@kroening kroening commented Jan 18, 2026

  • Adds const_post_depth_iteratort for post-order depth-first traversal of expressions
  • Adds const_post_depth_iterator_range_adaptert and post_traversal() function for range-based for loops

This complements the existing pre-order pre_traversal() from #8819

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

🤖 Generated with Claude Code

@kroening kroening changed the title post_traversal range for expressions post-order traversal range for expressions Jan 18, 2026
This adds a post-order depth-first-search iterator (const_post_depth_iteratort)
that visits children before their parent nodes. This complements the existing
pre-order iterator (const_depth_iteratort) where parents are visited first.

For an expression like (a + (b * c)), post-order visits: a, b, c, *, +

Includes a range adapter (post_traversal) for convenient use in range-based
for loops, matching the style of the existing pre_traversal function.

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@kroening kroening force-pushed the post_depth_iterator branch from 345b51d to 199d931 Compare January 18, 2026 01:13
@codecov
Copy link

codecov bot commented Jan 18, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.00%. Comparing base (35fbe06) to head (199d931).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8822   +/-   ##
========================================
  Coverage    80.00%   80.00%           
========================================
  Files         1700     1700           
  Lines       188285   188332   +47     
  Branches        73       73           
========================================
+ Hits        150632   150679   +47     
  Misses       37653    37653           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@tautschnig tautschnig merged commit 844c8e6 into develop Jan 18, 2026
41 of 42 checks passed
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.

3 participants