Repository navigation
expr: Reclaim zombies transitively in reclaimZombies(). - #13052
Merged
Merged
Conversation
mpreiner
requested review from
daniel-larraz
and
a balanced review from Copilot
October 7, 2026 21:52
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
The new transitive garbage-collection behavior needs targeted regression coverage.
1 open finding
What changed in this PR
Updates zombie collection to reclaim dead expression DAGs transitively, addressing memory growth across solver resets.
Changes:
- Reclaims newly created zombies in repeated rounds.
- Extracts single-node cleanup into
reclaimZombie().
| File | Description |
|---|---|
src/expr/node_manager_template.h |
Declares the single-zombie reclamation helper. |
src/expr/node_manager_template.cpp |
Implements transitive zombie reclamation. |
🧠 Review effort: Balanced
Give feedback about Copilot approvals in this survey to enter a drawing for a $150 gift card.
Each call only reclaimed the zombies present when it started, so dead DAGs were reclaimed one layer per call. Deep DAGs such as bit-blasted circuits thus survived for a long time, and memory grew across (reset)s. Now reclaim in rounds until no zombies are left. Fixes cvc5#12984. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
mpreiner
force-pushed
the
reset-memory-consumption
branch
from
October 7, 2026 22:52
687d06b to
63e3240
Compare
Checks that a single collection pass reclaims a whole dead chain rather than only its top layer (see cvc5#12984). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
mpreiner
commented
Oct 8, 2026
Comment on lines
+410
to
+462
| void NodeManager::reclaimZombie(NodeValue* nv) | ||
| { | ||
| Assert(d_inReclaimZombies); | ||
| Assert(nv->d_rc == 0); | ||
|
|
||
| if (TraceIsOn("gc")) | ||
| { | ||
| Trace("gc") << "deleting node value " << nv << " [" << nv->d_id << "]: "; | ||
| nv->printAst(Trace("gc")); | ||
| Trace("gc") << endl; | ||
| } | ||
|
|
||
| // remove from the pool | ||
| kind::MetaKind mk = nv->getMetaKind(); | ||
| if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) | ||
| { | ||
| poolRemove(nv); | ||
| } | ||
|
|
||
| // whether exit is normal or exceptional, the NVReclaim dtor is | ||
| // called and ensures that d_nodeUnderDeletion is set back to | ||
| // NULL. | ||
| NVReclaim rc(d_nodeUnderDeletion); | ||
| d_nodeUnderDeletion = nv; | ||
|
|
||
| // remove attributes | ||
| { // notify listeners of deleted node | ||
| TNode n; | ||
| n.d_nv = nv; | ||
| nv->d_rc = 1; // so that TNode doesn't assert-fail | ||
| // this would mean that one of the listeners stowed away | ||
| // a reference to this node! | ||
| Assert(nv->d_rc == 1); | ||
| } | ||
| nv->d_rc = 0; | ||
| d_attrManager->deleteAllAttributes(nv); | ||
|
|
||
| // decr ref counts of children | ||
| nv->decrRefCounts(); | ||
| if (mk == kind::metakind::CONSTANT) | ||
| { | ||
| // Destroy (call the destructor for) the C++ type representing | ||
| // the constant in this NodeValue. This is needed for | ||
| // e.g. cvc5::internal::Rational, since it has a gmp internal | ||
| // representation that mallocs memory and should be cleaned | ||
| // up. (This won't delete a pointer value if used as a | ||
| // constant, but then, you should probably use a smart-pointer | ||
| // type for a constant payload.) | ||
| kind::metakind::deleteNodeValueConstant(nv); | ||
| } | ||
| free(nv); | ||
| } /* NodeManager::reclaimZombie() */ | ||
|
|
Member
Author
There was a problem hiding this comment.
This is just a code move from reclaimZombies().
mpreiner
marked this pull request as ready for review
October 8, 2026 14:34
daniel-larraz
approved these changes
Oct 8, 2026
Member
Author
|
Here are the measurements from #12984 before/after the fix.
|
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.
Each call only reclaimed the zombies present when it started, so dead DAGs were reclaimed one layer per call. Deep DAGs such as bit-blasted circuits thus survived for a long time, and memory grew across (reset)s. Now reclaim in rounds until no zombies are left.
Fixes #12984.
Co-Authored-By: Claude Opus 5.5 noreply@anthropic.com