diff options
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 123 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 21 |
2 files changed, 101 insertions, 43 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index e4741b29..fe5a8c36 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -146,10 +146,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) { memset( p, 0, sizeof(Gia_ParVta_t) ); p->nFramesStart = 5; // starting frame - p->nFramesMax = 10; // maximum frames - p->nFramesOver = 3; // overlap frames + p->nFramesOver = 2; // overlap frames + p->nFramesMax = 0; // maximum frames p->nConfLimit = 0; // conflict limit - p->nTimeOut = 60; // timeout in seconds + p->nTimeOut = 0; // timeout in seconds p->fUseTermVars = 0; // use terminal variables p->fVerbose = 0; // verbose flag p->iFrame = -1; // the number of frames covered @@ -1138,48 +1138,78 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat SeeAlso [] ***********************************************************************/ -void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCexes, int fVerbose ) +void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, int Time ) { unsigned * pInfo; int * pCountAll, * pCountUni; int i, k, iFrame, iObj, Entry; // print info about frames - pCountAll = ABC_CALLOC( int, nFrames + 1 ); - pCountUni = ABC_CALLOC( int, nFrames + 1 ); - Vec_IntForEachEntry( vCore, Entry, i ) + if ( vCore ) { - iObj = (Entry & p->nObjMask); - iFrame = (Entry >> p->nObjBits); - assert( iFrame < nFrames ); - pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj ); - if ( !Abc_InfoHasBit(pInfo, iFrame) ) - { - Abc_InfoSetBit( pInfo, iFrame ); - pCountUni[iFrame+1]++; - pCountUni[0]++; - } - pCountAll[iFrame+1]++; - pCountAll[0]++; - if ( !Vec_BitEntry(p->vSeenGla, iObj) ) + pCountAll = ABC_CALLOC( int, nFrames + 1 ); + pCountUni = ABC_CALLOC( int, nFrames + 1 ); + Vec_IntForEachEntry( vCore, Entry, i ) { - Vec_BitWriteEntry(p->vSeenGla, iObj, 1); - p->nSeenGla++; + iObj = (Entry & p->nObjMask); + iFrame = (Entry >> p->nObjBits); + assert( iFrame < nFrames ); + pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj ); + if ( !Abc_InfoHasBit(pInfo, iFrame) ) + { + Abc_InfoSetBit( pInfo, iFrame ); + pCountUni[iFrame+1]++; + pCountUni[0]++; + } + pCountAll[iFrame+1]++; + pCountAll[0]++; + if ( !Vec_BitEntry(p->vSeenGla, iObj) ) + { + Vec_BitWriteEntry(p->vSeenGla, iObj, 1); + p->nSeenGla++; + } } } - if ( fVerbose ) +// printf( "%5d%5d", pCountAll[0], pCountUni[0] ); + printf( "%3d :", nFrames-1 ); + printf( "%6d", p->nSeenGla ); + printf( "%8d", nConfls ); + printf( "%5d", nCexes ); + if ( vCore == NULL ) + { + printf( " ..." ); + for ( k = 0; k < 10; k++ ) + printf( " " ); + printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) ); + printf( "\r" ); + } + else { - // printf( "%5d%5d", pCountAll[0], pCountUni[0] ); - printf( "%6d", p->nSeenGla ); - printf( "%5d", nCexes ); printf( "%7d", pCountAll[0] ); - for ( k = 0; k < nFrames; k++ ) - // printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); - printf( "%5d", pCountAll[k+1] ); + if ( nFrames > 10 ) + { + for ( k = 0; k < 4; k++ ) + printf( "%5d", pCountAll[k+1] ); + printf( " ..." ); + for ( k = nFrames-5; k < nFrames; k++ ) + printf( "%5d", pCountAll[k+1] ); + } + else + { + for ( k = 0; k < nFrames; k++ ) + printf( "%5d", pCountAll[k+1] ); + for ( k = nFrames; k < 10; k++ ) + printf( " " ); + } + printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) ); printf( "\n" ); - fflush( stdout ); } - ABC_FREE( pCountAll ); - ABC_FREE( pCountUni ); + fflush( stdout ); + + if ( vCore ) + { + ABC_FREE( pCountAll ); + ABC_FREE( pCountUni ); + } } /**Function************************************************************* @@ -1364,13 +1394,19 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); // start the manager p = Vga_ManStart( pAig, pPars ); + // set runtime limit + if ( p->pPars->nTimeOut ) + sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); // perform initial abstraction if ( p->pPars->fVerbose ) - printf( "Frame Confl One Cex All F0 F1 F2 F3 ...\n" ); + { + printf( "Running VTA with FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d.\n", + p->pPars->nFramesStart, p->pPars->nFramesOver, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut ); + printf( "Frame Abs Confl Cex Core F0 F1 F2 F3 ...\n" ); + } for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) { - if ( p->pPars->fVerbose ) - printf( "%3d :", f ); + int nConflsBeg = sat_solver2_nconflicts(p->pSat); p->pPars->iFrame = f; // realloc storage for abstraction marks if ( f == p->nWords * 32 ) @@ -1413,6 +1449,9 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) p->timeCex += clock() - clk2; if ( pCex != NULL ) goto finish; + // print the result + if ( p->pPars->fVerbose ) + Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); } assert( Status == 1 ); // valid core is obtained @@ -1431,8 +1470,6 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) clk2 = clock(); vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); p->timeUnsat += clock() - clk2; - if ( p->pPars->fVerbose ) - printf( "%6d", nConfls ); assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached break; @@ -1450,7 +1487,8 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Vec_IntSort( vCore, 1 ); Vec_PtrPush( p->vCores, vCore ); // print the result - Vta_ManAbsPrintFrame( p, vCore, f+1, i, p->pPars->fVerbose ); + if ( p->pPars->fVerbose ) + Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); } finish: // analize the results @@ -1462,7 +1500,14 @@ finish: Vec_IntFreeP( &pAig->vObjClasses ); pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); if ( Status == -1 ) - printf( "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); + { + 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 ); + 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 ); + else + printf( "SAT solver ran out of resources in frame %d. ", f ); + } else printf( "SAT solver completed %d frames and produced an abstraction. ", f ); } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index fd8bb062..c5ded61b 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -278,7 +278,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) nObjMask = (1 << nObjBits) - 1; assert( Gia_ManObjNum(p) <= nObjMask ); // print info about frames - printf( "Frame All F0 F1 F2 F3 ...\n" ); + printf( "Frame Core F0 F1 F2 F3 ...\n" ); for ( i = 0; i < nFrames; i++ ) { iStart = Vec_IntEntry( vAbs, i+1 ); @@ -303,10 +303,23 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) // printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); printf( "%3d :", i ); printf( "%7d", pCountAll[0] ); - for ( k = 0; k < nFrames; k++ ) - if ( k <= i ) -// printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); + if ( i >= 10 ) + { + for ( k = 0; k < 4; k++ ) + printf( "%5d", pCountAll[k+1] ); + printf( " ..." ); + for ( k = i-4; k <= i; k++ ) printf( "%5d", pCountAll[k+1] ); + } + else + { + for ( k = 0; k <= i; k++ ) + if ( k <= i ) + printf( "%5d", pCountAll[k+1] ); + } +// for ( k = 0; k < nFrames; k++ ) +// if ( k <= i ) +// printf( "%5d", pCountAll[k+1] ); printf( "\n" ); } assert( iStop == Vec_IntSize(vAbs) ); |