Definitional Skolem constants - #3960
Merged
Merged
Conversation
unp1
force-pushed
the
bubel/definitional-skolems-on-main
branch
from
August 13, 2026 21:28
74e21a5 to
1175707
Compare
…on time from the constant itself Make definitional Skolem constants aware of their introduction time (removes need for caches) and formalizes the notion of definitional formerly known as small constants. Definitional Skolem constants are smaller then most terms in termordering. A PR with a rework of term orderings is coming "A skolem constant was created while a taclet application was instantiated, so its name and its introduction time depended on when the strategy considered the application, not on when the proof used it, and the introduction time had to be remembered in a cache of its own. The constant now carries its kind and the number of rule applications the goal had performed when it was created, and the goal creates the constants when it applies the rule. The function kind also distinguishes the constants a definition introduces, which the term ordering can then place below the term they name." (created with AI tooling support)
unp1
force-pushed
the
bubel/definitional-skolems-on-main
branch
from
August 14, 2026 12:12
1175707 to
ad575b7
Compare
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.
As mentioned at the devloper meeting. This is the first PR of three cleaning up the AI supported work.
Make definitional Skolem constants aware of their introduction time (removes need for caches) and
formalizes the notion of definitional formerly known as small constants. Definitional Skolem constants
are smaller then most terms in termordering.
Speeds up Skolem heavy proof by up to 10% bet, 5% on the whole runAllFunProof collection.
Type of pull request
Ensuring quality
Additional information and contact(s)
Created with AI tooling support
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.