From c93461d6ea402f8b16af65c04dcf08909fc20f49 Mon Sep 17 00:00:00 2001 From: Daniel James Date: Sat, 3 Oct 2026 17:15:50 -0700 Subject: [PATCH 1/5] Add Scratch for per-call working stacks and use it in substitution application SubstHelper::applyImpl and BottomUpEvaluation::apply took their stacks from Recycled on every call, which on small terms costs more than the work itself. Scratch keeps one object per nesting depth instead. Co-Authored-By: Claude Opus 5.5 (1M context) --- Kernel/BottomUpEvaluation.hpp | 32 ++++++++--------- Kernel/SubstHelper.hpp | 66 +++++++++++++++++------------------ Lib/Recycled.hpp | 28 +++++++++++++++ 3 files changed, 76 insertions(+), 50 deletions(-) diff --git a/Kernel/BottomUpEvaluation.hpp b/Kernel/BottomUpEvaluation.hpp index 3aef9f0da..7580b7f3d 100644 --- a/Kernel/BottomUpEvaluation.hpp +++ b/Kernel/BottomUpEvaluation.hpp @@ -327,51 +327,51 @@ class BottomUpEvaluation { Result apply(Arg const& toEval) { /* recursion state. Contains a stack of items that are being recursed on. */ - Recycled>> recState; - Recycled> recResults; + Scratch>, Stack>> stacks; + auto& [recState, recResults] = *stacks; - recState->push(BottomUpChildIter(toEval, _context)); + recState.push(BottomUpChildIter(toEval, _context)); - while (!recState->isEmpty()) { - if (recState->top().hasNext(_context)) { - Arg t = recState->top().next(_context); + while (!recState.isEmpty()) { + if (recState.top().hasNext(_context)) { + Arg t = recState.top().next(_context); Option nonRec = _evNonRec(t); if (nonRec) { - recResults->push(move_if_value(*nonRec)); + recResults.push(move_if_value(*nonRec)); } else { Option cached = _memo.get(t); if (cached.isSome()) { - recResults->push(std::move(cached).unwrap()); + recResults.push(std::move(cached).unwrap()); } else { - recState->push(BottomUpChildIter(t, _context)); + recState.push(BottomUpChildIter(t, _context)); } } } else { - BottomUpChildIter orig = recState->pop(); + BottomUpChildIter orig = recState.pop(); ASS_GE(recResults.size(), orig.nChildren(_context)) Result* argLst = orig.nChildren(_context) == 0 ? nullptr - : static_cast(&((*recResults)[recResults->size() - orig.nChildren(_context)])); + : static_cast(&(recResults[recResults.size() - orig.nChildren(_context)])); Result eval = _memo.getOrInit(orig.self(), [&](){ return _function(orig.self(), argLst); }); DEBUG_BOTTOM_UP(0, "evaluated: ", orig.self(), " -> ", eval); - recResults->pop(orig.nChildren(_context)); - recResults->push(std::move(eval)); + recResults.pop(orig.nChildren(_context)); + recResults.push(std::move(eval)); } } - ASS(recState->isEmpty()) + ASS(recState.isEmpty()) - ASS(recResults->size() == 1); - auto result = recResults->pop(); + ASS(recResults.size() == 1); + auto result = recResults.pop(); DEBUG_BOTTOM_UP(0, "eval result: ", toEval, " -> ", result); return result; } diff --git a/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp index cc961d6bd..1345c3332 100644 --- a/Kernel/SubstHelper.hpp +++ b/Kernel/SubstHelper.hpp @@ -345,33 +345,31 @@ Term* SubstHelper::applyImpl(Term* trm, Applicator& applicator, bool noSharing) ASSERTION_VIOLATION; } - Recycled> toDo; - Recycled> terms; - Recycled> modified; - Recycled> args; + Scratch, Stack, Stack, Stack>> stacks; + auto& [toDo, terms, modified, args] = *stacks; - modified->push(false); - toDo->push(trm->args()); + modified.push(false); + toDo.push(trm->args()); for(;;) { - TermList* tt=toDo->pop(); + TermList* tt=toDo.pop(); if(tt->isEmpty()) { - if(terms->isEmpty()) { + if(terms.isEmpty()) { //we're done, args stack contains modified arguments //of the topleve term/literal. - ASS(toDo->isEmpty()); + ASS(toDo.isEmpty()); break; } - Term* orig=terms->pop(); - if(!modified->pop()) { - args->truncate(args->length() - orig->arity()); - args->push(TermList(orig)); + Term* orig=terms.pop(); + if(!modified.pop()) { + args.truncate(args.length() - orig->arity()); + args.push(TermList(orig)); continue; } //here we assume, that stack is an array with //second topmost element as &top()-1, third at //&top()-2, etc... - TermList* argLst=&args->top() - (orig->arity()-1); + TermList* argLst=&args.top() - (orig->arity()-1); bool shouldShare=!noSharing && canBeShared(argLst, orig->arity()); @@ -386,61 +384,61 @@ Term* SubstHelper::applyImpl(Term* trm, Applicator& applicator, bool noSharing) else { newTrm=Term::createNonShared(orig,argLst); } - args->truncate(args->length() - orig->arity()); - args->push(TermList(newTrm)); + args.truncate(args.length() - orig->arity()); + args.push(TermList(newTrm)); - modified->setTop(true); + modified.setTop(true); continue; } - toDo->push(tt->next()); + toDo.push(tt->next()); TermList tl=*tt; if(tl.isOrdinaryVar()) { TermList tDest=applicator.apply(tl.var()); - args->push(tDest); + args.push(tDest); if(tDest!=tl) { - modified->setTop(true); + modified.setTop(true); } continue; } if(tl.isSpecialVar()) { TermList tDest=SpecVarHandler::apply(applicator,tl.var()); - args->push(tDest); + args.push(tDest); if(tDest!=tl) { - modified->setTop(true); + modified.setTop(true); } continue; } ASS(tl.isTerm()); if(tl.isVar() || (tl.term()->shared() && tl.term()->ground())) { - args->push(tl); + args.push(tl); continue; } Term* t = tl.term(); if(t->isSpecial()) { //we handle specal terms at the top level of this function - args->push(TermList(applyImpl(t, applicator, noSharing))); + args.push(TermList(applyImpl(t, applicator, noSharing))); continue; } - terms->push(t); - modified->push(false); - toDo->push(t->args()); + terms.push(t); + modified.push(false); + toDo.push(t->args()); } - ASS(toDo->isEmpty()); - ASS(terms->isEmpty()); - ASS_EQ(modified->length(),1); - ASS_EQ(args->length(),trm->arity()); + ASS(toDo.isEmpty()); + ASS(terms.isEmpty()); + ASS_EQ(modified.length(),1); + ASS_EQ(args.length(),trm->arity()); Term* result; - if(!modified->pop()) { + if(!modified.pop()) { result=trm; } else { //here we assume, that stack is an array with //second topmost element as &top()-1, third at //&top()-2, etc... - TermList* argLst=&args->top() - (trm->arity()-1); - ASS_EQ(args->size(), trm->arity()); + TermList* argLst=&args.top() - (trm->arity()-1); + ASS_EQ(args.size(), trm->arity()); if(trm->isLiteral()) { ASS(!noSharing); Literal* lit = static_cast(trm); diff --git a/Lib/Recycled.hpp b/Lib/Recycled.hpp index 0ac200197..ed2fb8d02 100644 --- a/Lib/Recycled.hpp +++ b/Lib/Recycled.hpp @@ -218,6 +218,34 @@ class Recycled template bool Recycled::memAlive = true; +/** + * Like Recycled, but cheaper for objects needed on every call of a small, + * possibly reentrant function: one object is kept for each nesting depth. + * The object is reset when taken. + */ +template +class Scratch +{ + static inline Stack _all; + static inline unsigned _depth = 0; + T* _self; +public: + Scratch() + { + if (_depth == _all.size()) { + _all.push(new T()); + } + _self = _all[_depth++]; + Reset()(*_self); + } + ~Scratch() { _depth--; } + Scratch(Scratch const&) = delete; + Scratch& operator=(Scratch const&) = delete; + + T& operator* () { return *_self; } + T* operator->() { return _self; } +}; + }; template From 675fad8617ec0d60dcd526cacfd256405d552dcf Mon Sep 17 00:00:00 2001 From: Daniel James Date: Sat, 3 Oct 2026 17:15:50 -0700 Subject: [PATCH 2/5] Skip subterms that cannot contain the replaced term in EqHelper::replace A subterm no heavier than the term being replaced (or a ground one, when it is a variable) cannot contain it, so it need not be traversed. Co-Authored-By: Claude Opus 5.5 (1M context) --- Kernel/EqHelper.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Kernel/EqHelper.cpp b/Kernel/EqHelper.cpp index a75ddda33..885986699 100644 --- a/Kernel/EqHelper.cpp +++ b/Kernel/EqHelper.cpp @@ -109,6 +109,9 @@ Term* EqHelper::replace(Term* trm0, TermList tSrc, TermList tDest) modified.push(false); toDo.push(trm0->args()); + // subterms no heavier than tSrc (or ground ones, if tSrc is a variable) cannot contain it + unsigned srcWeight = tSrc.isVar() ? 1 : tSrc.term()->weight(); + for (;;) { TermList* tt=toDo.pop(); if (tt->isEmpty()) { @@ -148,6 +151,10 @@ Term* EqHelper::replace(Term* trm0, TermList tSrc, TermList tDest) } ASS(tl.isTerm()); Term* t=tl.term(); + if (t->weight() <= srcWeight || (tSrc.isVar() && t->ground())) { + args.push(tl); + continue; + } terms.push(t); modified.push(false); toDo.push(t->args()); From 411bb13d18ce99502f691a1c55ce6ed749deaa4f Mon Sep 17 00:00:00 2001 From: Daniel James Date: Sat, 3 Oct 2026 17:17:31 -0700 Subject: [PATCH 3/5] Make Recycled no larger than the pointer it holds Its default reset and keep policies are empty, so [[no_unique_address]] keeps them from taking space. Index query result iterators then fit the small object allocator. Co-Authored-By: Claude Opus 5.5 (1M context) --- Lib/Recycled.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Lib/Recycled.hpp b/Lib/Recycled.hpp index ed2fb8d02..b55baef3f 100644 --- a/Lib/Recycled.hpp +++ b/Lib/Recycled.hpp @@ -134,8 +134,8 @@ class Recycled { using Self = IF_USE_PTRS(std::unique_ptr,T); Self _self; - Reset _reset; - Keep _keep; + [[no_unique_address]] Reset _reset; + [[no_unique_address]] Keep _keep; static bool memAlive; static Stack& mem() { From 8598d365773e70ce2f80177957b152b053e21bb5 Mon Sep 17 00:00:00 2001 From: Daniel James Date: Sat, 3 Oct 2026 17:17:31 -0700 Subject: [PATCH 4/5] Do not walk an empty Map on reset Co-Authored-By: Claude Opus 5.5 (1M context) --- Lib/Map.hpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Lib/Map.hpp b/Lib/Map.hpp index 7ba894a4e..802aaf31b 100644 --- a/Lib/Map.hpp +++ b/Lib/Map.hpp @@ -514,6 +514,9 @@ class Map */ void reset() { + if (_noOfEntries == 0) { + return; + } for (int i = _capacity-1;i >= 0;i--) { _entries[i].reset(); } From 0857982ff19ae44f1c83d1db2f77f89f979ac9a0 Mon Sep 17 00:00:00 2001 From: Daniel James Date: Sat, 3 Oct 2026 17:17:32 -0700 Subject: [PATCH 5/5] Keep passive queue sort keys in the skip list nodes Inserting into or removing from the age and weight queues compared against the clause of every node passed, through a virtual call. Nodes now store the age and weight packed into one word, and the clause is only read on ties. Co-Authored-By: Claude Opus 5.5 (1M context) --- Kernel/ClauseQueue.cpp | 19 +++++++- Kernel/ClauseQueue.hpp | 12 ++++- Saturation/AWPassiveClauseContainers.cpp | 62 +++--------------------- Saturation/AWPassiveClauseContainers.hpp | 4 +- 4 files changed, 37 insertions(+), 60 deletions(-) diff --git a/Kernel/ClauseQueue.cpp b/Kernel/ClauseQueue.cpp index e016098b8..1321bee89 100644 --- a/Kernel/ClauseQueue.cpp +++ b/Kernel/ClauseQueue.cpp @@ -33,6 +33,18 @@ ClauseQueue::ClauseQueue() _left->nodes()[0] = 0; } +/** + * Clauses with equal keys go first by input type (a larger one first), + * then by number. + */ +bool ClauseQueue::tieLessThan(Clause* c1, Clause* c2) +{ + if (c1->inputType() != c2->inputType()) { + return c2->inputType() < c1->inputType(); + } + return c1->number() < c2->number(); +} + /** Temporary!!! */ ClauseQueue::~ClauseQueue () { @@ -62,6 +74,8 @@ void ClauseQueue::insert(Clause* c) void* mem = ALLOC_KNOWN(Node::bytesRequiredFor(h + 1), "ClauseQueue::Node"); Node* newNode = reinterpret_cast(mem); newNode->clause = c; + uint64_t k = key(c); + newNode->key = k; // left is a node with a value smaller than that of newNode and having // a large enough height. @@ -71,7 +85,7 @@ void ClauseQueue::insert(Clause* c) unsigned lh = _height; for (;;) { Node* next = left->nodes()[lh]; - if (next == 0 || lessThan(c,next->clause)) { + if (next == 0 || lessThan(k,c,next)) { if (lh <= h) { left->nodes()[lh] = newNode; newNode->nodes()[lh] = next; @@ -94,6 +108,7 @@ bool ClauseQueue::remove(Clause* c) { unsigned h = _height; Node* left = _left; + uint64_t k = key(c); for (;;) { Node* next = left->nodes()[h]; @@ -118,7 +133,7 @@ bool ClauseQueue::remove(Clause* c) return true; } - if (next == 0 || lessThan(c,next->clause)) { + if (next == 0 || lessThan(k,c,next)) { if(h==0) { #if VDEBUG diff --git a/Kernel/ClauseQueue.hpp b/Kernel/ClauseQueue.hpp index dfdd5c89f..8f6cb8f71 100644 --- a/Kernel/ClauseQueue.hpp +++ b/Kernel/ClauseQueue.hpp @@ -17,6 +17,8 @@ #ifndef __ClauseQueue__ #define __ClauseQueue__ +#include + #if VDEBUG #include #endif @@ -51,11 +53,14 @@ class ClauseQueue friend class Iterator; protected: - /** comparison of clauses */ - virtual bool lessThan(Clause*,Clause*) = 0; + /** primary sort key of a clause, ties are broken by tieLessThan() */ + virtual uint64_t key(Clause*) = 0; + static bool tieLessThan(Clause* c1, Clause* c2); /** Nodes in the skip list */ class Node : public Lib::FlexibleTail { public: + /** key() of the clause */ + uint64_t key; /** Clause at this node */ Clause* clause; /** Links to other nodes on the right, can be of any length */ @@ -66,6 +71,9 @@ class ClauseQueue unsigned _height; /** the leftmost node with the dummy key and value */ Node* _left; + /** true if the clause with key @b k goes before @b node */ + static bool lessThan(uint64_t k, Clause* c, const Node* node) + { return k < node->key || (k == node->key && tieLessThan(c, node->clause)); } public: /** Iterator over the queue diff --git a/Saturation/AWPassiveClauseContainers.cpp b/Saturation/AWPassiveClauseContainers.cpp index 8b255bf94..9fa748c32 100644 --- a/Saturation/AWPassiveClauseContainers.cpp +++ b/Saturation/AWPassiveClauseContainers.cpp @@ -35,18 +35,6 @@ using namespace std; using namespace Lib; using namespace Kernel; -/** - * Weight comparison of clauses. - * @return the result of comparison (LESS, EQUAL or GREATER) - * @warning if the option increased_numeral_weight is on, then each comparison - * recomputes the numeral weight of clauses, see Clause::getNumeralWeight(), so it - * it can be expensive - */ -static Comparison compareWeight(Clause* cl1, Clause* cl2, const Options& opt) -{ - return Int::compare(cl1->weightForClauseSelection(opt), cl2->weightForClauseSelection(opt)); -} - /** * Comparison of clauses. The comparison uses four orders in the * following order: @@ -55,31 +43,13 @@ static Comparison compareWeight(Clause* cl1, Clause* cl2, const Options& opt) *
  • by input type;
    • *
  • by number.
    • * + * The key holds the first two, ClauseQueue::tieLessThan the rest. * @since 30/12/2007 Manchester */ -bool AgeQueue::lessThan(Clause* c1,Clause* c2) +uint64_t AgeQueue::key(Clause* c) { - if (c1->age() < c2->age()) { - return true; - } - if (c2->age() < c1->age()) { - return false; - } - - Comparison weightCmp=compareWeight(c1, c2, _opt); - if (weightCmp!=EQUAL) { - return weightCmp==LESS; - } - - if (c1->inputType() < c2->inputType()) { - return false; - } - if (c2->inputType() < c1->inputType()) { - return true; - } - - return c1->number() < c2->number(); -} // AgeQueue::lessThan + return (uint64_t(c->age()) << 32) | c->weightForClauseSelection(_opt); +} // AgeQueue::key AgeQueue::OrdVal AgeQueue::getOrdVal(Clause* cl) const { @@ -94,29 +64,13 @@ AgeQueue::OrdVal AgeQueue::getOrdVal(Clause* cl) const *
  • by input type;
    • *
  • by number.
    • * + * The key holds the first two, ClauseQueue::tieLessThan the rest. * @since 30/12/2007 Manchester */ -bool WeightQueue::lessThan(Clause* c1,Clause* c2) +uint64_t WeightQueue::key(Clause* c) { - Comparison weightCmp=compareWeight(c1, c2, _opt); - if (weightCmp!=EQUAL) { - return weightCmp==LESS; - } - - if (c1->age() < c2->age()) { - return true; - } - if (c2->age() < c1->age()) { - return false; - } - if (c1->inputType() < c2->inputType()) { - return false; - } - if (c2->inputType() < c1->inputType()) { - return true; - } - return c1->number() < c2->number(); -} // WeightQueue::lessThan + return (uint64_t(c->weightForClauseSelection(_opt)) << 32) | c->age(); +} // WeightQueue::key WeightQueue::OrdVal WeightQueue::getOrdVal(Clause* cl) const { diff --git a/Saturation/AWPassiveClauseContainers.hpp b/Saturation/AWPassiveClauseContainers.hpp index 9d45e31f8..154080b34 100644 --- a/Saturation/AWPassiveClauseContainers.hpp +++ b/Saturation/AWPassiveClauseContainers.hpp @@ -37,7 +37,7 @@ class AgeQueue static constexpr OrdVal maxOrdVal = std::make_pair(UINT_MAX,UINT_MAX); OrdVal getOrdVal(Clause* cl) const; protected: - bool lessThan(Clause*,Clause*) override; + uint64_t key(Clause*) override; private: const Shell::Options& _opt; }; @@ -52,7 +52,7 @@ class WeightQueue static constexpr OrdVal maxOrdVal = std::make_pair(UINT_MAX,UINT_MAX); OrdVal getOrdVal(Clause* cl) const; protected: - bool lessThan(Clause*,Clause*) override; + uint64_t key(Clause*) override; private: const Shell::Options& _opt; };