gia: skip the mapped network when only the CNF is wanted

[TrevorHansen]

Mf_ManGenerateCnf() asks Mf_ManPerformMapping() for a mapping and then throws the network away — Gia_ManStopP(&pNew) on the next line — keeping only the Cnf_Dat_t hung off the original manager. Building that network is not free: Mf_ManDeriveMappingGia() walks every node in the mapping and runs each chosen cut's truth table through Kit_TruthToGia(), filling a second Gia manager that nothing ever reads.

The CNF does not come from that network. Mf_ManDeriveCnf() and Mf_ManDeriveCnfs() read the map references, each node's best cut, the truth-table memory and the per-function clause counts — all of which cut computation has already produced.

The change

A new fCnfOnly field on Jf_Par_t. With it set, Mf_ManPerformMapping() skips the derivation and returns no network. Two places would then dereference a null pointer and are guarded:

• Gia_ManMappingVerify(pNew), which asserts the network has a mapping;
• the memory line in Mf_ManPrintQuit(), which reads pNew->vMapping before its own fVerbose early return, so it faults even in a quiet run. It now reports 0 MB when there is no network, which is what was built.

Mf_ManGenerateCnf() sets the flag, so every caller that wants only a CNF stops paying for the network.

Why this is safe for the rest of the tree

• Mf_ManPerformMapping() has two callers: Mf_ManGenerateCnf(), and &mf in abc.c. The latter initialises its parameters with Mf_ManSetDefaultPars(), which memsets the structure, so it gets fCnfOnly == 0 and behaves exactly as before.
• Jf_Par_t is shared with the Jf, Lf, Of, Pf, Nf and Kf mappers. Every one of them initialises through a *_ManSetDefaultPars() that memsets the whole structure, and none of them reads the new field. Adding it changes nothing for them.
• Every in-tree caller of Mf_ManGenerateCnf() — around forty-five sites across bmc, cec, pdr, glucose, acb and the gia files — takes the Cnf_Dat_t and discards the manager, which Mf_ManGenerateCnf() frees before returning. None of them can observe the missing network.

Measurements

Measured through a bit-vector solver that reaches Mf_ManGenerateCnf() for every query it solves. Profiling a bit-blasted circuit of about 12M gates put roughly 14% of the time inside Mf_ManGenerateCnf() in Mf_ManDeriveMappingGia().

Whole-run retired instructions on three large bit-vector queries, stopping the solver right after CNF generation, median of three runs:

query	LUT 6	LUT 3
unrolled hardware model, unsat	−8.9%	−12.9%
512-bit rewrite-rule candidate	−15.0%	−27.5%
composed packet-processing pipeline	−10.6%	−22.1%

The share is larger at LUT size 3 because the CNF derivation itself is cheaper there, so the discarded network is a bigger fraction of the whole.

Peak resident memory on the 512-bit query at LUT 6 falls from 2.50 GB to 1.96 GB, since the second Gia manager is never allocated.

CNF equivalence

51 queries drawn across a corpus of large bit-vector benchmarks, at each of four CNF-generation settings (two LUT sizes over two front ends), comparing the generated CNF byte for byte against the same solver built on unpatched ABC: 204 comparisons, 204 identical, none mismatched, none skipped.