summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-03-02 01:06:53 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-03-02 01:06:53 -0800
commit4db9c63627301329530465ea459588a98411f79b (patch)
tree8c448e00423ca73c0dfbb1669a383ffe95dc012a /src
parent7926d75ecb4ffd4441bea0c2d731e5b533534ee3 (diff)
downloadabc-4db9c63627301329530465ea459588a98411f79b.tar.gz
abc-4db9c63627301329530465ea459588a98411f79b.tar.bz2
abc-4db9c63627301329530465ea459588a98411f79b.zip
Redirecting printf messages.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaAbsVta.c92
1 files changed, 42 insertions, 50 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 87eb5e6c..cb2dfa23 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -466,9 +466,7 @@ void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore )
pThis = Vta_ManObj( p, Entry );
Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
Vec_IntWriteEntry( vCore, i, Entry );
-//printf( "%d^%d ", pThis->iObj, pThis->iFrame );
}
-//printf( "\n" );
}
/**Function*************************************************************
@@ -746,7 +744,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis->Prio = Counter++;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
pThis->Prio = Counter++;
-// printf( "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
+// Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
Vec_PtrFree( vTermsUsed );
Vec_PtrFree( vTermsUnused );
@@ -908,7 +906,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
-// printf( "AND %d %d %d ", Vta_ObjId(p, pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Value = VTA_VAR1;
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
@@ -929,30 +926,26 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis->Value = VTA_VAR1;
else
pThis->Value = VTA_VARX;
-// printf( "RO %d ", Vta_ObjId(p, pThis), Vta_ObjId(p,pThis0) );
}
else
{
-// printf( "RO %d frame0 ", Vta_ObjId(p, pThis) );
pThis->Value = VTA_VAR0;
}
}
else if ( Gia_ObjIsConst0(pObj) )
{
-// printf( "CONST0 %d ", Vta_ObjId(p, pThis) );
pThis->Value = VTA_VAR0;
}
else assert( 0 );
-// printf( "val = %d. \n", (pThis->Value==VTA_VAR0) ? 0 : ((pThis->Value==VTA_VAR0) ? 1 : 2 ) );
// double check the solver
assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
}
// check the output
if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
- printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
+ Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
// else
-// printf( "Verification OK.\n" );
+// Abc_Print( 1, "Verification OK.\n" );
}
@@ -1013,12 +1006,12 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
// update parameters
if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) )
{
- printf( "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) );
+ Abc_Print( 1, "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) );
pPars->nFramesStart = Vec_PtrSize(p->vFrames);
}
if ( pPars->nFramesMax && pPars->nFramesMax < pPars->nFramesStart )
{
- printf( "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart );
+ Abc_Print( 1, "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart );
pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart );
}
}
@@ -1044,7 +1037,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
void Vga_ManStop( Vta_Man_t * p )
{
// if ( p->pPars->fVerbose )
- printf( "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n",
+ Abc_Print( 1, "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
@@ -1097,8 +1090,8 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
}
if ( fVerbose )
{
-// printf( "%6d", (int)pSat->stats.conflicts - nConfPrev );
-// printf( "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
+// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
+// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
assert( RetValue == l_False );
@@ -1108,7 +1101,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( fVerbose )
{
-// printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
+// Abc_Print( 1, "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
@@ -1128,7 +1121,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
Vec_IntFree( vPres );
if ( fVerbose )
{
-// printf( "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
+// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
return vCore;
@@ -1177,43 +1170,43 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nC
}
}
}
-// printf( "%5d%5d", pCountAll[0], pCountUni[0] );
- printf( "%3d :", nFrames-1 );
- printf( "%6d", p->nSeenGla );
- printf( "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
- printf( "%8d", nConfls );
+// Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
+ Abc_Print( 1, "%3d :", nFrames-1 );
+ Abc_Print( 1, "%6d", p->nSeenGla );
+ Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
+ Abc_Print( 1, "%8d", nConfls );
if ( nCexes == 0 )
- printf( "%5c", '-' );
+ Abc_Print( 1, "%5c", '-' );
else
- printf( "%5d", nCexes );
+ Abc_Print( 1, "%5d", nCexes );
if ( vCore == NULL )
{
- printf( " ..." );
+ Abc_Print( 1, " ..." );
for ( k = 0; k < 10; k++ )
- printf( " " );
- printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
- printf( "\r" );
+ Abc_Print( 1, " " );
+ Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+ Abc_Print( 1, "\r" );
}
else
{
- printf( "%7d", pCountAll[0] );
+ Abc_Print( 1, "%7d", pCountAll[0] );
if ( nFrames > 10 )
{
for ( k = 0; k < 4; k++ )
- printf( "%5d", pCountAll[k+1] );
- printf( " ..." );
+ Abc_Print( 1, "%5d", pCountAll[k+1] );
+ Abc_Print( 1, " ..." );
for ( k = nFrames-5; k < nFrames; k++ )
- printf( "%5d", pCountAll[k+1] );
+ Abc_Print( 1, "%5d", pCountAll[k+1] );
}
else
{
for ( k = 0; k < nFrames; k++ )
- printf( "%5d", pCountAll[k+1] );
+ Abc_Print( 1, "%5d", pCountAll[k+1] );
for ( k = nFrames; k < 10; k++ )
- printf( " " );
+ Abc_Print( 1, " " );
}
- printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
- printf( "\n" );
+ Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+ Abc_Print( 1, "\n" );
}
fflush( stdout );
@@ -1309,7 +1302,6 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
Vec_IntForEachEntry( vOne, Entry, i )
Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
sat_solver2_simplify( p->pSat );
-// printf( "\n\n" );
}
/**Function*************************************************************
@@ -1349,9 +1341,9 @@ void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift )
{
iObj = (Entry & p->nObjMask);
iFrame = (Entry >> p->nObjBits);
- printf( "%d*%d ", iObj, iFrame+Lift );
+ Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift );
}
- printf( "\n" );
+ Abc_Print( 1, "\n" );
}
/**Function*************************************************************
@@ -1414,11 +1406,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// perform initial abstraction
if ( p->pPars->fVerbose )
{
- printf( "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
- printf( "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
+ Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
+ Abc_Print( 1, "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax,
p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
- printf( "Frame Abs %% Confl Cex Core F0 F1 F2 F3 ...\n" );
+ Abc_Print( 1, "Frame Abs %% Confl Cex Core F0 F1 F2 F3 ...\n" );
}
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
@@ -1522,30 +1514,30 @@ finish:
{
assert( Vec_PtrSize(p->vCores) > 0 );
if ( pAig->vObjClasses != NULL )
- printf( "Replacing the old abstraction by a new one.\n" );
+ Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
Vec_IntFreeP( &pAig->vObjClasses );
pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit )
- printf( "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
+ Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
- printf( "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
+ Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
- printf( "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
+ Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
- printf( "Abstraction stopped for unknown reason in frame %d. ", f );
+ Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
- printf( "SAT solver completed %d frames and produced an abstraction. ", f );
+ Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
}
else
{
ABC_FREE( p->pGia->pCexSeq );
p->pGia->pCexSeq = pCex;
if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
- printf( " Gia_VtaPerform(): CEX verification has failed!\n" );
- printf( "Counter-example detected in frame %d. ", f );
+ Abc_Print( 1, " Gia_VtaPerform(): CEX verification has failed!\n" );
+ Abc_Print( 1, "Counter-example detected in frame %d. ", f );
p->pPars->iFrame = pCex->iFrame - 1;
}
Abc_PrintTime( 1, "Time", clock() - clk );