diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 37 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 2 |
2 files changed, 16 insertions, 23 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 8e932cf3..4dcdb975 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -1417,10 +1417,10 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) if ( p->pPars->fVerbose ) { Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" ); - Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%.\n", - pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin ); - Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", - pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); + Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %% RatioMax = %d %%\n", + pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMax ); + Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n", + pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs ); Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } // iterate unrolling @@ -1517,9 +1517,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Vec_IntFree( vPPis ); if ( pPars->fVerbose ) Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, clock() - clk, 0 ); - // verify -// if ( Vec_IntCheckUnique(p->vAbs) ) -// Abc_Print( 1, "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); continue; } p->timeUnsat += clock() - clk2; @@ -1527,7 +1524,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) goto finish; if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout goto finish; -// assert( RetValue == l_False ); if ( c == 0 ) { if ( p->pPars->nFramesNoChange >= 0 ) @@ -1548,8 +1544,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // purify UNSAT core if ( fUseSecondCore ) { - int nOldCore = Vec_IntSize(vCore); - Vec_IntSort( vCore, 0 ); +// int nOldCore = Vec_IntSize(vCore); + // reverse the order of objects in the core +// Vec_IntSort( vCore, 0 ); // Vec_IntPrint( vCore ); // create bookmark to be used for rollback assert( nVarsOld == p->pSat->size ); @@ -1565,8 +1562,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Ga2_ManAddToAbs( p, vCore ); Vec_IntFree( vCore ); -// if ( pPars->fVerbose ) -// Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, clock() - clk, 0 ); } // run SAT solver clk2 = clock(); @@ -1587,18 +1582,23 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Ga2_ManAddToAbs( p, vCore ); Vec_IntFree( vCore ); - // verify -// if ( Vec_IntCheckUnique(p->vAbs) ) -// Abc_Print( 1, "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); break; } if ( pPars->fVerbose ) Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); + // set model if ( c > 0 ) { Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); + // check if the number of objects is below limit + if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 ) + { + Status = l_Undef; + goto finish; + } + if ( Abc_FrameIsBridgeMode() ) { // cancel old one if it was sent @@ -1634,13 +1634,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) } } } - - // check if the number of objects is below limit - if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 ) - { - Status = l_Undef; - break; - } } finish: p->pPars->nFramesNoChange = Abc_MaxInt( p->pPars->nFramesNoChange, 0 ); diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index c243584c..136455f8 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -157,7 +157,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) p->nLearnedDelta = 200; // max number of learned clauses p->nLearnedPerce = 70; // max number of learned clauses p->nTimeOut = 0; // timeout in seconds - p->nRatioMin = 10; // stop when less than this % of object is abstracted + p->nRatioMin = 20; // stop when less than this % of object is abstracted p->nRatioMax = 30; // restart when more than this % of object is abstracted p->fUseTermVars = 0; // use terminal variables p->fUseRollback = 0; // use rollback to the starting number of frames |