From c47dc99a9402b57762073a786ac71027509a537b Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 2 Mar 2012 01:15:40 -0800
Subject: Redirecting printf messages.
---
src/proof/pdr/pdrClass.c | 14 +++++++-------
src/proof/pdr/pdrCore.c | 42 +++++++++++++++++++++---------------------
src/proof/pdr/pdrInv.c | 30 +++++++++++++++---------------
src/proof/pdr/pdrMan.c | 4 ++--
src/proof/pdr/pdrTsim.c | 8 ++++----
src/proof/pdr/pdrUtil.c | 7 +------
6 files changed, 50 insertions(+), 55 deletions(-)
(limited to 'src/proof')
diff --git a/src/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c
index 519384c5..4b28c196 100644
--- a/src/proof/pdr/pdrClass.c
+++ b/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
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 02cb4876..3cf47a92 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/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" );
/*
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 92bd6d00..1cb18afd 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/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 );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 33c94d40..73c12a7d 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/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 );
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 32843489..428c20c7 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/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
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index c0570988..97261a7f 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/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*************************************************************
--
cgit v1.2.3