diff options
Diffstat (limited to 'src/opt/mfs/mfsCore.c')
| -rw-r--r-- | src/opt/mfs/mfsCore.c | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 7104d3b3..a941f153 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -241,21 +241,23 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) if ( pNtk->pExcare ) { Abc_Ntk_t * pTemp; - pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 ); - p->pCare = Abc_NtkToDar( pTemp, 0 ); - Abc_NtkDelete( pTemp ); - p->vSuppsInv = Aig_ManSupportsInverse( p->pCare ); - } -// if ( pPars->fVerbose ) - { - if ( p->pCare != NULL ) - printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); -// else -// printf( "Performing optimization without constraints.\n" ); + if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) ) + printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n", + Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) ); + else + { + pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 ); + p->pCare = Abc_NtkToDar( pTemp, 0 ); + Abc_NtkDelete( pTemp ); + p->vSuppsInv = Aig_ManSupportsInverse( p->pCare ); + } } + if ( p->pCare != NULL ) + printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); + // prepare the BDC manager if ( !pPars->fResub ) { - pDecPars->nVarsMax = nFaninMax; + pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax; pDecPars->fVerbose = pPars->fVerbose; p->vTruth = Vec_IntAlloc( 0 ); p->pManDec = Bdc_ManAlloc( pDecPars ); |