diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 15:02:46 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 15:02:46 -0700 |
commit | d3ad7fbaf33540075d02255741b4d35b90779cff (patch) | |
tree | 4ba53c2756de06fb24cfbd51be5642607872a46e /src/aig | |
parent | 86a0ae0bca9c604c95e90d802785ff73338efba1 (diff) | |
download | abc-d3ad7fbaf33540075d02255741b4d35b90779cff.tar.gz abc-d3ad7fbaf33540075d02255741b4d35b90779cff.tar.bz2 abc-d3ad7fbaf33540075d02255741b4d35b90779cff.zip |
Several small changes and fixes.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 19 | ||||
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 17 |
3 files changed, 24 insertions, 15 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 97a7b7b7..c537a31b 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -223,7 +223,8 @@ struct Gia_ParVta_t_ int fDumpVabs; // dumps the abstracted model char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag - int iFrame; // the number of frames covered + int iFrame; // the number of frames covered + int nFramesNoChange; // the number of last frames without changes }; static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 6505c2f2..117ad3e0 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -509,7 +509,7 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v { int i;//, Id = Gia_ObjId(p->pGia, pObj); Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f ); - assert( (int)pRef->Sign == Sign ); +// assert( (int)pRef->Sign == Sign ); if ( pRef->fVisit ) return; if ( p->pPars->fPropFanout ) @@ -1214,8 +1214,9 @@ void Gla_ManStop( Gla_Man_t * p ) Gla_Obj_t * pGla; int i; // if ( p->pPars->fVerbose ) - Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", - sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + 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 ); for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) ABC_FREE( p->pvRefis[i].pArray ); Gla_ManForEachObj( p, pGla ) @@ -1805,7 +1806,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) 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, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); + Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i ) { @@ -1891,9 +1892,13 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) nCoreSize = Vec_IntSize( vCore ); Gia_GlaAddToCounters( p, vCore ); if ( i == 0 ) + { + p->pPars->nFramesNoChange++; Vec_IntFree( vCore ); + } else { + p->pPars->nFramesNoChange = 0; // update the SAT solver sat_solver2_rollback( p->pSat ); // update storage @@ -1967,9 +1972,9 @@ finish: if ( Status == -1 ) { 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 ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); else @@ -1978,7 +1983,7 @@ finish: else { p->pPars->iFrame++; - Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); } } else diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index f7c1e5a5..85d51a42 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1062,8 +1062,9 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) void Vga_ManStop( Vta_Man_t * p ) { // if ( p->pPars->fVerbose ) - Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", - sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + 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 ); Vec_VecFreeP( (Vec_Vec_t **)&p->vCores ); Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames ); Vec_BitFreeP( &p->vSeenGla ); @@ -1534,7 +1535,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { printf( "Sequential miter is trivially UNSAT.\n" ); return 1; - } + } ABC_FREE( pAig->pCexSeq ); pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); printf( "Sequential miter is trivially SAT.\n" ); @@ -1564,7 +1565,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); // Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" ); - Abc_Print( 1, "Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" ); + Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" ); } assert( Vec_PtrSize(p->vFrames) > 0 ); for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) @@ -1665,9 +1666,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { // reset the counter of frames without change nCountNoChange = 1; + p->pPars->nFramesNoChange = 0; } else if ( ++nCountNoChange == 2 ) // time to send { + p->pPars->nFramesNoChange++; if ( Abc_FrameIsBridgeMode() ) { // cancel old one if it was sent @@ -1709,9 +1712,9 @@ finish: if ( Status == -1 ) { 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 ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 ) Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); else @@ -1720,7 +1723,7 @@ finish: else { p->pPars->iFrame++; - Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); } } } |