Repository navigation
gia: skip the mapped network when only the CNF is wanted (pinned line) - #18
Merged
Merged
Conversation
Mf_ManGenerateCnf() asks Mf_ManPerformMapping() for a mapping and then throws the network away, 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. Add fCnfOnly to Jf_Par_t. With it set, Mf_ManPerformMapping() skips the derivation and returns no network, and the two places that would then dereference a null pointer are guarded: Gia_ManMappingVerify(), and the memory line in Mf_ManPrintQuit(), which reads pNew->vMapping ahead of its own fVerbose early return. Mf_ManGenerateCnf() sets the flag, so every caller that wants only a CNF stops paying for the network. The flag defaults to zero, which every Jf_Par_t user already gets from the memset in its *_ManSetDefaultPars(), so &mf and the other mappers sharing the structure are unchanged. Every in-tree caller of Mf_ManGenerateCnf() discards the manager it returns, which that function frees before returning, so none of them can observe the difference. Measured through a bit-vector solver that reaches this path for every query. On a bit-blasted circuit of about 12M gates, deriving the mapped network was around 14% of the time spent inside Mf_ManGenerateCnf(). Over three large queries, whole-run retired instructions fall by 8.9% to 15.0% at LUT size 6 and by 12.9% to 27.5% at LUT size 3, and peak resident memory on the largest drops from 2.50 GB to 1.96 GB. The CNF is byte-identical: 51 queries at each of four generator settings, 204 comparisons, no difference.
Mf_ManPerformMapping() returns no network under fCnfOnly, so a caller that sets it without fGenCnf gets neither a network nor a CNF, and nothing says so. Mf_ManGenerateCnf() sets both and &mf sets neither, so no caller in the tree can reach it, but fCnfOnly is a public field of Jf_Par_t and the pairing is not evident from the field alone.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Mf_ManGenerateCnf()asksMf_ManPerformMapping()for a mapping and throws the network away on the next line. Building it is not free:Mf_ManDeriveMappingGia()walks every node in the mapping and runs each chosen cut's truth table throughKit_TruthToGia(), filling a second Gia manager that nothing ever reads. The CNF is derived from the cuts, not from that network.fCnfOnlyskips the derivation and returns no network, and guards the two places that would then read a null pointer. The second commit asserts thatfCnfOnlyis only set together withfGenCnf, since between them they are the whole output: set alone it would produce neither a network nor a CNF, and say nothing. Checked by inverting it —&satokoreachesMf_ManPerformMapping()with both flags set and&mf -cwith neither, so the assert is live on both callers and holds.What it saves
Profiling a bit-blasted circuit of about 12M gates put roughly 14% of the time inside
Mf_ManGenerateCnf()inMf_ManDeriveMappingGia()— time spent building a network that is immediately freed.Whole-run retired instructions through a bit-vector solver stopped just after CNF generation, median of three runs:
The share is larger at LUT 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.
The CNF does not change: 51 queries at each of four generation settings, 204 comparisons, all byte-identical against unpatched ABC.
Base
This is #11 rebased onto
pin-two-commits, the lineABC_GIT_TAGpoints into; #11 targetedstpand so reached no build. Identical patch-id.Mf_ManDeriveMappingGia()is byte-identical on this base andMf_ManPerformMapping()has the same two callers with the same memset-ing parameter init, so #11's containment argument holds unchanged.