Skip to content

A
abc
Commit 63dab645 by Alan Mishchenko
Options

Replacing printf() by Abc_Print().

parent 448eec77
Showing with 42 additions and 42 deletions
src/aig/gia/giaAbsGla.c
...@@ -142,21 +142,21 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { ...@@ -142,21 +142,21 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
***********************************************************************/ ***********************************************************************/
static inline void Abc_PrintInt( int i ) static inline void Abc_PrintInt( int i )
{ {
printf( " " ); Abc_Print( 1, " " );
if ( i > -1000 && i < 1000 ) if ( i > -1000 && i < 1000 )
printf( " %4d", i ); Abc_Print( 1, " %4d", i );
else if ( i > -10000 && i < 10000 ) else if ( i > -10000 && i < 10000 )
printf( "%4.2fk", (float)i/1000 ); Abc_Print( 1, "%4.2fk", (float)i/1000 );
else if ( i > -100000 && i < 100000 ) else if ( i > -100000 && i < 100000 )
printf( "%4.1fk", (float)i/1000 ); Abc_Print( 1, "%4.1fk", (float)i/1000 );
else if ( i > -1000000 && i < 1000000 ) else if ( i > -1000000 && i < 1000000 )
printf( "%4.0fk", (float)i/1000 ); Abc_Print( 1, "%4.0fk", (float)i/1000 );
else if ( i > -10000000 && i < 10000000 ) else if ( i > -10000000 && i < 10000000 )
printf( "%4.2fm", (float)i/1000000 ); Abc_Print( 1, "%4.2fm", (float)i/1000000 );
else if ( i > -100000000 && i < 100000000 ) else if ( i > -100000000 && i < 100000000 )
printf( "%4.1fm", (float)i/1000000 ); Abc_Print( 1, "%4.1fm", (float)i/1000000 );
else if ( i > -1000000000 && i < 1000000000 ) else if ( i > -1000000000 && i < 1000000000 )
printf( "%4.0fm", (float)i/1000000 ); Abc_Print( 1, "%4.0fm", (float)i/1000000 );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -192,14 +192,14 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi ...@@ -192,14 +192,14 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi
// verify the counter example // verify the counter example
if ( !Gia_ManVerifyCex( p, pCex, 0 ) ) if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
{ {
printf( "Gia_ManCexRemap(): Counter-example is invalid.\n" ); Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
Abc_CexFree( pCex ); Abc_CexFree( pCex );
pCex = NULL; pCex = NULL;
} }
else else
{ {
printf( "Counter-example verification is successful.\n" ); Abc_Print( 1, "Counter-example verification is successful.\n" );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
} }
return pCex; return pCex;
} }
...@@ -230,7 +230,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -230,7 +230,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
int nOnes = 0, Counter = 0; int nOnes = 0, Counter = 0;
if ( p->vGateClasses == NULL ) if ( p->vGateClasses == NULL )
{ {
printf( "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" ); Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
return -1; return -1;
} }
// derive abstraction // derive abstraction
...@@ -239,18 +239,18 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -239,18 +239,18 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
if ( Gia_ManPiNum(pAbs) != pCex->nPis ) if ( Gia_ManPiNum(pAbs) != pCex->nPis )
{ {
printf( "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" ); Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
Gia_ManStop( pAbs ); Gia_ManStop( pAbs );
return -1; return -1;
} }
if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) ) if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
{ {
printf( "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" ); Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
Gia_ManStop( pAbs ); Gia_ManStop( pAbs );
return -1; return -1;
} }
// else // else
// printf( "Gia_ManGlaRefine(): The initial counter-example is correct.\n" ); // Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
// get inputs // get inputs
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL ); Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
...@@ -287,10 +287,10 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -287,10 +287,10 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
if ( Gia_ObjTerSimGet1(pObj) ) if ( Gia_ObjTerSimGet1(pObj) )
{ {
pCexNew = Gia_ManCexRemap( p, pCex, vPis ); pCexNew = Gia_ManCexRemap( p, pCex, vPis );
printf( "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame ); Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
} }
// else // else
// printf( "CEX is not real.\n" ); // Abc_Print( 1, "CEX is not real.\n" );
Gia_ManForEachObj( pAbs, pObj, i ) Gia_ManForEachObj( pAbs, pObj, i )
Gia_ObjTerSimSetC( pObj ); Gia_ObjTerSimSetC( pObj );
if ( pCexNew == NULL ) if ( pCexNew == NULL )
...@@ -303,7 +303,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -303,7 +303,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
} }
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Additional objects = %d. ", Vec_IntSize(vPPis) ); Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
} }
...@@ -315,7 +315,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -315,7 +315,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose ); pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
if ( pCare == NULL ) if ( pCare == NULL )
printf( "Counter-example minimization has failed.\n" ); Abc_Print( 1, "Counter-example minimization has failed.\n" );
// add new objects to the map // add new objects to the map
iObjId = -1; iObjId = -1;
for ( f = 0; f <= pCare->iFrame; f++ ) for ( f = 0; f <= pCare->iFrame; f++ )
...@@ -330,21 +330,21 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -330,21 +330,21 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
continue; continue;
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 ); assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 ); Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
// printf( "Adding object %d.\n", iObjId ); // Abc_Print( 1, "Adding object %d.\n", iObjId );
// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) ); // Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
Counter++; Counter++;
} }
Abc_CexFree( pCare ); Abc_CexFree( pCare );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Essential bits = %d. Additional objects = %d. ", nOnes, Counter ); Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
// consider the case of SAT // consider the case of SAT
if ( iObjId == -1 ) if ( iObjId == -1 )
{ {
pCexNew = Gia_ManCexRemap( p, pCex, vPis ); pCexNew = Gia_ManCexRemap( p, pCex, vPis );
printf( "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame ); Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
} }
} }
Vec_IntFree( vPis ); Vec_IntFree( vPis );
...@@ -663,7 +663,7 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi ...@@ -663,7 +663,7 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi
} }
pObj = Gia_ManPo( p->pGia, 0 ); pObj = Gia_ManPo( p->pGia, 0 );
if ( !Gia_ObjTerSimGet1(pObj) ) if ( !Gia_ObjTerSimGet1(pObj) )
printf( "\nRefinement verification has failed!!!\n" ); Abc_Print( 1, "\nRefinement verification has failed!!!\n" );
// clear // clear
Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) ); Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
...@@ -709,19 +709,19 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) ...@@ -709,19 +709,19 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// check how many pseudo PIs have variables // check how many pseudo PIs have variables
Gla_ManForEachObjAbsVec( vPis, p, pGla, i ) Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
{ {
printf( " %5d : ", Gla_ObjId(p, pGla) ); Abc_Print( 1, " %5d : ", Gla_ObjId(p, pGla) );
for ( f = 0; f <= p->pPars->iFrame; f++ ) for ( f = 0; f <= p->pPars->iFrame; f++ )
printf( "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) ); Abc_Print( 1, "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) );
printf( "\n" ); Abc_Print( 1, "\n" );
} }
// check how many pseudo PIs have variables // check how many pseudo PIs have variables
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i ) Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
{ {
printf( "%5d : ", Gla_ObjId(p, pGla) ); Abc_Print( 1, "%5d : ", Gla_ObjId(p, pGla) );
for ( f = 0; f <= p->pPars->iFrame; f++ ) for ( f = 0; f <= p->pPars->iFrame; f++ )
printf( "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) ); Abc_Print( 1, "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) );
printf( "\n" ); Abc_Print( 1, "\n" );
} }
*/ */
// propagate values // propagate values
...@@ -785,7 +785,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) ...@@ -785,7 +785,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) && Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) &&
(int)pRef->Value != Gla_ObjSatValue(p, Gia_ObjId(p->pGia, pObj), f) ) (int)pRef->Value != Gla_ObjSatValue(p, Gia_ObjId(p->pGia, pObj), f) )
{ {
printf( "Object has value mismatch " ); Abc_Print( 1, "Object has value mismatch " );
Gia_ObjPrint( p->pGia, pObj ); Gia_ObjPrint( p->pGia, pObj );
} }
...@@ -816,7 +816,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) ...@@ -816,7 +816,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pObj = Gia_ManPo( p->pGia, 0 ); pObj = Gia_ManPo( p->pGia, 0 );
pRef = Gla_ObjRef( p, pObj, p->pPars->iFrame ); pRef = Gla_ObjRef( p, pObj, p->pPars->iFrame );
if ( pRef->Value != 1 ) if ( pRef->Value != 1 )
printf( "\nCounter-example verification has failed!!!\n" ); Abc_Print( 1, "\nCounter-example verification has failed!!!\n" );
// check the CEX // check the CEX
if ( pRef->Prio == 0 ) if ( pRef->Prio == 0 )
......
src/aig/gia/giaAbsVta.c
...@@ -148,21 +148,21 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); ...@@ -148,21 +148,21 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
***********************************************************************/ ***********************************************************************/
static inline void Abc_PrintInt( int i ) static inline void Abc_PrintInt( int i )
{ {
printf( " " ); Abc_Print( 1, " " );
if ( i > -1000 && i < 1000 ) if ( i > -1000 && i < 1000 )
printf( " %4d", i ); Abc_Print( 1, " %4d", i );
else if ( i > -10000 && i < 10000 ) else if ( i > -10000 && i < 10000 )
printf( "%4.2fk", (float)i/1000 ); Abc_Print( 1, "%4.2fk", (float)i/1000 );
else if ( i > -100000 && i < 100000 ) else if ( i > -100000 && i < 100000 )
printf( "%4.1fk", (float)i/1000 ); Abc_Print( 1, "%4.1fk", (float)i/1000 );
else if ( i > -1000000 && i < 1000000 ) else if ( i > -1000000 && i < 1000000 )
printf( "%4.0fk", (float)i/1000 ); Abc_Print( 1, "%4.0fk", (float)i/1000 );
else if ( i > -10000000 && i < 10000000 ) else if ( i > -10000000 && i < 10000000 )
printf( "%4.2fm", (float)i/1000000 ); Abc_Print( 1, "%4.2fm", (float)i/1000000 );
else if ( i > -100000000 && i < 100000000 ) else if ( i > -100000000 && i < 100000000 )
printf( "%4.1fm", (float)i/1000000 ); Abc_Print( 1, "%4.1fm", (float)i/1000000 );
else if ( i > -1000000000 && i < 1000000000 ) else if ( i > -1000000000 && i < 1000000000 )
printf( "%4.0fm", (float)i/1000000 ); Abc_Print( 1, "%4.0fm", (float)i/1000000 );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -621,8 +621,8 @@ void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd ) ...@@ -621,8 +621,8 @@ void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd )
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i ) Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
pCounters[pThis->iFrame]++; pCounters[pThis->iFrame]++;
for ( i = 0; i <= p->pPars->iFrame; i++ ) for ( i = 0; i <= p->pPars->iFrame; i++ )
printf( "%2d", pCounters[i] ); Abc_Print( 1, "%2d", pCounters[i] );
printf( "***\n" ); Abc_Print( 1, "***\n" );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/base/main/main.c
...@@ -219,7 +219,7 @@ int Abc_RealMain( int argc, char * argv[] ) ...@@ -219,7 +219,7 @@ int Abc_RealMain( int argc, char * argv[] )
pAbc->pGia = Gia_ManFromBridge( stdin, NULL ); pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
} }
else if ( fBatch && sCommandUsr[0] ) else if ( fBatch && sCommandUsr[0] )
printf( "ABC command line: \"%s\".\n", sCommandUsr ); Abc_Print( 1, "ABC command line: \"%s\".\n", sCommandUsr );
if ( fBatch ) if ( fBatch )
{ {
......
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