diff options
| -rw-r--r-- | src/aig/aig/aigJust.c | 29 | ||||
| -rw-r--r-- | src/aig/aig/aigPack.c | 350 |
2 files changed, 372 insertions, 7 deletions
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c index c6b3a8c0..87ea8f69 100644 --- a/src/aig/aig/aigJust.c +++ b/src/aig/aig/aigJust.c @@ -230,6 +230,13 @@ int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLi return Aig_ObjTerSimulate_rec( pAig, pNode ); } + +typedef struct Aig_ManPack_t_ Aig_ManPack_t; +extern Aig_ManPack_t * Aig_ManPackStart( Aig_Man_t * pAig ); +extern void Aig_ManPackStop( Aig_ManPack_t * p ); +extern void Aig_ManPackAddPattern( Aig_ManPack_t * p, Vec_Int_t * vLits ); +extern Vec_Int_t * Aig_ManPackConstNodes( Aig_ManPack_t * p ); + /**Function************************************************************* Synopsis [Testing of the framework.] @@ -241,24 +248,29 @@ int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLi SeeAlso [] ***********************************************************************/ -void Aig_ManTerSimulate( Aig_Man_t * pAig ) +void Aig_ManJustExperiment( Aig_Man_t * pAig ) { - Vec_Int_t * vSuppLits; + Aig_ManPack_t * pPack; + Vec_Int_t * vSuppLits, * vNodes; Aig_Obj_t * pObj; int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0; int nTotalLits = 0; vSuppLits = Vec_IntAlloc( 100 ); - Aig_ManForEachPo( pAig, pObj, i ) + pPack = Aig_ManPackStart( pAig ); + vNodes = Aig_ManPackConstNodes( pPack ); +// Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachNodeVec( pAig, vNodes, pObj, i ) { if ( pObj->fPhase ) // const 1 { if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) ) { // assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 ); - if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 ) - printf( "Justification error!\n" ); +// if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 ) +// printf( "Justification error!\n" ); Count0++; nTotalLits += Vec_IntSize(vSuppLits); + Aig_ManPackAddPattern( pPack, vSuppLits ); } else Count0f++; @@ -268,10 +280,11 @@ void Aig_ManTerSimulate( Aig_Man_t * pAig ) if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) ) { // assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 ); - if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 ) - printf( "Justification error!\n" ); +// if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 ) +// printf( "Justification error!\n" ); Count1++; nTotalLits += Vec_IntSize(vSuppLits); + Aig_ManPackAddPattern( pPack, vSuppLits ); } else Count1f++; @@ -282,6 +295,8 @@ void Aig_ManTerSimulate( Aig_Man_t * pAig ) Aig_ManPoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManPoNum(pAig), 1.0*nTotalLits/(Count0+Count1) ); Abc_PrintTime( 1, "T", clock() - clk ); Aig_ManCleanMarkAB( pAig ); + Aig_ManPackStop( pPack ); + Vec_IntFree( vNodes ); } diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c index 8d7b54df..493e4995 100644 --- a/src/aig/aig/aigPack.c +++ b/src/aig/aig/aigPack.c @@ -27,6 +27,25 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +// resubstitution manager +typedef struct Aig_ManPack_t_ Aig_ManPack_t; +struct Aig_ManPack_t_ +{ + Aig_Man_t * pAig; // working manager + Vec_Wrd_t * vSigns; // object signatures + Vec_Wrd_t * vPiPats; // PI assignments + Vec_Wrd_t * vPiCare; // PI care set + int iPatCur; // current pattern + int fVerbose; // verbosiness flag + // statistics + int nPatTotal; // number of all patterns + int nPatSkip; // number of skipped patterns + int nPatRepeat; // number of repeated patterns +}; + +static inline int Aig_Word6CountOnes( word t ) { return Aig_WordCountOnes( (unsigned)(t >> 32) ) + Aig_WordCountOnes( (unsigned)(t & 0xFFFFFFFF) ); } +static inline int Aig_Word6HasOneBit( word t ) { return (t & (t-1)) == 0; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -43,7 +62,338 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +Aig_ManPack_t * Aig_ManPackAlloc( Aig_Man_t * pAig ) +{ + Aig_ManPack_t * p; + p = ABC_CALLOC( Aig_ManPack_t, 1 ); + p->pAig = pAig; + p->vSigns = Vec_WrdStart( Aig_ManObjNumMax(pAig) ); + p->vPiPats = Vec_WrdStart( Aig_ManPiNum(pAig) ); + p->vPiCare = Vec_WrdStart( Aig_ManPiNum(pAig) ); + p->iPatCur = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManPackCountCares( Aig_ManPack_t * p ) +{ + Aig_Obj_t * pObj; + int i, Total = 0; + Aig_ManForEachPi( p->pAig, pObj, i ) + Total += Aig_Word6CountOnes( Vec_WrdEntry(p->vPiCare, i) ); + return Total; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackPrintCare( Aig_ManPack_t * p ) +{ + Aig_Obj_t * pObj; + word Sign; + int i; + Aig_ManForEachPi( p->pAig, pObj, i ) + { + Sign = Vec_WrdEntry( p->vPiCare, i ); + Extra_PrintBinary( stdout, (unsigned *)&Sign, 64 ); + printf( "\n" ); + } + printf( "\n" ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackFree( Aig_ManPack_t * p ) +{ +// Aig_ManPackPrintCare( p ); + printf( "Patterns: " ); + printf( "Total = %6d. ", p->nPatTotal ); + printf( "Skipped = %6d. ", p->nPatSkip ); + printf( "Cares = %6.2f %% ", 100.0*Aig_ManPackCountCares(p)/Aig_ManPiNum(p->pAig)/64 ); + printf( "\n" ); + Vec_WrdFree( p->vSigns ); + Vec_WrdFree( p->vPiPats ); + Vec_WrdFree( p->vPiCare ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackSetRandom( Aig_ManPack_t * p ) +{ + Aig_Obj_t * pObj; + word Sign; + int i; + Aig_ManForEachPi( p->pAig, pObj, i ) + { + Sign = (((word)Aig_ManRandom(0)) << 32) | ((word)Aig_ManRandom(0)); + Vec_WrdWriteEntry( p->vPiPats, i, Sign << 1 ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackSimulate( Aig_ManPack_t * p ) +{ + Aig_Obj_t * pObj; + word Sign, Sign0, Sign1; + int i; + // set the constant + Vec_WrdWriteEntry( p->vSigns, 0, (word)~0 ); + // transfer into the array + Aig_ManForEachPi( p->pAig, pObj, i ) + Vec_WrdWriteEntry( p->vSigns, Aig_ObjId(pObj), Vec_WrdEntry(p->vPiPats, i) ); + // simulate internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + { + Sign0 = Vec_WrdEntry( p->vSigns, Aig_ObjFaninId0(pObj) ); + Sign1 = Vec_WrdEntry( p->vSigns, Aig_ObjFaninId1(pObj) ); + if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) + Sign = ~(Sign0 | Sign1); + else if ( Aig_ObjFaninC0(pObj) ) + Sign = ~Sign0 & Sign1; + else if ( Aig_ObjFaninC1(pObj) ) + Sign = Sign0 & ~Sign1; + else + Sign = Sign0 & Sign1; + Vec_WrdWriteEntry( p->vSigns, Aig_ObjId(pObj), Sign ); + } + // set the outputs + Aig_ManForEachPo( p->pAig, pObj, i ) + { + Sign0 = Vec_WrdEntry( p->vSigns, Aig_ObjFaninId0(pObj) ); + Sign = Aig_ObjFaninC0(pObj) ? ~Sign0 : Sign0; + Vec_WrdWriteEntry( p->vSigns, Aig_ObjId(pObj), Sign ); + } +} + +/**Function************************************************************* + + Synopsis [] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackPrintStats( Aig_ManPack_t * p ) +{ + word Sign; + Aig_Obj_t * pObj; + int i, Total, Count, Counts[33] = {0}; // the number of nodes having that many patterns + Aig_ManForEachNode( p->pAig, pObj, i ) + { + Sign = Vec_WrdEntry( p->vSigns, Aig_ObjId(pObj) ); + Count = Aig_Word6CountOnes( Sign ); + if ( Count > 32 ) + Count = 64 - Count; + Counts[Count]++; + } + // print statistics + Total = 0; + for ( i = 0; i <= 32; i++ ) + { + Total += Counts[i]; + printf( "%2d : ", i ); + printf( "%6d ", Counts[i] ); + printf( "%6.1f %%", 100.0*Counts[i]/Aig_ManNodeNum(p->pAig) ); + printf( "%6.1f %%", 100.0*Total/Aig_ManNodeNum(p->pAig) ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_ManPackConstNodes( Aig_ManPack_t * p ) +{ + Vec_Int_t * vNodes; + Aig_Obj_t * pObj; + word Sign; + int i; + vNodes = Vec_IntAlloc( 1000 ); + Aig_ManForEachNode( p->pAig, pObj, i ) + { + Sign = Vec_WrdEntry( p->vSigns, Aig_ObjId(pObj) ); + if ( Sign == 0 || ~Sign == 0 || Aig_Word6HasOneBit(Sign) || Aig_Word6HasOneBit(~Sign) ) + Vec_IntPush( vNodes, Aig_ObjId(pObj) ); + } + return vNodes; +} + + +/**Function************************************************************* + + Synopsis [Packs patterns into array of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +*************************************`**********************************/ +int Aig_ManPackAddPatternTry( Aig_ManPack_t * p, int iBit, Vec_Int_t * vLits ) +{ + word * pInfo, * pPres; + int i, Lit; + Vec_IntForEachEntry( vLits, Lit, i ) + { + pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) ); + pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) ); + if ( Aig_InfoHasBit( (unsigned *)pPres, iBit ) && + Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) ) + return 0; + } + Vec_IntForEachEntry( vLits, Lit, i ) + { + pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) ); + pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) ); + Aig_InfoSetBit( (unsigned *)pPres, iBit ); + if ( Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) ) + Aig_InfoXorBit( (unsigned *)pInfo, iBit ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackAddPattern( Aig_ManPack_t * p, Vec_Int_t * vLits ) +{ + int k; + for ( k = 1; k < 64; k++ ) + if ( Aig_ManPackAddPatternTry( p, k, vLits ) ) + break; + if ( k == 64 ) + { +/* + word * pInfo, * pPres; + int i, Lit; + Vec_IntForEachEntry( vLits, Lit, i ) + printf( "%d", Aig_LitIsCompl(Lit) ); + printf( "\n\n" ); + for ( k = 1; k < 64; k++ ) + { + Vec_IntForEachEntry( vLits, Lit, i ) + { + pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) ); + pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) ); + if ( Aig_InfoHasBit( (unsigned *)pPres, k ) ) + printf( "%d", Aig_InfoHasBit( (unsigned *)pInfo, k ) ); + else + printf( "-" ); + } + printf( "\n" ); + } +*/ + p->nPatSkip++; + } + p->nPatTotal++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_ManPack_t * Aig_ManPackStart( Aig_Man_t * pAig ) +{ + Aig_ManPack_t * p; + p = Aig_ManPackAlloc( pAig ); + Aig_ManPackSetRandom( p ); + Aig_ManPackSimulate( p ); + Aig_ManPackPrintStats( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPackStop( Aig_ManPack_t * p ) +{ + Aig_ManPackSimulate( p ); + Aig_ManPackPrintStats( p ); + Aig_ManPackFree( p ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |