diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-07 17:46:54 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-07 17:46:54 -0700 |
commit | 3aab7245738a69f1dd4d898493d5dabf6596ea61 (patch) | |
tree | 16a23107ca27a250e82c492dcdd1a2bea640cff6 /src/aig/gia/giaAbsGla.c | |
parent | 16d96fcf533fb77ff4a45992991e38ac7ea74bb3 (diff) | |
download | abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.tar.gz abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.tar.bz2 abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.zip |
Fixing time primtouts throughout the code.
Diffstat (limited to 'src/aig/gia/giaAbsGla.c')
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 1a4e9cd2..c25c6e48 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -800,13 +800,10 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) // select objects vSelect = Vec_IntAlloc( 100 ); -// Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 ); Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 ); Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign ); Vec_IntUniqify( vSelect ); -// printf( "\nSelected %d.\n", Vec_IntSize(vSelect) ); - /* for ( f = 0; f < p->pPars->iFrame; f++ ) printf( "%2d", Vec_IntEntry(p->vObjCounts, f) ); @@ -976,7 +973,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping ); if ( pPars->fPropFanout ) Gia_ManStaticFanoutStart( p->pGia ); -//printf( "Old GIA = %d. New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) ); // derive new gate map assert( pGia0->vGateClasses != 0 ); @@ -1797,7 +1793,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) p->timeInit = clock() - clk; // set runtime limit if ( p->pPars->nTimeOut ) - sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() ); // perform initial abstraction if ( p->pPars->fVerbose ) { @@ -1831,9 +1827,9 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) goto finish; } // check timeout - if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit ) + if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) { - Gla_ManRollBack( p ); // 1155046 + Gla_ManRollBack( p ); goto finish; } if ( vCore != NULL ) @@ -1960,7 +1956,7 @@ finish: pAig->vGateClasses = Gla_ManTranslate( p ); if ( Status == -1 ) { - if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) + if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) Abc_Print( 1, "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 ) Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); |