luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Printout changes.

This commit is contained in:
Alan Mishchenko 2023-10-23 10:48:43 -07:00
parent 538ecb4515
commit 76e8d21aaf
4 changed files with 39 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/base/cmd/cmd.c
View File

@ -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] <file>\n" );
Abc_Print( -2, "usage: starter [-P num] [-C cmd] [-vh] <file>\n" );
Abc_Print( -2, "\t runs command lines listed in <file> concurrently on <num> 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 <file>\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");

10
src/base/cmd/cmdStarter.c
View File

@ -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 )

40
src/proof/cec/cecProve.c
View File

@ -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 );

6
src/proof/ssw/sswRarity.c
View File

@ -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();