diff options
-rw-r--r-- | src/aig/gia/gia.h | 4 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 44 | ||||
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 270 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 7 | ||||
-rw-r--r-- | src/base/abci/abc.c | 120 |
5 files changed, 257 insertions, 188 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 40c74d8a..0d1c6ff1 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -213,6 +213,7 @@ struct Gia_ParVta_t_ int fUseTermVars; // use terminal variables int fUseRollback; // use rollback to the starting number of frames int fPropFanout; // propagate fanout implications + int fAddLayer; // refinement strategy by adding layers int fDumpVabs; // dumps the abstracted model char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag @@ -704,7 +705,8 @@ extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ); extern Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs ); extern Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames ); -extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs ); +extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ); +extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ); extern int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 53c95650..f6ada0c8 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -445,7 +445,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int ***********************************************************************/ void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign ) { - int i, Id = Gia_ObjId(p->pGia, pObj); + int i;//, Id = Gia_ObjId(p->pGia, pObj); Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f ); Gia_Obj_t * pFanout; int k; @@ -506,7 +506,7 @@ void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec ***********************************************************************/ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign ) { - int i, Id = Gia_ObjId(p->pGia, pObj); + int i;//, Id = Gia_ObjId(p->pGia, pObj); Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f ); assert( (int)pRef->Sign == Sign ); if ( pRef->fVisit ) @@ -1100,6 +1100,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) // other p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 ); p->pSat = sat_solver2_new(); +// p->pSat->fVerbose = p->pPars->fVerbose; + sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); p->nSatVars = 1; return p; } @@ -1214,7 +1216,7 @@ void Gla_ManStop( Gla_Man_t * p ) Gla_Obj_t * pGla; int i; // if ( p->pPars->fVerbose ) - Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Confs = %d. Cexes = %d. ObjAdded = %d\n", + Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n", sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded ); for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) ABC_FREE( p->pvRefis[i].pArray ); @@ -1754,8 +1756,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) clk = clock(); p = Gla_ManStart( pAig, pPars ); p->timeInit = clock() - clk; - p->pSat->fVerbose = p->pPars->fVerbose; - sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); // set runtime limit if ( p->pPars->nTimeOut ) sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); @@ -1763,21 +1763,23 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) if ( p->pPars->fVerbose ) { Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" ); - Abc_Print( 1, "FrameStart = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n", - p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin ); - Abc_Print( 1, "Frame %% Abs PPI FF AND Confl Cex SatVar Core Time\n" ); + Abc_Print( 1, "FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%.\n", + pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin ); + Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex SatVar Core Time\n" ); } for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) { int nConflsBeg = sat_solver2_nconflicts(p->pSat); p->pPars->iFrame = f; + // load timeframe Gia_GlaAddTimeFrame( p, f ); + // create bookmark to be used for rollback -// sat_solver2_reducedb( p->pSat ); sat_solver2_bookmark( p->pSat ); Vec_IntClear( p->vAddedNew ); p->nAbsOld = Vec_IntSize( p->vAbs ); + // iterate as long as there are counter-examples for ( i = 0; ; i++ ) { @@ -1805,17 +1807,20 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) p->nCexes++; // perform the refinement clk2 = clock(); - - vPPis = Gla_ManRefinement( p ); - if ( vPPis == NULL ) + if ( pPars->fAddLayer ) { - pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL; - break; + vPPis = Gla_ManCollectPPis( p, NULL ); +// Gla_ManExplorePPis( p, vPPis ); + } + else + { + vPPis = Gla_ManRefinement( p ); + if ( vPPis == NULL ) + { + pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL; + break; + } } - -// vPPis = Gla_ManCollectPPis( p, NULL ); -// Gla_ManExplorePPis( p, vPPis ); - Gia_GlaAddToAbs( p, vPPis, 1 ); Gia_GlaAddOneSlice( p, f, vPPis ); Vec_IntFree( vPPis ); @@ -1905,7 +1910,10 @@ finish: Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); } else + { + p->pPars->iFrame++; Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + } } else { diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index c6f5e238..1a442a79 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -61,6 +61,7 @@ struct Vta_Man_t_ Vec_Ptr_t * vFrames; // start abstraction for each frame int nWords; // the number of words in the record int nCexes; // the number of CEXes + int nObjAdded; // objects added to the abstraction Vec_Int_t * vSeens; // seen objects Vec_Bit_t * vSeenGla; // seen objects in all frames int nSeenGla; // seen objects in all frames @@ -149,10 +150,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) { memset( p, 0, sizeof(Gia_ParVta_t) ); p->nFramesMax = 0; // maximum frames - p->nFramesStart = 5; // starting frame + p->nFramesStart = 0; // starting frame p->nFramesPast = 4; // overlap frames p->nConfLimit = 0; // conflict limit - p->nLearntMax = 15000; // max number of learned clauses + p->nLearntMax = 1000; // max number of learned clauses p->nTimeOut = 0; // timeout in seconds p->nRatioMin = 10; // stop when less than this % of object is abstracted p->fUseTermVars = 1; // use terminal variables @@ -236,31 +237,31 @@ Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs ) +Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ) { Gia_Obj_t * pObj; - Vec_Int_t * vPresent; + Vec_Int_t * vGla; int nObjMask, nObjs = Gia_ManObjNum(p); - int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 ); - assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) ); + int i, Entry, nFrames = Vec_IntEntry( vVta, 0 ); + assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); // get the bitmask nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; assert( nObjs <= nObjMask ); // go through objects - vPresent = Vec_IntStart( nObjs ); - Vec_IntWriteEntry( vPresent, 0, 1 ); - Vec_IntForEachEntryStart( vAbs, Entry, i, nFrames+2 ) + vGla = Vec_IntStart( nObjs ); + Vec_IntWriteEntry( vGla, 0, 1 ); + Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 ) { pObj = Gia_ManObj( p, (Entry & nObjMask) ); assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) ); - Vec_IntWriteEntry( vPresent, (Entry & nObjMask), 1 ); + Vec_IntWriteEntry( vGla, (Entry & nObjMask), 1 ); } - return vPresent; + return vGla; } /**Function************************************************************* - Synopsis [Detects how many frames are completed.] + Synopsis [Converting GLA vector to VTA vector.] Description [] @@ -269,26 +270,31 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs ) SeeAlso [] ***********************************************************************/ -static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords ) +Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ) { - unsigned * pTotal, * pThis; - int i, w, nObjs = Vec_IntSize(p) / nWords; - assert( Vec_IntSize(p) % nWords == 0 ); - pTotal = ABC_CALLOC( unsigned, nWords ); - for ( i = 0; i < nObjs; i++ ) - { - pThis = (unsigned *)Vec_IntEntryP( p, nWords * i ); - for ( w = 0; w < nWords; w++ ) - pTotal[w] |= pThis[i]; - } - for ( i = nWords * 32 - 1; i >= 0; i-- ) - if ( Abc_InfoHasBit(pTotal, i) ) - { - ABC_FREE( pTotal ); - return i+1; - } - ABC_FREE( pTotal ); - return -1; + Vec_Int_t * vVta; + int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p); + int i, k, j, Entry, Counter, nGlaSize; + //. get the GLA size + nGlaSize = Vec_IntSum(vGla); + // get the bitmask + nObjBits = Abc_Base2Log(nObjs); + nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; + assert( nObjs <= nObjMask ); + // go through objects + vVta = Vec_IntAlloc( 1000 ); + Vec_IntPush( vVta, nFrames ); + Counter = nFrames + 2; + for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize ) + Vec_IntPush( vVta, Counter ); + for ( i = 0; i < nFrames; i++ ) + for ( k = 0; k <= i; k++ ) + Vec_IntForEachEntry( vGla, Entry, j ) + if ( Entry ) + Vec_IntPush( vVta, (k << nObjBits) | j ); + Counter = Vec_IntEntry(vVta, nFrames+1); + assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); + return vVta; } /**Function************************************************************* @@ -949,25 +955,28 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) assert( 0 ); } - // mark those currently included - Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) - { - assert( pThis->fVisit == 0 ); - pThis->fVisit = 1; - } - // add used terms, which have close relationship - Counter = Vec_IntSize(vTermsToAdd); - Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + if ( p->pPars->fAddLayer ) { - if ( pThis->fVisit ) - continue; -// Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 ); -// if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) ) - Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) ); + // mark those currently included + Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) + { + assert( pThis->fVisit == 0 ); + pThis->fVisit = 1; + } + // add used terms, which have close relationship + Counter = Vec_IntSize(vTermsToAdd); + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + { + if ( pThis->fVisit ) + continue; + // Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 ); + // if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) ) + Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) ); + } + // remove those currenty included + Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) + pThis->fVisit = 0; } - // remove those currenty included - Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) - pThis->fVisit = 0; // printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) ); //Vec_IntReverseOrder( vTermsToAdd ); //Vec_IntSort( vTermsToAdd, 1 ); @@ -1054,6 +1063,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame ); sat_solver2_simplify( p->pSat ); } + p->nObjAdded += Vec_IntSize(vTermsToAdd); Vec_IntFree( vTermsToAdd ); return pCex; } @@ -1091,28 +1101,15 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) ); p->nSeenGla = 1; p->nSeenAll = 1; - // start the abstraction - if ( pGia->vObjClasses == NULL ) - p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart ); - else - { - p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses ); - // update parameters - if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) ) - { - Abc_Print( 1, "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) ); - pPars->nFramesStart = Vec_PtrSize(p->vFrames); - } - if ( pPars->nFramesMax && pPars->nFramesMax < pPars->nFramesStart ) - { - Abc_Print( 1, "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart ); - pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart ); - } - } // other data p->vCla2Var = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Var, -1 ); p->vCores = Vec_PtrAlloc( 100 ); p->pSat = sat_solver2_new(); +// p->pSat->fVerbose = p->pPars->fVerbose; + sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); + // start the abstraction + assert( pGia->vObjClasses != NULL ); + p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses ); p->vAddedNew = Vec_IntAlloc( 1000 ); return p; } @@ -1131,9 +1128,8 @@ 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: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n", - sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes ); - + Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n", + sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded ); Vec_VecFreeP( (Vec_Vec_t **)&p->vCores ); Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames ); Vec_BitFreeP( &p->vSeenGla ); @@ -1624,8 +1620,6 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); - -/* // compute intial abstraction if ( pAig->vObjClasses == NULL ) { @@ -1635,11 +1629,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Vec_IntPush( pAig->vObjClasses, 4 ); Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ); } -*/ // start the manager p = Vga_ManStart( pAig, pPars ); - p->pSat->fVerbose = p->pPars->fVerbose; - sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); // set runtime limit if ( p->pPars->nTimeOut ) sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); @@ -1647,11 +1638,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) if ( p->pPars->fVerbose ) { Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" ); - Abc_Print( 1, "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n", - p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax, - p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin ); + Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%\n", + pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin ); Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" ); } + assert( Vec_PtrSize(p->vFrames) > 0 ); for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) { int nConflsBeg = sat_solver2_nconflicts(p->pSat); @@ -1659,72 +1650,72 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // realloc storage for abstraction marks if ( f == p->nWords * 32 ) p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords ); - // check this timeframe - if ( f < p->pPars->nFramesStart ) - { - Vga_ManAddClausesOne( p, 0, f ); + + // create bookmark to be used for rollback + nObjOld = p->nObjs; + sat_solver2_bookmark( p->pSat ); + Vec_IntClear( p->vAddedNew ); + + // load new timeframe + Vga_ManAddClausesOne( p, 0, f ); + if ( f < Vec_PtrSize(p->vFrames) ) Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 ); - } else { - // create bookmark to be used for rollback - nObjOld = p->nObjs; -// sat_solver2_reducedb( p->pSat ); - sat_solver2_bookmark( p->pSat ); - Vec_IntClear( p->vAddedNew ); - // load the time frame - for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, p->pPars->nFramesStart); i++ ) + for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ ) Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i ); - // iterate as long as there are counter-examples - for ( i = 0; ; i++ ) - { - clk2 = clock(); - vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); - assert( (vCore != NULL) == (Status == 1) ); - if ( Status == -1 ) // resource limit is reached - { - Vga_ManRollBack( p, nObjOld ); - goto finish; - } - // check timeout - if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit ) - { - Vga_ManRollBack( p, nObjOld ); - goto finish; - } - if ( vCore != NULL ) - { - p->timeUnsat += clock() - clk2; - break; - } - p->timeSat += clock() - clk2; - assert( Status == 0 ); - p->nCexes++; - // perform the refinement - clk2 = clock(); - pCex = Vta_ManRefineAbstraction( p, f ); - p->timeCex += clock() - clk2; - if ( pCex != NULL ) - { - RetValue = 0; - goto finish; - } - // print the result (do not count it towards change) - Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ); + } + + // iterate as long as there are counter-examples + for ( i = 0; ; i++ ) + { + clk2 = clock(); + vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); + assert( (vCore != NULL) == (Status == 1) ); + if ( Status == -1 ) // resource limit is reached + { + Vga_ManRollBack( p, nObjOld ); + goto finish; + } + // check timeout + if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit ) + { + Vga_ManRollBack( p, nObjOld ); + goto finish; + } + if ( vCore != NULL ) + { + p->timeUnsat += clock() - clk2; + break; + } + p->timeSat += clock() - clk2; + assert( Status == 0 ); + p->nCexes++; + // perform the refinement + clk2 = clock(); + pCex = Vta_ManRefineAbstraction( p, f ); + p->timeCex += clock() - clk2; + if ( pCex != NULL ) + { + RetValue = 0; + goto finish; } - assert( Status == 1 ); - // valid core is obtained - Vta_ManUnsatCoreRemap( p, vCore ); - Vec_IntSort( vCore, 1 ); - // update the SAT solver - sat_solver2_rollback( p->pSat ); - // update storage - Vga_ManRollBack( p, nObjOld ); - Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 ); - // load this timeframe - Vga_ManLoadSlice( p, vCore, 0 ); - Vec_IntFree( vCore ); - } + // print the result (do not count it towards change) + Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ); + } + assert( Status == 1 ); + // valid core is obtained + Vta_ManUnsatCoreRemap( p, vCore ); + Vec_IntSort( vCore, 1 ); + // update the SAT solver + sat_solver2_rollback( p->pSat ); + // update storage + Vga_ManRollBack( p, nObjOld ); + Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 ); + // load this timeframe + Vga_ManLoadSlice( p, vCore, 0 ); + Vec_IntFree( vCore ); + // run SAT solver clk2 = clock(); vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); @@ -1808,7 +1799,10 @@ finish: Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); } else + { + p->pPars->iFrame++; Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + } } } else diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index c116f5e7..0ab6c091 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -202,6 +202,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) void Gia_ManPrintGateClasses( Gia_Man_t * p ) { Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes; + int nTotal; if ( p->vGateClasses == NULL ) return; if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) ) @@ -211,10 +212,12 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p ) } // create additional arrays Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes ); - printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n", + nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes); + printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n", Vec_IntSize(vPis), Vec_IntSize(vPPis), Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), - Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) ); + Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1), + nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) ); Vec_IntFree( vPis ); Vec_IntFree( vPPis ); Vec_IntFree( vFlops ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d1c1e5a9..8983ba39 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -352,6 +352,7 @@ static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Vta2Gla ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Gla2Vta ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BackReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -797,6 +798,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&vta_gla", Abc_CommandAbc9Vta2Gla, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla_vta", Abc_CommandAbc9Gla2Vta, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&back_reach", Abc_CommandAbc9BackReach, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 ); @@ -27384,10 +27386,8 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ParVta_t Pars, * pPars = &Pars; int c, fStartVta = 0; Gia_VtaSetDefaultParams( pPars ); - pPars->nFramesStart = 30; - pPars->nLearntMax = 100000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfdavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfkadvh" ) ) != EOF ) { switch ( c ) { @@ -27486,11 +27486,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': pPars->fPropFanout ^= 1; break; - case 'd': - pPars->fDumpVabs ^= 1; + case 'k': + fStartVta ^= 1; break; case 'a': - fStartVta ^= 1; + pPars->fAddLayer ^= 1; + break; + case 'd': + pPars->fDumpVabs ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -27526,32 +27529,25 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); return 0; } - if ( pPars->nFramesStart < 1 ) - { - Abc_Print( 1, "The starting frame should be 1 or larger.\n" ); - return 0; - } pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fdavh]\n" ); - Abc_Print( -2, "\t performs gate-level abstraction of a sequential miter\n" ); + Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fkadvh]\n" ); + Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); -// Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin ); Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" ); -// Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" ); -// Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" ); Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" ); + Abc_Print( -2, "\t-k : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle using VTA to kick start GLA [default = %s]\n", fStartVta? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -27574,7 +27570,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Gia_VtaSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtradvh" ) ) != EOF ) { switch ( c ) { @@ -27670,6 +27666,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': pPars->fUseRollback ^= 1; break; + case 'a': + pPars->fAddLayer ^= 1; + break; case 'd': pPars->fDumpVabs ^= 1; break; @@ -27707,21 +27706,14 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); return 0; } - if ( pPars->nFramesStart < 1 ) - { - Abc_Print( 1, "The starting frame should be 1 or larger.\n" ); - return 0; - } -// if ( argc == globalUtilOptind + 1 ) -// pPars->pFileVabs = argv[globalUtilOptind]; pAbc->Status = Gia_VtaPerform( pAbc->pGia, pPars ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-trdvh]\n" ); - Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); + Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-tradvh]\n" ); + Abc_Print( -2, "\t variable-time-frame gate-level proof- and cex-based abstraction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast ); @@ -27732,6 +27724,7 @@ usage: Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"vabs.aig\"]\n" ); Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -27773,7 +27766,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia->vObjClasses == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction defines.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" ); return 1; } Vec_IntFreeP( &pAbc->pGia->vGateClasses ); @@ -27783,7 +27776,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &vta_gla [-vh]\n" ); - Abc_Print( -2, "\t maps variable- into fixed-time-frame abstraction\n" ); + Abc_Print( -2, "\t maps variable- into fixed-time-frame gate-level abstraction\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -27800,6 +27793,75 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c, fVerbose = 0; + int nFrames = pAbc->nFrames; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" ); + return 1; + } + if ( pAbc->pGia->vGateClasses == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" ); + return 1; + } + if ( pAbc->nFrames < 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames ); + return 1; + } + Vec_IntFreeP( &pAbc->pGia->vObjClasses ); + pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames ); + Vec_IntFreeP( &pAbc->pGia->vGateClasses ); + return 0; + +usage: + Abc_Print( -2, "usage: &gla_vta [-F num] [-vh]\n" ); + Abc_Print( -2, "\t maps fixed- into variable-time-frame gate-level abstraction\n" ); + Abc_Print( -2, "\t-F num : timeframes in the resulting variable-time-frame abstraction [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp = NULL; |