diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-02 17:09:07 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-02 17:09:07 +0700 |
| commit | 11ed724766dd0748dcdfd9c50954e90f363390cc (patch) | |
| tree | d927b7efd0caf2766708d3917b079d6e8d86c5e4 /src/aig/saig | |
| parent | 8cde0dd33c00fb9525e835551f87a1525ad70f3b (diff) | |
| download | abc-11ed724766dd0748dcdfd9c50954e90f363390cc.tar.gz abc-11ed724766dd0748dcdfd9c50954e90f363390cc.tar.bz2 abc-11ed724766dd0748dcdfd9c50954e90f363390cc.zip | |
Added timeout to &abc_pba.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigAbsPba.c | 13 |
2 files changed, 12 insertions, 3 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 5a515eb0..36b41daf 100644 --- a/src/aig/saig/saig.h +++ b/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 ); diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index e3c49142..e37d62fa 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/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), |