diff options
| -rw-r--r-- | src/aig/gia/giaAbsRef2.c | 200 |
1 files changed, 198 insertions, 2 deletions
diff --git a/src/aig/gia/giaAbsRef2.c b/src/aig/gia/giaAbsRef2.c index ac47333d..03f1d9a2 100644 --- a/src/aig/gia/giaAbsRef2.c +++ b/src/aig/gia/giaAbsRef2.c @@ -93,6 +93,7 @@ struct Rf2_Man_t_ Vec_Int_t * vObjs; // internal objects used in value propagation Vec_Int_t * vFanins; // fanins of the PPI nodes Vec_Int_t * pvVecs; // vectors of integers for each object + Vec_Vec_t * vNod2Ppi; // for each node, the set of PPIs to include // internal data Rf2_Obj_t * pObjs; // refinement objects int nObjs; // the number of used objects @@ -145,6 +146,7 @@ Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ) p->vObjs = Vec_IntAlloc( 1000 ); p->vFanins = Vec_IntAlloc( 1000 ); p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) ); + p->vNod2Ppi = Vec_VecStart( 100 ); Gia_ManCleanMark0(pGia); Gia_ManCleanMark1(pGia); return p; @@ -169,6 +171,7 @@ void Rf2_ManStop( Rf2_Man_t * p, int fProfile ) } Vec_IntFree( p->vObjs ); Vec_IntFree( p->vFanins ); + Vec_VecFree( p->vNod2Ppi ); ABC_FREE( p->pvVecs ); ABC_FREE( p ); } @@ -300,6 +303,8 @@ int Rf2_ManSensitize( Rf2_Man_t * p ) return pRnm->Prio; } + + /**Function************************************************************* Synopsis [Performs refinement.] @@ -457,6 +462,189 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth ) /**Function************************************************************* + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rf2_ManCountPis( Rf2_Man_t * p ) +{ + return 0; +} + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) +{ + int i, j, k, Entry, Entry2; + k = 0; + Vec_IntForEachEntry( p, Entry, i ) + if ( Gia_WordCountOnes((unsigned)Entry) <= Limit ) + Vec_IntWriteEntry( p, k++, Entry ); + Vec_IntShrink( p, k ); + Vec_IntSort( p, 0 ); + k = 0; + Vec_IntForEachEntry( p, Entry, i ) + { + Vec_IntForEachEntryStop( p, Entry2, j, i ) + if ( (Entry2 & Entry) == Entry2 ) // Entry2 is a subset of Entry + break; + if ( j == i ) // Entry is not contained in any Entry2 + Vec_IntWriteEntry( p, k++, Entry ); + } + Vec_IntShrink( p, k ); +} + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManPrintVector( Vec_Int_t * p, int Num ) +{ + extern void Extra_PrintBinary( FILE * pFile, unsigned * p, int nBits ); + int i, Entry; + printf( "Justification containing %d subsets.\n", Vec_IntSize(p) ); + Vec_IntForEachEntry( p, Entry, i ) + Extra_PrintBinary( stdout, (unsigned *)&Entry, Num ), printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Assigns a unique justifification ID for each PPI.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManAssignJustIds( Rf2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, k = 0; + Vec_VecClear( p->vNod2Ppi ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + Vec_VecPushInt( p->vNod2Ppi, k++, i ); + printf( "Considering %d PPIs with unique justification IDs.\n", k ); +} + +/**Function************************************************************* + + Synopsis [Performs justification propagation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) +{ + Vec_Int_t * vVec, * vVec0, * vVec1; + Gia_Obj_t * pObj; + int f, i, k, j, Entry, Entry2, iBit = p->pCex->nRegs; + // init constant + pObj = Gia_ManConst0(p->pGia); + pObj->fMark0 = 0; + Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); + // iterate through the timeframes + for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) + { + // initialize frontier values and init justification sets + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i ); + Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); + } + // assign justification sets for PPis + Vec_VecForEachLevelInt( p->vNod2Ppi, vVec, i ) + Vec_IntForEachEntry( vVec, Entry, k ) + { + assert( i < 31 ); + pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vMap, Entry) ); + assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 1 ); + Vec_IntAddToEntry( Rf2_ObjVec(p, pObj), 0, (1 << i) ); + } + // propagate internal nodes + Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) + { + pObj->fMark0 = 0; + vVec = Rf2_ObjVec(p, pObj); + Vec_IntClear( vVec ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + Vec_IntPush( vVec, 0 ); + continue; + } + pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0; + vVec0 = Rf2_ObjVec( p, Gia_ObjRoToRi(p->pGia, pObj) ); + Vec_IntAppend( vVec, vVec0 ); + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); + vVec0 = Rf2_ObjVec( p, Gia_ObjFanin0(pObj) ); + Vec_IntAppend( vVec, vVec0 ); + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + if ( pObj->fMark0 == 1 ) + { + vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj)); + vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj)); + Vec_IntForEachEntry( vVec0, Entry, k ) + Vec_IntForEachEntry( vVec1, Entry2, j ) + Vec_IntPush( vVec, Entry | Entry2 ); + Rf2_ManProcessVector( vVec, Limit ); + } + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + Vec_IntAppend( vVec, vVec0 ); + Vec_IntAppend( vVec, vVec1 ); + Rf2_ManProcessVector( vVec, Limit ); + } + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) + Vec_IntAppend( vVec, vVec0 ); + else + Vec_IntAppend( vVec, vVec1 ); + } + } + assert( iBit == p->pCex->nBits ); + if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 ) + printf( "Output value is incorrect.\n" ); + return Rf2_ObjVec(p, Gia_ManPo(p->pGia, 0)); +} + +/**Function************************************************************* + Synopsis [Computes the refinement for a given counter-example.] Description [] @@ -468,6 +656,7 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth ) ***********************************************************************/ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) { + Vec_Int_t * vJusts; Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); clock_t clk, clk2 = clock(); p->nCalls++; @@ -479,9 +668,16 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in // collects used objects Rf2_ManCollect( p ); // collect reconvergence points - Rf2_ManGatherFanins( p, 2 ); +// Rf2_ManGatherFanins( p, 2 ); // propagate justification IDs - + Rf2_ManAssignJustIds( p ); + vJusts = Rf2_ManPropagate( p, 100 ); + Rf2_ManPrintVector( vJusts, Rf2_ManCountPis(p) ); + if ( Vec_IntSize(vJusts) == 0 ) + { + printf( "Empty set of justifying subsets.\n" ); + return NULL; + } // select the result // verify (empty) refinement |