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

Making 'pdr', &gla, &vta print correctly in batch mode.

This commit is contained in:
Alan Mishchenko 2012-07-07 10:44:34 -07:00
parent 31d85e732b
commit 8b881d235a
10 changed files with 35 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/gia/giaAbsGla.c
View File

@ -1618,6 +1618,8 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
***********************************************************************/
void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time )
{
if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
return;
Abc_Print( 1, "%3d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
@ -1820,7 +1822,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break;
}
}
}
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );

3
src/aig/gia/giaAbsVta.c
View File

@ -1226,6 +1226,9 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
return fChanges;
}
if ( Abc_FrameIsBatchMode() && !vCore )
return fChanges;
// Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
Abc_Print( 1, "%3d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) );

3
src/aig/gia/giaMan.c
View File

@ -412,7 +412,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
printf( " and =%8d", Gia_ManAndNum(p) );
printf( " lev =%5d", Gia_ManLevelNum(p) );
printf( " cut =%5d", Gia_ManCrossCut(p) );
printf( " mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
printf( " mem =%5.2f Mb", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
// printf( " mem =%5.2f Mb", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
if ( Gia_ManHasDangling(p) )
printf( " ch =%5d", Gia_ManEquivCountClasses(p) );
if ( fSwitch )

1
src/base/main/main.h
View File

@ -104,6 +104,7 @@ extern ABC_DLL void * Abc_FrameReadManDd();
extern ABC_DLL void * Abc_FrameReadManDec();
extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag );
extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag );
extern ABC_DLL int Abc_FrameIsBatchMode();
extern ABC_DLL int Abc_FrameIsBridgeMode();
extern ABC_DLL void Abc_FrameSetBridgeMode();

2
src/base/main/mainFrame.c
View File

@ -79,6 +79,8 @@ void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateVal
void Abc_FrameSetCex( Abc_Cex_t * pCex ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; }
void Abc_FrameSetNFrames( int nFrames ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->nFrames = nFrames; }
int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; }
int Abc_FrameIsBridgeMode() { return s_GlobalFrame ? s_GlobalFrame->fBridgeMode : 0; }
void Abc_FrameSetBridgeMode() { if ( s_GlobalFrame ) s_GlobalFrame->fBridgeMode = 1; }

4
src/base/main/mainInt.h
View File

@ -69,8 +69,8 @@ struct Abc_Frame_t_
Abc_Ntk_t * pNtkBestArea; // the current network
int nSteps; // the counter of different network processed
int fAutoexac; // marks the autoexec mode
int fBatchMode; // are we invoked in batch mode?
int fBridgeMode; // are we invoked in bridge mode?
int fBatchMode; // batch mode flag
int fBridgeMode; // bridge mode flag
// output streams
FILE * Out;
FILE * Err;

10
src/misc/bar/bar.c
View File

@ -144,7 +144,10 @@ void Bar_ProgressStop( Bar_Progress_t * p )
void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
{
int i;
if ( p == NULL ) return;
if ( p == NULL )
return;
if ( Abc_FrameIsBatchMode() )
return;
if ( pString )
fprintf( p->pFile, "%s ", pString );
for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
@ -171,7 +174,10 @@ void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
void Bar_ProgressClean( Bar_Progress_t * p )
{
int i;
if ( p == NULL ) return;
if ( p == NULL )
return;
if ( Abc_FrameIsBatchMode() )
return;
for ( i = 0; i <= p->posTotal; i++ )
fprintf( p->pFile, " " );
fprintf( p->pFile, "\r" );

10
src/misc/extra/extraUtilProgress.c
View File

@ -136,7 +136,10 @@ void Extra_ProgressBarStop( ProgressBar * p )
void Extra_ProgressBarShow( ProgressBar * p, char * pString )
{
int i;
if ( p == NULL ) return;
if ( p == NULL )
return;
if ( Abc_FrameIsBatchMode() )
return;
if ( pString )
fprintf( p->pFile, "%s ", pString );
for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
@ -163,7 +166,10 @@ void Extra_ProgressBarShow( ProgressBar * p, char * pString )
void Extra_ProgressBarClean( ProgressBar * p )
{
int i;
if ( p == NULL ) return;
if ( p == NULL )
return;
if ( Abc_FrameIsBatchMode() )
return;
for ( i = 0; i <= p->posTotal; i++ )
fprintf( p->pFile, " " );
fprintf( p->pFile, "\r" );

4
src/proof/pdr/pdrInv.c
View File

@ -50,6 +50,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 )
return;
if ( Abc_FrameIsBatchMode() && !fClose )
return;
// count the total length of the printout
Length = 0;
Vec_VecForEachLevel( p->vClauses, vVec, i )
@ -78,7 +80,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
for ( i = ThisSize; i < 70; i++ )
Abc_Print( 1, " " );
Abc_Print( 1, "%6d", p->nQueMax );
Abc_Print( 1, " %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%s", fClose ? "\n":"\r" );
if ( fClose )
p->nQueMax = 0;

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

@ -20,6 +20,7 @@
#include "sswInt.h"
#include "src/aig/gia/giaAig.h"
#include "src/base/main/main.h"
ABC_NAMESPACE_IMPL_START
@ -1074,7 +1075,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( !fVerbose )
printf( "\r" );
printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
Ssw_RarManPrepareRandom( nRandSeed );
Abc_CexFree( pAig->pSeqModel );
@ -1108,7 +1109,7 @@ finish:
if ( r == nRounds && f == nFrames )
{
if ( !fVerbose )
printf( "\r" );
printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}