Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
TrevorHansen wants to merge 1 commit into
base: stp
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/aig/gia/gia.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -361,6 +361,7 @@ struct Jf_Par_t_
int fCnfObjIds;
int fAddOrCla;
int fCnfMapping;
int fCnfOnly;
int fPureAig;
int fDoAverage;
int fCutHashing;
Expand Down
14 changes: 11 additions & 3 deletions src/aig/gia/giaMf.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
Expand Down Expand Up @@ -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 );
Expand All @@ -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 )
Expand Down Expand Up @@ -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 );
Expand Down
Loading