From 76e8d21aafe3a5ae31d7516e33fbac5569384181 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 23 Oct 2023 10:48:43 -0700 Subject: [PATCH] Printout changes. --- src/base/cmd/cmd.c | 14 +++++++------- src/base/cmd/cmdStarter.c | 10 ++++++---- src/proof/cec/cecProve.c | 40 +++++++++++++++++++++------------------ src/proof/ssw/sswRarity.c | 6 ++++-- 4 files changed, 39 insertions(+), 31 deletions(-) diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index d8ba90f58..708fc3f5b 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1956,7 +1956,7 @@ int CmdCommandScrGenLinux( Abc_Frame_t * pAbc, int argc, char **argv ) char * pExt = strstr(pName, "."); if ( !pExt || !strcmp(pExt, ".") || !strcmp(pExt, "..") || !strcmp(pExt, ".s") || !strcmp(pExt, ".txt") ) continue; - sprintf( Line, "%s%sread %s%s%-*s ; %s", fBatch ? "./abc -c \"":"", fAndSpace ? "&" : "", pDirStr?pDirStr:"", pDirStr?"/":"", nFileNameMax, pName, pComStr ); + sprintf( Line, "%s%sread %s%s%-*s ; %s", fBatch ? "./abc -q \"":"", fAndSpace ? "&" : "", pDirStr?pDirStr:"", pDirStr?"/":"", nFileNameMax, pName, pComStr ); for ( c = (int)strlen(Line)-1; c >= 0; c-- ) if ( Line[c] == '\\' ) Line[c] = '/'; @@ -2549,18 +2549,18 @@ usage: ***********************************************************************/ int CmdCommandStarter( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCores ); + extern void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCores, int fVerbose ); FILE * pFile; char * pFileName; char * pCommand = NULL; int c, nCores = 3; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NCvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF ) { switch ( c ) { - case 'N': + case 'P': if ( globalUtilOptind >= argc ) { Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); @@ -2607,13 +2607,13 @@ int CmdCommandStarter( Abc_Frame_t * pAbc, int argc, char ** argv ) } fclose( pFile ); // run commands - Cmd_RunStarter( pFileName, pAbc->sBinary, pCommand, nCores ); + Cmd_RunStarter( pFileName, pAbc->sBinary, pCommand, nCores, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: starter [-N num] [-C cmd] [-vh] \n" ); + Abc_Print( -2, "usage: starter [-P num] [-C cmd] [-vh] \n" ); Abc_Print( -2, "\t runs command lines listed in concurrently on CPUs\n" ); - Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controller [default = %d]\n", nCores ); + Abc_Print( -2, "\t-P num : the number of concurrent jobs including the controller [default = %d]\n", nCores ); Abc_Print( -2, "\t-C cmd : (optional) ABC command line to execute on benchmarks in \n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/cmd/cmdStarter.c b/src/base/cmd/cmdStarter.c index ffb2b7522..bfbe5533d 100644 --- a/src/base/cmd/cmdStarter.c +++ b/src/base/cmd/cmdStarter.c @@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START #ifndef ABC_USE_PTHREADS -void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCores ) {} +void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCores, int fVerbose ) {} #else // pthreads are used @@ -104,7 +104,7 @@ void * Abc_RunThread( void * pCommand ) SeeAlso [] ***********************************************************************/ -void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCores ) +void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCores, int fVerbose ) { FILE * pFile, * pFileTemp; pthread_t * pThreadIds; @@ -204,8 +204,10 @@ void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCor } else BufferCopy = Abc_UtilStrsav( Buffer ); - fprintf( stdout, "Calling: %s\n", (char *)BufferCopy ); - fflush( stdout ); + if ( fVerbose ) { + fprintf( stdout, "Calling: %s\n", (char *)BufferCopy ); + fflush( stdout ); + } // wait till there is an empty thread while ( 1 ) diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index b3ddcd8a1..b6325ea2c 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -283,24 +283,27 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL ); // meanwhile, perform scorr - Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr ); - clkScorr2 = Abc_Clock() - clkStart; - if ( Gia_ManAndNum(pScorr2) == 0 ) - RetValue = 1; - - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); - if ( RetValue == -1 ) + if ( Gia_ManAndNum(pScorr) < 100000 ) { - if ( !fSilent && fVerbose ) { - printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) ); - Abc_PrintTime( 1, "Time", clkScorr2 ); - } - Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL ); + Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr ); + clkScorr2 = Abc_Clock() - clkStart; + if ( Gia_ManAndNum(pScorr2) == 0 ) + RetValue = 1; + + RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + if ( RetValue == -1 ) + { + if ( !fSilent && fVerbose ) { + printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) ); + Abc_PrintTime( 1, "Time", clkScorr2 ); + } + Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL ); - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); - // do something else + RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + // do something else + } + Gia_ManStop( pScorr2 ); } - Gia_ManStop( pScorr2 ); } Gia_ManStop( pScorr ); @@ -312,12 +315,13 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in } if ( !fSilent ) { + printf( "Problem \"%s\" is ", p->pSpec ); if ( RetValue == 0 ) - printf( "Problem is SAT (solved by %d) ", RetEngine ); + printf( "SAT (solved by %d).", RetEngine ); else if ( RetValue == 1 ) - printf( "Problem is UNSAT (solved by %d) ", RetEngine ); + printf( "UNSAT (solved by %d).", RetEngine ); else if ( RetValue == -1 ) - printf( "Problem is UNDECIDED " ); + printf( "UNDECIDED." ); else assert( 0 ); printf( " " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 1b7cab23d..679d30666 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -1040,8 +1040,10 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose ); // print final report - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + if ( !pPars->fSilent ) { + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + } goto finish; } timeLastSolved = Abc_Clock();