| /**CFile**************************************************************** |
| |
| FileName [absVta.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Abstraction package.] |
| |
| Synopsis [Variable time-frame abstraction.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: absVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "sat/bsat/satSolver2.h" |
| #include "base/main/main.h" |
| #include "abs.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| #define VTA_LARGE 0xFFFFFFF |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Vta_Obj_t_ Vta_Obj_t; // object |
| struct Vta_Obj_t_ |
| { |
| int iObj; |
| int iFrame; |
| int iNext; |
| unsigned Prio : 28; // related to VTA_LARGE |
| unsigned Value : 2; |
| unsigned fAdded : 1; |
| unsigned fVisit : 1; |
| }; |
| |
| typedef struct Vta_Man_t_ Vta_Man_t; // manager |
| struct Vta_Man_t_ |
| { |
| // user data |
| Gia_Man_t * pGia; // AIG manager |
| Abs_Par_t * pPars; // parameters |
| // internal data |
| int nObjs; // the number of objects |
| int nObjsAlloc; // the number of objects allocated |
| int nBins; // number of hash table entries |
| int * pBins; // hash table bins |
| Vta_Obj_t * pObjs; // storage for objects |
| Vec_Int_t * vOrder; // objects in DPS order |
| // abstraction |
| int nObjBits; // the number of bits to represent objects |
| unsigned nObjMask; // object mask |
| 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 |
| int nSeenAll; // seen objects in all frames |
| // other data |
| Vec_Ptr_t * vCores; // unsat core for each frame |
| sat_solver2 * pSat; // incremental SAT solver |
| Vec_Int_t * vAddedNew; // the IDs of variables added to the solver |
| // statistics |
| abctime timeSat; |
| abctime timeUnsat; |
| abctime timeCex; |
| abctime timeOther; |
| }; |
| |
| |
| // ternary simulation |
| |
| #define VTA_VAR0 1 |
| #define VTA_VAR1 2 |
| #define VTA_VARX 3 |
| |
| static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl ) |
| { |
| if ( pThis->Value == VTA_VAR1 && fCompl ) |
| return 1; |
| if ( pThis->Value == VTA_VAR0 && !fCompl ) |
| return 1; |
| return 0; |
| } |
| static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl ) |
| { |
| if ( pThis->Value == VTA_VAR0 && fCompl ) |
| return 1; |
| if ( pThis->Value == VTA_VAR1 && !fCompl ) |
| return 1; |
| return 0; |
| } |
| |
| static inline Vta_Obj_t * Vta_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } |
| static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } |
| |
| #define Vta_ManForEachObj( p, pObj, i ) \ |
| for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ ) |
| #define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i ) \ |
| for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ ) |
| #define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i ) \ |
| for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ ) |
| |
| #define Vta_ManForEachObjVec( vVec, p, pObj, i ) \ |
| for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ ) |
| #define Vta_ManForEachObjVecReverse( vVec, p, pObj, i ) \ |
| for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- ) |
| |
| #define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i ) \ |
| for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ ) |
| #define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i ) \ |
| for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- ) |
| |
| |
| // abstraction is given as an array of integers: |
| // - the first entry is the number of timeframes (F) |
| // - the next (F+1) entries give the beginning position of each timeframe |
| // - the following entries give the object IDs |
| // invariant: assert( vec[vec[0]+1] == size(vec) ); |
| |
| extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting from one array to per-frame arrays.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs ) |
| { |
| Vec_Ptr_t * vFrames; |
| Vec_Int_t * vFrame; |
| int i, k, Entry, iStart, iStop = -1; |
| int nFrames = Vec_IntEntry( vAbs, 0 ); |
| assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) ); |
| vFrames = Vec_PtrAlloc( nFrames ); |
| for ( i = 0; i < nFrames; i++ ) |
| { |
| iStart = Vec_IntEntry( vAbs, i+1 ); |
| iStop = Vec_IntEntry( vAbs, i+2 ); |
| vFrame = Vec_IntAlloc( iStop - iStart ); |
| Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop ) |
| Vec_IntPush( vFrame, Entry ); |
| Vec_PtrPush( vFrames, vFrame ); |
| } |
| assert( iStop == Vec_IntSize(vAbs) ); |
| return vFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting from per-frame arrays to one integer array.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames ) |
| { |
| Vec_Int_t * vOne, * vAbs; |
| int i, k, Entry, nSize; |
| vAbs = Vec_IntAlloc( 2 + Vec_VecSize(vFrames) + Vec_VecSizeSize(vFrames) ); |
| Vec_IntPush( vAbs, Vec_VecSize(vFrames) ); |
| nSize = Vec_VecSize(vFrames) + 2; |
| Vec_VecForEachLevelInt( vFrames, vOne, i ) |
| { |
| Vec_IntPush( vAbs, nSize ); |
| nSize += Vec_IntSize( vOne ); |
| } |
| Vec_IntPush( vAbs, nSize ); |
| assert( Vec_IntSize(vAbs) == Vec_VecSize(vFrames) + 2 ); |
| Vec_VecForEachLevelInt( vFrames, vOne, i ) |
| Vec_IntForEachEntry( vOne, Entry, k ) |
| Vec_IntPush( vAbs, Entry ); |
| assert( Vec_IntEntry(vAbs, Vec_IntEntry(vAbs,0)+1) == Vec_IntSize(vAbs) ); |
| return vAbs; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Detects how many frames are completed.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline Vec_Int_t * Vta_ManDeriveAbsAll( Vec_Int_t * p, int nWords ) |
| { |
| Vec_Int_t * vRes; |
| unsigned * pThis; |
| int i, w, nObjs = Vec_IntSize(p) / nWords; |
| assert( Vec_IntSize(p) % nWords == 0 ); |
| vRes = Vec_IntAlloc( nObjs ); |
| for ( i = 0; i < nObjs; i++ ) |
| { |
| pThis = (unsigned *)Vec_IntEntryP( p, nWords * i ); |
| for ( w = 0; w < nWords; w++ ) |
| if ( pThis[w] ) |
| break; |
| Vec_IntPush( vRes, (int)(w < nWords) ); |
| } |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect nodes/flops involved in different timeframes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Vec_IntDoubleWidth( Vec_Int_t * p, int nWords ) |
| { |
| int * pArray = ABC_CALLOC( int, Vec_IntSize(p) * 2 ); |
| int i, w, nObjs = Vec_IntSize(p) / nWords; |
| assert( Vec_IntSize(p) % nWords == 0 ); |
| for ( i = 0; i < nObjs; i++ ) |
| for ( w = 0; w < nWords; w++ ) |
| pArray[2 * nWords * i + w] = p->pArray[nWords * i + w]; |
| ABC_FREE( p->pArray ); |
| p->pArray = pArray; |
| p->nSize *= 2; |
| p->nCap = p->nSize; |
| return 2 * nWords; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Vga_ManHash( int iObj, int iFrame, int nBins ) |
| { |
| return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins; |
| } |
| static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame ) |
| { |
| Vta_Obj_t * pThis; |
| int * pPlace = p->pBins + Vga_ManHash( iObj, iFrame, p->nBins ); |
| for ( pThis = Vta_ManObj(p, *pPlace); |
| pThis; pPlace = &pThis->iNext, |
| pThis = Vta_ManObj(p, *pPlace) ) |
| if ( pThis->iObj == iObj && pThis->iFrame == iFrame ) |
| break; |
| return pPlace; |
| } |
| static inline Vta_Obj_t * Vga_ManFind( Vta_Man_t * p, int iObj, int iFrame ) |
| { |
| int * pPlace = Vga_ManLookup( p, iObj, iFrame ); |
| return Vta_ManObj(p, *pPlace); |
| } |
| static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame ) |
| { |
| Vta_Obj_t * pThis; |
| int i, * pPlace; |
| assert( iObj >= 0 && iFrame >= -1 ); |
| if ( p->nObjs == p->nObjsAlloc ) |
| { |
| // resize objects |
| p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc ); |
| memset( p->pObjs + p->nObjsAlloc, 0, p->nObjsAlloc * sizeof(Vta_Obj_t) ); |
| p->nObjsAlloc *= 2; |
| // rehash entries in the table |
| ABC_FREE( p->pBins ); |
| p->nBins = Abc_PrimeCudd( 2 * p->nBins ); |
| p->pBins = ABC_CALLOC( int, p->nBins ); |
| Vta_ManForEachObj( p, pThis, i ) |
| { |
| pThis->iNext = 0; |
| pPlace = Vga_ManLookup( p, pThis->iObj, pThis->iFrame ); |
| assert( *pPlace == 0 ); |
| *pPlace = i; |
| } |
| } |
| pPlace = Vga_ManLookup( p, iObj, iFrame ); |
| if ( *pPlace ) |
| return Vta_ManObj(p, *pPlace); |
| *pPlace = p->nObjs++; |
| pThis = Vta_ManObj(p, *pPlace); |
| pThis->iObj = iObj; |
| pThis->iFrame = iFrame; |
| return pThis; |
| } |
| static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame ) |
| { |
| int * pPlace = Vga_ManLookup( p, iObj, iFrame ); |
| Vta_Obj_t * pThis = Vta_ManObj(p, *pPlace); |
| assert( pThis != NULL ); |
| *pPlace = pThis->iNext; |
| pThis->iNext = -1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives counter-example using current assignments.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Vga_ManDeriveCex( Vta_Man_t * p ) |
| { |
| Abc_Cex_t * pCex; |
| Vta_Obj_t * pThis; |
| Gia_Obj_t * pObj; |
| int i; |
| pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 ); |
| pCex->iPo = 0; |
| pCex->iFrame = p->pPars->iFrame; |
| Vta_ManForEachObjObj( p, pThis, pObj, i ) |
| if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ) |
| Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); |
| return pCex; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Remaps core into frame/node pairs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore ) |
| { |
| Vta_Obj_t * pThis; |
| int i, Entry; |
| Vec_IntForEachEntry( vCore, Entry, i ) |
| { |
| pThis = Vta_ManObj( p, Entry ); |
| Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj; |
| Vec_IntWriteEntry( vCore, i, Entry ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compares two objects by their distance.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Vta_ManComputeDepthIncrease( Vta_Obj_t ** pp1, Vta_Obj_t ** pp2 ) |
| { |
| int Diff = (*pp1)->Prio - (*pp2)->Prio; |
| if ( Diff < 0 ) |
| return -1; |
| if ( Diff > 0 ) |
| return 1; |
| Diff = (*pp1) - (*pp2); |
| if ( Diff < 0 ) |
| return -1; |
| if ( Diff > 0 ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if the object is already used.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj ) |
| { |
| int i; |
| unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj ); |
| for ( i = 0; i < p->nWords; i++ ) |
| if ( pInfo[i] ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds predecessors of the node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * pObj, Vta_Obj_t ** ppThis0, Vta_Obj_t ** ppThis1 ) |
| { |
| *ppThis0 = NULL; |
| *ppThis1 = NULL; |
| // if ( !pThis->fAdded ) |
| // return; |
| assert( !Gia_ObjIsPi(p->pGia, pObj) ); |
| if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) ) |
| return; |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame ); |
| *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame ); |
| // assert( *ppThis0 && *ppThis1 ); |
| return; |
| } |
| assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 ); |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); |
| // assert( *ppThis0 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect const/PI/RO/AND in a topological order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrder ) |
| { |
| Gia_Obj_t * pObj; |
| Vta_Obj_t * pThis0, * pThis1; |
| if ( pThis->fVisit ) |
| return; |
| pThis->fVisit = 1; |
| pObj = Gia_ManObj( p->pGia, pThis->iObj ); |
| if ( pThis->fAdded ) |
| { |
| Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); |
| if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder ); |
| if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder ); |
| } |
| Vec_IntPush( vOrder, Vta_ObjId(p, pThis) ); |
| } |
| Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f ) |
| { |
| Vta_Obj_t * pThis; |
| Gia_Obj_t * pObj; |
| Vec_IntClear( p->vOrder ); |
| pObj = Gia_ManPo( p->pGia, 0 ); |
| pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); |
| assert( pThis != NULL ); |
| assert( !pThis->fVisit ); |
| Vta_ManCollectNodes_rec( p, pThis, p->vOrder ); |
| assert( pThis->fVisit ); |
| return p->vOrder; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines abstraction.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vta_ManSatVerify( Vta_Man_t * p ) |
| { |
| Vta_Obj_t * pThis, * pThis0, * pThis1; |
| Gia_Obj_t * pObj; |
| int i; |
| Vta_ManForEachObj( p, pThis, i ) |
| pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0); |
| Vta_ManForEachObjObj( p, pThis, pObj, i ) |
| { |
| if ( !pThis->fAdded ) |
| continue; |
| Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| if ( pThis->Value == VTA_VAR1 ) |
| assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) ); |
| else if ( pThis->Value == VTA_VAR0 ) |
| assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ); |
| else assert( 0 ); |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| { |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| if ( pThis->iFrame == 0 ) |
| assert( pThis->Value == VTA_VAR0 ); |
| else if ( pThis->Value == VTA_VAR0 ) |
| assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) ); |
| else if ( pThis->Value == VTA_VAR1 ) |
| assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) ); |
| else assert( 0 ); |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines abstraction.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd ) |
| { |
| Vta_Obj_t * pThis; |
| Gia_Obj_t * pObj; |
| // profile the added ones |
| int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 ); |
| Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i ) |
| pCounters[pThis->iFrame]++; |
| for ( i = 0; i <= p->pPars->iFrame; i++ ) |
| Abc_Print( 1, "%2d", pCounters[i] ); |
| Abc_Print( 1, "***\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines abstraction.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) |
| { |
| int fVerify = 0; |
| Abc_Cex_t * pCex = NULL; |
| Vec_Int_t * vOrder, * vTermsToAdd; |
| Vec_Ptr_t * vTermsUsed, * vTermsUnused; |
| Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop; |
| Gia_Obj_t * pObj; |
| int i, Counter; |
| |
| if ( fVerify ) |
| Vta_ManSatVerify( p ); |
| |
| // collect nodes in a topological order |
| vOrder = Vta_ManCollectNodes( p, f ); |
| Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) |
| { |
| pThis->Prio = VTA_LARGE; |
| pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0; |
| pThis->fVisit = 0; |
| } |
| |
| // verify |
| if ( fVerify ) |
| Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) |
| { |
| if ( !pThis->fAdded ) |
| continue; |
| Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| if ( pThis->Value == VTA_VAR1 ) |
| assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) ); |
| else if ( pThis->Value == VTA_VAR0 ) |
| assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ); |
| else assert( 0 ); |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| { |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| if ( pThis->iFrame == 0 ) |
| assert( pThis->Value == VTA_VAR0 ); |
| else if ( pThis->Value == VTA_VAR0 ) |
| assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) ); |
| else if ( pThis->Value == VTA_VAR1 ) |
| assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) ); |
| else assert( 0 ); |
| } |
| } |
| |
| // compute distance in reverse order |
| pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) ); |
| pThis->Prio = 1; |
| // collect used and unused terms |
| vTermsUsed = Vec_PtrAlloc( 1015 ); |
| vTermsUnused = Vec_PtrAlloc( 1016 ); |
| Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i ) |
| { |
| // there is no unreachable states |
| assert( pThis->Prio < VTA_LARGE ); |
| // skip constants and PIs |
| if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ) |
| { |
| pThis->Prio = 0; // set highest priority |
| continue; |
| } |
| // collect terminals |
| assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); |
| if ( !pThis->fAdded ) |
| { |
| assert( pThis->Prio > 0 ); |
| if ( Vta_ManObjIsUsed(p, pThis->iObj) ) |
| Vec_PtrPush( vTermsUsed, pThis ); |
| else |
| Vec_PtrPush( vTermsUnused, pThis ); |
| continue; |
| } |
| // propagate |
| Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); |
| if ( pThis0 ) |
| pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 ); |
| if ( pThis1 ) |
| pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 ); |
| } |
| |
| /* |
| Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i ) |
| if ( pThis->Prio > 0 ) |
| pThis->Prio = 10; |
| */ |
| /* |
| // update priorities according to reconvergence counters |
| Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) |
| { |
| Vta_Obj_t * pThis0, * pThis1; |
| Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj ); |
| Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); |
| pThis->Prio += 10000000; |
| if ( pThis0 ) |
| pThis->Prio -= 1000000 * pThis0->fAdded; |
| if ( pThis1 ) |
| pThis->Prio -= 1000000 * pThis1->fAdded; |
| } |
| Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i ) |
| { |
| Vta_Obj_t * pThis0, * pThis1; |
| Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj ); |
| Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 ); |
| pThis->Prio += 10000000; |
| if ( pThis0 ) |
| pThis->Prio -= 1000000 * pThis0->fAdded; |
| if ( pThis1 ) |
| pThis->Prio -= 1000000 * pThis1->fAdded; |
| } |
| */ |
| |
| |
| // update priorities according to reconvergence counters |
| Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) |
| pThis->Prio = pThis->iObj; |
| Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i ) |
| pThis->Prio = pThis->iObj; |
| |
| |
| // objects with equal distance should receive priority based on number |
| // those objects whose prototypes have been added in other timeframes |
| // should have higher priority than the current object |
| Vec_PtrSort( vTermsUsed, (int (*)(void))Vta_ManComputeDepthIncrease ); |
| Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease ); |
| if ( Vec_PtrSize(vTermsUsed) > 1 ) |
| { |
| pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0); |
| pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed); |
| assert( pThis0->Prio <= pThis1->Prio ); |
| } |
| // assign the priority based on these orders |
| Counter = 1; |
| Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) |
| pThis->Prio = Counter++; |
| Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i ) |
| pThis->Prio = Counter++; |
| // Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) ); |
| |
| |
| // propagate in the direct order |
| Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) |
| { |
| assert( pThis->fVisit == 0 ); |
| assert( pThis->Prio < VTA_LARGE ); |
| // skip terminal objects |
| if ( !pThis->fAdded ) |
| continue; |
| // assumes that values are assigned!!! |
| assert( pThis->Value != 0 ); |
| // propagate |
| 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 ); |
| assert( pThis0 && pThis1 ); |
| if ( pThis->Value == VTA_VAR1 ) |
| { |
| assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) ); |
| pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio ); |
| } |
| else if ( pThis->Value == VTA_VAR0 ) |
| { |
| if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) |
| pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!! |
| else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) ) |
| pThis->Prio = pThis0->Prio; |
| else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) |
| pThis->Prio = pThis1->Prio; |
| else assert( 0 ); |
| } |
| else assert( 0 ); |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| { |
| if ( pThis->iFrame > 0 ) |
| { |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); |
| assert( pThis0 ); |
| pThis->Prio = pThis0->Prio; |
| } |
| else |
| pThis->Prio = 0; |
| } |
| else if ( Gia_ObjIsConst0(pObj) ) |
| pThis->Prio = 0; |
| else |
| assert( 0 ); |
| } |
| |
| // select important values |
| pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) ); |
| pTop->fVisit = 1; |
| vTermsToAdd = Vec_IntAlloc( 100 ); |
| Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i ) |
| { |
| if ( !pThis->fVisit ) |
| continue; |
| pThis->fVisit = 0; |
| assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio ); |
| // skip terminal objects |
| if ( !pThis->fAdded ) |
| { |
| assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ); |
| Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) ); |
| continue; |
| } |
| // assumes that values are assigned!!! |
| assert( pThis->Value != 0 ); |
| // propagate |
| 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 ); |
| assert( pThis0 && pThis1 ); |
| if ( pThis->Value == VTA_VAR1 ) |
| { |
| assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) ); |
| assert( pThis0->Prio <= pThis->Prio ); |
| assert( pThis1->Prio <= pThis->Prio ); |
| pThis0->fVisit = 1; |
| pThis1->fVisit = 1; |
| } |
| else if ( pThis->Value == VTA_VAR0 ) |
| { |
| if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) |
| { |
| if ( pThis0->fVisit ) |
| { |
| } |
| else if ( pThis1->fVisit ) |
| { |
| } |
| else if ( pThis0->Prio <= pThis1->Prio ) // choice!!! |
| { |
| pThis0->fVisit = 1; |
| assert( pThis0->Prio == pThis->Prio ); |
| } |
| else |
| { |
| pThis1->fVisit = 1; |
| assert( pThis1->Prio == pThis->Prio ); |
| } |
| } |
| else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) ) |
| { |
| pThis0->fVisit = 1; |
| assert( pThis0->Prio == pThis->Prio ); |
| } |
| else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) |
| { |
| pThis1->fVisit = 1; |
| assert( pThis1->Prio == pThis->Prio ); |
| } |
| else assert( 0 ); |
| } |
| else assert( 0 ); |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| { |
| if ( pThis->iFrame > 0 ) |
| { |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); |
| assert( pThis0 ); |
| pThis0->fVisit = 1; |
| assert( pThis0->Prio == pThis->Prio ); |
| } |
| } |
| else if ( !Gia_ObjIsConst0(pObj) ) |
| assert( 0 ); |
| } |
| |
| if ( p->pPars->fAddLayer ) |
| { |
| // 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; |
| } |
| // printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) ); |
| //Vec_IntReverseOrder( vTermsToAdd ); |
| //Vec_IntSort( vTermsToAdd, 1 ); |
| |
| |
| // cleanup |
| Vec_PtrFree( vTermsUsed ); |
| Vec_PtrFree( vTermsUnused ); |
| |
| |
| if ( fVerify ) |
| { |
| // verify |
| Vta_ManForEachObjVec( vOrder, p, pThis, i ) |
| pThis->Value = VTA_VARX; |
| Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) |
| { |
| assert( !pThis->fAdded ); |
| pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0; |
| } |
| // simulate |
| Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) |
| { |
| assert( pThis->fVisit == 0 ); |
| if ( !pThis->fAdded ) |
| continue; |
| 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 ); |
| assert( pThis0 && pThis1 ); |
| if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) ) |
| pThis->Value = VTA_VAR1; |
| else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) |
| pThis->Value = VTA_VAR0; |
| else |
| pThis->Value = VTA_VARX; |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| { |
| if ( pThis->iFrame > 0 ) |
| { |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); |
| assert( pThis0 ); |
| if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) ) |
| pThis->Value = VTA_VAR0; |
| else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) ) |
| pThis->Value = VTA_VAR1; |
| else |
| pThis->Value = VTA_VARX; |
| } |
| else |
| { |
| pThis->Value = VTA_VAR0; |
| } |
| } |
| else if ( Gia_ObjIsConst0(pObj) ) |
| { |
| pThis->Value = VTA_VAR0; |
| } |
| else assert( 0 ); |
| // double check the solver |
| assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) ); |
| } |
| |
| // check the output |
| if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) ) |
| Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" ); |
| // else |
| // Abc_Print( 1, "Verification OK.\n" ); |
| } |
| |
| |
| // produce true counter-example |
| if ( pTop->Prio == 0 ) |
| pCex = Vga_ManDeriveCex( p ); |
| else |
| { |
| // Vta_ManProfileAddition( p, vTermsToAdd ); |
| |
| Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i ) |
| if ( !Gia_ObjIsPi(p->pGia, pObj) ) |
| Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame ); |
| sat_solver2_simplify( p->pSat ); |
| } |
| p->nObjAdded += Vec_IntSize(vTermsToAdd); |
| Vec_IntFree( vTermsToAdd ); |
| return pCex; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars ) |
| { |
| Vta_Man_t * p; |
| p = ABC_CALLOC( Vta_Man_t, 1 ); |
| p->pGia = pGia; |
| p->pPars = pPars; |
| // internal data |
| p->nObjsAlloc = (1 << 18); |
| p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc ); |
| p->nObjs = 1; |
| p->nBins = Abc_PrimeCudd( 2*p->nObjsAlloc ); |
| p->pBins = ABC_CALLOC( int, p->nBins ); |
| p->vOrder = Vec_IntAlloc( 1013 ); |
| // abstraction |
| p->nObjBits = Abc_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->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) ); |
| p->nSeenGla = 1; |
| p->nSeenAll = 1; |
| // other data |
| p->vCores = Vec_PtrAlloc( 100 ); |
| p->pSat = sat_solver2_new(); |
| p->pSat->pPrf1 = Vec_SetAlloc( 20 ); |
| // p->pSat->fVerbose = p->pPars->fVerbose; |
| // sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax ); |
| p->pSat->nLearntStart = p->pPars->nLearnedStart; |
| p->pSat->nLearntDelta = p->pPars->nLearnedDelta; |
| p->pSat->nLearntRatio = p->pPars->nLearnedPerce; |
| p->pSat->nLearntMax = p->pSat->nLearntStart; |
| // start the abstraction |
| assert( pGia->vObjClasses != NULL ); |
| p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses ); |
| p->vAddedNew = Vec_IntAlloc( 1000 ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Delete manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vga_ManStop( Vta_Man_t * p ) |
| { |
| 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 ); |
| Vec_VecFreeP( (Vec_Vec_t **)&p->vCores ); |
| Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames ); |
| Vec_BitFreeP( &p->vSeenGla ); |
| Vec_IntFreeP( &p->vSeens ); |
| Vec_IntFreeP( &p->vOrder ); |
| Vec_IntFreeP( &p->vAddedNew ); |
| sat_solver2_delete( p->pSat ); |
| ABC_FREE( p->pBins ); |
| ABC_FREE( p->pObjs ); |
| ABC_FREE( p ); |
| } |
| |
| /**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 ); |
| if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) ) |
| return -Vta_ObjId(p, pThis); |
| return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds the set of clauses involved in the UNSAT core.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) |
| { |
| abctime clk = Abc_Clock(); |
| Vec_Int_t * vCore; |
| int RetValue, nConfPrev = pSat->stats.conflicts; |
| if ( piRetValue ) |
| *piRetValue = 1; |
| // consider special case when PO points to the flop |
| // this leads to immediate conflict in the first timeframe |
| if ( iLit < 0 ) |
| { |
| vCore = Vec_IntAlloc( 1 ); |
| Vec_IntPush( vCore, -iLit ); |
| return vCore; |
| } |
| // 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 ( pnConfls ) |
| *pnConfls = (int)pSat->stats.conflicts - nConfPrev; |
| if ( RetValue == l_Undef ) |
| { |
| if ( piRetValue ) |
| *piRetValue = -1; |
| return NULL; |
| } |
| if ( RetValue == l_True ) |
| { |
| if ( piRetValue ) |
| *piRetValue = 0; |
| return NULL; |
| } |
| if ( fVerbose ) |
| { |
| // Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev ); |
| // Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); |
| // Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| assert( RetValue == l_False ); |
| // derive the UNSAT core |
| clk = Abc_Clock(); |
| vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); |
| if ( fVerbose ) |
| { |
| // Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); |
| // Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| return vCore; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose ) |
| { |
| unsigned * pInfo; |
| int * pCountAll = NULL, * pCountUni = NULL; |
| int i, iFrame, iObj, Entry, fChanges = 0; |
| // print info about frames |
| if ( vCore ) |
| { |
| pCountAll = ABC_CALLOC( int, nFrames + 1 ); |
| pCountUni = ABC_CALLOC( int, nFrames + 1 ); |
| Vec_IntForEachEntry( vCore, Entry, i ) |
| { |
| iObj = (Entry & p->nObjMask); |
| iFrame = (Entry >> p->nObjBits); |
| assert( iFrame < nFrames ); |
| pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj ); |
| if ( !Abc_InfoHasBit(pInfo, iFrame) ) |
| { |
| Abc_InfoSetBit( pInfo, iFrame ); |
| pCountUni[iFrame+1]++; |
| pCountUni[0]++; |
| p->nSeenAll++; |
| } |
| pCountAll[iFrame+1]++; |
| pCountAll[0]++; |
| if ( !Vec_BitEntry(p->vSeenGla, iObj) ) |
| { |
| Vec_BitWriteEntry(p->vSeenGla, iObj, 1); |
| p->nSeenGla++; |
| fChanges = 1; |
| } |
| } |
| } |
| if ( !fVerbose ) |
| { |
| ABC_FREE( pCountAll ); |
| ABC_FREE( pCountUni ); |
| return fChanges; |
| } |
| |
| if ( Abc_FrameIsBatchMode() && !vCore ) |
| return fChanges; |
| |
| // Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] ); |
| Abc_Print( 1, "%4d :", nFrames-1 ); |
| Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) ); |
| Abc_Print( 1, "%6d", p->nSeenGla ); |
| Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) ); |
| Abc_Print( 1, "%8d", nConfls ); |
| if ( nCexes == 0 ) |
| Abc_Print( 1, "%5c", '-' ); |
| else |
| Abc_Print( 1, "%5d", nCexes ); |
| // Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); |
| Abc_PrintInt( sat_solver2_nvars(p->pSat) ); |
| Abc_PrintInt( sat_solver2_nclauses(p->pSat) ); |
| Abc_PrintInt( sat_solver2_nlearnts(p->pSat) ); |
| if ( vCore == NULL ) |
| { |
| Abc_Print( 1, " ..." ); |
| // for ( k = 0; k < 7; k++ ) |
| // Abc_Print( 1, " " ); |
| Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); |
| Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); |
| Abc_Print( 1, "\r" ); |
| } |
| else |
| { |
| Abc_PrintInt( pCountAll[0] ); |
| /* |
| if ( nFrames > 7 ) |
| { |
| for ( k = 0; k < 3; k++ ) |
| Abc_Print( 1, "%5d", pCountAll[k+1] ); |
| Abc_Print( 1, " ..." ); |
| for ( k = nFrames-3; k < nFrames; k++ ) |
| Abc_Print( 1, "%5d", pCountAll[k+1] ); |
| } |
| else |
| { |
| for ( k = 0; k < nFrames; k++ ) |
| Abc_Print( 1, "%5d", pCountAll[k+1] ); |
| for ( k = nFrames; k < 7; k++ ) |
| Abc_Print( 1, " " ); |
| } |
| */ |
| Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); |
| Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); |
| Abc_Print( 1, "\n" ); |
| } |
| fflush( stdout ); |
| |
| if ( vCore ) |
| { |
| ABC_FREE( pCountAll ); |
| ABC_FREE( pCountUni ); |
| } |
| return fChanges; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds clauses to the solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ) |
| { |
| Vta_Obj_t * pThis0, * pThis1; |
| Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); |
| Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame ); |
| int iThis0, iMainVar = Vta_ObjId(p, pThis); |
| assert( pThis->iObj == iObj && pThis->iFrame == iFrame ); |
| if ( pThis->fAdded ) |
| return; |
| pThis->fAdded = 1; |
| Vec_IntPush( p->vAddedNew, iMainVar ); |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame ); |
| iThis0 = Vta_ObjId(p, pThis0); |
| pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame ); |
| sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1), |
| Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar ); |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| { |
| if ( iFrame == 0 ) |
| { |
| if ( p->pPars->fUseTermVars ) |
| { |
| pThis0 = Vga_ManFindOrAdd( p, iObj, -1 ); |
| sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar ); |
| } |
| else |
| { |
| sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar ); |
| } |
| } |
| else |
| { |
| pObj = Gia_ObjRoToRi( p->pGia, pObj ); |
| pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 ); |
| sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar ); |
| } |
| } |
| else if ( Gia_ObjIsConst0(pObj) ) |
| { |
| sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar ); |
| } |
| else //if ( !Gia_ObjIsPi(p->pGia, pObj) ) |
| assert( 0 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift ) |
| { |
| int i, Entry; |
| Vec_IntForEachEntry( vOne, Entry, i ) |
| Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift ); |
| sat_solver2_simplify( p->pSat ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift ) |
| { |
| int i, Entry, iObj, iFrame; |
| Vec_IntForEachEntry( vCore, Entry, i ) |
| { |
| iObj = (Entry & p->nObjMask); |
| iFrame = (Entry >> p->nObjBits); |
| Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift ); |
| } |
| Abc_Print( 1, "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Vga_ManRollBack( Vta_Man_t * p, int nObjOld ) |
| { |
| Vta_Obj_t * pThis = p->pObjs + nObjOld; |
| Vta_Obj_t * pLimit = p->pObjs + p->nObjs; |
| int i, Entry; |
| for ( ; pThis < pLimit; pThis++ ) |
| Vga_ManDelete( p, pThis->iObj, pThis->iFrame ); |
| memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) ); |
| p->nObjs = nObjOld; |
| Vec_IntForEachEntry( p->vAddedNew, Entry, i ) |
| if ( Entry < p->nObjs ) |
| { |
| pThis = Vta_ManObj(p, Entry); |
| assert( pThis->fAdded == 1 ); |
| pThis->fAdded = 0; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Send abstracted model or send cancel.] |
| |
| Description [Counter-example will be sent automatically when &vta terminates.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_VtaSendAbsracted( Vta_Man_t * p, int fVerbose ) |
| { |
| Gia_Man_t * pAbs; |
| assert( Abc_FrameIsBridgeMode() ); |
| // if ( fVerbose ) |
| // Abc_Print( 1, "Sending abstracted model...\n" ); |
| // create obj classes |
| Vec_IntFreeP( &p->pGia->vObjClasses ); |
| p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); |
| // create gate classes |
| Vec_IntFreeP( &p->pGia->vGateClasses ); |
| p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses ); |
| Vec_IntFreeP( &p->pGia->vObjClasses ); |
| // create abstrated model |
| pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses ); |
| Vec_IntFreeP( &p->pGia->vGateClasses ); |
| // send it out |
| Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST ); |
| Gia_ManStop( pAbs ); |
| } |
| void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose ) |
| { |
| extern int Gia_ManToBridgeBadAbs( FILE * pFile ); |
| assert( Abc_FrameIsBridgeMode() ); |
| // if ( fVerbose ) |
| // Abc_Print( 1, "Cancelling previously sent model...\n" ); |
| Gia_ManToBridgeBadAbs( stdout ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Send abstracted model or send cancel.] |
| |
| Description [Counter-example will be sent automatically when &vta terminates.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose ) |
| { |
| char * pFileNameDef = "vabs.aig"; |
| char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef; |
| Gia_Man_t * pAbs; |
| if ( fVerbose ) |
| Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); |
| // create obj classes |
| Vec_IntFreeP( &p->pGia->vObjClasses ); |
| p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); |
| // create gate classes |
| Vec_IntFreeP( &p->pGia->vGateClasses ); |
| p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses ); |
| Vec_IntFreeP( &p->pGia->vObjClasses ); |
| // create abstrated model |
| pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses ); |
| Vec_IntFreeP( &p->pGia->vGateClasses ); |
| // send it out |
| Gia_AigerWrite( pAbs, pFileName, 0, 0 ); |
| Gia_ManStop( pAbs ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Print memory report.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_VtaPrintMemory( Vta_Man_t * p ) |
| { |
| double memTot = 0; |
| double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); |
| double memSat = sat_solver2_memory( p->pSat, 1 ); |
| double memPro = sat_solver2_memory_proof( p->pSat ); |
| double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int); |
| double memOth = sizeof(Vta_Man_t); |
| memOth += Vec_IntCap(p->vOrder) * sizeof(int); |
| memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames ); |
| memOth += Vec_BitCap(p->vSeenGla) * sizeof(int); |
| memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores ); |
| memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); |
| memTot = memAig + memSat + memPro + memMap + memOth; |
| ABC_PRMP( "Memory: AIG ", memAig, memTot ); |
| ABC_PRMP( "Memory: SAT ", memSat, memTot ); |
| ABC_PRMP( "Memory: Proof ", memPro, memTot ); |
| ABC_PRMP( "Memory: Map ", memMap, memTot ); |
| ABC_PRMP( "Memory: Other ", memOth, memTot ); |
| ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect nodes/flops involved in different timeframes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) |
| { |
| Vta_Man_t * p; |
| Vec_Int_t * vCore; |
| Abc_Cex_t * pCex = NULL; |
| int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0; |
| abctime clk = Abc_Clock(), clk2; |
| // preconditions |
| assert( Gia_ManPoNum(pAig) == 1 ); |
| assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); |
| if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) |
| { |
| if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ) |
| { |
| 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" ); |
| return 0; |
| } |
| |
| // compute intial abstraction |
| if ( pAig->vObjClasses == NULL ) |
| { |
| pAig->vObjClasses = Vec_IntAlloc( 5 ); |
| Vec_IntPush( pAig->vObjClasses, 1 ); |
| Vec_IntPush( pAig->vObjClasses, 3 ); |
| Vec_IntPush( pAig->vObjClasses, 4 ); |
| Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ); |
| } |
| // start the manager |
| p = Vga_ManStart( pAig, pPars ); |
| // set runtime limit |
| if ( p->pPars->nTimeOut ) |
| sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() ); |
| // perform initial abstraction |
| if ( p->pPars->fVerbose ) |
| { |
| Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" ); |
| Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%\n", |
| pPars->nFramesPast, 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 %% Confl Cex SatVar Core F0 F1 F2 ...\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++ ) |
| { |
| int nConflsBeg = sat_solver2_nconflicts(p->pSat); |
| p->pPars->iFrame = f; |
| // realloc storage for abstraction marks |
| if ( f == p->nWords * 32 ) |
| p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords ); |
| |
| // 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 |
| { |
| 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 = Abc_Clock(); |
| vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), 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 && Abc_Clock() > p->pSat->nRuntimeLimit ) |
| { |
| Vga_ManRollBack( p, nObjOld ); |
| goto finish; |
| } |
| if ( vCore != NULL ) |
| { |
| p->timeUnsat += Abc_Clock() - clk2; |
| break; |
| } |
| p->timeSat += Abc_Clock() - clk2; |
| assert( Status == 0 ); |
| p->nCexes++; |
| // perform the refinement |
| clk2 = Abc_Clock(); |
| pCex = Vta_ManRefineAbstraction( p, f ); |
| p->timeCex += Abc_Clock() - clk2; |
| if ( pCex != NULL ) |
| goto finish; |
| // print the result (do not count it towards change) |
| Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_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 ); |
| // load this timeframe |
| Vga_ManLoadSlice( p, vCore, 0 ); |
| Vec_IntFree( vCore ); |
| |
| // run SAT solver |
| clk2 = Abc_Clock(); |
| vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); |
| p->timeUnsat += Abc_Clock() - clk2; |
| assert( (vCore != NULL) == (Status == 1) ); |
| if ( Status == -1 ) // resource limit is reached |
| break; |
| if ( Status == 0 ) |
| { |
| Vta_ManSatVerify( p ); |
| // make sure, there was no initial abstraction (otherwise, it was invalid) |
| assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart ); |
| pCex = Vga_ManDeriveCex( p ); |
| break; |
| } |
| // add the core |
| Vta_ManUnsatCoreRemap( p, vCore ); |
| // add in direct topological order |
| Vec_IntSort( vCore, 1 ); |
| Vec_PtrPush( p->vCores, vCore ); |
| // print the result |
| if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) ) |
| { |
| // 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 |
| if ( fOneIsSent ) |
| Gia_VtaSendCancel( p, pPars->fVerbose ); |
| // send new one |
| Gia_VtaSendAbsracted( p, pPars->fVerbose ); |
| fOneIsSent = 1; |
| } |
| } |
| // dump the model |
| if ( p->pPars->fDumpVabs && (f & 1) ) |
| { |
| char Command[1000]; |
| Abc_FrameSetStatus( -1 ); |
| Abc_FrameSetCex( NULL ); |
| Abc_FrameSetNFrames( f+1 ); |
| sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "vtabs.aig"), ".status") ); |
| Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ); |
| Gia_VtaDumpAbsracted( p, pPars->fVerbose ); |
| } |
| // check if the number of objects is below limit |
| if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 ) |
| { |
| Status = -1; |
| break; |
| } |
| } |
| finish: |
| // analize the results |
| if ( pCex == NULL ) |
| { |
| if ( p->pPars->fVerbose && Status == -1 ) |
| printf( "\n" ); |
| if ( Vec_PtrSize(p->vCores) == 0 ) |
| Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " ); |
| else |
| { |
| assert( Vec_PtrSize(p->vCores) > 0 ); |
| // 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 ) |
| { |
| if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) |
| 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, "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 |
| Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); |
| } |
| else |
| { |
| p->pPars->iFrame++; |
| Abc_Print( 1, "VTA completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); |
| } |
| } |
| } |
| else |
| { |
| if ( p->pPars->fVerbose ) |
| printf( "\n" ); |
| ABC_FREE( p->pGia->pCexSeq ); |
| p->pGia->pCexSeq = pCex; |
| if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) ) |
| Abc_Print( 1, " Gia_VtaPerform(): CEX verification has failed!\n" ); |
| Abc_Print( 1, "Counter-example detected in frame %d. ", f ); |
| p->pPars->iFrame = pCex->iFrame - 1; |
| Vec_IntFreeP( &pAig->vObjClasses ); |
| RetValue = 0; |
| } |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| |
| if ( p->pPars->fVerbose ) |
| { |
| p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex; |
| ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk ); |
| ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk ); |
| ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk ); |
| ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk ); |
| ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk ); |
| Gia_VtaPrintMemory( p ); |
| } |
| |
| Vga_ManStop( p ); |
| fflush( stdout ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect nodes/flops involved in different timeframes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars ) |
| { |
| int RetValue = -1; |
| if ( pAig->vObjClasses == NULL && pPars->fUseRollback ) |
| { |
| int nFramesMaxOld = pPars->nFramesMax; |
| pPars->nFramesMax = pPars->nFramesStart; |
| RetValue = Gia_VtaPerformInt( pAig, pPars ); |
| pPars->nFramesMax = nFramesMaxOld; |
| } |
| if ( RetValue == 0 ) |
| return RetValue; |
| return Gia_VtaPerformInt( pAig, pPars ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
