shrink Clause memory footprint by fiddling with layout#831
shrink Clause memory footprint by fiddling with layout#831quickbeam123 merged 1 commit intomasterfrom
Conversation
| protected: | ||
| /** number of literals */ | ||
| unsigned _length : 20; | ||
| unsigned _length; |
There was a problem hiding this comment.
Shrinking this from 32 bytes to 20 doesn't help in the wider picture of things.
| /** for splitting: timestamp marking when has the clause been reduced or restored by splitting */ | ||
| unsigned _reductionTimestamp; | ||
| /** a map that translates Literal* to its index in the clause */ | ||
| InverseLookup<Literal>* _literalPositions; |
There was a problem hiding this comment.
This needed to be aligned to 8 bytes because it's a pointer, so the compiler generates some padding. Move things around so that it's already 8-byte aligned.
| /** age */ | ||
| unsigned _age; | ||
|
|
||
| SplitSet* _splits; |
There was a problem hiding this comment.
Pointers have to be 8-byte aligned. Move them to the start of the class because removing _XXnarrows and _reductions now throws us off.
| /** Sine level computed in SineUtils and used in various heuristics. | ||
| * May stay uninitialized (i.e. always MAX), if not needed | ||
| **/ | ||
| unsigned char _sineLevel : 8; // updated as the minimum from parents to children |
There was a problem hiding this comment.
Things that already bytes may as well stay on byte boundaries so the machine can manipulate them (mostly) without shifts.
|
|
||
| /** Number of this unit, used for printing and statistics */ | ||
| unsigned _number; | ||
| unsigned _number : 29; |
There was a problem hiding this comment.
Is 2^29 sufficient for numbers? We'd need roughly half a billion units to overflow this.
There was a problem hiding this comment.
Should be enough for our current use cases ...
|
A Let me see how we proceed if we also remove |
quickbeam123
force-pushed
the
michael-clause-diet
branch
from
b9dc670 to
af37407
Compare
3 participants
On my machine this shrinks
sizeof(Clause)from 104 bytes to 88. This is done partially by @mezpusz's tip that_XXnarrowsand_reductionsare no longer used, but also by moving some fields around. I'll explain the changes in comments inline.