Repository navigation
Eliminate hacky UnitInputTypes - #1057
Merged
Merged
Conversation
The Vampire-only TPTP role "extensionality" gave a unit the input type EXTENSIONALITY_AXIOM, which the Clause constructor turned into _extensionalityTag (resetting the type to AXIOM). The tag was read only under -er tagged, which no schedule or sampler uses, and nothing in checks/ or UnitTests/ exercised it beyond printing the role. It was also fragile: children do not inherit the tag, so any rewrite of the clause before activation dropped it. And a fof formula with the role looked like a goal to everything testing == AXIOM or derivedFromGoal() until clausification (SInE seed, Property goal count), and beat a real goal premise in the max of input types. Remove the role from the TPTP parser (it is now a parse error), the input type (MODEL_DEFINITION becomes 5), the -er value tagged (OFF becomes 2), the Clause bit (donated to _numSelected, now 25 bits) and the corresponding printing code. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
MODEL_DEFINITION was not a TPTP role but a marker for the section between vampire(model_check,model_start) and vampire(model_check,model_end), read only by FMB/ModelCheck. As an input type it caused trouble: - Statistics::inputTypeCnts excluded it (sized toNumber(MODEL_DEFINITION)), but Statistics::reportUnit, called from every Unit constructor, indexes the array by the input type of each input unit. So every model definition unit wrote one StatPair past the end of the array, in every mode; UBSan does not see it through std::array::operator[]. - Outside --mode model_check, model units were the top of the max of input types and counted as derivedFromGoal(); in a debug build they tripped ASS_LE(type, CLAIM) in SaturationAlgorithm::addInputClause. Now the TPTP parser records the model units in a side set, like it records unit names, and ModelCheck asks TPTP::isModelDefinition(). Model units get type AXIOM; their stated role is ignored as before. modelCheckMode rejects --input_syntax smtlib2, since only the TPTP parser records model units. Statistics counts input types up to CLAIM, and the assertion in addInputClause, now vacuous, is removed. Reproducer for the out-of-bounds write: any TPTP file containing vampire(model_check,model_start). ... vampire(model_check,model_end). For the assertion, the same file in the default mode with a debug build: script -q /dev/null ./vampire file.p Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CLAIM was set only by the Vampire-only TPTP role claim, and only for the parser to know to call processClaimFormula. The claim machinery itself (ConsequenceFinder, LiteralSelector, Ordering) reads the label flag of the introduced predicate, never the input type. Being the top value of the enum, CLAIM merely made claims count as derivedFromGoal() and come first in ClauseQueue::tieLessThan and Normalisation::lessThan, while the SMT-LIB assert-claim, documented as analogous, used ASSUMPTION. The TPTP parser now records a claim in a flag, like a question, and gives it the input type AXIOM. The SMT-LIB parser is unchanged; the discrepancy between the two is left for later. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
MichaelRawson
approved these changes
Nov 11, 2026
MichaelRawson
left a comment
MichaelRawson
left a comment
Contributor
There was a problem hiding this comment.
Nice! This slowly reduces the insanity. :)
| /** Used in parsing and preprocessing for extensionality clause tagging, should not appear in proof search */ | ||
| EXTENSIONALITY_AXIOM = 5, | ||
| /** Used to separate model definitions in model_check mode, should not appear in proof search */ | ||
| MODEL_DEFINITION = 6 |
Contributor
There was a problem hiding this comment.
We can now save a bit with the `_inputType : 3' bitfield later in the file.
Collaborator
Author
There was a problem hiding this comment.
Great pick!
(Induction depth will be happy ;))
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
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.
CLAIM,MODEL_DEFINITION, andEXTENSIONALITY_AXIOMare eliminated fromUnitInputTypewhile preserving most of the functionality:CLAIMis treated as before, only spelled out "axiom" in proof outputUnitInputTypebut a map kept in the TPTP parser