Redirecting printf messages.

6 files changed, 50 insertions, 55 deletions

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*************************************************************