Skip to content

A
abc
Commit 11ed7247 by Alan Mishchenko
Options

Added timeout to &abc_pba.

parent 8cde0dd3
Showing with 32 additions and 10 deletions
src/aig/gia/gia.h
......@@ -600,7 +600,7 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
extern void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars );
Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
......
src/aig/gia/giaAbs.c
......@@ -316,7 +316,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
......@@ -332,7 +332,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, fVerbose, piFrame );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, nTimeLimit, fVerbose, piFrame );
// derive new classes
if ( pAig->pSeqModel == NULL )
{
......
src/aig/saig/saig.h
......@@ -135,7 +135,7 @@ extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t
extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
/*=== sswAbsPba.c ==========================================================*/
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
/*=== sswAbsStart.c ==========================================================*/
extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
......
src/aig/saig/saigAbsPba.c
......@@ -247,7 +247,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int TimeLimit, int fVerbose, int * piFrame )
{
Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
Aig_Man_t * pFrames;
......@@ -257,7 +257,12 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nF
int nCoreLits, * pCoreLits;
int i, iVar, RetValue, clk;
if ( fVerbose )
printf( "Performing abstraction with starting frame %d and total number of frames %d.\n", nStart, nFrames );
{
if ( TimeLimit )
printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFrames, TimeLimit );
else
printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFrames );
}
// create SAT solver
clk = clock();
pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap );
......@@ -287,6 +292,10 @@ Abc_PrintTime( 1, "Preparing", clock() - clk );
Vec_IntWriteEntry( vMapVar2FF, iVar, i );
}
// set runtime limit
if ( TimeLimit )
sat_solver_set_runtime_limit( pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
// run SAT solver
clk = clock();
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
......
src/base/abci/abc.c
......@@ -28477,12 +28477,13 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
int nStart = 0;
int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
int nConfMax = 10000000;
int nTimeLimit = 0;
int fVerbose = 0;
int iFrame = -1;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
{
switch ( c )
{
......@@ -28519,6 +28520,17 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nTimeLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeLimit < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -28548,18 +28560,19 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The starting frame (%d) should be less than the total number of frames (%d).\n", nStart, nFramesMax );
return 0;
}
Gia_ManPbaPerform( pAbc->pGia, nStart, nFramesMax, nConfMax, fVerbose, &iFrame );
Gia_ManPbaPerform( pAbc->pGia, nStart, nFramesMax, nConfMax, nTimeLimit, fVerbose, &iFrame );
if ( iFrame >= 0 )
pAbc->nFrames = iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &abs_pba [-SFC num] [-vh]\n" );
Abc_Print( -2, "usage: &abs_pba [-SFCT num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted flop map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting timeframe for SAT check [default = %d]\n", nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", nConfMax );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", nTimeLimit );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......@@ -28663,7 +28676,7 @@ usage:
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : the time out in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment