From 719b06f91295cc0dd811241b7bc30707546241bd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 20 Jan 2012 17:55:34 -0800 Subject: Variable timeframe abstraction. --- src/aig/gia/giaAbsVta.c | 388 +++++++++++++++++++++++++++--------------------- src/aig/gia/giaFrames.c | 9 +- src/aig/gia/giaMan.c | 8 +- 3 files changed, 227 insertions(+), 178 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 50ae53e2..c3574e26 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -98,7 +98,7 @@ static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert // - the following entries give the object IDs // invariant: assert( vec[vec[0]+2] == size(vec) ); -extern void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ); +extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -342,6 +342,7 @@ static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame { Vta_Obj_t * pThis; int * pPlace; + assert( iObj >= 0 && iFrame >= -1 ); if ( p->nObjs == p->nObjsAlloc ) { p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc ); @@ -368,78 +369,6 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame ) pThis->iNext = -1; } -/**Function************************************************************* - - Synopsis [Finds the set of clauses involved in the UNSAT core.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Vta_ManUnsatCore( Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue ) -{ - Vec_Int_t * vPres; - Vec_Int_t * vCore; - int k, i, Entry, RetValue, clk = clock(); - if ( piRetValue ) - *piRetValue = -1; - // solve the problem - RetValue = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( RetValue == l_Undef ) - { -// if ( fVerbose ) - printf( "Conflict limit is reached.\n" ); - return NULL; - } - if ( RetValue == l_True ) - { -// if ( fVerbose ) - printf( "The BMC problem is SAT.\n" ); - if ( piRetValue ) - *piRetValue = 0; - return NULL; - } - if ( fVerbose ) - { - printf( "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); - Abc_PrintTime( 1, "Time", clock() - clk ); - } - assert( RetValue == l_False ); - - // derive the UNSAT core - clk = clock(); - vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); - if ( fVerbose ) - { - printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) ); - Abc_PrintTime( 1, "Time", clock() - clk ); - } - - // remap core into variables - clk = clock(); - vPres = Vec_IntStart( sat_solver2_nvars(pSat) ); - k = 0; - Vec_IntForEachEntry( vCore, Entry, i ) - { - Entry = Vec_IntEntry(vCla2Var, Entry); - if ( Vec_IntEntry(vPres, Entry) ) - continue; - Vec_IntWriteEntry( vPres, Entry, 1 ); - Vec_IntWriteEntry( vCore, k++, Entry ); - } - Vec_IntShrink( vCore, k ); - Vec_IntFree( vPres ); - if ( fVerbose ) - { - printf( "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); - Abc_PrintTime( 1, "Time", clock() - clk ); - } - return vCore; -} - /**Function************************************************************* Synopsis [Remaps core into frame/node pairs.] @@ -460,7 +389,9 @@ void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore ) pThis = Vta_ManObj( p, Entry ); Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj; Vec_IntWriteEntry( vCore, i, Entry ); +//printf( "%d^%d ", pThis->iObj, pThis->iFrame ); } +//printf( "\n" ); } /**Function************************************************************* @@ -804,7 +735,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p ) } // add clauses Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) - Vga_ManAddClausesOne( p, pThis ); + Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame ); } Vec_PtrFree( vTermsUsed ); @@ -827,38 +758,43 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) { Vta_Man_t * p; p = ABC_CALLOC( Vta_Man_t, 1 ); - p->pGia = pGia; - p->pPars = pPars; + p->pGia = pGia; + p->pPars = pPars; // internal data - p->nObjsAlloc = (1 << 20); - p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc ); - p->nObjs = 1; - p->nBins = Abc_PrimeCudd( p->nObjsAlloc/2 ); - p->pBins = ABC_CALLOC( int, p->nBins ); - p->vOrder = Vec_IntAlloc( 1013 ); + p->nObjsAlloc = (1 << 20); + p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc ); + p->nObjs = 1; + p->nBins = Abc_PrimeCudd( p->nObjsAlloc/2 ); + p->pBins = ABC_CALLOC( int, p->nBins ); + p->vOrder = Vec_IntAlloc( 1013 ); // abstraction - p->nObjBits = Gia_Base2Log( Gia_ManObjNum(pGia) ); - p->nObjMask = (1 << p->nObjBits) - 1; + p->nObjBits = Gia_Base2Log( Gia_ManObjNum(pGia) ); + p->nObjMask = (1 << p->nObjBits) - 1; assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask ); - p->nWords = 1; - p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords ); + p->nWords = 1; + p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords ); // start the abstraction if ( pGia->vObjClasses == NULL ) - p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart ); + p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart ); else { - p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses ); + p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses ); // update parameters if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) ) - printf( "Starting frame count is set in accordance with abstraction (%d).\n", Vec_PtrSize(p->vFrames) ); - pPars->nFramesStart = Vec_PtrSize(p->vFrames); - if ( pPars->nFramesMax ) + { + printf( "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 ) + { + printf( "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 ); - p->vCores = Vec_PtrAlloc( 100 ); - p->pSat = sat_solver2_new(); + p->vCla2Var = Vec_IntAlloc( 1000 ); + p->vCores = Vec_PtrAlloc( 100 ); + p->pSat = sat_solver2_new(); return p; } @@ -886,6 +822,82 @@ void Vga_ManStop( Vta_Man_t * p ) ABC_FREE( p ); } +/**Function************************************************************* + + Synopsis [Finds the set of clauses involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue ) +{ + Vec_Int_t * vPres; + Vec_Int_t * vCore; + int k, i, Entry, RetValue, clk = clock(); + int nConfPrev = pSat->stats.conflicts; + if ( piRetValue ) + *piRetValue = 1; + // solve the problem + RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( RetValue == l_Undef ) + { +// if ( fVerbose ) + printf( "Conflict limit is reached.\n" ); + if ( piRetValue ) + *piRetValue = -1; + return NULL; + } + if ( RetValue == l_True ) + { +// if ( fVerbose ) + printf( "The BMC problem is SAT.\n" ); + if ( piRetValue ) + *piRetValue = 0; + return NULL; + } + if ( fVerbose ) + { + printf( "%6d", (int)pSat->stats.conflicts - nConfPrev ); +// printf( "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + assert( RetValue == l_False ); + + // derive the UNSAT core + clk = clock(); + vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); + if ( fVerbose ) + { +// printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + + // remap core into variables + clk = clock(); + vPres = Vec_IntStart( sat_solver2_nvars(pSat) ); + k = 0; + Vec_IntForEachEntry( vCore, Entry, i ) + { + Entry = Vec_IntEntry(vCla2Var, Entry); + if ( Vec_IntEntry(vPres, Entry) ) + continue; + Vec_IntWriteEntry( vPres, Entry, 1 ); + Vec_IntWriteEntry( vCore, k++, Entry ); + } + Vec_IntShrink( vCore, k ); + Vec_IntFree( vPres ); + if ( fVerbose ) + { +// printf( "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + return vCore; +} + /**Function************************************************************* Synopsis [] @@ -918,12 +930,13 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames ) } pCountAll[iFrame+1]++; pCountAll[0]++; - - printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); - for ( k = 0; k < nFrames; k++ ) - printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); - printf( "\n" ); } +// printf( "%5d%5d", pCountAll[0], pCountUni[0] ); + printf( "%7d", pCountAll[0] ); + for ( k = 0; k < nFrames; k++ ) +// printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); + printf( "%4d", pCountAll[k+1] ); + printf( "\n" ); ABC_FREE( pCountAll ); ABC_FREE( pCountUni ); } @@ -939,59 +952,56 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames ) SeeAlso [] ***********************************************************************/ -void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ) +void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ) { Vta_Obj_t * pThis0, * pThis1; - Gia_Obj_t * pObj; - int i = Vta_ObjId( p, pThis ); - assert( !pThis->fAdded && !pThis->fNew ); - pObj = Gia_ManObj( p->pGia, pThis->iObj ); + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame ); + int iMainVar = Vta_ObjId(p, pThis); + assert( pThis->iObj == iObj && pThis->iFrame == iFrame ); + assert( pThis->fAdded == 0 ); + pThis->fAdded = 1; if ( Gia_ObjIsAnd(pObj) ) { - pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame ); - pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame ); - if ( pThis0 && pThis1 ) - { - pThis->fAdded = 1; - sat_solver2_add_and( p->pSat, - Vta_ObjId(p, pThis), Vta_ObjId(p, pThis0), Vta_ObjId(p, pThis1), - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - Vec_IntPush( p->vCla2Var, i ); - Vec_IntPush( p->vCla2Var, i ); - Vec_IntPush( p->vCla2Var, i ); - } + pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame ); + pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame ); + sat_solver2_add_and( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Vta_ObjId(p, pThis1), + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + Vec_IntPush( p->vCla2Var, iMainVar ); + Vec_IntPush( p->vCla2Var, iMainVar ); + Vec_IntPush( p->vCla2Var, iMainVar ); +//printf( "Adding node %d (var %d)\n", iObj, iMainVar ); } else if ( Gia_ObjIsRo(p->pGia, pObj) ) { - if ( pThis->iFrame == 0 ) +//printf( "Adding flop %d (var %d)\n", iObj, iMainVar ); + if ( iFrame == 0 ) { - pThis->fAdded = 1; - sat_solver2_add_constraint( p->pSat, pThis->iObj, 1, 0 ); - Vec_IntPush( p->vCla2Var, i ); - Vec_IntPush( p->vCla2Var, i ); + /* + pThis0 = Vga_ManFindOrAdd( p, iObj, -1 ); + sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0 ); + Vec_IntPush( p->vCla2Var, iMainVar ); + Vec_IntPush( p->vCla2Var, iMainVar ); + */ + sat_solver2_add_const( p->pSat, iMainVar, 1, 0 ); + Vec_IntPush( p->vCla2Var, iMainVar ); } else { pObj = Gia_ObjRoToRi( p->pGia, pObj ); - pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); - if ( pThis0 ) - { - pThis->fAdded = 1; - sat_solver2_add_buffer( p->pSat, - Vta_ObjId(p, pThis), Vta_ObjId(p, pThis0), - Gia_ObjFaninC0(pObj), 0 ); - Vec_IntPush( p->vCla2Var, i ); - Vec_IntPush( p->vCla2Var, i ); - } + pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); + sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0 ); + Vec_IntPush( p->vCla2Var, iMainVar ); + Vec_IntPush( p->vCla2Var, iMainVar ); } } else if ( Gia_ObjIsConst0(pObj) ) { - pThis->fAdded = 1; - sat_solver2_add_const( p->pSat, Vta_ObjId(p, pThis), 1, 0 ); - Vec_IntPush( p->vCla2Var, i ); +//printf( "Adding const %d (var %d)\n", iObj, iMainVar ); + sat_solver2_add_const( p->pSat, iMainVar, 1, 0 ); + Vec_IntPush( p->vCla2Var, iMainVar ); } - else if ( !Gia_ObjIsPi(p->pGia, pObj) ) + else //if ( !Gia_ObjIsPi(p->pGia, pObj) ) assert( 0 ); } @@ -1008,25 +1018,28 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ) ***********************************************************************/ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift ) { - Gia_Obj_t * pObj; - Vta_Obj_t * pThis; - int i, Entry, iObjPrev = p->nObjs; + int i, Entry; Vec_IntForEachEntry( vOne, Entry, i ) - { - pObj = Gia_ManObj( p->pGia, Entry & p->nObjMask ); - if ( Gia_ObjIsPi(p->pGia, pObj) ) - continue; - pThis = Vga_ManFindOrAdd( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift ); - pThis->fNew = 0; - // add constraint variable - if ( Gia_ObjIsRo(p->pGia, pObj) && (Entry >> p->nObjBits) + Lift == 0 ) - { - pThis = Vga_ManFindOrAdd( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift ); - pThis->fNew = 0; - } - } - for ( i = iObjPrev; i < p->nObjs; i++ ) - Vga_ManAddClausesOne( p, Vta_ManObj(p, i) ); + Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift ); +} + +/**Function************************************************************* + + Synopsis [Returns the output literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f ) +{ + Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0); + Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); + assert( pThis != NULL && pThis->fAdded ); + return Gia_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) ); } /**Function************************************************************* @@ -1043,19 +1056,24 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift ) int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { Vta_Man_t * p; + Vta_Obj_t * pThis; Vec_Int_t * vCore; Abc_Cex_t * pCex = NULL; - int f, i, Limit, Status, RetValue = -1; + Gia_Obj_t * pObj; + int i, f, Status, RetValue = -1; // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); // start the manager p = Vga_ManStart( pAig, pPars ); // perform initial abstraction + if ( p->pPars->fVerbose ) + printf( "Frame Confl All F0 F1 F2 F3 ...\n" ); for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) { if ( p->pPars->fVerbose ) - printf( "Frame %4d : ", f ); + printf( "%3d :", f ); +//printf( "\n" ); p->pPars->iFrame = f; // realloc storage for abstraction marks if ( f == p->nWords * 32 ) @@ -1065,43 +1083,54 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { // load this timeframe Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 ); +// Vga_ManAddClausesOne( p, 0, f ); // run SAT solver - vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status ); - if ( vCore == NULL && Status == 0 ) + vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status ); + assert( (vCore != NULL) == (Status == 1) ); + if ( Status == -1 ) + break; + if ( Status == 0 ) { // make sure, there was no initial abstraction (otherwise, it was invalid) assert( pAig->vObjClasses == NULL ); // derive counter-example - pCex = NULL; + pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 ); + pCex->iPo = 0; + pCex->iFrame = p->pPars->iFrame; + Vta_ManForEachObj( p, pThis, i ) + { + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ) + Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); + } } } else { - break; - +/* // load the time frame - Limit = Abc_MinInt(3, p->pPars->nFramesStart); + int Limit = Abc_MinInt(3, p->pPars->nFramesStart); for ( i = 1; i <= Limit; i++ ) Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i ); +// Vga_ManAddClausesOne( p, 0, f ); // iterate as long as there are counter-examples - while ( 1 ) - { - vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &RetValue ); - if ( RetValue ) // resource limit is reached - { - assert( vCore == NULL ); + do { + vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status ); + assert( (vCore != NULL) == (Status == 1) ); + if ( Status == -1 ) // resource limit is reached break; - } if ( vCore != NULL ) { - // unroll the solver, add the core + // rollback and add the core // return and double check break; } pCex = Vta_ManRefineAbstraction( p ); - if ( pCex != NULL ) - break; - } + } + while ( pCex == NULL ); + if ( Status == -1 ) // resource limit is reached + break; +*/ } if ( pCex != NULL ) { @@ -1121,7 +1150,11 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // print the result if ( p->pPars->fVerbose ) Vta_ManAbsPrintFrame( p, vCore, f+1 ); + + if ( f == p->pPars->nFramesStart-1 ) + break; } + // analize the results if ( pCex == NULL ) { assert( Vec_PtrSize(p->vCores) > 0 ); @@ -1129,6 +1162,17 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) printf( "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 ) + printf( "SAT solver ran out of resources at %d conflicts in frame %d.\n", pPars->nConfLimit, f ); + else + printf( "SAT solver completed %d frames and produced an abstraction.\n", f+1 ); + } + else + { + ABC_FREE( p->pGia->pCexSeq ); + p->pGia->pCexSeq = pCex; + if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) ) + printf( "Gia_VtaPerform(): CEX verification has failed!\n" ); } Vga_ManStop( p ); return RetValue; diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index bee181c3..480326bd 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -189,11 +189,12 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames ) iStop = (f+1 < Vec_IntSize(vLimit)) ? Vec_IntEntry(vLimit, f+1) : 0; for ( k = iStop - 1; k >= iStart; k-- ) { - pObj = Gia_ManObj(pNew, k); - if ( Gia_ObjIsCo(pObj) ) + assert( Gia_ManObj(pNew, k)->Value > 0 ); + pObj = Gia_ManObj(p, Gia_ManObj(pNew, k)->Value); + if ( Gia_ObjIsCo(pObj) || Gia_ObjIsPi(p, pObj) ) continue; - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - Entry = ((fMax-f) << nObjBits) | pObj->Value; + assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) ); + Entry = ((fMax-f) << nObjBits) | Gia_ObjId(p, pObj); Vec_IntPush( vOne, Entry ); // printf( "%d ", Gia_ManObj(pNew, k)->Value ); } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index b787f713..769006c2 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -277,6 +277,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) nObjMask = (1 << nObjBits) - 1; assert( Gia_ManObjNum(p) <= nObjMask ); // print info about frames + printf( "Frame All F0 F1 F2 F3 ...\n" ); for ( i = 0; i < nFrames; i++ ) { iStart = Vec_IntEntry( vAbs, i+1 ); @@ -298,10 +299,13 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) pCountAll[0]++; } assert( pCountAll[0] == (unsigned)(iStop - iStart) ); - printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); +// printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); + printf( "%3d :", i ); + printf( "%6d", pCountAll[0] ); for ( k = 0; k < nFrames; k++ ) if ( k <= i ) - printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); +// printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); + printf( "%4d", pCountAll[k+1] ); printf( "\n" ); } assert( iStop == Vec_IntSize(vAbs) ); -- cgit v1.2.3