diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaIso.c | 19 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 14 |
3 files changed, 24 insertions, 11 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b2905571..4cfa39b7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -951,7 +951,7 @@ extern void Gia_ManSetIfParsDefault( void * pIfPars ); extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars ); /*=== giaIso.c ===========================================================*/ extern Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose ); +extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose, int fVeryVerbose ); /*=== giaLogic.c ===========================================================*/ extern void Gia_ManTestDistance( Gia_Man_t * p ); extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars ); diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index eab828db..1110f306 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -1080,9 +1080,8 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_ SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose ) +Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose, int fVeryVerbose ) { - int fVeryVerbose = 0; Gia_Man_t * p, * pPart; Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings; Vec_Int_t * vRemain, * vLevel, * vLevel2; @@ -1118,8 +1117,8 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P Gia_ManStop( p ); return NULL; } -// printf( "Reduced %d outputs to %d outputs. ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) ); -// Abc_PrintTime( 1, "Time", clock() - clk ); + printf( "Reduced %d outputs to %d candidate classes. ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) ); + Abc_PrintTime( 1, "Time", clock() - clk ); // perform refinement of equivalence classes Counter = 0; @@ -1134,6 +1133,16 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P printf( "%6d finished...\r", Counter ); continue; } + + if ( fVerbose ) + { + iPo = Vec_IntEntry(vLevel, 0); + printf( "%6d %6d %6d : ", i, Vec_IntSize(vLevel), iPo ); + pPart = Gia_ManDupCones( p, &iPo, 1, 1 ); + Gia_ManPrintStats(pPart, 0, 0, 0); + Gia_ManStop( pPart ); + } + sStart = Vec_PtrSize( vEquivs2 ); vStrings = Vec_PtrAlloc( 100 ); Vec_IntForEachEntry( vLevel, iPo, k ) @@ -1283,7 +1292,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ) //Gia_AigerWrite( pDouble, "test.aig", 0, 0 ); // analyze the two-output miter - pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0 ); + pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0 ); Vec_VecFree( (Vec_Vec_t *)vPosEquivs ); // given CEX for output 0, derive CEX for output 1 diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b18704f7..32282dd7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29808,9 +29808,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pAig; Vec_Ptr_t * vPosEquivs; // Vec_Ptr_t * vPiPerms; - int c, fDualOut = 0, fVerbose = 0; + int c, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "dvwh" ) ) != EOF ) { switch ( c ) { @@ -29820,6 +29820,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -29836,8 +29839,8 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Iso(): The AIG has only one PO. Isomorphism detection is not performed.\n" ); return 1; } - pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose ); -// pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose ); + pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose, fVeryVerbose ); +// pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose, fVeryVerbose ); // Vec_VecFree( (Vec_Vec_t *)vPiPerms ); if ( pAig == NULL ) { @@ -29851,10 +29854,11 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &iso [-dvh]\n" ); + Abc_Print( -2, "usage: &iso [-dvwh]\n" ); Abc_Print( -2, "\t removes POs with isomorphic sequential COI\n" ); Abc_Print( -2, "\t-d : treat the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } |