diff --git a/src/aig/gia/giaTranStoch.c b/src/aig/gia/giaTranStoch.c index f7e473d0a..78dc1424d 100644 --- a/src/aig/gia/giaTranStoch.c +++ b/src/aig/gia/giaTranStoch.c @@ -80,6 +80,7 @@ struct Gia_ManTranStochParam { int fResetHop; int fTruth; int fNewLine; + Gia_Man_t * pExdc; int nVerbose; }; @@ -92,9 +93,9 @@ Gia_Man_t * Gia_ManTranStochOpt1( Gia_ManTranStochParam * p, Gia_Man_t * pOld ) do { n = Gia_ManAndNum( pGia ); if ( p->fTruth ) - pNew = Gia_ManTransductionTt( pGia, (p->fMerge? 8: 7), !p->fCspf, p->nSeed++, 0, 0, 0, 0, NULL, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 ); + pNew = Gia_ManTransductionTt( pGia, (p->fMerge? 8: 7), !p->fCspf, p->nSeed++, 0, 0, 0, 0, p->pExdc, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 ); else - pNew = Gia_ManTransductionBdd( pGia, (p->fMerge? 8: 7), !p->fCspf, p->nSeed++, 0, 0, 0, 0, NULL, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 ); + pNew = Gia_ManTransductionBdd( pGia, (p->fMerge? 8: 7), !p->fCspf, p->nSeed++, 0, 0, 0, 0, p->pExdc, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 ); Gia_ManStop( pGia ); pGia = pNew; pNew = Gia_ManCompress2( pGia, 1, 0 ); @@ -152,7 +153,7 @@ Gia_Man_t * Gia_ManTranStochOpt3( Gia_ManTranStochParam * p, Gia_Man_t * pOld ) p->nSeed = 1234 * (i + p->nSeedBase); pNew = Gia_ManTranStochOpt2( p, pOld ); if ( p->nRestarts && p->nVerbose ) - printf( "* res %d : #nodes = %5d\n", i, Gia_ManAndNum( pNew ) ); + printf( "* res %2d : #nodes = %5d\n", i, Gia_ManAndNum( pNew ) ); if ( n > Gia_ManAndNum( pNew ) ) { n = Gia_ManAndNum( pNew ); Gia_ManStop( pBest ); @@ -164,7 +165,7 @@ Gia_Man_t * Gia_ManTranStochOpt3( Gia_ManTranStochParam * p, Gia_Man_t * pOld ) return pBest; } -Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nSeedBase, int fCspf, int fMerge, int fResetHop, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, int nVerbose ) { +Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nSeedBase, int fCspf, int fMerge, int fResetHop, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, Gia_Man_t * pExdc, int nVerbose ) { int i, j = 0; Gia_Man_t * pNew, * pBest, * pStart; Abc_Ntk_t * pNtk, * pNtkRes; Vec_Ptr_t * vpStarts; @@ -177,6 +178,7 @@ Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nS p->fResetHop = fResetHop; p->fTruth = fTruth; p->fNewLine = fNewLine; + p->pExdc = pExdc; p->nVerbose = nVerbose; // setup start points vpStarts = Vec_PtrAlloc( 4 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f3c2e1635..cb403e315 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42755,8 +42755,8 @@ usage: ***********************************************************************/ int Abc_CommandAbc9TranStoch( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nSeedBase, int fCspf, int fMerge, int fResetHop, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, int nVerbose ); - Gia_Man_t * pTemp; + extern Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nSeedBase, int fCspf, int fMerge, int fResetHop, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, Gia_Man_t * pExdc, int nVerbose ); + Gia_Man_t * pTemp, * pExdc = NULL; int c, nRestarts = 0, nHops = 10, nSeedBase = 0, fCspf = 0, fMerge = 1, fResetHop = 1, fTruth = 0, fSingle = 0, fOriginalOnly = 0, fNewLine = 0, nVerbose = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "NMRVcmrtsonh" ) ) != EOF ) @@ -42825,18 +42825,41 @@ int Abc_CommandAbc9TranStoch( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( argc > globalUtilOptind + 1 ) + { + Abc_Print( -1, "Wrong number of auguments.\n" ); + goto usage; + } if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Empty GIA network.\n" ); return 1; } + if ( argc == globalUtilOptind + 1 ) + { + FILE * pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", argv[globalUtilOptind] ); + return 1; + } + fclose( pFile ); + pExdc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pExdc == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 1; + } + } - pTemp = Gia_ManTranStoch( pAbc->pGia, nRestarts, nHops, nSeedBase, fCspf, fMerge, fResetHop, fTruth, fSingle, fOriginalOnly, fNewLine, nVerbose ); + pTemp = Gia_ManTranStoch( pAbc->pGia, nRestarts, nHops, nSeedBase, fCspf, fMerge, fResetHop, fTruth, fSingle, fOriginalOnly, fNewLine, pExdc, nVerbose ); + if ( pExdc != NULL ) + Gia_ManStop( pExdc ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &transtoch [-NMRV num] [-cmrtsonh]\n" ); + Abc_Print( -2, "usage: &transtoch [-NMRV num] [-cmrtsonh] \n" ); Abc_Print( -2, "\t iterates transduction with randomized parameters\n" ); Abc_Print( -2, "\t-N num : number of restarts [default = %d]\n", nRestarts ); Abc_Print( -2, "\t-M num : number of hops (if; mfs2; strash) [default = %d]\n", nHops ); @@ -42850,6 +42873,7 @@ usage: Abc_Print( -2, "\t-o : toggles starting from the given AIG [default = %s]\n", fOriginalOnly? "yes": "no" ); Abc_Print( -2, "\t-n : toggles printing with a new line [default = %s]\n", fNewLine? "yes": "no" ); Abc_Print( -2, "\t-h : prints the command usage\n" ); + Abc_Print( -2, "\t : AIGER specifying external don't-cares\n" ); Abc_Print( -2, "\t\n" ); Abc_Print( -2, "\t This command was contributed by Yukio Miyasaka.\n" ); return 1;