diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/pdr/pdrClass.c | 14 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 42 | ||||
-rw-r--r-- | src/proof/pdr/pdrInv.c | 30 | ||||
-rw-r--r-- | src/proof/pdr/pdrMan.c | 4 | ||||
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 8 | ||||
-rw-r--r-- | src/proof/pdr/pdrUtil.c | 7 |
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************************************************************* |