luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Variable timeframe abstraction.

This commit is contained in:
Alan Mishchenko 2012-02-11 19:32:45 -08:00
parent 33261c33cb
commit d81aa6d697
2 changed files with 101 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

123
src/aig/gia/giaAbsVta.c
View File

@ -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) )
pCountAll = ABC_CALLOC( int, nFrames + 1 );
pCountUni = ABC_CALLOC( int, nFrames + 1 );
Vec_IntForEachEntry( vCore, Entry, i )
{
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++;
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 );
}

21
src/aig/gia/giaMan.c
View File

@ -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) );