From d81aa6d697a8fd2128acef9cf7b2be24a4066f63 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 11 Feb 2012 19:32:45 -0800
Subject: Variable timeframe abstraction.
---
src/aig/gia/giaAbsVta.c | 123 +++++++++++++++++++++++++++++++++---------------
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) );
--
cgit v1.2.3