Index the structural hash tables by mask rather than remainder

[TrevorHansen]

Aig_Hash() and Gia_ManHashOne() both end in Key % TableSize, with TableSize a prime read out of the manager on every call. That is a hardware divide by a runtime value on the hottest path either package has. Profiling STP converting a large bit-blasted query, Aig_TableInsert(), Aig_TableLookup() and Aig_TableResize() are 50.8% of the whole run between them.

This sizes both tables to a power of two and reduces the key by multiplying it by an odd 64-bit constant, taking bits out of the high half of the product. The mixing steps are untouched, and so is the growth policy: both tables still grow once the entries reach twice the buckets, and still grow to hold twice the entries — rounded up to a power of two rather than up to a prime.

Does the mask distribute as well as the modulus?

Yes. Over 400,000 keys drawn the way an AIG draws them — dense fanin ids at small offsets, both polarities — each table leaves as many buckets empty as a uniform hash predicts for the load it is at.

reduction	load	empty buckets	uniform-hash prediction	mean successful probe
% prime	1.00	36.8%	36.79%	1.50
multiply-mask	0.76	46.7%	46.77%	1.38

The probe difference is the load, not the function: rounding a size up to a power of two rather than to a prime leaves the table a little emptier than it was. Feeding the same test a fully structured stream — consecutive ids at fixed small offsets, which is what a bit-blaster actually produces — gives the same figures to a tenth of a percent, so the mask is not sensitive to that regularity.

Speed

Measured on STP's own bit-blasting timer, interleaved against the same build without the patch, arm order rotated per round, medians of five reps (nine for the last row). Three large queries at STP's two cheapest conversion levels.

query	level	Bit Blasting	CNF Conversion
rw_rule_candidate_vmcai_2022_bw512_11	very-low	3682 → 3190 ms −13.4%	2280 → 2278 ms −0.1%
ponylink-slaveTXlen-unsat-unrolled-nomem	very-low	1230 → 1191 ms −3.1%	725 → 728 ms +0.3%
compose.s4._bit8_na6_nr4_paired	very-low	2164 → 1658 ms −23.4%	1155 → 1160 ms +0.4%
rw_rule_candidate_vmcai_2022_bw512_11	gia-low	2908 → 2688 ms −7.6%	10524 → 10398 ms −1.2%
ponylink-slaveTXlen-unsat-unrolled-nomem	gia-low	956 → 940 ms −1.8%	2022 → 1994 ms −1.3%
compose.s4._bit8_na6_nr4_paired	gia-low	1478 → 1365 ms −7.7%	4790 → 4717 ms −1.5%

Whole-run CPU cycles to the point where the CNF is complete move −2.0% to −7.0% across the same six, and retired instructions move by −0.63% to +0.08%. The instruction count staying flat is the point: one divide becomes a multiply, a shift and an and, so counting instructions scores this change as neutral-to-worse and only cycles show it.

Part of the gain is not the divide. Because a power of two above 2n is at least the prime above 2n, the manager has to grow further before the next trigger and so rehashes less often: on the first query above, Aig_TableResize falls from 9.3% of the run to 4.7%.

Memory

The same rounding is the cost. The power of two above 2n can be nearly twice the prime above 2n, so where a run's last resize lands just past a boundary the table doubles.

query	level	peak RSS
rw_rule_candidate_vmcai_2022_bw512_11	very-low	−1.1%
ponylink-slaveTXlen-unsat-unrolled-nomem	very-low	+5.7%
compose.s4._bit8_na6_nr4_paired	very-low	−1.8%
rw_rule_candidate_vmcai_2022_bw512_11	gia-low	−0.7%
ponylink-slaveTXlen-unsat-unrolled-nomem	gia-low	−0.1%
compose.s4._bit8_na6_nr4_paired	gia-low	−1.5%

Rounding down instead bounds the table at 2n and takes that +5.7% to +1.2%, but it leaves the table between one and two times the entries rather than two to four, so the manager rehashes about half again as often: it gives back most of the speed and turns the fourth row above into a +6.8% regression. Rounding up is the better trade.

Tried and dropped: growing at load factor one

The obvious companion change — resize when the entries reach the buckets rather than twice the buckets — is a loss, by up to 16.9% of cycles, and is not in this PR.

Both tables oscillate between load 0.5 and load 2, so the mean load is 1.0, not 2.0, and the mean successful probe is 1.50. Growing at load 1 only takes that to about 1.36, while n then doubles rather than quadruples between resizes, so the manager makes about 2 full rehash passes over its lifetime instead of about 1.33. perf shows the trade directly: Aig_TableResize goes from 9.3% to 15.3% of the run while Aig_TableInsert (25.2% → 21.9%) and Aig_TableLookup (16.3% → 13.0%) both fall. Fifty per cent more rehashing for nine per cent fewer probes.

Output neutrality

A lookup decides identity by comparing fanins inside the chain walk, and a key is in the table at most once, so neither the bucket a node lands in nor the order within a chain can change which node is found. The AIG built is the same one.

Checked rather than assumed. STP derives CNF from these tables by six different routes; over 12 large queries at each of those six levels plus 25 fuzz-corpus queries at the default level, the emitted CNF is byte-identical to the CNF the same build without the patch emits — 97 of 97, no mismatches and no skips. The same 97 were also byte-identical for the load-factor variant above before it was dropped on speed, which is the stronger test of the ordering argument since it reshuffles the buckets on a different schedule as well.

Both arms of that comparison are the same STP revision, built in the same tree, differing only by this patch, and each is reached through a wrapper that pins it to its own libstp so neither can pick up the other's.

The only places either package walks a table in bucket order are Aig_TableProfile(), Gia_ManHashProfile() and Aig_TableCountEntries() — two debug prints and a count used in an equality assertion — and every reader of vHTable outside giaHash.c only tests it against zero.

Notes

• Aig_TableSizeFor() is exported from aigTable.c because Aig_ManStart() needs the same rounding for the table it allocates up front; that is the one line in the header.
• Table sizes start at 1024 entries and are capped at 2^30, so the doubling cannot overflow the int the manager stores them in.