aig, gia: reduce the structural hash key without a divide

[TrevorHansen]

This branch was force-pushed; the earlier mask-and-power-of-two version is withdrawn. It was unsound — see "Why not a mask" below. What is on the branch now is a two-multiply reduction that makes no assumption about the table size.

Aig_Hash() and Gia_ManHashOne() both end in Key % TableSize, with TableSize read out of the manager on every call: a hardware divide by a runtime value on the hottest path either package has. Profiled over a bit-blasted query, Aig_TableInsert(), Aig_TableLookup() and Aig_TableResize() are between 66% and 80% of AIG construction, and Gia_ManHashAnd() with Gia_ManHashResize() is 86% of the GIA one.

The change reduces the key with two multiplies instead: multiply by an odd 64-bit constant and take the high half of the product, which every input bit has had an effect on, then map that onto the table by multiplying by the table size and taking the high half again. The mixing steps above are untouched, and so is every table size — Abc_PrimeCudd() still chooses it, the growth policy keeps its trigger and its factor, and no table allocates a byte it did not allocate before. The diff is two functions.

Why not a mask

A power-of-two table indexed by a mask is the shorter way to drop the divide, and it is not available here. nTableSize and pTable are public fields of Aig_Man_t, and a client that knows how many nodes it is about to build can swap in a table of its own sizing. STP does exactly that in BBNodeManagerAIG::hintExpectedAnds(), with a prime. A mask then collapses the table onto the buckets the size's set bits reach, and the blast stops finishing: one 62 MB query that converts in 24 seconds was still in Aig_TableInsert() and Aig_TableLookup() nine minutes later, with no Aig_TableResize() samples at all.

Dumping the real keys of that blast — 1,890,878 distinct keys into the 2,191,451-bucket table the client installed:

reduction	buckets used	max chain	probes per lookup
mask of the multiply-mixed key	512	3,858	1847.6
mask of the raw key	512	6,192	2084.2
Key % TableSize (today)	1,267,806	7	1.430
two multiplies (this PR)	1,266,734	8	1.432
what a uniform hash predicts	1,266,744	—	—

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 52 large queries at each of those six conversion levels, plus 25 fuzzer outputs at the default settings, the emitted CNF is byte-identical to the CNF the same build without the patch emits: 337 of 337, no mismatches and no skips. Both arms are the same STP revision built in the same tree, differing only by this patch, and each is reached through a wrapper pinning 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 the two rehash loops, Aig_TableCountEntries() (a count, used in an equality assertion), and Aig_TableProfile() / Gia_ManHashProfile(), which are debug prints with no live call sites. Every reader of vHTable outside giaHash.c only tests it against zero.

Speed: none

This is the part that argues against merging. Interleaved against the same build without the patch, run by run, medians of seven reps on an idle machine, three large queries at the two cheapest conversion levels:

query	level	instructions	cycles	Bit Blasting
rw_rule_candidate_vmcai_2022_bw512_11	very-low	+0.09%	+0.30%	+0.33%
ponylink-slaveTXlen-unsat-unrolled-nomem	very-low	+0.01%	+0.02%	−0.28%
compose.s4._bit8_na6_nr4_paired	very-low	+0.05%	+0.22%	+0.93%
rw_rule_candidate_vmcai_2022_bw512_11	gia-low	+0.25%	−1.09%	+0.76%
ponylink-slaveTXlen-unsat-unrolled-nomem	gia-low	+0.10%	+0.46%	+1.21%
compose.s4._bit8_na6_nr4_paired	gia-low	+0.21%	−1.11%	−1.27%

Every stage figure is inside the run-to-run spread, and retired instructions rise slightly, which is expected: one divide becomes two multiplies and two shifts. The divide sits on the dependency path to the bucket load, but that load misses cache often enough to hide it.

Peak RSS is unchanged, as it must be — nothing here allocates: 1,003,300 → 1,006,436 kB at very-low and 1,028,048 → 1,028,620 kB at gia-low on the largest of the three, both smaller than the spread between two runs of the same binary.

An earlier reading of this branch had it 3% to 23% cheaper. That was the withdrawn version, and the gain was not the mask: rounding a resize request up to a power of two overshoots by 2x whenever the request lands just above one, so that version was quietly running at half the load factor. The load factor is the whole effect. Sizing the client's table four times larger, with the divide left in place, moves the same three queries by −26.0%, −22.3% and −22.5% on the bit-blasting timer, for 5.6% more peak memory — twenty times what removing the divide is worth, and it belongs on the client side, not here.

So: correct, exact, free, and pointless on today's hardware. Worth taking only if a divide-free hash is wanted for its own sake, or as the prerequisite for a client that does want to size its own table.

---

A second commit rebuilds the table from vObjs on resize instead of walking the old buckets, so the old array is freed before the new one is allocated: the resize transient becomes the larger of the two arrays rather than their sum, and the refill reads the nodes sequentially. Membership is unchanged - the table holds exactly the AND and EXOR nodes, which is the invariant the resize's own Counter assert has always stated. Byte-identical CNF on the hard-set sample under both generators that drive this table, and the full STP suite passes against it. Measured honestly: peak RSS on real queries does not move, because the last resize fires mid-blast at about two thirds of the final node count and the process peak comes later - the bound matters for callers whose footprint peaks at the resize, and the earlier free and sequential sweep are worth having regardless.