coroutines for clause generation - #920
Open
quickbeam123 wants to merge 4 commits into
Open
Conversation
It was a function-level static, so every Factoring inference in the process shared one substitution. That only works because the iterator chain is consumed strictly one element at a time -- the same fragile contract as the `static AbstractingUnifier` in EqualityResolution. It also survives across Problems in the same process, which is the hazard CLAUDE.md warns about under "static members that hold per-problem state". Making it an ordinary member is cheap: DHMap's default constructor allocates nothing (_entries(0), _capacity(0)) and grows lazily, so constructing a RobSubstitution is a handful of field initialisations. The cost that does appear is the destructor freeing whatever the maps grew, once per generateClauses call, which the static previously amortised away. The chain passed its iterators as lvalues, which used to be free but would now copy the substitution twice; they become moves, matching Superposition. Split out from the coroutine rewrite so this cost can be measured on its own. ctest 100/100 and checks/sanity pass on the debug + UBSan build; no performance measurement -- that is for the server. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Generating inference rules state "iterate over every opportunity for this rule, build a clause from each" as a chain of IterTraits combinators, with the core function buried in the middle of it. Superposition was the worst case in the tree: two chains, each flatMap -> flatMap -> map, with an explicit pair<pair<Literal*, TypedTermList>, QueryRes<AbstractingUnifier*, TermLiteralClause>> spelled out in a lambda parameter list, then concatIters + NonzeroFn. What the rule actually does -- three nested loops, forwards and backwards -- was not visible. Add Lib/Generator.hpp: a move-only Generator<T> produced by a coroutine, satisfying the duck-typed iterator protocol (DECL_ELEMENT_TYPE plus hasNext/next) so it drops into pvi(), iterTraits() and TIME_TRACE_ITER like any other iterator. Nothing runs until the first hasNext(); frames go through Lib::alloc; an exception thrown by the body is stashed and rethrown on the consumer's stack rather than escaping a half-unwound frame. Superposition::generateClauses becomes a one-line wrapper over a private coroutine of three nested for loops -- ~55 lines of chain down to ~25 lines of loops, and the nested-pair type is gone entirely. The lifetime constraint that made this look risky is respected for free. QueryRes::unifier is a raw pointer to an AbstractingUnifier owned by the still-live substitution-tree iterator, undone by backtracking as soon as that iterator advances. performSuperposition runs *before* the co_yield and the query loop only advances *after* the resume, which is exactly the ordering .map(performSuperposition) gave. The rule is now written down in a comment: never carry a QueryRes across a co_yield. For the same reason the TIME_TRACE scope stays outside the coroutine -- TimeTrace keeps a stack of open scopes, so one left open across a suspension would be charged for the consumer's work, adopt the consumer's scopes as children, and break the LIFO discipline when the frame is destroyed. One behavioural change, in the safe direction: FlatteningIterator's constructor is eager, so building the old chain already fired the first index query of both directions. The coroutine keeps only one tree iterator alive at a time. Indices are frozen during activation, so this cannot change results. Verification. ctest 100/100, including 11 new tGenerator cases -- among them that destroying a partially consumed generator runs its frame locals' destructors (what releases and backtracks the tree iterators), and the LookaheadLiteralSelector::pickTheBest pattern of several generators advanced round-robin then abandoned. checks/sanity passes on a debug + UBSan build, so the ASS_EQ(_iterCnt, 0) index guards hold. Output is byte-identical to the parent commit across 1503 problem runs in six configurations: discount, otter, --unification_with_abstraction all, higher-order/THF (covering Superposition<true>), and --selection 11 / 1011. Performance is NOT measured: this laptop's run-to-run variance on the same binary is ~8%, an order of magnitude above the effect size. To be measured on the server. GCC and Cygwin builds likewise still to be confirmed in CI -- this is the first use of coroutines in the codebase. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Second use of Lib::Generator, after Superposition. Factoring's chain was short -- getCombinationIterator -> getMappingIterator -> getFilteredIterator -- but it needed a ~75-line ResultsFn class whose only reason to exist was to carry the loop-local state (_cl, _cLen, _afterCheck, _sel, _ord, and the substitution) from generateClauses into the map. The class is gone; those are now ordinary locals of the coroutine, and the substitution introduced in the previous commit is a plain stack variable. getCombinationIterator(0, numSelected, length) is exactly for fst in [0, numSelected) for snd in (fst, length) so the pair enumeration is now written as the two loops it always was, and "return nullptr" becomes "continue". Two things worth noting for review: - the l1->isEquality() and isNegativeForSelection(l1) guards are hoisted to the outer loop, since they depend only on the first literal. Both are pure (isNegativeForSelection is const and just negates isPositiveForSelection) and both previously rejected every pair sharing that l1, so the generated clauses and their order are unchanged -- only redundant calls are saved. - the aftercheck's "return nullptr" becomes break-then-continue, so inferencesBlockedDueToOrderingAftercheck is still bumped exactly once per blocked factor. The RStack scratch buffer is scoped so it is released before the co_yield rather than being held across the suspension. ctest 100/100 (including the 8 Inferences_Factoring cases) and checks/sanity pass on the debug + UBSan build. No performance measurement and no TPTP sweep -- both are for the server. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Third use of Lib::Generator. GenIteratorIterator was a hand-written continuation: an int stage, a bool prepared, a goto start, a stashed VirtualIterator nextIt, and a nested TermUnificationRetriever functor -- a little over 100 lines whose entire job was remembering which of four stages it was in. It also yielded iterators, which getGeneraingInferenceIterator then had to flatten. The coroutine is the four stages written out as four sequential if blocks yielding directly, so the flattening goes away too. Beyond readability this fixes a latent lifetime smell. The index handles were locals of hasNext(), destroyed at the end of their case block, while the iterator queried from that index lived on in nextIt -- sound only because IndexManager keeps the index alive independently. As frame locals the shared_ptrs now live exactly as long as the queries walking into them. pickTheBest is untouched: getGeneraingInferenceIterator still returns VirtualIterator<std::tuple<>>, now as pvi over the coroutine. That matters, because pickTheBest is the one place in Vampire that holds several of these iterators open at once, advances them round-robin, and abandons them all when the first runs dry -- the exact pattern tGenerator's round_robin_then_abandon case pins down. Only the number of elements matters here (substitutions are not retrieved), and the stage order and per-stage counts are unchanged. Verification: ctest 100/100 and checks/sanity pass on the debug + UBSan build, and the selector runs clean under both --selection 11 and 1011 on a few problems. Output matches the parent of this branch on 12 sampled problems under both selections, bounded by --activation_limit with a time limit generous enough never to bite, and with the Version line filtered. Twelve problems is a smoke test, not a sweep; the real sweep and all timing belong on the server. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
🤯 |
| // route the coroutine frame through Vampire's allocator; the compiler prefers the | ||
| // sized deallocation function, which is the one Lib::free needs | ||
| void *operator new(size_t size) { return Lib::alloc(size); } | ||
| void operator delete(void *ptr, size_t size) { Lib::free(ptr, size); } |
Contributor
There was a problem hiding this comment.
This should not be necessary.
Contributor
|
This is awesome. I think I'd much prefer this to #917 - although we should be very careful to understand coroutine semantics before committing to this too hard. |
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.
Another idea for how to address what #917 is proposing to fix.
This is just cosmetics and readability. Perf check found no measurable difference on TPTP.