From 126b3d39215fbf8c58503934b6ee818afc2c810f Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Tue, 1 Sep 2026 12:34:36 +1000 Subject: [PATCH] gia: skip the mapped network when only the CNF is wanted 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. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaMf.c | 14 +++++++++++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a8f3c4875..befbc421d 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -361,6 +361,7 @@ struct Jf_Par_t_ int fCnfObjIds; int fAddOrCla; int fCnfMapping; + int fCnfOnly; int fPureAig; int fDoAverage; int fCutHashing; diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 0e1ae9a97..bfed62a13 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -1500,7 +1500,8 @@ void Mf_ManPrintQuit( Mf_Man_t * p, Gia_Man_t * pNew ) float MemMan = 1.0 * sizeof(Mf_Obj_t) * Gia_ManObjNum(p->pGia) / (1<<20); float MemCuts = 1.0 * sizeof(int) * (1 << 16) * Vec_PtrSize(&p->vPages) / (1<<20); float MemTt = p->vTtMem ? Vec_MemMemory(p->vTtMem) / (1<<20) : 0; - float MemMap = Vec_IntMemory(pNew->vMapping) / (1<<20); + // pNew is NULL under fCnfOnly: no mapped network was built + float MemMap = pNew ? Vec_IntMemory(pNew->vMapping) / (1<<20) : 0; if ( p->CutCount[0] == 0 ) p->CutCount[0] = 1; if ( !p->pPars->fVerbose ) @@ -1845,7 +1846,11 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) //Mf_ManOptimization( p ); if ( pPars->fVeryVerbose && pPars->fCutMin ) Vec_MemDumpTruthTables( p->vTtMem, Gia_ManName(p->pGia), pPars->nLutSize ); - if ( pPars->fCutMin ) + // the CNF is derived from the cuts, not from the mapped network, so a + // caller that wants only the CNF gets no network and does not pay for one + if ( pPars->fCnfOnly ) + pNew = NULL; + else if ( pPars->fCutMin ) pNew = Mf_ManDeriveMappingGia( p ); else if ( pPars->fCoarsen ) pNew = Mf_ManDeriveMappingCoarse( p ); @@ -1855,7 +1860,8 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) pGia->pData = Mf_ManDeriveCnf( p, p->pPars->fCnfObjIds, p->pPars->fAddOrCla ); //if ( p->pPars->fGenCnf || p->pPars->fGenLit ) // Mf_ManProfileTruths( p ); - Gia_ManMappingVerify( pNew ); + if ( pNew ) + Gia_ManMappingVerify( pNew ); Mf_ManPrintQuit( p, pNew ); Mf_ManFree( p ); if ( pCls != pGia ) @@ -1887,6 +1893,8 @@ void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fA pPars->fAddOrCla = fAddOrCla; pPars->fCnfMapping = fMapping; pPars->fVerbose = fVerbose; + // the mapped network is dropped below, so ask for the CNF alone + pPars->fCnfOnly = 1; pNew = Mf_ManPerformMapping( pGia, pPars ); Gia_ManStopP( &pNew ); // Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 );