cnf: cache the ISOP cover of each distinct cut function

[TrevorHansen]

Cnf_ComputeClauses() calls Kit_TruthIsop() twice for every non-AND cone it turns into clauses — once for the function and once for its complement — and computes both covers from scratch every time. A cover depends on nothing but the truth table and the leaf count, and the cuts of a bit-blasted circuit are a handful of adder, mux and xor functions repeated across the netlist, so nearly all of that work is recomputation. Profiling STP's CNF generation at Cnf_DeriveFast puts the ISOP family — Kit_TruthIsop5_rec, Kit_TruthIsop_rec, Kit_TruthCofactor0/1, Kit_TruthVarInSupport — at 38-45% of the generation phase.

This keys the covers by (truth table, leaf count) in a table that lives for one Cnf_DeriveFastClauses() call, and replays a stored cover cube for cube. Mf_ManDeriveCnfs() does the same thing one package over, where the mapper has already assigned each truth function an id; Cnf_DeriveFast has no such id, so the truth words themselves are the key (Vec_Mem_t with a two-word entry, the same structure the mapper hashes truth tables in).

Cnf_ComputeClauses() keeps its signature and its uncached behaviour: the callers outside this file derive clauses for one cone at a time, where there is nothing to reuse.

The CNF is unchanged

The clauses are pushed from the same cubes in the same order, so the output is identical by construction rather than by tolerance. Checked against an unpatched build over SMT-LIB QF_BV, comparing sha256 of the emitted CNF: 52/52 files byte-identical at --cnf-generation-effort very-low (the setting that reaches Cnf_DeriveFast), and 52/52 byte-identical at medium, which routes through Cnf_Derive instead and so is a control on the shared code in this file. A 12-file subset was rerun against the final binary: 12/12 and 12/12.

How much reuse there is

Instrumented counts for one CNF derivation, very-low:

SMT-LIB QF_BV query	cover requests	distinct functions	ints stored
rw_rule_candidate_vmcai_2022_bw512_11	7,049,762	42	135
compose.s4._bit8_na6_nr4_paired	3,193,568	26	83
ponylink-slaveTXlen-unsat-unrolled-nomem	2,408,452	196	706

Two hundred functions is the worst case seen; the table never exceeds a few hundred ints.

What it costs and saves

Release build, GCC 12, medians of five interleaved runs for the stage times and of three for the instruction counts:

query	CNF derivation	retired instructions to end of CNF	peak RSS
rw_rule_candidate_vmcai_2022_bw512_11	2528 → 1643 ms (−35.0%)	31.32G → 20.40G (−34.9%)	1474.7 → 1474.5 MB
compose.s4._bit8_na6_nr4_paired	1244 → 754 ms (−39.4%)	31.70G → 26.07G (−17.8%)	920 → 951 MB, see below
ponylink-slaveTXlen-unsat-unrolled-nomem	793 → 448 ms (−43.5%)	50.55G → 46.25G (−8.5%)	967.9 → 958.1 MB

The instruction counts fall further than the times because the removed work has an unusually high IPC (roughly 3, against ~1 for the run as a whole): a tight recursion over one 64-bit word is cheap per instruction next to the hash-table traffic around it. The stage times are the honest number.

The one memory row that moves is an allocator artifact, not the table. Rebuilding with the table allocated but never consulted reproduces the unpatched peak exactly, and setting the allocator's purge delay to zero makes the two builds agree to 0.1% (884.2 MB against 884.3 MB). The faster run simply reaches its peak before deferred purging has returned as much; true demand is unchanged, which the 135-to-706 ints of table already imply.

Scope

The cache is created and freed inside Cnf_DeriveFastClauses() — nothing global, nothing that outlives a derivation. Cnf_CutCountClauses() has the same double-ISOP pattern but is only reachable from the diagnostic Cnf_CountCnfSize(), and is left alone.