Skip to content

A
abc
Commit c47dc99a by Alan Mishchenko
Options

Redirecting printf messages.

parent 4db9c636
Showing with 56 additions and 73 deletions
src/misc/util/abc_global.h
......@@ -200,12 +200,12 @@ typedef ABC_UINT64_T word;
#define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; }
#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTr(a,t) (printf("%s = ", (a)), printf("%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
#define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.3f Mb ", 1.0*(f)/(1<<20)))
#define ABC_PRMP(a,f,F) (printf("%s = ", (a)), printf("%7.3f Mb (%6.2f %%) ", (1.0*(f)/(1<<20)), ((F)? 100.0*(f)/(F) : 0.0) ) )
#define ABC_PRT(a,t) (Abc_Print(1, "%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTr(a,t) (Abc_Print(1, "%s = ", (a)), printf("%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTn(a,t) (Abc_Print(1, "%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTP(a,t,T) (Abc_Print(1, "%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
#define ABC_PRM(a,f) (Abc_Print(1, "%s = ", (a)), printf("%7.3f Mb ", 1.0*(f)/(1<<20)))
#define ABC_PRMP(a,f,F) (Abc_Print(1, "%s = ", (a)), printf("%7.3f Mb (%6.2f %%) ", (1.0*(f)/(1<<20)), ((F)? 100.0*(f)/(F) : 0.0) ) )
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#define ABC_CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
......@@ -280,28 +280,16 @@ static inline void Abc_Print( int level, const char * format, ... )
static inline void Abc_PrintTime( int level, const char * pStr, int time )
{
if ( level == ABC_ERROR )
printf( "Error: " );
else if ( level == ABC_WARNING )
printf( "Warning: " );
ABC_PRT( pStr, time );
}
static inline void Abc_PrintTimeP( int level, const char * pStr, int time, int Time )
{
if ( level == ABC_ERROR )
printf( "Error: " );
else if ( level == ABC_WARNING )
printf( "Warning: " );
ABC_PRTP( pStr, time, Time );
}
static inline void Abc_PrintMemoryP( int level, const char * pStr, int time, int Time )
{
if ( level == ABC_ERROR )
printf( "Error: " );
else if ( level == ABC_WARNING )
printf( "Warning: " );
ABC_PRMP( pStr, time, Time );
}
......
src/proof/pdr/pdrClass.c
......@@ -148,11 +148,11 @@ void Pdr_ManPrintMap( Vec_Int_t * vMap )
{
Vec_Int_t * vMarks;
int f, i, iClass, Entry, Counter = 0;
printf( " Consts: " );
Abc_Print( 1, " Consts: " );
Vec_IntForEachEntry( vMap, Entry, i )
if ( Entry == -1 )
printf( "%d ", i );
printf( "\n" );
Abc_Print( 1, "%d ", i );
Abc_Print( 1, "\n" );
vMarks = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vMap, iClass, f )
{
......@@ -165,11 +165,11 @@ void Pdr_ManPrintMap( Vec_Int_t * vMap )
continue;
Vec_IntPush( vMarks, iClass );
// print class
printf( " Class %d : ", iClass );
Abc_Print( 1, " Class %d : ", iClass );
Vec_IntForEachEntry( vMap, Entry, i )
if ( Entry == iClass )
printf( "%d ", i );
printf( "\n" );
Abc_Print( 1, "%d ", i );
Abc_Print( 1, "\n" );
}
Vec_IntFree( vMarks );
}
......@@ -200,7 +200,7 @@ void Pdr_ManEquivClasses( Aig_Man_t * pAig )
// implement variable map
pTemp = Pdr_ManRehashWithMap( pAig, vMap );
// report the result
printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n",
Abc_Print( 1, "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n",
f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap),
Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
// recreate the map
......
src/proof/pdr/pdrCore.c
......@@ -162,7 +162,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
if ( pCubeMin != NULL )
{
// printf( "%d ", pCubeK->nLits - pCubeMin->nLits );
// Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
Pdr_SetDeref( pCubeK );
pCubeK = pCubeMin;
}
......@@ -201,11 +201,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
continue;
/*
printf( "===\n" );
Abc_Print( 1, "===\n" );
Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
printf( "\n" );
Abc_Print( 1, "\n" );
Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
printf( "\n" );
Abc_Print( 1, "\n" );
*/
Pdr_SetDeref( pTemp );
Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
......@@ -273,8 +273,8 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
}
/*
for ( i = 0; i < pCube->nLits; i++ )
printf( "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
printf( "\n" );
Abc_Print( 1, "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
Abc_Print( 1, "\n" );
*/
return pArray;
}
......@@ -486,9 +486,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
// add new clause
if ( p->pPars->fVeryVerbose )
{
printf( "Adding cube " );
Abc_Print( 1, "Adding cube " );
Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
printf( " to frame %d.\n", k );
Abc_Print( 1, " to frame %d.\n", k );
}
// set priority flops
for ( i = 0; i < pCubeMin->nLits; i++ )
......@@ -564,7 +564,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
p->pPars->iFrame = k;
return -1;
}
......@@ -575,7 +575,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
p->pPars->iFrame = k;
return -1;
}
......@@ -583,7 +583,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( fPrintClauses )
{
printf( "*** Clauses after frame %d:\n", k );
Abc_Print( 1, "*** Clauses after frame %d:\n", k );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
......@@ -605,7 +605,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManCreateSolver( p, ++k );
if ( fPrintClauses )
{
printf( "*** Clauses after frame %d:\n", k );
Abc_Print( 1, "*** Clauses after frame %d:\n", k );
Pdr_ManPrintClauses( p, 0 );
}
// push clauses into this timeframe
......@@ -614,7 +614,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
p->pPars->iFrame = k;
return -1;
}
......@@ -637,12 +637,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( fPrintClauses )
{
printf( "*** Clauses after frame %d:\n", k );
Abc_Print( 1, "*** Clauses after frame %d:\n", k );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
printf( "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
p->pPars->iFrame = k;
return -1;
}
......@@ -650,7 +650,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
p->pPars->iFrame = k;
return -1;
}
......@@ -681,7 +681,7 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
// if ( *ppCex && pPars->fVerbose )
// printf( "Found counter-example in frame %d after exploring %d frames.\n",
// Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n",
// (*ppCex)->iFrame, p->nFrames );
p->tTotal += clock() - clk;
if ( pvPrioInit )
......@@ -706,12 +706,12 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
***********************************************************************/
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
{
// printf( "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
printf( "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ",
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ",
pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
if ( pPars->iOutput >= 0 )
printf( "Output = %d. ", pPars->iOutput );
printf( "MonoCNF = %s. SkipGen = %s.\n",
Abc_Print( 1, "Output = %d. ", pPars->iOutput );
Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n",
pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
/*
......
src/proof/pdr/pdrInv.c
......@@ -56,11 +56,11 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
// determine the starting point
LengthStart = Abc_MaxInt( 0, Length - 60 );
printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 );
ThisSize = 5;
if ( LengthStart > 0 )
{
printf( " ..." );
Abc_Print( 1, " ..." );
ThisSize += 4;
}
Length = 0;
......@@ -71,13 +71,13 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
continue;
}
printf( " %d", Vec_PtrSize(vVec) );
Abc_Print( 1, " %d", Vec_PtrSize(vVec) );
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
}
for ( i = ThisSize; i < 70; i++ )
printf( " " );
printf( "%6d", p->nQueMax );
Abc_Print( 1, " " );
Abc_Print( 1, "%6d", p->nQueMax );
printf(" %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
printf("%s", fClose ? "\n":"\r" );
if ( fClose )
......@@ -130,7 +130,7 @@ int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
return k;
// return -1;
// if there is no starting point (as in case of SAT or undecided), return the last frame
// printf( "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
// Abc_Print( 1, "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
return kMax;
}
......@@ -204,9 +204,9 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
printf( "C=%4d. F=%4d ", Counter++, k );
Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
printf( "\n" );
Abc_Print( 1, "\n" );
}
}
}
......@@ -235,7 +235,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing invariant.\n", pFileName );
Abc_Print( 1, "Cannot open file \"%s\" for writing invariant.\n", pFileName );
return;
}
// collect cubes
......@@ -276,9 +276,9 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
Vec_IntFreeP( &vFlopCounts );
Vec_PtrFree( vCubes );
if ( fProved )
printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
Abc_Print( 1, "Inductive invariant was written into file \"%s\".\n", pFileName );
else
printf( "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
}
......@@ -298,7 +298,7 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p )
Vec_Ptr_t * vCubes;
int kStart = Pdr_ManFindInvariantStart( p );
vCubes = Pdr_ManCollectCubes( p, kStart );
printf( "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
Vec_PtrFree( vCubes );
}
......@@ -344,15 +344,15 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
if ( RetValue != l_False )
{
printf( "Verification of clause %d failed.\n", i );
Abc_Print( 1, "Verification of clause %d failed.\n", i );
Counter++;
}
}
if ( Counter )
printf( "Verification of %d clauses has failed.\n", Counter );
Abc_Print( 1, "Verification of %d clauses has failed.\n", Counter );
else
{
printf( "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
Abc_Print( 1, "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// sat_solver_delete( pSat );
......
src/proof/pdr/pdrMan.c
......@@ -95,7 +95,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
Aig_ManCleanMarkAB( p->pAig );
if ( p->pPars->fVerbose )
{
printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
......@@ -107,7 +107,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
}
// printf( "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
// Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
sat_solver_delete( pSat );
Vec_PtrFree( p->vSolvers );
......
src/proof/pdr/pdrTsim.c
......@@ -327,7 +327,7 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
if ( vCi2Rem )
Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
pBuff[Aig_ObjPioNum(pObj)] = 'x';
printf( "%s\n", pBuff );
Abc_Print( 1, "%s\n", pBuff );
ABC_FREE( pBuff );
}
......@@ -381,12 +381,12 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
}
if ( p->pPars->fVeryVerbose )
{
printf( "Trying to justify cube " );
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
else
printf( "<prop=fail>" );
printf( " in frame %d.\n", k );
Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
// collect CI objects
......
src/proof/pdr/pdrUtil.c
......@@ -78,11 +78,6 @@ Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
p->Sign |= ((word)1 << (p->Lits[i] % 63));
}
Vec_IntSelectSort( p->Lits, p->nLits );
/*
for ( i = 0; i < p->nLits; i++ )
printf( "%d ", p->Lits[i] );
printf( "\n" );
*/
// remember PI literals
for ( i = p->nLits; i < p->nTotal; i++ )
p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
......@@ -549,7 +544,7 @@ void Pdr_QueuePrint( Pdr_Man_t * p )
{
Pdr_Obl_t * pObl;
for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
printf( "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
Abc_Print( 1, "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
}
/**Function*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment