diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 736 |
1 files changed, 627 insertions, 109 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 32e06b02..0afec5e0 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -23,6 +23,7 @@ ABC_NAMESPACE_IMPL_START +#define VTA_LARGE 0xFFFFFF //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -34,14 +35,10 @@ struct Vta_Obj_t_ int iObj; int iFrame; int iNext; - unsigned Prio : 24; + unsigned Prio : 24; // related to VTA_LARGE unsigned Value : 2; unsigned fAdded : 1; unsigned fNew : 1; -// unsigned fPi : 1; -// unsigned fConst : 1; -// int fFlop : 1; -// int fAnd : 1; }; typedef struct Vta_Man_t_ Vta_Man_t; // manager @@ -54,24 +51,50 @@ struct Vta_Man_t_ int nTimeMax; // runtime limit int fVerbose; // verbose flag // internal data + int iFrame; // current frame 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; // hash table bins + Vec_Int_t * vOrder; // objects in DPS order // abstraction int nWords; // the number of sim words for abs - int nFrames; // the number of copmleted frames - Vec_Int_t * vAbs; // abstraction + int nFramesS; // the number of copmleted frames + Vec_Int_t * vAbs; // starting abstraction + Vec_Int_t * vAbsNew; // computed abstraction + Vec_Int_t * vAbsAll; // abstraction of all timeframes // other data Vec_Int_t * vCla2Var; // map clauses into variables + Vec_Ptr_t * vCores; // unsat core for each frame sat_solver2 * pSat; // incremental SAT solver }; +#define VTA_VAR0 1 +#define VTA_VAR1 2 +#define VTA_VARX 3 + +static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl ) +{ + return (pThis->Value == VTA_VAR0 && !fCompl) || (pThis->Value == VTA_VAR1 && fCompl); +} +static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl ) +{ + return (pThis->Value == VTA_VAR1 && !fCompl) || (pThis->Value == VTA_VAR0 && fCompl); +} + 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; } -static inline unsigned * Vta_ObjAbs( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbs, i*p->nWords ); } +static inline unsigned * Vta_ObjAbsOld( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbs, i*p->nWords ); } +static inline unsigned * Vta_ObjAbsNew( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbsNew, i*p->nWords ); } + +#define Vta_ManForEachObj( p, pObj, i ) \ + for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); 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 >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -112,6 +135,35 @@ static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords ) /**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 [] Description [] @@ -137,14 +189,18 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Vec_Int_t * vAbs, int nFramesMax, in p->nObjs = 1; p->nBins = Gia_PrimeCudd( p->nObjsAlloc/2 ); p->pBins = ABC_CALLOC( int, p->nBins ); + p->vOrder = Vec_IntAlloc( 1013 ); // abstraction p->nWords = vAbs ? Vec_IntSize(vAbs) / Gia_ManObjNum(p->pGia) : 1; - p->nFrames = vAbs ? Vta_ManReadFrameStart( vAbs, p->nWords ) : 0; - p->vAbs = vAbs ? vAbs : Vec_IntStart( Gia_ManObjNum(p->pGia) * p->nWords ); + p->nFramesS = vAbs ? Vta_ManReadFrameStart( vAbs, p->nWords ) : Abc_MinInt( p->nFramesMax, 10 ); + p->vAbs = vAbs ? Vec_IntDup(vAbs) : Vec_IntStartFull( Gia_ManObjNum(p->pGia) * p->nWords ); + p->vAbsNew = Vec_IntStart( Gia_ManObjNum(p->pGia) * p->nWords ); + p->vAbsAll = Vta_ManDeriveAbsAll( vAbs, p->nWords ); // other data p->vCla2Var = Vec_IntAlloc( 1000 ); + p->vCores = Vec_PtrAlloc( 100 ); p->pSat = sat_solver2_new(); - assert( nFramesMax == 0 || p->nFrames < nFramesMax ); + assert( nFramesMax == 0 || p->nFramesS <= nFramesMax ); return p; } @@ -162,6 +218,10 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Vec_Int_t * vAbs, int nFramesMax, in void Vga_ManStop( Vta_Man_t * p ) { assert( p->vAbs == NULL ); + Vec_VecFreeP( (Vec_Vec_t **)&p->vCores ); + Vec_IntFreeP( &p->vAbs ); + Vec_IntFreeP( &p->vAbsAll ); + Vec_IntFreeP( &p->vOrder ); Vec_IntFreeP( &p->vCla2Var ); sat_solver2_delete( p->pSat ); ABC_FREE( p->pBins ); @@ -255,110 +315,60 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame ) SeeAlso [] ***********************************************************************/ -void Vga_ManAddClauses( Vta_Man_t * p, int iObjStart ) +void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ) { - Vta_Obj_t * pThis, * pThis0, * pThis1; + Vta_Obj_t * pThis0, * pThis1; Gia_Obj_t * pObj; - int i; - for ( i = iObjStart; i < p->nObjs; i++ ) + int i = Vta_ObjId( p, pThis ); + assert( !pThis->fAdded && !pThis->fNew ); + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + if ( Gia_ObjIsAnd(pObj) ) { - pThis = Vta_ManObj( p, i ); - assert( !pThis->fAdded && !pThis->fNew ); - pObj = Gia_ManObj( p->pGia, pThis->iObj ); - 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 ); - } - } - else if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( pThis->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 ); - } - 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 ); - } - } - } - else if ( Gia_ObjIsConst0(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_const( p->pSat, Vta_ObjId(p, pThis), 1, 0 ); + 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 ); } - else if ( !Gia_ObjIsPi(p->pGia, pObj) ) - assert( 0 ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame ) -{ - Gia_Obj_t * pObj; - Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame ); - assert( !Gia_ObjIsCo(pObj) ); - if ( !pThis->fNew ) - return; - pThis->fNew = 0; - pObj = Gia_ManObj( p->pGia, iObj ); - if ( Gia_ObjIsAnd(pObj) ) - { - Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame ); - Vga_ManUnroll_rec( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame ); } else if ( Gia_ObjIsRo(p->pGia, pObj) ) { - if ( iFrame == 0 ) + if ( pThis->iFrame == 0 ) { - pThis = Vga_ManFindOrAdd( p, iObj, -1 ); - assert( pThis->fNew ); - pThis->fNew = 0; + pThis->fAdded = 1; + sat_solver2_add_constraint( p->pSat, pThis->iObj, 1, 0 ); + Vec_IntPush( p->vCla2Var, i ); + Vec_IntPush( p->vCla2Var, i ); } else { pObj = Gia_ObjRoToRi( p->pGia, pObj ); - Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 ); + 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 ); + } } } - else if ( Gia_ObjIsPi(p->pGia, pObj) ) - {} else if ( Gia_ObjIsConst0(pObj) ) - {} - else assert( 0 ); + { + pThis->fAdded = 1; + sat_solver2_add_const( p->pSat, Vta_ObjId(p, pThis), 1, 0 ); + Vec_IntPush( p->vCla2Var, i ); + } + else if ( !Gia_ObjIsPi(p->pGia, pObj) ) + assert( 0 ); } /**Function************************************************************* @@ -372,10 +382,11 @@ static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Vta_ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue ) +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 RetValue, clk = clock(); + int k, i, Entry, RetValue, clk = clock(); if ( piRetValue ) *piRetValue = -1; // solve the problem @@ -409,9 +420,359 @@ Vec_Int_t * Vta_ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, in 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 + 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 [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 [Refines abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p ) +{ + Abc_Cex_t * pCex = NULL; + Vec_Ptr_t * vTermsUsed, * vTermsUnused; + Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop; + Gia_Obj_t * pObj; + int i, Counter; + assert( Vec_IntSize(p->vOrder) == p->nObjs - 1 ); + // clean depth field + Vta_ManForEachObj( p, pThis, i ) + { + pThis->Prio = VTA_LARGE; + pThis->Value = sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0; + } + + // set the last node + pThis = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) ); + pThis->Prio = 1; + + // consider nodes in the reverse order + vTermsUsed = Vec_PtrAlloc( 1015 ); + vTermsUnused = Vec_PtrAlloc( 1016 ); + Vta_ManForEachObjVecReverse( p->vOrder, p, pThis, i ) + { + // skip unreachable ones + if ( pThis->Prio == VTA_LARGE ) + continue; + // skip contants and PIs + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ) + { + pThis->Prio = 0; + continue; + } + // collect useful terminals + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); + if ( !pThis->fAdded ) + { + assert( pThis->Prio > 0 || pThis->Prio < VTA_LARGE ); + if ( Vec_IntEntry(p->vAbsAll, pThis->iObj) ) + Vec_PtrPush( vTermsUsed, pThis ); + else + Vec_PtrPush( vTermsUnused, pThis ); + continue; + } + // 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 ); + pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 ); + pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 ); + } + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( pThis->iFrame == 0 ) + pThis->Prio = 0; + else + { + pObj = Gia_ObjRoToRi( p->pGia, pObj ); + pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); + assert( pThis0 ); + pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 ); + } + } + else assert( 0 ); + } + // 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 ); + // 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++; + + + // propagate in the direct order + Vta_ManForEachObjVec( p->vOrder, p, pThis, i ) + { + assert( pThis->fNew == 0 ); + // skip unreachable ones + if ( pThis->Prio == VTA_LARGE ) + continue; + // skip terminal objects + if ( !pThis->fAdded ) + continue; + // assumes that values are assigned!!! + assert( pThis->Value != 0 ); + // propagate + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); + + 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 ); + 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; + } + } + } + + Vec_PtrClear( vTermsUsed ); + + // select important values + pTop = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) ); + pTop->fNew = 1; + Vta_ManForEachObjVec( p->vOrder, p, pThis, i ) + { + if ( pThis->fNew == 0 ) + continue; + pThis->fNew = 0; + assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio ); + // skip terminal objects + if ( !pThis->fAdded ) + { + Vec_PtrPush( vTermsUsed, pThis ); + continue; + } + // assumes that values are assigned!!! + assert( pThis->Value != 0 ); + // propagate + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); + 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)) ); + pThis0->fNew = 1; + pThis1->fNew = 1; + } + else if ( pThis->Value == VTA_VAR0 ) + { + if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) + { + assert( pThis0->Prio <= pThis->Prio ); + assert( pThis1->Prio <= pThis->Prio ); + if ( pThis0->Prio <= pThis1->Prio ) + pThis0->fNew = 1; + else + pThis1->fNew = 1; + } + else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) ) + pThis0->fNew = 1; + else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) ) + pThis1->fNew = 1; + 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->fNew = 1; + } + } + } + + // verify + Vta_ManForEachObj( p, pThis, i ) + pThis->Value = VTA_VARX; + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0; + // simulate + Vta_ManForEachObjVec( p->vOrder, p, pThis, i ) + { + assert( pThis->fNew == 0 ); + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + 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; + } + } + // double check the solver + if ( pThis->Value != VTA_VARX ) + assert( (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) ); + } + + // check the output + if ( pTop->Value != VTA_VAR1 ) + printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" ); + + // produce true counter-example + if ( pTop->Prio == 0 ) + { + pCex = NULL; + pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->iFrame+1 ); + pCex->iPo = 0; + pCex->iFrame = p->iFrame; + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + { + assert( pThis->Value == VTA_VAR0 || pThis->Value == VTA_VAR1 ); + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsCi(pObj) ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 ); + else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 ) + Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); + } + } + // perform refinement + else + { + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + { + assert( !pThis->fAdded ); + pObj = Gia_ManObj( p->pGia, pThis->iObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame ); + Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame ); + } + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( pThis->iFrame > 0 ) + { + pObj = Gia_ObjRoToRi( p->pGia, pObj ); + Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); + } + } + else assert( 0 ); + } + // add clauses + Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) + Vga_ManAddClausesOne( p, pThis ); + } + + Vec_PtrFree( vTermsUsed ); + Vec_PtrFree( vTermsUnused ); + return pCex; +} + + /**Function************************************************************* Synopsis [Collect nodes/flops involved in different timeframes.] @@ -439,6 +800,112 @@ void Vec_IntDoubleWidth( Vec_Int_t * p, int nWords ) /**Function************************************************************* + Synopsis [Prints the results.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Vta_ManAbsPrint( Vta_Man_t * p, int fThis ) +{ + Vec_Ptr_t * vInfos; + Vec_Int_t * vPres; + unsigned * pInfo; + int CountAll, CountUni; + int Entry, i, w, f; + // collected used nodes + vInfos = Vec_PtrAlloc( 1000 ); + Vec_IntForEachEntry( p->vAbsAll, Entry, i ) + { + if ( Entry ) + Vec_PtrPush( vInfos, Vta_ObjAbsNew(p, i) ); + + pInfo = Vta_ObjAbsNew(p, i); + for ( w = 0; w < p->nWords; w++ ) + if ( pInfo[w] ) + break; + assert( Entry == (int)(w < p->nWords) ); + } + printf( "%d", Vec_PtrSize(vInfos) ); + // print results for used nodes + vPres = Vec_IntStart( Vec_PtrSize(vInfos) ); + for ( f = 0; f <= fThis; f++ ) + { + CountAll = CountUni = 0; + Vec_PtrForEachEntry( unsigned *, vInfos, pInfo, i ) + { + if ( !Gia_InfoHasBit(pInfo, f) ) + continue; + CountAll++; + if ( Vec_IntEntry(vPres, i) ) + continue; + CountUni++; + Vec_IntWriteEntry( vPres, i, 1 ); + } + printf( " %d(%d)", CountAll, CountUni ); + } + printf( "\n" ); + Vec_PtrFree( vInfos ); + Vec_IntFree( vPres ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame ) +{ + int iVar; + Gia_Obj_t * pObj; + Vta_Obj_t * pThis; + if ( !Gia_InfoHasBit( Vta_ObjAbsOld(p, iObj), iFrame ) ) + return; + pThis = Vga_ManFindOrAdd( p, iObj, iFrame ); + if ( !pThis->fNew ) + return; + pThis->fNew = 0; + iVar = Vta_ObjId( p, pThis ); + pObj = Gia_ManObj( p->pGia, iObj ); + assert( !Gia_ObjIsCo(pObj) ); + if ( Gia_ObjIsAnd(pObj) ) + { + Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame ); + Vga_ManUnroll_rec( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame ); + } + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( iFrame == 0 ) + { + pThis = Vga_ManFindOrAdd( p, iObj, -1 ); + assert( pThis->fNew ); + pThis->fNew = 0; + } + else + { + pObj = Gia_ObjRoToRi( p->pGia, pObj ); + Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 ); + } + } + else if ( Gia_ObjIsPi(p->pGia, pObj) ) + {} + else if ( Gia_ObjIsConst0(pObj) ) + {} + else assert( 0 ); + Vec_IntPush( p->vOrder, iVar ); +} + +/**Function************************************************************* + Synopsis [Collect nodes/flops involved in different timeframes.] Description [] @@ -452,6 +919,7 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax, { Vta_Man_t * p; Gia_Obj_t * pObj; + Abc_Cex_t * pCex; Vec_Int_t * vCore; Vec_Int_t * vAbs = NULL; int f, i, iObjPrev, RetValue, Entry; @@ -460,8 +928,9 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax, // start the manager p = Vga_ManStart( pAig, vAbs, nFramesMax, nConfMax, nTimeMax, fVerbose ); // iteragte though time frames - for ( f = p->nFrames; f < nFramesMax; f++ ) + for ( f = 0; f < nFramesMax; f++ ) { + p->iFrame = f; if ( fVerbose ) printf( "Frame %4d : ", f ); if ( p->nWords * 32 == f ) @@ -469,19 +938,68 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax, Vec_IntDoubleWidth( vAbs, p->nWords ); p->nWords *= 2; } - iObjPrev = p->nObjs; - Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); - Vga_ManAddClauses( p, iObjPrev ); - // run SAT solver - vCore = Vta_ManUnsatCore( p->pSat, nConfMax, fVerbose, &RetValue ); + + if ( f < p->nFramesS ) + { + // unroll and create clauses + iObjPrev = p->nObjs; + assert( Gia_InfoHasBit( Vta_ObjAbsOld(p, Gia_ObjFaninId0p(p->pGia, pObj)), f ) ); + Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); + for ( i = iObjPrev; i < p->nObjs; i++ ) + Vga_ManAddClausesOne( p, Vta_ManObj(p, i) ); + // run SAT solver + vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, nConfMax, fVerbose, &RetValue ); + if ( vCore == NULL && RetValue == 0 ) + pCex = NULL; + } + else + { + // consider the last p->nFramesS/2 cores + + // add them for the last time frame + + // iterate as long as there are counter-examples + while ( 1 ) + { + vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, nConfMax, fVerbose, &RetValue ); + if ( vCore != NULL ) + { + // unroll the solver, add the core + + // return and dobule check + break; + } + pCex = Vta_ManRefineAbstraction( p ); + if ( pCex != NULL ) + break; + } + } + + if ( pCex != NULL ) + { + // the problem is SAT + } if ( vCore == NULL ) - break; + { + // resource limit is reached + } + // add core to storage Vec_IntForEachEntry( vCore, Entry, i ) - Gia_InfoSetBit( Vta_ObjAbs(p, Vec_IntEntry(p->vCla2Var, Entry)), f ); - Vec_IntFree( vCore ); + { + Vta_Obj_t * pThis = Vta_ManObj( p, Entry ); + unsigned * pInfo = Vta_ObjAbsNew( p, pThis->iObj ); + Vec_IntWriteEntry( p->vAbsAll, pThis->iObj, 1 ); + Gia_InfoSetBit( pInfo, pThis->iFrame ); + } +// Vec_IntFree( vCore ); + Vec_PtrPush( p->vCores, vCore ); + // print the result + if ( fVerbose ) + Vta_ManAbsPrint( p, f ); } - vAbs = p->vAbs; p->vAbs = NULL; + + vAbs = p->vAbsNew; p->vAbsNew = NULL; Vga_ManStop( p ); // print statistics about the core |