From a019dd216e949bece9f5adb53693f20482e4ef49 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 9 Aug 2012 19:16:25 -0700 Subject: Improved abstraction refinement. --- src/aig/gia/giaAbsGla.c | 6 +++--- src/aig/gia/giaAbsGla2.c | 16 ++++++++++------ src/aig/gia/giaAbsRef.c | 22 +++++++++++++--------- src/aig/gia/giaAbsVta.c | 6 +++--- 4 files changed, 29 insertions(+), 21 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 25a3ebf7..160e47e1 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1303,7 +1303,7 @@ void Gla_ManStop( Gla_Man_t * p ) Gla_Obj_t * pGla; int i; -// if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose ) Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n", sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); @@ -2102,8 +2102,8 @@ finish: { if ( p->pPars->fVerbose && Status == -1 ) printf( "\n" ); - if ( pAig->vGateClasses != NULL ) - Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); +// if ( pAig->vGateClasses != NULL ) +// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Gla_ManTranslate( p ); if ( Status == -1 ) diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index d8a18930..dd8846c4 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -440,7 +440,7 @@ void Ga2_ManStop( Ga2_Man_t * p ) { Vec_IntFreeP( &p->pGia->vMapping ); Gia_ManSetPhase( p->pGia ); -// if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose ) Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d ObjsAdded = %d\n", sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), @@ -1527,7 +1527,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) goto finish; assert( RetValue == l_False ); if ( c == 0 ) + { + p->pPars->nFramesNoChange++; break; + } + p->pPars->nFramesNoChange = 0; // derive the core assert( p->pSat->pPrf2 != NULL ); @@ -1601,16 +1605,16 @@ finish: // analize the results if ( pAig->pCexSeq == NULL ) { - if ( pAig->vGateClasses != NULL ) - Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); +// if ( pAig->vGateClasses != NULL ) +// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); if ( Status == l_Undef ) { 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 ); + Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange ); 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 ); + Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange ); else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 ) Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); else @@ -1619,7 +1623,7 @@ finish: else { p->pPars->iFrame++; - Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + Abc_Print( 1, "SAT solver completed %d frames and produced a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); } } else diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index 21a87c33..a30250a5 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -721,6 +721,7 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect ) Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) { int fVerify = 0; + int fPostProcess = 1; Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); Vec_Int_t * vNew; clock_t clk, clk2 = clock(); @@ -754,16 +755,19 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in p->timeBwd += clock() - clk; } - vNew = Ga2_FilterSelected( p, vSelected ); - if ( Vec_IntSize(vNew) > 0 ) + if ( fPostProcess ) { - Vec_IntFree( vSelected ); - vSelected = vNew; - } - else - { - Vec_IntFree( vNew ); -// printf( "\nBig refinement.\n" ); + vNew = Ga2_FilterSelected( p, vSelected ); + if ( Vec_IntSize(vNew) > 0 ) + { + Vec_IntFree( vSelected ); + vSelected = vNew; + } + else + { + Vec_IntFree( vNew ); + // printf( "\nBig refinement.\n" ); + } } // clean values diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 86b3b055..11765db6 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1064,7 +1064,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) ***********************************************************************/ void Vga_ManStop( Vta_Man_t * p ) { -// if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose ) Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n", sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); @@ -1706,8 +1706,8 @@ finish: else { assert( Vec_PtrSize(p->vCores) > 0 ); - if ( pAig->vObjClasses != NULL ) - Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); +// if ( pAig->vObjClasses != NULL ) +// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); Vec_IntFreeP( &pAig->vObjClasses ); pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); if ( Status == -1 ) -- cgit v1.2.3