Repository navigation
Beta-eta reduction improvements - #1011
Merged
Merged
Conversation
…fix some bugs in BottomUpTermTransformer
Collaborator
|
Can you please explain a bit the changes in |
mezpusz
commented
Oct 7, 2026
mezpusz
commented
Oct 7, 2026
quickbeam123
reviewed
Oct 7, 2026
quickbeam123
reviewed
Oct 7, 2026
mezpusz
commented
Oct 7, 2026
Contributor
Author
|
I tried to comment inline the places where something not related to transforming sorts. |
…r term BottomUpTermTransformer::transform(TermList) now calls transformSubterm on the root itself, so the extra transformSubterm in transformTermList ran it a second time. That function is not a pure lookup: for a recursive term it allocates a Function and introduces a fresh symbol, and for the synthesis ITE symbol it builds a special $ite term, which the second pass then received. The repeat happened to be the identity on the cases traced, but only by luck. Co-Authored-By: Claude Opus 5.5 <[email protected]>
transform(TermList) now applies transformSubterm to the root, which is what
transformSpecial uses for ITE branches, the LET body and MATCH arguments. When
such a component is itself special (e.g. the inner $ite of
$ite(c, $ite(d, a, b), e), or a $formula{...} branch), transformSubterm
received a special term. The main loop of transform(Term*) never does that,
and subclasses are not written for it: InterpretedLiteralEvaluator would call
getEvaluator with a functor near UINT_MAX and expand its DArray to that size.
Short-circuit special terms to transformSpecial, as the main loop does.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
transform(Formula*) held a static BottomUpTermTransformerFormulaTransformer
built from *this. A static local is initialised once, so every later
BottomUpTermTransformer instance went on transforming its formulas (inside
$ite conditions, $let bindings, $formula{...}) through the first instance
that ever got there, which is a use-after-free once that instance is gone.
The adapter only holds a reference, so construct it per call, as
TermTransformer::transform(Formula*) already does.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
quickbeam123
approved these changes
Oct 7, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Apply some optimizations to beta-eta reductions:
BottomUpTermTransformerand avoids creating intermediate terms over and over again.BottomUpTermtransformer.TermShiftershifts free DB indices by an integer amount and gets the index of the minimal DB index at the same time, but the functionality is never used together. Factor out the latter part and simplify it.ToPlaceholderswhich is not going to be used anymore due to the UWA HOL unification implementation.I only used Claude to generate unit tests.
HOL TPTP Discount:
Only beta improvements:
master unsat: 2104 (0) sat: 1 (0) cputime: 10070.68 s instructions: 49939702 Mi memory: 196318.64 MB
branch unsat: 2111 (7) sat: 1 (0) cputime: 10092.84 s instructions: 49803051 Mi memory: 197046.09 MB
Beta-eta improvements:
master unsat: 2106 (0) sat: 1 (0) cputime: 10133.06 s instructions: 49911393 Mi memory: 200420.11 MB
branch unsat: 2118 (12) sat: 1 (0) cputime: 10167.87 s instructions: 49687596 Mi memory: 209745.55 MB
HOL TPTP Otter:
Only beta improvements:
master unsat: 2083 (0) sat: 1 (0) cputime: 10309.42 s instructions: 50375500 Mi memory: 246390.01 MB
branch unsat: 2087 (4) sat: 1 (0) cputime: 10336.92 s instructions: 50289588 Mi memory: 261380.23 MB
Beta-eta improvements:
master unsat: 2084 (0) sat: 1 (0) cputime: 10320.71 s instructions: 50342125 Mi memory: 251330.52 MB
branch unsat: 2091 (7) sat: 1 (0) cputime: 10336.29 s instructions: 50189498 Mi memory: 276181.34 MB
FOL TPTP has no regression change.