diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2019-11-25 17:54:18 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2019-11-25 17:54:18 +0700 |
commit | 787e3e1d12b5d17aadfed472784ec9f0313eddd4 (patch) | |
tree | 3959292a97bcacd9942ddc00d91f05517dc44a3b /src/base | |
parent | 4deaaa852a1a6cb9d06a88b3b81133330a350c7e (diff) | |
download | abc-787e3e1d12b5d17aadfed472784ec9f0313eddd4.tar.gz abc-787e3e1d12b5d17aadfed472784ec9f0313eddd4.tar.bz2 abc-787e3e1d12b5d17aadfed472784ec9f0313eddd4.zip |
Adding logfile dump to print_status.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 51 | ||||
-rw-r--r-- | src/base/io/io.c | 26 |
2 files changed, 70 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1bae5e24..17741905 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2819,15 +2819,26 @@ usage: ***********************************************************************/ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex ); extern void Abc_NtkPrintPoEquivs( Abc_Ntk_t * pNtk ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c, fOutStatus = 0, fShort = 1; + char * pLogFileName = NULL; // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "osh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Losh" ) ) != EOF ) { switch ( c ) { + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" ); + goto usage; + } + pLogFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'o': fOutStatus ^= 1; break; @@ -2883,7 +2894,32 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->vStatuses ) { - if ( fShort ) + if ( pLogFileName ) + { + Abc_Cex_t * pTemp = NULL; + FILE * pFile = fopen( pLogFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pLogFileName ); + return 0; + } + Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c ) + { + int Status = Vec_IntEntry( pAbc->vStatuses, c ); + if ( Status == -1 ) // undec + fprintf( pFile, "STATUS: ABORTED " ); + else if ( Status == 0 ) + fprintf( pFile, "STATUS: SAT " ); + else if ( Status == 1 ) + fprintf( pFile, "STATUS: UNSAT " ); + fprintf( pFile, "%s\n", Abc_ObjName(Abc_NtkPo(pNtk, c)) ); + if ( Status != 0 ) + continue; + Abc_NtkDumpOneCexSpecial( pFile, pNtk, pTemp ); + } + fclose( pFile ); + } + else if ( fShort ) { printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).", Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1), @@ -2900,11 +2936,12 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: print_status [-osh]\n" ); - Abc_Print( -2, "\t prints verification status\n" ); - Abc_Print( -2, "\t-o : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle using short print-out [default = %s]\n", fShort? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: print_status [-L file] [-osh]\n" ); + Abc_Print( -2, "\t prints verification status\n" ); + Abc_Print( -2, "\t-L file : the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); + Abc_Print( -2, "\t-o : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using short print-out [default = %s]\n", fShort? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/io/io.c b/src/base/io/io.c index 669405cc..843b0ff6 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2326,6 +2326,32 @@ int Abc_NtkCheckSpecialPi( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ +void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex ) +{ + Abc_Cex_t * pCare = NULL; int i, f; Abc_Obj_t * pObj; + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); + //fprintf( pFile, "# FALSIFYING OUTPUTS:"); + //fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, 0, 0 ); + Aig_ManStop( pAig ); + if( pCare == NULL ) + { + printf( "Counter-example minimization has failed.\n" ); + return; + } + // output flop values (unaffected by the minimization) + Abc_NtkForEachLatch( pNtk, pObj, i ) + fprintf( pFile, "CEX: %s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + // output PI values (while skipping the minimized ones) + for ( f = 0; f <= pCex->iFrame; f++ ) + Abc_NtkForEachPi( pNtk, pObj, i ) + if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) ) + fprintf( pFile, "CEX: %s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + Abc_CexFreeP( &pCare ); +} + + void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose ) |