From 813245b29af60137f5bb94dfa2831d2454c8a9b5 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 15 Apr 2011 09:29:13 -0700
Subject: Improving timeout in the interpolation package.
---
src/aig/int/intCheck.c | 6 +++++-
src/aig/int/intCore.c | 36 ++++++++++++++++++++++++++----------
src/aig/int/intInt.h | 4 ++--
src/aig/int/intM114.c | 6 +++++-
src/base/abci/abc.c | 5 -----
5 files changed, 38 insertions(+), 19 deletions(-)
diff --git a/src/aig/int/intCheck.c b/src/aig/int/intCheck.c
index 54bb7ad9..6b36fe30 100644
--- a/src/aig/int/intCheck.c
+++ b/src/aig/int/intCheck.c
@@ -217,7 +217,7 @@ void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
SeeAlso []
***********************************************************************/
-int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt )
+int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut )
{
Aig_Obj_t * pObj, * pObj2;
int i, f, VarA, VarB, RetValue, Entry, status;
@@ -225,6 +225,10 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt )
assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
+ // set runtime limit
+ if ( nTimeNewOut )
+ sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );
+
// add clauses to the SAT solver
Cnf_DataLift( pCnfInt, p->nVars );
for ( f = 0; f <= p->nFramesK; f++ )
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index fdc2241e..ceb0025c 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -80,7 +80,13 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
Inter_Man_t * p;
Inter_Check_t * pCheck = NULL;
Aig_Man_t * pAigTemp;
- int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
+ int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
+ int nTimeNewOut = 0;
+
+ // set runtime limit
+ if ( pPars->nSecLimit )
+ nTimeNewOut = clock() + pPars->nSecLimit * CLOCKS_PER_SEC;
+
// sanity checks
assert( Saig_ManRegNum(pAig) > 0 );
assert( Saig_ManPiNum(pAig) > 0 );
@@ -171,7 +177,7 @@ p->timeCnf += clock() - clk;
clk = clock();
pCnfInter2 = Cnf_Derive( p->pInter, 1 );
p->timeCnf += clock() - clk;
- RetValue = Inter_CheckPerform( pCheck, pCnfInter2 );
+ RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
// assert( RetValue == 0 );
Cnf_DataFree( pCnfInter2 );
}
@@ -200,7 +206,7 @@ p->timeCnf += clock() - clk;
}
else
#endif
- RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward );
+ RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward, nTimeNewOut );
if ( pPars->fVerbose )
{
@@ -228,11 +234,19 @@ p->timeCnf += clock() - clk;
Inter_ManClean( p );
break;
}
- else if ( RetValue == -1 ) // timed out
+ else if ( RetValue == -1 )
{
- if ( pPars->fVerbose )
- printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
- assert( p->nConfCur >= p->nConfLimit );
+ if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
+ {
+ if ( pPars->fVerbose )
+ printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
+ }
+ else
+ {
+ assert( p->nConfCur >= p->nConfLimit );
+ if ( pPars->fVerbose )
+ printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
+ }
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
Inter_CheckStop( pCheck );
@@ -275,7 +289,9 @@ clk = clock();
clk2 = clock();
pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );
p->timeCnf += clock() - clk2;
- Status = Inter_CheckPerform( pCheck, pCnfInter2 );
+timeTemp = clock() - clk2;
+
+ Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
Cnf_DataFree( pCnfInter2 );
}
}
@@ -289,7 +305,7 @@ p->timeCnf += clock() - clk2;
else
Status = 0;
}
-p->timeEqu += clock() - clk;
+p->timeEqu += clock() - clk - timeTemp;
if ( Status ) // contained
{
if ( pPars->fVerbose )
@@ -299,7 +315,7 @@ p->timeEqu += clock() - clk;
Inter_CheckStop( pCheck );
return 1;
}
- if ( pPars->nSecLimit && ((float)pPars->nSecLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( pPars->nSecLimit && clock() > nTimeNewOut )
{
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
p->timeTotal = clock() - clkTotal;
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index d5e8ed00..3eab7883 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -93,7 +93,7 @@ typedef struct Inter_Check_t_ Inter_Check_t;
/*=== intCheck.c ============================================================*/
extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
extern void Inter_CheckStop( Inter_Check_t * p );
-extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf );
+extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut );
/*=== intContain.c ============================================================*/
extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
@@ -117,7 +117,7 @@ extern void Inter_ManClean( Inter_Man_t * p );
extern void Inter_ManStop( Inter_Man_t * p );
/*=== intM114.c ============================================================*/
-extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
+extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );
/*=== intM114p.c ============================================================*/
#ifdef ABC_USE_LIBRARIES
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c
index c1718eae..139c9bbd 100644
--- a/src/aig/int/intM114.c
+++ b/src/aig/int/intM114.c
@@ -200,7 +200,7 @@ sat_solver * Inter_ManDeriveSatSolver(
SeeAlso []
***********************************************************************/
-int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
+int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut )
{
sat_solver * pSat;
void * pSatCnf = NULL;
@@ -219,6 +219,10 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
return 1;
}
+ // set runtime limit
+ if ( nTimeNewOut )
+ sat_solver_set_runtime_limit( pSat, nTimeNewOut );
+
// collect global variables
pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
Vec_IntForEachEntry( p->vVarsAB, Var, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e8ac4d76..f4fb5ccc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8535,11 +8535,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
*/
-{
-// extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
-// Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
-}
-
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
--
cgit v1.2.3