From 07d3351c31c6f76f77c6881cd2fd7294eca091c1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 7 Jul 2013 22:37:29 -0700 Subject: Adding timeout to AIG rewriting inside 'int'. --- src/aig/aig/aig.h | 1 + src/opt/dar/darBalance.c | 17 +++++++++++++++++ src/opt/dar/darCore.c | 2 ++ src/opt/dar/darRefact.c | 2 ++ src/opt/dar/darScript.c | 18 +++++++++++++++++- src/proof/int/intCore.c | 12 ++++++++++++ 6 files changed, 51 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 697238ae..2a1e7d7d 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -160,6 +160,7 @@ struct Aig_Man_t_ Vec_Int_t * vProbs; // probability of node being 1 Vec_Int_t * vCiNumsOrig; // original CI names int nComplEdges; // complemented edges + abctime Time2Quit; // timing statistics abctime time1; abctime time2; diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c index c2ebfc61..01cd7953 100644 --- a/src/opt/dar/darBalance.c +++ b/src/opt/dar/darBalance.c @@ -521,6 +521,8 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) { pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); + if ( pObjNew == NULL ) + return NULL; vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) ); } // build the supergate @@ -529,6 +531,8 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * #else pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel ); #endif + if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit ) + return NULL; // make sure the balanced node is not assigned // assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); assert( pObjOld->pData == NULL ); @@ -559,6 +563,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->nAsserts = p->nAsserts; pNew->nConstrs = p->nConstrs; + pNew->Time2Quit = p->Time2Quit; if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // map the PI nodes @@ -588,6 +593,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) // perform balancing pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + if ( pObjNew == NULL ) + { + Vec_VecFree( vStore ); + Aig_ManStop( pNew ); + return NULL; + } pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); // save arrival time of the output arrTime = (float)Aig_Regular(pObjNew)->Level; @@ -613,6 +624,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) { pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + if ( pObjNew == NULL ) + { + Vec_VecFree( vStore ); + Aig_ManStop( pNew ); + return NULL; + } pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); } diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c index 17074123..24e5a741 100644 --- a/src/opt/dar/darCore.c +++ b/src/opt/dar/darCore.c @@ -112,6 +112,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) // Aig_ManOrderStart( pAig ); // Aig_ManForEachNodeInOrder( pAig, pObj ) { + if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit ) + break; // Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL ); // Bar_ProgressUpdate( pProgress, i, NULL ); if ( !Aig_ObjIsNode(pObj) ) diff --git a/src/opt/dar/darRefact.c b/src/opt/dar/darRefact.c index 45e150c4..6083c035 100644 --- a/src/opt/dar/darRefact.c +++ b/src/opt/dar/darRefact.c @@ -526,6 +526,8 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) continue; if ( i > nNodesOld ) break; + if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit ) + break; Vec_VecClear( p->vCuts ); //printf( "\nConsidering node %d.\n", pObj->Id ); diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c index f1a30a82..f8fa3788 100644 --- a/src/opt/dar/darScript.c +++ b/src/opt/dar/darScript.c @@ -72,6 +72,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) //alias rwsat "st; rw -l; b -l; rw -l; rf -l" { Aig_Man_t * pTemp; + abctime Time = pAig->Time2Quit; Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; @@ -92,41 +93,56 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) // balance if ( fBalance ) { + pAig->Time2Quit = Time; pAig = Dar_ManBalance( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig ); + if ( Time && Abc_Clock() > Time ) + { if ( pAig ) Aig_ManStop( pAig ); return NULL; } } //Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL ); //printf( "3" ); // rewrite + pAig->Time2Quit = Time; Dar_ManRewrite( pAig, pParsRwr ); pAig = Aig_ManDupDfs( pTemp = pAig ); Aig_ManStop( pTemp ); if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig ); + if ( Time && Abc_Clock() > Time ) + { if ( pAig ) Aig_ManStop( pAig ); return NULL; } //printf( "4" ); // refactor + pAig->Time2Quit = Time; Dar_ManRefactor( pAig, pParsRef ); pAig = Aig_ManDupDfs( pTemp = pAig ); Aig_ManStop( pTemp ); if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig ); + if ( Time && Abc_Clock() > Time ) + { if ( pAig ) Aig_ManStop( pAig ); return NULL; } //printf( "5" ); // balance if ( fBalance ) { + pAig->Time2Quit = Time; pAig = Dar_ManBalance( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig ); + if ( Time && Abc_Clock() > Time ) + { if ( pAig ) Aig_ManStop( pAig ); return NULL; } } - + //printf( "6" ); // rewrite + pAig->Time2Quit = Time; Dar_ManRewrite( pAig, pParsRwr ); pAig = Aig_ManDupDfs( pTemp = pAig ); Aig_ManStop( pTemp ); if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig ); + if ( Time && Abc_Clock() > Time ) + { if ( pAig ) Aig_ManStop( pAig ); return NULL; } //printf( "7" ); return pAig; diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c index dedf987e..1418402c 100644 --- a/src/proof/int/intCore.c +++ b/src/proof/int/intCore.c @@ -280,10 +280,22 @@ p->timeEqu += Abc_Clock() - clk; clk = Abc_Clock(); if ( p->pInterNew ) { + Abc_PrintTime( 1, "Before time", clock() - clkTotal ); + // save the timeout value + p->pInterNew->Time2Quit = nTimeNewOut; // Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 ); p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 ); // p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 ); + Abc_PrintTime( 1, "After time", clock() - clkTotal ); Aig_ManStop( pAigTemp ); + if ( p->pInterNew == NULL ) + { + printf( "Reached timeout (%d seconds) during rewriting.\n", pPars->nSecLimit ); + p->timeTotal = Abc_Clock() - clkTotal; + Inter_ManStop( p, 1 ); + Inter_CheckStop( pCheck ); + return -1; + } } p->timeRwr += Abc_Clock() - clk; -- cgit v1.2.3