Skip to content

Conversation

@unp1
Copy link
Member

@unp1 unp1 commented Jan 8, 2026

Intended Change

Possible alternative to one step simplifier.
This PR evaluates an option to bypass cost computation for specific rules.
Experimental. Maybe a possibility to adapt macros to work by replacing the rule app manager

Plan

  • Implement delegate rule app manager
  • Optimize behavior of delegate rule app manager
    • use different queues for concrete, simplify etc.
    • sort some queues (prefer higher positions for concrete or simplify) etc.
  • Code cleanup
  • Document the changes

Type of pull request

  • New feature (non-breaking change which adds functionality)
  • There are changes to the (Java) code

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I have tested the feature as follows: ...
  • I have checked that runtime performance has not deteriorated.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@unp1 unp1 force-pushed the notAlwaysCostBased branch from 6d78630 to 5e6d5f1 Compare January 8, 2026 13:48
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.

2 participants