From d8c47d56b7c525d9ab303d945318ebf3166c3fe2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 17 Sep 2018 12:13:54 -0700 Subject: Fixing mismatch in exact NPN computation (by XueGong Zhou) --- src/opt/dau/dau.h | 4 + src/opt/dau/dauCanon.c | 1467 ++++++++++++++++++++++++------------------------ src/opt/dau/dauNpn.c | 18 +- 3 files changed, 751 insertions(+), 738 deletions(-) (limited to 'src/opt') diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index df8c8f40..82e9b83b 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -60,6 +60,7 @@ typedef enum { typedef struct Dss_Man_t_ Dss_Man_t; typedef struct Abc_TtHieMan_t_ Abc_TtHieMan_t; +typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag); //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// @@ -83,6 +84,9 @@ extern int Abc_TtCountOnesInCofsSimple( word * pTruth, int nVars, int extern unsigned Abc_TtCanonicizeHie(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int fExact ); extern Abc_TtHieMan_t * Abc_TtHieManStart( int nVars, int nLevels ); extern void Abc_TtHieManStop(Abc_TtHieMan_t * p ); +extern unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag); +extern unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres); +extern unsigned Abc_TtCanonicizeHie(Abc_TtHieMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact); /*=== dauCount.c ==========================================================*/ extern int Abc_TtCountOnesInCofsQuick( word * pTruth, int nVars, int * pStore ); /*=== dauDsd.c ==========================================================*/ diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c index 0c93cc85..ae9b7761 100644 --- a/src/opt/dau/dauCanon.c +++ b/src/opt/dau/dauCanon.c @@ -64,11 +64,11 @@ static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar ) return Cof0 < Cof1 ? -1 : 1; return 0; } - if ( iVar <= 5 ) - { + if ( iVar <= 5 ) + { word Cof0, Cof1; - int w, shift = (1 << iVar); - for ( w = 0; w < nWords; w++ ) + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) { Cof0 = pTruth[w] & s_Truths6Neg[iVar]; Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; @@ -76,18 +76,18 @@ static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar ) return Cof0 < Cof1 ? -1 : 1; } return 0; - } - // if ( iVar > 5 ) - { + } + // if ( iVar > 5 ) + { word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); + int i, iStep = Abc_TtWordNum(iVar); assert( nWords >= 2 ); - for ( ; pTruth < pLimit; pTruth += 2*iStep ) - for ( i = 0; i < iStep; i++ ) + for ( ; pTruth < pLimit; pTruth += 2*iStep ) + for ( i = 0; i < iStep; i++ ) if ( pTruth[i] != pTruth[i + iStep] ) return pTruth[i] < pTruth[i + iStep] ? -1 : 1; return 0; - } + } } static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar ) { @@ -99,11 +99,11 @@ static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar return Cof0 < Cof1 ? -1 : 1; return 0; } - if ( iVar <= 5 ) - { + if ( iVar <= 5 ) + { word Cof0, Cof1; - int w, shift = (1 << iVar); - for ( w = nWords - 1; w >= 0; w-- ) + int w, shift = (1 << iVar); + for ( w = nWords - 1; w >= 0; w-- ) { Cof0 = pTruth[w] & s_Truths6Neg[iVar]; Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; @@ -111,18 +111,18 @@ static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar return Cof0 < Cof1 ? -1 : 1; } return 0; - } - // if ( iVar > 5 ) - { + } + // if ( iVar > 5 ) + { word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); + int i, iStep = Abc_TtWordNum(iVar); assert( nWords >= 2 ); - for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep ) - for ( i = iStep - 1; i >= 0; i-- ) + for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep ) + for ( i = iStep - 1; i >= 0; i-- ) if ( pLimit[i] != pLimit[i + iStep] ) return pLimit[i] < pLimit[i + iStep] ? -1 : 1; return 0; - } + } } */ @@ -142,35 +142,35 @@ static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, assert( Num1 < Num2 && Num2 < 4 ); if ( nWords == 1 ) return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]); - if ( iVar <= 4 ) - { - int w, shift = (1 << iVar); - for ( w = 0; w < nWords; w++ ) + if ( iVar <= 4 ) + { + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) ) return 0; return 1; - } - if ( iVar == 5 ) - { + } + if ( iVar == 5 ) + { unsigned * pTruthU = (unsigned *)pTruth; unsigned * pLimitU = (unsigned *)(pTruth + nWords); assert( nWords >= 2 ); - for ( ; pTruthU < pLimitU; pTruthU += 4 ) + for ( ; pTruthU < pLimitU; pTruthU += 4 ) if ( pTruthU[Num2] != pTruthU[Num1] ) return 0; return 1; - } - // if ( iVar > 5 ) - { + } + // if ( iVar > 5 ) + { word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); + int i, iStep = Abc_TtWordNum(iVar); assert( nWords >= 4 ); - for ( ; pTruth < pLimit; pTruth += 4*iStep ) - for ( i = 0; i < iStep; i++ ) + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] ) return 0; return 1; - } + } } /**Function************************************************************* @@ -195,11 +195,11 @@ static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, in return Cof1 < Cof2 ? -1 : 1; return 0; } - if ( iVar <= 4 ) - { + if ( iVar <= 4 ) + { word Cof1, Cof2; - int w, shift = (1 << iVar); - for ( w = 0; w < nWords; w++ ) + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) { Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; @@ -207,30 +207,30 @@ static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, in return Cof1 < Cof2 ? -1 : 1; } return 0; - } - if ( iVar == 5 ) - { + } + if ( iVar == 5 ) + { unsigned * pTruthU = (unsigned *)pTruth; unsigned * pLimitU = (unsigned *)(pTruth + nWords); assert( nWords >= 2 ); - for ( ; pTruthU < pLimitU; pTruthU += 4 ) + for ( ; pTruthU < pLimitU; pTruthU += 4 ) if ( pTruthU[Num1] != pTruthU[Num2] ) return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1; return 0; - } - // if ( iVar > 5 ) - { + } + // if ( iVar > 5 ) + { word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); + int i, iStep = Abc_TtWordNum(iVar); int Offset1 = Num1*iStep; int Offset2 = Num2*iStep; assert( nWords >= 4 ); - for ( ; pTruth < pLimit; pTruth += 4*iStep ) - for ( i = 0; i < iStep; i++ ) + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) if ( pTruth[i + Offset1] != pTruth[i + Offset2] ) return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1; return 0; - } + } } static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) { @@ -243,11 +243,11 @@ static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, return Cof1 < Cof2 ? -1 : 1; return 0; } - if ( iVar <= 4 ) - { + if ( iVar <= 4 ) + { word Cof1, Cof2; - int w, shift = (1 << iVar); - for ( w = nWords - 1; w >= 0; w-- ) + int w, shift = (1 << iVar); + for ( w = nWords - 1; w >= 0; w-- ) { Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; @@ -255,30 +255,30 @@ static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, return Cof1 < Cof2 ? -1 : 1; } return 0; - } - if ( iVar == 5 ) - { + } + if ( iVar == 5 ) + { unsigned * pTruthU = (unsigned *)pTruth; unsigned * pLimitU = (unsigned *)(pTruth + nWords); assert( nWords >= 2 ); - for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 ) + for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 ) if ( pLimitU[Num1] != pLimitU[Num2] ) return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1; return 0; - } - // if ( iVar > 5 ) - { + } + // if ( iVar > 5 ) + { word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); + int i, iStep = Abc_TtWordNum(iVar); int Offset1 = Num1*iStep; int Offset2 = Num2*iStep; assert( nWords >= 4 ); - for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep ) - for ( i = iStep - 1; i >= 0; i-- ) + for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep ) + for ( i = iStep - 1; i >= 0; i-- ) if ( pLimit[i + Offset1] != pLimit[i + Offset2] ) return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1; return 0; - } + } } /**Function************************************************************* @@ -292,13 +292,24 @@ static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, SeeAlso [] ***********************************************************************/ -#define DO_SMALL_TRUTHTABLE 0 +void Abc_TtNormalizeSmallTruth(word * pTruth, int nVars) +{ + if (nVars < 6) { + int shift, bits = (1 << nVars); + word base = *pTruth = *pTruth & ((((word)1) << bits) - 1); + for (shift = bits; shift < 64; shift += bits) + *pTruth |= base << shift; + } +} -static inline void Abc_TtNormalizeSmallTruth(word * pTruth, int nVars) +inline void Abc_TtVerifySmallTruth(word * pTruth, int nVars) { -#if DO_SMALL_TRUTHTABLE - if (nVars < 6) - *pTruth &= (1ULL << (1 << nVars)) - 1; +#ifndef NDEBUG + if (nVars < 6) { + word nTruth = *pTruth; + Abc_TtNormalizeSmallTruth(&nTruth, nVars); + assert(*pTruth == nTruth); + } #endif } @@ -306,7 +317,7 @@ static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars ) { int nWords = Abc_TtWordNum( nVars ); int k, Counter = 0; - Abc_TtNormalizeSmallTruth(pTruth, nVars); + Abc_TtVerifySmallTruth(pTruth, nVars); for ( k = 0; k < nWords; k++ ) if ( pTruth[k] ) Counter += Abc_TtCountOnes( pTruth[k] ); @@ -318,7 +329,7 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore int i, k, Counter, nWords; if ( nVars <= 6 ) { - Abc_TtNormalizeSmallTruth(pTruth, nVars); + Abc_TtVerifySmallTruth(pTruth, nVars); for ( i = 0; i < nVars; i++ ) pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] ); return; @@ -1154,77 +1165,79 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars ) struct Abc_TtHieMan_t_ { - int nLastLevel, nWords; - Vec_Mem_t * vTtMem[TT_MAX_LEVELS]; // truth table memory and hash tables - Vec_Int_t * vRepres[TT_MAX_LEVELS]; // pointers to the representatives from the last hierarchical level - int vTruthId[TT_MAX_LEVELS]; + int nLastLevel, nWords; + Vec_Mem_t * vTtMem[TT_MAX_LEVELS]; // truth table memory and hash tables + Vec_Int_t * vRepres[TT_MAX_LEVELS]; // pointers to the representatives from the last hierarchical level + int vTruthId[TT_MAX_LEVELS]; }; Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels) { - Abc_TtHieMan_t * p = NULL; - int i; - if (nLevels > TT_MAX_LEVELS) return p; - p = ABC_CALLOC(Abc_TtHieMan_t, 1); - p->nLastLevel = nLevels - 1; - p->nWords = Abc_TtWordNum(nVars); - for (i = 0; i < nLevels; i++) - { - p->vTtMem[i] = Vec_MemAlloc(p->nWords, 12); - Vec_MemHashAlloc(p->vTtMem[i], 10000); - p->vRepres[i] = Vec_IntAlloc(1); - } - return p; + Abc_TtHieMan_t * p = NULL; + int i; + if (nLevels > TT_MAX_LEVELS) return p; + p = ABC_CALLOC(Abc_TtHieMan_t, 1); + p->nLastLevel = nLevels - 1; + p->nWords = Abc_TtWordNum(nVars); + for (i = 0; i < nLevels; i++) + { + p->vTtMem[i] = Vec_MemAlloc(p->nWords, 12); + Vec_MemHashAlloc(p->vTtMem[i], 10000); + p->vRepres[i] = Vec_IntAlloc(1); + } + return p; } void Abc_TtHieManStop(Abc_TtHieMan_t * p) { - int i; - for (i = 0; i <= p->nLastLevel; i++) - { - Vec_MemHashFree(p->vTtMem[i]); - Vec_MemFreeP(&p->vTtMem[i]); - Vec_IntFree(p->vRepres[i]); - } - ABC_FREE(p); + int i; + for (i = 0; i <= p->nLastLevel; i++) + { + Vec_MemHashFree(p->vTtMem[i]); + Vec_MemFreeP(&p->vTtMem[i]); + Vec_IntFree(p->vRepres[i]); + } + ABC_FREE(p); } int Abc_TtHieRetrieveOrInsert(Abc_TtHieMan_t * p, int level, word * pTruth, word * pResult) { - int i, iSpot, truthId; - word * pRepTruth; - if (level < 0) level += p->nLastLevel + 1; - if (level < 0 || level > p->nLastLevel) return -1; - iSpot = *Vec_MemHashLookup(p->vTtMem[level], pTruth); - if (iSpot == -1) { - p->vTruthId[level] = Vec_MemHashInsert(p->vTtMem[level], pTruth); - if (level < p->nLastLevel) return 0; - iSpot = p->vTruthId[level]; - } - // return the class representative - if (level < p->nLastLevel) - truthId = Vec_IntEntry(p->vRepres[level], iSpot); - else - truthId = iSpot; - for (i = 0; i < level; i++) - Vec_IntSetEntry(p->vRepres[i], p->vTruthId[i], truthId); - - pRepTruth = Vec_MemReadEntry(p->vTtMem[p->nLastLevel], truthId); - if (level < p->nLastLevel) { - Abc_TtCopy(pResult, pRepTruth, p->nWords, 0); - return 1; - } - assert(Abc_TtEqual(pTruth, pRepTruth, p->nWords)); - if (pTruth != pResult) - Abc_TtCopy(pResult, pRepTruth, p->nWords, 0); - return 0; + int i, iSpot, truthId; + word * pRepTruth; + if (!p) return -1; + if (level < 0) level += p->nLastLevel + 1; + if (level < 0 || level > p->nLastLevel) return -1; + iSpot = *Vec_MemHashLookup(p->vTtMem[level], pTruth); + if (iSpot == -1) { + p->vTruthId[level] = Vec_MemHashInsert(p->vTtMem[level], pTruth); + if (level < p->nLastLevel) return 0; + iSpot = p->vTruthId[level]; + } + // return the class representative + if (level < p->nLastLevel) + truthId = Vec_IntEntry(p->vRepres[level], iSpot); + else + truthId = iSpot; + for (i = 0; i < level; i++) + Vec_IntSetEntry(p->vRepres[i], p->vTruthId[i], truthId); + + pRepTruth = Vec_MemReadEntry(p->vTtMem[p->nLastLevel], truthId); + if (level < p->nLastLevel) { + Abc_TtCopy(pResult, pRepTruth, p->nWords, 0); + return 1; + } + assert(Abc_TtEqual(pTruth, pRepTruth, p->nWords)); + if (pTruth != pResult) + Abc_TtCopy(pResult, pRepTruth, p->nWords, 0); + return 0; } unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact ) { int fNaive = 1; int pStore[17]; - static word pTruth[1024]; + //static word pTruth[1024]; + word * pTruth = pTruthInit; unsigned uCanonPhase = 0; int nOnes, nWords = Abc_TtWordNum( nVars ); int i, k; @@ -1237,7 +1250,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, return 0; } - Abc_TtCopy( pTruth, pTruthInit, nWords, 0 ); + //Abc_TtCopy( pTruth, pTruthInit, nWords, 0 ); for ( i = 0; i < nVars; i++ ) pCanonPerm[i] = i; @@ -1265,7 +1278,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, pStore[i] = nOnes - pStore[i]; } // check cache - if (Abc_TtHieRetrieveOrInsert(p, 1, pTruth, pTruthInit) > 0) return 0; + if (Abc_TtHieRetrieveOrInsert(p, 1, pTruth, pTruthInit) > 0) return 0; // normalize permutation { @@ -1289,7 +1302,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, } } // check cache - if (Abc_TtHieRetrieveOrInsert(p, 2, pTruth, pTruthInit) > 0) return 0; + if (Abc_TtHieRetrieveOrInsert(p, 2, pTruth, pTruthInit) > 0) return 0; // iterate TT permutations for tied variables for ( k = 0; k < 5; k++ ) @@ -1308,7 +1321,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, break; } // check cache - if (Abc_TtHieRetrieveOrInsert(p, 3, pTruth, pTruthInit) > 0) return 0; + if (Abc_TtHieRetrieveOrInsert(p, 3, pTruth, pTruthInit) > 0) return 0; // perform exact NPN using groups if ( fExact ) { @@ -1350,7 +1363,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtHieMan_t * p, word * pTruthInit, int nVars, } } // update cache - Abc_TtHieRetrieveOrInsert(p, 4, pTruth, pTruthInit); + Abc_TtHieRetrieveOrInsert(p, 4, pTruth, pTruthInit); return 0; } @@ -1369,26 +1382,26 @@ SeeAlso [] typedef struct TiedGroup_ { - char iStart; // index of Abc_TgMan_t::pPerm - char nGVars; // the number of variables in the group - char fPhased; // if the phases of the variables are determined + char iStart; // index of Abc_TgMan_t::pPerm + char nGVars; // the number of variables in the group + char fPhased; // if the phases of the variables are determined } TiedGroup; typedef struct Abc_TgMan_t_ { - word *pTruth; - int nVars; // the number of variables - int nGVars; // the number of variables in groups ( symmetric variables purged ) - int nGroups; // the number of tied groups - unsigned uPhase; // phase of each variable and the function - char pPerm[16]; // permutation of variables, symmetric variables purged, for grouping - char pPermT[16]; // permutation of variables, symmetric variables expanded, actual transformation for pTruth - char pPermTRev[16]; // reverse permutation of pPermT - signed char pPermDir[16]; // for generating the next permutation - TiedGroup pGroup[16]; // tied groups - // symemtric group attributes - char symPhase[16]; // phase type of symemtric groups - signed char symLink[17]; // singly linked list, indicate the variables in symemtric groups + word *pTruth; + int nVars; // the number of variables + int nGVars; // the number of variables in groups ( symmetric variables purged ) + int nGroups; // the number of tied groups + unsigned uPhase; // phase of each variable and the function + char pPerm[16]; // permutation of variables, symmetric variables purged, for grouping + char pPermT[16]; // permutation of variables, symmetric variables expanded, actual transformation for pTruth + char pPermTRev[16]; // reverse permutation of pPermT + signed char pPermDir[16]; // for generating the next permutation + TiedGroup pGroup[16]; // tied groups + // symemtric group attributes + char symPhase[16]; // phase type of symemtric groups + signed char symLink[17]; // singly linked list, indicate the variables in symemtric groups } Abc_TgMan_t; #if !defined(NDEBUG) && !defined(CANON_VERIFY) @@ -1409,59 +1422,59 @@ SeeAlso [] // Johnson¨CTrotter algorithm static int Abc_NextPermSwapC(char * pData, signed char * pDir, int size) { - int i, j, k = -1; - for (i = 0; i < size; i++) - { - j = i + pDir[i]; - if (j >= 0 && j < size && pData[i] > pData[j] && (k < 0 || pData[i] > pData[k])) - k = i; - } - if (k < 0) k = 0; - - for (i = 0; i < size; i++) - if (pData[i] > pData[k]) - pDir[i] = -pDir[i]; - - j = k + pDir[k]; - return j < k ? j : k; + int i, j, k = -1; + for (i = 0; i < size; i++) + { + j = i + pDir[i]; + if (j >= 0 && j < size && pData[i] > pData[j] && (k < 0 || pData[i] > pData[k])) + k = i; + } + if (k < 0) k = 0; + + for (i = 0; i < size; i++) + if (pData[i] > pData[k]) + pDir[i] = -pDir[i]; + + j = k + pDir[k]; + return j < k ? j : k; } typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag); unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag) { - int nWords = Abc_TtWordNum(nVars); - unsigned uCanonPhase1, uCanonPhase2; - char pCanonPerm2[16]; - static word pTruth2[1024]; - - if (Abc_TtCountOnesInTruth(pTruth, nVars) != (1 << (nVars - 1))) - return func(p, pTruth, nVars, pCanonPerm, flag); - Abc_TtCopy(pTruth2, pTruth, nWords, 1); - Abc_TtNormalizeSmallTruth(pTruth2, nVars); - uCanonPhase1 = func(p, pTruth, nVars, pCanonPerm, flag); - uCanonPhase2 = func(p, pTruth2, nVars, pCanonPerm2, flag); - if (Abc_TtCompareRev(pTruth, pTruth2, nWords) <= 0) - return uCanonPhase1; - Abc_TtCopy(pTruth, pTruth2, nWords, 0); - memcpy(pCanonPerm, pCanonPerm2, nVars); - return uCanonPhase2; + int nWords = Abc_TtWordNum(nVars); + unsigned uCanonPhase1, uCanonPhase2; + char pCanonPerm2[16]; + static word pTruth2[1024]; + + Abc_TtNormalizeSmallTruth(pTruth, nVars); + if (Abc_TtCountOnesInTruth(pTruth, nVars) != nWords * 32) + return func(p, pTruth, nVars, pCanonPerm, flag); + Abc_TtCopy(pTruth2, pTruth, nWords, 1); + uCanonPhase1 = func(p, pTruth, nVars, pCanonPerm, flag); + uCanonPhase2 = func(p, pTruth2, nVars, pCanonPerm2, flag); + if (Abc_TtCompareRev(pTruth, pTruth2, nWords) <= 0) + return uCanonPhase1; + Abc_TtCopy(pTruth, pTruth2, nWords, 0); + memcpy(pCanonPerm, pCanonPerm2, nVars); + return uCanonPhase2; } word gpVerCopy[1024]; static int Abc_TtCannonVerify(word* pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase) { #ifdef CANON_VERIFY - int nWords = Abc_TtWordNum(nVars); - char pCanonPermCopy[16]; - static word pCopy2[1024]; - Abc_TtCopy(pCopy2, pTruth, nWords, 0); - memcpy(pCanonPermCopy, pCanonPerm, sizeof(char) * nVars); - Abc_TtImplementNpnConfig(pCopy2, nVars, pCanonPermCopy, uCanonPhase); - Abc_TtNormalizeSmallTruth(pCopy2, nVars); - return Abc_TtEqual(gpVerCopy, pCopy2, nWords); + int nWords = Abc_TtWordNum(nVars); + char pCanonPermCopy[16]; + static word pCopy2[1024]; + Abc_TtVerifySmallTruth(pTruth, nVars); + Abc_TtCopy(pCopy2, pTruth, nWords, 0); + memcpy(pCanonPermCopy, pCanonPerm, sizeof(char) * nVars); + Abc_TtImplementNpnConfig(pCopy2, nVars, pCanonPermCopy, uCanonPhase); + return Abc_TtEqual(gpVerCopy, pCopy2, nWords); #else - return 1; + return 1; #endif } @@ -1479,44 +1492,44 @@ SeeAlso [] static void Abc_TginitMan(Abc_TgMan_t * pMan, word * pTruth, int nVars) { - int i; - pMan->pTruth = pTruth; - pMan->nVars = pMan->nGVars = nVars; - pMan->uPhase = 0; - for (i = 0; i < nVars; i++) - { - pMan->pPerm[i] = i; - pMan->pPermT[i] = i; - pMan->pPermTRev[i] = i; - pMan->symPhase[i] = 1; - } + int i; + pMan->pTruth = pTruth; + pMan->nVars = pMan->nGVars = nVars; + pMan->uPhase = 0; + for (i = 0; i < nVars; i++) + { + pMan->pPerm[i] = i; + pMan->pPermT[i] = i; + pMan->pPermTRev[i] = i; + pMan->symPhase[i] = 1; + } } static inline void Abc_TgManCopy(Abc_TgMan_t* pDst, word* pDstTruth, Abc_TgMan_t* pSrc) { - *pDst = *pSrc; - Abc_TtCopy(pDstTruth, pSrc->pTruth, Abc_TtWordNum(pSrc->nVars), 0); - pDst->pTruth = pDstTruth; + *pDst = *pSrc; + Abc_TtCopy(pDstTruth, pSrc->pTruth, Abc_TtWordNum(pSrc->nVars), 0); + pDst->pTruth = pDstTruth; } static inline int Abc_TgCannonVerify(Abc_TgMan_t* pMan) { - return Abc_TtCannonVerify(pMan->pTruth, pMan->nVars, pMan->pPermT, pMan->uPhase); + return Abc_TtCannonVerify(pMan->pTruth, pMan->nVars, pMan->pPermT, pMan->uPhase); } void Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pPerm, char * pDest); static void CheckConfig(Abc_TgMan_t * pMan) { #ifndef NDEBUG - int i; - char pPermE[16]; - Abc_TgExpendSymmetry(pMan, pMan->pPerm, pPermE); - for (i = 0; i < pMan->nVars; i++) - { - assert(pPermE[i] == pMan->pPermT[i]); - assert(pMan->pPermTRev[(int)pMan->pPermT[i]] == i); - } - assert(Abc_TgCannonVerify(pMan)); + int i; + char pPermE[16]; + Abc_TgExpendSymmetry(pMan, pMan->pPerm, pPermE); + for (i = 0; i < pMan->nVars; i++) + { + assert(pPermE[i] == pMan->pPermT[i]); + assert(pMan->pPermTRev[(int)pMan->pPermT[i]] == i); + } + assert(Abc_TgCannonVerify(pMan)); #endif } @@ -1534,84 +1547,84 @@ SeeAlso [] static inline void Abc_TgFlipVar(Abc_TgMan_t* pMan, int iVar) { - int nWords = Abc_TtWordNum(pMan->nVars); - int ivp = pMan->pPermTRev[iVar]; - Abc_TtFlip(pMan->pTruth, nWords, ivp); - pMan->uPhase ^= 1 << ivp; + int nWords = Abc_TtWordNum(pMan->nVars); + int ivp = pMan->pPermTRev[iVar]; + Abc_TtFlip(pMan->pTruth, nWords, ivp); + pMan->uPhase ^= 1 << ivp; } static inline void Abc_TgFlipSymGroupByVar(Abc_TgMan_t* pMan, int iVar) { - for (; iVar >= 0; iVar = pMan->symLink[iVar]) - if (pMan->symPhase[iVar]) - Abc_TgFlipVar(pMan, iVar); + for (; iVar >= 0; iVar = pMan->symLink[iVar]) + if (pMan->symPhase[iVar]) + Abc_TgFlipVar(pMan, iVar); } static inline void Abc_TgFlipSymGroup(Abc_TgMan_t* pMan, int idx) { - Abc_TgFlipSymGroupByVar(pMan, pMan->pPerm[idx]); + Abc_TgFlipSymGroupByVar(pMan, pMan->pPerm[idx]); } static inline void Abc_TgClearSymGroupPhase(Abc_TgMan_t* pMan, int iVar) { - for (; iVar >= 0; iVar = pMan->symLink[iVar]) - pMan->symPhase[iVar] = 0; + for (; iVar >= 0; iVar = pMan->symLink[iVar]) + pMan->symPhase[iVar] = 0; } static void Abc_TgImplementPerm(Abc_TgMan_t* pMan, const char *pPermDest) { - int i, nVars = pMan->nVars; - char *pPerm = pMan->pPermT; - char *pRev = pMan->pPermTRev; - unsigned uPhase = pMan->uPhase & (1 << nVars); - - for (i = 0; i < nVars; i++) - pRev[(int)pPerm[i]] = i; - for (i = 0; i < nVars; i++) - pPerm[i] = pRev[(int)pPermDest[i]]; - for (i = 0; i < nVars; i++) - pRev[(int)pPerm[i]] = i; - - Abc_TtImplementNpnConfig(pMan->pTruth, nVars, pRev, 0); - Abc_TtNormalizeSmallTruth(pMan->pTruth, nVars); - - for (i = 0; i < nVars; i++) - { - if (pMan->uPhase & (1 << pPerm[i])) - uPhase |= (1 << i); - pPerm[i] = pPermDest[i]; - pRev[(int)pPerm[i]] = i; - } - pMan->uPhase = uPhase; + int i, nVars = pMan->nVars; + char *pPerm = pMan->pPermT; + char *pRev = pMan->pPermTRev; + unsigned uPhase = pMan->uPhase & (1 << nVars); + + for (i = 0; i < nVars; i++) + pRev[(int)pPerm[i]] = i; + for (i = 0; i < nVars; i++) + pPerm[i] = pRev[(int)pPermDest[i]]; + for (i = 0; i < nVars; i++) + pRev[(int)pPerm[i]] = i; + + Abc_TtImplementNpnConfig(pMan->pTruth, nVars, pRev, 0); +// Abc_TtVerifySmallTruth(pMan->pTruth, nVars); + + for (i = 0; i < nVars; i++) + { + if (pMan->uPhase & (1 << pPerm[i])) + uPhase |= (1 << i); + pPerm[i] = pPermDest[i]; + pRev[(int)pPerm[i]] = i; + } + pMan->uPhase = uPhase; } static void Abc_TgSwapAdjacentSymGroups(Abc_TgMan_t* pMan, int idx) { - int iVar, jVar, ix; - char pPermNew[16]; - assert(idx < pMan->nGVars - 1); - iVar = pMan->pPerm[idx]; - jVar = pMan->pPerm[idx + 1]; - pMan->pPerm[idx] = jVar; - pMan->pPerm[idx + 1] = iVar; - ABC_SWAP(char, pMan->pPermDir[idx], pMan->pPermDir[idx + 1]); - if (pMan->symLink[iVar] >= 0 || pMan->symLink[jVar] >= 0) - { - Abc_TgExpendSymmetry(pMan, pMan->pPerm, pPermNew); - Abc_TgImplementPerm(pMan, pPermNew); - return; - } - // plain variable swap - ix = pMan->pPermTRev[iVar]; - assert(pMan->pPermT[ix] == iVar && pMan->pPermT[ix + 1] == jVar); - Abc_TtSwapAdjacent(pMan->pTruth, Abc_TtWordNum(pMan->nVars), ix); - pMan->pPermT[ix] = jVar; - pMan->pPermT[ix + 1] = iVar; - pMan->pPermTRev[iVar] = ix + 1; - pMan->pPermTRev[jVar] = ix; - if (((pMan->uPhase >> ix) & 1) != ((pMan->uPhase >> (ix + 1)) & 1)) - pMan->uPhase ^= 1 << ix | 1 << (ix + 1); - assert(Abc_TgCannonVerify(pMan)); + int iVar, jVar, ix; + char pPermNew[16]; + assert(idx < pMan->nGVars - 1); + iVar = pMan->pPerm[idx]; + jVar = pMan->pPerm[idx + 1]; + pMan->pPerm[idx] = jVar; + pMan->pPerm[idx + 1] = iVar; + ABC_SWAP(char, pMan->pPermDir[idx], pMan->pPermDir[idx + 1]); + if (pMan->symLink[iVar] >= 0 || pMan->symLink[jVar] >= 0) + { + Abc_TgExpendSymmetry(pMan, pMan->pPerm, pPermNew); + Abc_TgImplementPerm(pMan, pPermNew); + return; + } + // plain variable swap + ix = pMan->pPermTRev[iVar]; + assert(pMan->pPermT[ix] == iVar && pMan->pPermT[ix + 1] == jVar); + Abc_TtSwapAdjacent(pMan->pTruth, Abc_TtWordNum(pMan->nVars), ix); + pMan->pPermT[ix] = jVar; + pMan->pPermT[ix + 1] = iVar; + pMan->pPermTRev[iVar] = ix + 1; + pMan->pPermTRev[jVar] = ix; + if (((pMan->uPhase >> ix) & 1) != ((pMan->uPhase >> (ix + 1)) & 1)) + pMan->uPhase ^= 1 << ix | 1 << (ix + 1); + assert(Abc_TgCannonVerify(pMan)); } /**Function************************************************************* @@ -1630,33 +1643,33 @@ static word pSymCopy[1024]; static int Abc_TtIsSymmetric(word * pTruth, int nVars, int iVar, int jVar, int fPhase) { - int rv; - int nWords = Abc_TtWordNum(nVars); - Abc_TtCopy(pSymCopy, pTruth, nWords, 0); - Abc_TtSwapVars(pSymCopy, nVars, iVar, jVar); - rv = Abc_TtEqual(pTruth, pSymCopy, nWords) * 2; - if (!fPhase) return rv; - Abc_TtFlip(pSymCopy, nWords, iVar); - Abc_TtFlip(pSymCopy, nWords, jVar); - return rv + Abc_TtEqual(pTruth, pSymCopy, nWords); + int rv; + int nWords = Abc_TtWordNum(nVars); + Abc_TtCopy(pSymCopy, pTruth, nWords, 0); + Abc_TtSwapVars(pSymCopy, nVars, iVar, jVar); + rv = Abc_TtEqual(pTruth, pSymCopy, nWords) * 2; + if (!fPhase) return rv; + Abc_TtFlip(pSymCopy, nWords, iVar); + Abc_TtFlip(pSymCopy, nWords, jVar); + return rv + Abc_TtEqual(pTruth, pSymCopy, nWords); } static int Abc_TtIsSymmetricHigh(Abc_TgMan_t * pMan, int iVar, int jVar, int fPhase) { - int rv, iv, jv, n; - int nWords = Abc_TtWordNum(pMan->nVars); - Abc_TtCopy(pSymCopy, pMan->pTruth, nWords, 0); - for (n = 0, iv = iVar, jv = jVar; iv >= 0 && jv >= 0; iv = pMan->symLink[iv], jv = pMan->symLink[jv], n++) - Abc_TtSwapVars(pSymCopy, pMan->nVars, iv, jv); - assert(iv < 0 && jv < 0); // two symmetric groups must have the same size - rv = Abc_TtEqual(pMan->pTruth, pSymCopy, nWords) * 2; - if (!fPhase) return rv; - for (iv = iVar, jv = jVar; iv >= 0 && jv >= 0; iv = pMan->symLink[iv], jv = pMan->symLink[jv]) - { - if (pMan->symPhase[iv]) Abc_TtFlip(pSymCopy, nWords, iv); - if (pMan->symPhase[jv]) Abc_TtFlip(pSymCopy, nWords, jv); - } - return rv + Abc_TtEqual(pMan->pTruth, pSymCopy, nWords); + int rv, iv, jv, n; + int nWords = Abc_TtWordNum(pMan->nVars); + Abc_TtCopy(pSymCopy, pMan->pTruth, nWords, 0); + for (n = 0, iv = iVar, jv = jVar; iv >= 0 && jv >= 0; iv = pMan->symLink[iv], jv = pMan->symLink[jv], n++) + Abc_TtSwapVars(pSymCopy, pMan->nVars, iv, jv); + assert(iv < 0 && jv < 0); // two symmetric groups must have the same size + rv = Abc_TtEqual(pMan->pTruth, pSymCopy, nWords) * 2; + if (!fPhase) return rv; + for (iv = iVar, jv = jVar; iv >= 0 && jv >= 0; iv = pMan->symLink[iv], jv = pMan->symLink[jv]) + { + if (pMan->symPhase[iv]) Abc_TtFlip(pSymCopy, nWords, iv); + if (pMan->symPhase[jv]) Abc_TtFlip(pSymCopy, nWords, jv); + } + return rv + Abc_TtEqual(pMan->pTruth, pSymCopy, nWords); } /**Function************************************************************* @@ -1665,7 +1678,7 @@ Synopsis [Create groups by cofactor signatures] Description [Similar to Abc_TtSemiCanonicize. Use stable insertion sort to keep the order of the variables in the groups. - Defer permutation. ] + Defer permutation. ] SideEffects [] @@ -1675,53 +1688,53 @@ SeeAlso [] static void Abc_TgCreateGroups(Abc_TgMan_t * pMan) { - int pStore[17]; - int i, j, nOnes; - int nVars = pMan->nVars, nWords = Abc_TtWordNum(nVars); - TiedGroup * pGrp = pMan->pGroup; - assert(nVars <= 16); - // normalize polarity - nOnes = Abc_TtCountOnesInTruth(pMan->pTruth, nVars); - if (nOnes > (1 << (nVars - 1))) - { - Abc_TtNot(pMan->pTruth, nWords); - nOnes = (1 << nVars) - nOnes; - pMan->uPhase |= (1 << nVars); - } - // normalize phase - Abc_TtCountOnesInCofs(pMan->pTruth, nVars, pStore); - pStore[nVars] = nOnes; - for (i = 0; i < nVars; i++) - { - if (pStore[i] >= nOnes - pStore[i]) - continue; - Abc_TtFlip(pMan->pTruth, nWords, i); - pMan->uPhase |= (1 << i); - pStore[i] = nOnes - pStore[i]; - } - - // sort variables - for (i = 1; i < nVars; i++) - { - int a = pStore[i]; char aa = pMan->pPerm[i]; - for (j = i; j > 0 && pStore[j - 1] > a; j--) - pStore[j] = pStore[j - 1], pMan->pPerm[j] = pMan->pPerm[j - 1]; - pStore[j] = a; pMan->pPerm[j] = aa; - } - // group variables -// Abc_SortIdxC(pStore, pMan->pPerm, nVars); - pGrp[0].iStart = 0; - pGrp[0].fPhased = pStore[0] * 2 != nOnes; - for (i = j = 1; i < nVars; i++) - { - if (pStore[i] == pStore[i - 1]) continue; - pGrp[j].iStart = i; - pGrp[j].fPhased = pStore[i] * 2 != nOnes; - pGrp[j - 1].nGVars = i - pGrp[j - 1].iStart; - j++; - } - pGrp[j - 1].nGVars = i - pGrp[j - 1].iStart; - pMan->nGroups = j; + int pStore[17]; + int i, j, nOnes; + int nVars = pMan->nVars, nWords = Abc_TtWordNum(nVars); + TiedGroup * pGrp = pMan->pGroup; + assert(nVars <= 16); + // normalize polarity + nOnes = Abc_TtCountOnesInTruth(pMan->pTruth, nVars); + if (nOnes > nWords * 32) + { + Abc_TtNot(pMan->pTruth, nWords); + nOnes = nWords * 64 - nOnes; + pMan->uPhase |= (1 << nVars); + } + // normalize phase + Abc_TtCountOnesInCofs(pMan->pTruth, nVars, pStore); + pStore[nVars] = nOnes; + for (i = 0; i < nVars; i++) + { + if (pStore[i] >= nOnes - pStore[i]) + continue; + Abc_TtFlip(pMan->pTruth, nWords, i); + pMan->uPhase |= (1 << i); + pStore[i] = nOnes - pStore[i]; + } + + // sort variables + for (i = 1; i < nVars; i++) + { + int a = pStore[i]; char aa = pMan->pPerm[i]; + for (j = i; j > 0 && pStore[j - 1] > a; j--) + pStore[j] = pStore[j - 1], pMan->pPerm[j] = pMan->pPerm[j - 1]; + pStore[j] = a; pMan->pPerm[j] = aa; + } + // group variables +// Abc_SortIdxC(pStore, pMan->pPerm, nVars); + pGrp[0].iStart = 0; + pGrp[0].fPhased = pStore[0] * 2 != nOnes; + for (i = j = 1; i < nVars; i++) + { + if (pStore[i] == pStore[i - 1]) continue; + pGrp[j].iStart = i; + pGrp[j].fPhased = pStore[i] * 2 != nOnes; + pGrp[j - 1].nGVars = i - pGrp[j - 1].iStart; + j++; + } + pGrp[j - 1].nGVars = i - pGrp[j - 1].iStart; + pMan->nGroups = j; } /**Function************************************************************* @@ -1738,135 +1751,135 @@ SeeAlso [] static int Abc_TgGroupSymmetry(Abc_TgMan_t * pMan, TiedGroup * pGrp, int doHigh) { - int i, j, iVar, jVar, nsym = 0; - int fDone[16], scnt[16], stype[16]; - signed char *symLink = pMan->symLink; -// char * symPhase = pMan->symPhase; - int nGVars = pGrp->nGVars; - char * pVars = pMan->pPerm + pGrp->iStart; - int modified; - - for (i = 0; i < nGVars; i++) - fDone[i] = 0, scnt[i] = 1; - - do { - modified = 0; - for (i = 0; i < nGVars - 1; i++) - { - iVar = pVars[i]; - if (iVar < 0 || fDone[i]) continue; -// if (!pGrp->fPhased && !Abc_TtHasVar(pMan->pTruth, pMan->nVars, iVar)) continue; - // Mark symmetric variables/groups - for (j = i + 1; j < nGVars; j++) - { - jVar = pVars[j]; - if (jVar < 0 || scnt[j] != scnt[i]) // || pMan->symPhase[jVar] != pMan->symPhase[iVar]) - stype[j] = 0; - else if (scnt[j] == 1) - stype[j] = Abc_TtIsSymmetric(pMan->pTruth, pMan->nVars, iVar, jVar, !pGrp->fPhased); - else - stype[j] = Abc_TtIsSymmetricHigh(pMan, iVar, jVar, !pGrp->fPhased); - } - fDone[i] = 1; - // Merge symmetric groups - for (j = i + 1; j < nGVars; j++) - { - int ii; - jVar = pVars[j]; - switch (stype[j]) - { - case 1: // E-Symmetry - Abc_TgFlipSymGroupByVar(pMan, jVar); - // fallthrough - case 2: // NE-Symmetry - pMan->symPhase[iVar] += pMan->symPhase[jVar]; - break; - case 3: // multiform Symmetry - Abc_TgClearSymGroupPhase(pMan, jVar); - break; - default: // case 0: No Symmetry - continue; - } - - for (ii = iVar; symLink[ii] >= 0; ii = symLink[ii]) - ; - symLink[ii] = jVar; - pVars[j] = -1; - scnt[i] += scnt[j]; - modified = 1; - fDone[i] = 0; - nsym++; - } - } -// if (++order > 3) printf("%d", order); - } while (doHigh && modified); - - return nsym; + int i, j, iVar, jVar, nsym = 0; + int fDone[16], scnt[16], stype[16]; + signed char *symLink = pMan->symLink; +// char * symPhase = pMan->symPhase; + int nGVars = pGrp->nGVars; + char * pVars = pMan->pPerm + pGrp->iStart; + int modified; + + for (i = 0; i < nGVars; i++) + fDone[i] = 0, scnt[i] = 1; + + do { + modified = 0; + for (i = 0; i < nGVars - 1; i++) + { + iVar = pVars[i]; + if (iVar < 0 || fDone[i]) continue; +// if (!pGrp->fPhased && !Abc_TtHasVar(pMan->pTruth, pMan->nVars, iVar)) continue; + // Mark symmetric variables/groups + for (j = i + 1; j < nGVars; j++) + { + jVar = pVars[j]; + if (jVar < 0 || scnt[j] != scnt[i]) // || pMan->symPhase[jVar] != pMan->symPhase[iVar]) + stype[j] = 0; + else if (scnt[j] == 1) + stype[j] = Abc_TtIsSymmetric(pMan->pTruth, pMan->nVars, iVar, jVar, !pGrp->fPhased); + else + stype[j] = Abc_TtIsSymmetricHigh(pMan, iVar, jVar, !pGrp->fPhased); + } + fDone[i] = 1; + // Merge symmetric groups + for (j = i + 1; j < nGVars; j++) + { + int ii; + jVar = pVars[j]; + switch (stype[j]) + { + case 1: // E-Symmetry + Abc_TgFlipSymGroupByVar(pMan, jVar); + // fallthrough + case 2: // NE-Symmetry + pMan->symPhase[iVar] += pMan->symPhase[jVar]; + break; + case 3: // multiform Symmetry + Abc_TgClearSymGroupPhase(pMan, jVar); + break; + default: // case 0: No Symmetry + continue; + } + + for (ii = iVar; symLink[ii] >= 0; ii = symLink[ii]) + ; + symLink[ii] = jVar; + pVars[j] = -1; + scnt[i] += scnt[j]; + modified = 1; + fDone[i] = 0; + nsym++; + } + } +// if (++order > 3) printf("%d", order); + } while (doHigh && modified); + + return nsym; } static void Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan, int doHigh) { - int i, j, k, sum = 0, nVars = pMan->nVars; - signed char *symLink = pMan->symLink; - char gcnt[16] = { 0 }; - char * pPerm = pMan->pPerm; - - for (i = 0; i <= nVars; i++) - symLink[i] = -1; - - // purge unsupported variables - if (!pMan->pGroup[0].fPhased) - { - int iVar = pMan->nVars; - for (j = 0; j < pMan->pGroup[0].nGVars; j++) - { - int jVar = pPerm[j]; - assert(jVar >= 0); - if (!Abc_TtHasVar(pMan->pTruth, nVars, jVar)) - { - symLink[jVar] = symLink[iVar]; - symLink[iVar] = jVar; - pPerm[j] = -1; - gcnt[0]++; - } - } - } - - for (k = 0; k < pMan->nGroups; k++) - gcnt[k] += Abc_TgGroupSymmetry(pMan, pMan->pGroup + k, doHigh); - - for (i = 0; i < nVars && pPerm[i] >= 0; i++) - ; - for (j = i + 1; ; i++, j++) - { - while (j < nVars && pPerm[j] < 0) j++; - if (j >= nVars) break; - pPerm[i] = pPerm[j]; - } - for (k = 0; k < pMan->nGroups; k++) - { - pMan->pGroup[k].nGVars -= gcnt[k]; - pMan->pGroup[k].iStart -= sum; - sum += gcnt[k]; - } - if (pMan->pGroup[0].nGVars == 0) - { - pMan->nGroups--; - memmove(pMan->pGroup, pMan->pGroup + 1, sizeof(TiedGroup) * pMan->nGroups); - assert(pMan->pGroup[0].iStart == 0); - } - pMan->nGVars -= sum; + int i, j, k, sum = 0, nVars = pMan->nVars; + signed char *symLink = pMan->symLink; + char gcnt[16] = { 0 }; + char * pPerm = pMan->pPerm; + + for (i = 0; i <= nVars; i++) + symLink[i] = -1; + + // purge unsupported variables + if (!pMan->pGroup[0].fPhased) + { + int iVar = pMan->nVars; + for (j = 0; j < pMan->pGroup[0].nGVars; j++) + { + int jVar = pPerm[j]; + assert(jVar >= 0); + if (!Abc_TtHasVar(pMan->pTruth, nVars, jVar)) + { + symLink[jVar] = symLink[iVar]; + symLink[iVar] = jVar; + pPerm[j] = -1; + gcnt[0]++; + } + } + } + + for (k = 0; k < pMan->nGroups; k++) + gcnt[k] += Abc_TgGroupSymmetry(pMan, pMan->pGroup + k, doHigh); + + for (i = 0; i < nVars && pPerm[i] >= 0; i++) + ; + for (j = i + 1; ; i++, j++) + { + while (j < nVars && pPerm[j] < 0) j++; + if (j >= nVars) break; + pPerm[i] = pPerm[j]; + } + for (k = 0; k < pMan->nGroups; k++) + { + pMan->pGroup[k].nGVars -= gcnt[k]; + pMan->pGroup[k].iStart -= sum; + sum += gcnt[k]; + } + if (pMan->pGroup[0].nGVars == 0) + { + pMan->nGroups--; + memmove(pMan->pGroup, pMan->pGroup + 1, sizeof(TiedGroup) * pMan->nGroups); + assert(pMan->pGroup[0].iStart == 0); + } + pMan->nGVars -= sum; } void Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pPerm, char * pDest) { - int i = 0, j, k; - for (j = 0; j < pMan->nGVars; j++) - for (k = pPerm[j]; k >= 0; k = pMan->symLink[k]) - pDest[i++] = k; - for (k = pMan->symLink[pMan->nVars]; k >= 0; k = pMan->symLink[k]) - pDest[i++] = k; - assert(i == pMan->nVars); + int i = 0, j, k; + for (j = 0; j < pMan->nGVars; j++) + for (k = pPerm[j]; k >= 0; k = pMan->symLink[k]) + pDest[i++] = k; + for (k = pMan->symLink[pMan->nVars]; k >= 0; k = pMan->symLink[k]) + pDest[i++] = k; + assert(i == pMan->nVars); } @@ -1883,130 +1896,130 @@ SeeAlso [] ***********************************************************************/ static int Abc_TgSymGroupPerm(Abc_TgMan_t* pMan, int idx, TiedGroup* pTGrp) { - word* pTruth = pMan->pTruth; - static word pCopy[1024]; - static word pBest[1024]; - int Config = 0; - int nWords = Abc_TtWordNum(pMan->nVars); - Abc_TgMan_t tgManCopy, tgManBest; - int fSwapOnly = pTGrp->fPhased; - - CheckConfig(pMan); - if (fSwapOnly) - { - Abc_TgManCopy(&tgManCopy, pCopy, pMan); - Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pTruth, pCopy, nWords) < 0) - { - Abc_TgManCopy(pMan, pTruth, &tgManCopy); - return 4; - } - return 0; - } - - // save two copies - Abc_TgManCopy(&tgManCopy, pCopy, pMan); - Abc_TgManCopy(&tgManBest, pBest, pMan); - // PXY - // 001 - Abc_TgFlipSymGroup(&tgManCopy, idx); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 1; - // PXY - // 011 - Abc_TgFlipSymGroup(&tgManCopy, idx + 1); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 3; - // PXY - // 010 - Abc_TgFlipSymGroup(&tgManCopy, idx); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 2; - // PXY - // 110 - Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 6; - // PXY - // 111 - Abc_TgFlipSymGroup(&tgManCopy, idx + 1); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 7; - // PXY - // 101 - Abc_TgFlipSymGroup(&tgManCopy, idx); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 5; - // PXY - // 100 - Abc_TgFlipSymGroup(&tgManCopy, idx + 1); - CheckConfig(&tgManCopy); - if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) - Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 4; - // PXY - // 000 - Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx); - CheckConfig(&tgManCopy); - assert(Abc_TtEqual(pTruth, pCopy, nWords)); - if (Config == 0) - return 0; - assert(Abc_TtCompareRev(pTruth, pBest, nWords) == 1); - Abc_TgManCopy(pMan, pTruth, &tgManBest); - return Config; + word* pTruth = pMan->pTruth; + static word pCopy[1024]; + static word pBest[1024]; + int Config = 0; + int nWords = Abc_TtWordNum(pMan->nVars); + Abc_TgMan_t tgManCopy, tgManBest; + int fSwapOnly = pTGrp->fPhased; + + CheckConfig(pMan); + if (fSwapOnly) + { + Abc_TgManCopy(&tgManCopy, pCopy, pMan); + Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pTruth, pCopy, nWords) < 0) + { + Abc_TgManCopy(pMan, pTruth, &tgManCopy); + return 4; + } + return 0; + } + + // save two copies + Abc_TgManCopy(&tgManCopy, pCopy, pMan); + Abc_TgManCopy(&tgManBest, pBest, pMan); + // PXY + // 001 + Abc_TgFlipSymGroup(&tgManCopy, idx); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 1; + // PXY + // 011 + Abc_TgFlipSymGroup(&tgManCopy, idx + 1); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 3; + // PXY + // 010 + Abc_TgFlipSymGroup(&tgManCopy, idx); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 2; + // PXY + // 110 + Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 6; + // PXY + // 111 + Abc_TgFlipSymGroup(&tgManCopy, idx + 1); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 7; + // PXY + // 101 + Abc_TgFlipSymGroup(&tgManCopy, idx); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 5; + // PXY + // 100 + Abc_TgFlipSymGroup(&tgManCopy, idx + 1); + CheckConfig(&tgManCopy); + if (Abc_TtCompareRev(pBest, pCopy, nWords) == 1) + Abc_TgManCopy(&tgManBest, pBest, &tgManCopy), Config = 4; + // PXY + // 000 + Abc_TgSwapAdjacentSymGroups(&tgManCopy, idx); + CheckConfig(&tgManCopy); + assert(Abc_TtEqual(pTruth, pCopy, nWords)); + if (Config == 0) + return 0; + assert(Abc_TtCompareRev(pTruth, pBest, nWords) == 1); + Abc_TgManCopy(pMan, pTruth, &tgManBest); + return Config; } static int Abc_TgPermPhase(Abc_TgMan_t* pMan, int iVar) { - static word pCopy[1024]; - int nWords = Abc_TtWordNum(pMan->nVars); - int ivp = pMan->pPermTRev[iVar]; - Abc_TtCopy(pCopy, pMan->pTruth, nWords, 0); - Abc_TtFlip(pCopy, nWords, ivp); - if (Abc_TtCompareRev(pMan->pTruth, pCopy, nWords) == 1) - { - Abc_TtCopy(pMan->pTruth, pCopy, nWords, 0); - pMan->uPhase ^= 1 << ivp; - return 16; - } - return 0; + static word pCopy[1024]; + int nWords = Abc_TtWordNum(pMan->nVars); + int ivp = pMan->pPermTRev[iVar]; + Abc_TtCopy(pCopy, pMan->pTruth, nWords, 0); + Abc_TtFlip(pCopy, nWords, ivp); + if (Abc_TtCompareRev(pMan->pTruth, pCopy, nWords) == 1) + { + Abc_TtCopy(pMan->pTruth, pCopy, nWords, 0); + pMan->uPhase ^= 1 << ivp; + return 16; + } + return 0; } static void Abc_TgSimpleEnumeration(Abc_TgMan_t * pMan) { - int i, j, k; - int pGid[16]; - - for (k = j = 0; j < pMan->nGroups; j++) - for (i = 0; i < pMan->pGroup[j].nGVars; i++, k++) - pGid[k] = j; - assert(k == pMan->nGVars); - - for (k = 0; k < 5; k++) - { - int fChanges = 0; - for (i = pMan->nGVars - 2; i >= 0; i--) - if (pGid[i] == pGid[i + 1]) - fChanges |= Abc_TgSymGroupPerm(pMan, i, pMan->pGroup + pGid[i]); - for (i = 1; i < pMan->nGVars - 1; i++) - if (pGid[i] == pGid[i + 1]) - fChanges |= Abc_TgSymGroupPerm(pMan, i, pMan->pGroup + pGid[i]); - - for (i = pMan->nVars - 1; i >= 0; i--) - if (pMan->symPhase[i]) - fChanges |= Abc_TgPermPhase(pMan, i); - for (i = 1; i < pMan->nVars; i++) - if (pMan->symPhase[i]) - fChanges |= Abc_TgPermPhase(pMan, i); - if (!fChanges) break; - } - assert(Abc_TgCannonVerify(pMan)); + int i, j, k; + int pGid[16]; + + for (k = j = 0; j < pMan->nGroups; j++) + for (i = 0; i < pMan->pGroup[j].nGVars; i++, k++) + pGid[k] = j; + assert(k == pMan->nGVars); + + for (k = 0; k < 5; k++) + { + int fChanges = 0; + for (i = pMan->nGVars - 2; i >= 0; i--) + if (pGid[i] == pGid[i + 1]) + fChanges |= Abc_TgSymGroupPerm(pMan, i, pMan->pGroup + pGid[i]); + for (i = 1; i < pMan->nGVars - 1; i++) + if (pGid[i] == pGid[i + 1]) + fChanges |= Abc_TgSymGroupPerm(pMan, i, pMan->pGroup + pGid[i]); + + for (i = pMan->nVars - 1; i >= 0; i--) + if (pMan->symPhase[i]) + fChanges |= Abc_TgPermPhase(pMan, i); + for (i = 1; i < pMan->nVars; i++) + if (pMan->symPhase[i]) + fChanges |= Abc_TgPermPhase(pMan, i); + if (!fChanges) break; + } + assert(Abc_TgCannonVerify(pMan)); } /**Function************************************************************* @@ -2023,194 +2036,198 @@ SeeAlso [] // enumeration time = exp((cost-27.12)*0.59) static int Abc_TgEnumerationCost(Abc_TgMan_t * pMan) { - int cSym = 0; - double cPerm = 0.0; - TiedGroup * pGrp = 0; - int i, j, n; - if (pMan->nGroups == 0) return 0; - - for (i = 0; i < pMan->nGroups; i++) - { - pGrp = pMan->pGroup + i; - n = pGrp->nGVars; - if (n > 1) - cPerm += 0.92 + log(n) / 2 + n * (log(n) - 1); - } - if (pMan->pGroup->fPhased) - n = 0; - else - { - char * pVars = pMan->pPerm; - n = pMan->pGroup->nGVars; - for (i = 0; i < n; i++) - for (j = pVars[i]; j >= 0; j = pMan->symLink[j]) - cSym++; - } - // coefficients computed by linear regression - return pMan->nVars + n * 1.09 + cPerm * 1.65 + 0.5; -// return (rv > 60 ? 100000000 : 0) + n * 1000000 + cSym * 10000 + cPerm * 100 + 0.5; + int cSym = 0; + double cPerm = 0.0; + TiedGroup * pGrp = 0; + int i, j, n; + if (pMan->nGroups == 0) return 0; + + for (i = 0; i < pMan->nGroups; i++) + { + pGrp = pMan->pGroup + i; + n = pGrp->nGVars; + if (n > 1) + cPerm += 0.92 + log(n) / 2 + n * (log(n) - 1); + } + if (pMan->pGroup->fPhased) + n = 0; + else + { + char * pVars = pMan->pPerm; + n = pMan->pGroup->nGVars; + for (i = 0; i < n; i++) + for (j = pVars[i]; j >= 0; j = pMan->symLink[j]) + cSym++; + } + // coefficients computed by linear regression + return pMan->nVars + n * 1.09 + cPerm * 1.65 + 0.5; +// return (rv > 60 ? 100000000 : 0) + n * 1000000 + cSym * 10000 + cPerm * 100 + 0.5; } static int Abc_TgIsInitPerm(char * pData, signed char * pDir, int size) { - int i; - if (pDir[0] != -1) return 0; - for (i = 1; i < size; i++) - if (pDir[i] != -1 || pData[i] < pData[i - 1]) - return 0; - return 1; + int i; + if (pDir[0] != -1) return 0; + for (i = 1; i < size; i++) + if (pDir[i] != -1 || pData[i] < pData[i - 1]) + return 0; + return 1; } static void Abc_TgFirstPermutation(Abc_TgMan_t * pMan) { - int i; - for (i = 0; i < pMan->nGVars; i++) - pMan->pPermDir[i] = -1; + int i; + for (i = 0; i < pMan->nGVars; i++) + pMan->pPermDir[i] = -1; #ifndef NDEBUG - for (i = 0; i < pMan->nGroups; i++) - { - TiedGroup * pGrp = pMan->pGroup + i; - int nGvars = pGrp->nGVars; - char * pVars = pMan->pPerm + pGrp->iStart; - signed char * pDirs = pMan->pPermDir + pGrp->iStart; - assert(Abc_TgIsInitPerm(pVars, pDirs, nGvars)); - } + for (i = 0; i < pMan->nGroups; i++) + { + TiedGroup * pGrp = pMan->pGroup + i; + int nGvars = pGrp->nGVars; + char * pVars = pMan->pPerm + pGrp->iStart; + signed char * pDirs = pMan->pPermDir + pGrp->iStart; + assert(Abc_TgIsInitPerm(pVars, pDirs, nGvars)); + } #endif } static int Abc_TgNextPermutation(Abc_TgMan_t * pMan) { - int i, j, nGvars; - TiedGroup * pGrp; - char * pVars; - signed char * pDirs; - for (i = 0; i < pMan->nGroups; i++) - { - pGrp = pMan->pGroup + i; - nGvars = pGrp->nGVars; - if (nGvars == 1) continue; - pVars = pMan->pPerm + pGrp->iStart; - pDirs = pMan->pPermDir + pGrp->iStart; - j = Abc_NextPermSwapC(pVars, pDirs, nGvars); - if (j >= 0) - { - Abc_TgSwapAdjacentSymGroups(pMan, j + pGrp->iStart); - return 1; - } - Abc_TgSwapAdjacentSymGroups(pMan, pGrp->iStart); - assert(Abc_TgIsInitPerm(pVars, pDirs, nGvars)); - } - return 0; + int i, j, nGvars; + TiedGroup * pGrp; + char * pVars; + signed char * pDirs; + for (i = 0; i < pMan->nGroups; i++) + { + pGrp = pMan->pGroup + i; + nGvars = pGrp->nGVars; + if (nGvars == 1) continue; + pVars = pMan->pPerm + pGrp->iStart; + pDirs = pMan->pPermDir + pGrp->iStart; + j = Abc_NextPermSwapC(pVars, pDirs, nGvars); + if (j >= 0) + { + Abc_TgSwapAdjacentSymGroups(pMan, j + pGrp->iStart); + return 1; + } + Abc_TgSwapAdjacentSymGroups(pMan, pGrp->iStart); + assert(Abc_TgIsInitPerm(pVars, pDirs, nGvars)); + } + return 0; } static inline unsigned grayCode(unsigned a) { return a ^ (a >> 1); } -static int grayFlip(unsigned a, int n) +static int grayFlip(unsigned a) { - unsigned d = grayCode(a) ^ grayCode(a + 1); - int i; - for (i = 0; i < n; i++) - if (d == 1U << i) return i; - assert(0); - return -1; -} + int i; + for (i = 0, a++; ; i++) + if (a & (1 << i)) return i; + } static inline void Abc_TgSaveBest(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest) { - if (Abc_TtCompare(pBest->pTruth, pMan->pTruth, Abc_TtWordNum(pMan->nVars)) == 1) - Abc_TgManCopy(pBest, pBest->pTruth, pMan); + if (Abc_TtCompare(pBest->pTruth, pMan->pTruth, Abc_TtWordNum(pMan->nVars)) == 1) + Abc_TgManCopy(pBest, pBest->pTruth, pMan); } static void Abc_TgPhaseEnumeration(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest) { - char pFGrps[16]; - TiedGroup * pGrp = pMan->pGroup; - int i, j, n = pGrp->nGVars; - - Abc_TgSaveBest(pMan, pBest); - if (pGrp->fPhased) return; - - // sort by symPhase - for (i = 0; i < n; i++) - { - char iv = pMan->pPerm[i]; - for (j = i; j > 0 && pMan->symPhase[(int)pFGrps[j-1]] > pMan->symPhase[(int)iv]; j--) - pFGrps[j] = pFGrps[j - 1]; - pFGrps[j] = iv; - } - - for (i = 0; i < (1 << n) - 1; i++) - { - Abc_TgFlipSymGroupByVar(pMan, pFGrps[grayFlip(i, n)]); - Abc_TgSaveBest(pMan, pBest); - } + char pFGrps[16]; + TiedGroup * pGrp = pMan->pGroup; + int i, j, n = pGrp->nGVars; + + Abc_TgSaveBest(pMan, pBest); + if (pGrp->fPhased) return; + + // sort by symPhase + for (i = 0; i < n; i++) + { + char iv = pMan->pPerm[i]; + for (j = i; j > 0 && pMan->symPhase[(int)pFGrps[j-1]] > pMan->symPhase[(int)iv]; j--) + pFGrps[j] = pFGrps[j - 1]; + pFGrps[j] = iv; + } + + for (i = 0; i < (1 << n) - 1; i++) + { + Abc_TgFlipSymGroupByVar(pMan, pFGrps[grayFlip(i)]); + Abc_TgSaveBest(pMan, pBest); + } } static void Abc_TgFullEnumeration(Abc_TgMan_t * pWork, Abc_TgMan_t * pBest) { -// static word pCopy[1024]; -// Abc_TgMan_t tgManCopy; -// Abc_TgManCopy(&tgManCopy, pCopy, pMan); - - Abc_TgFirstPermutation(pWork); - do Abc_TgPhaseEnumeration(pWork, pBest); - while (Abc_TgNextPermutation(pWork)); - pBest->uPhase |= 1U << 30; +// static word pCopy[1024]; +// Abc_TgMan_t tgManCopy; +// Abc_TgManCopy(&tgManCopy, pCopy, pMan); + + Abc_TgFirstPermutation(pWork); + do Abc_TgPhaseEnumeration(pWork, pBest); + while (Abc_TgNextPermutation(pWork)); + pBest->uPhase |= 1 << 30; } unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres) { - int nWords = Abc_TtWordNum(nVars); - unsigned fExac = 0, fHash = 1U << 29; - static word pCopy[1024]; - Abc_TgMan_t tgMan, tgManCopy; - int iCost; - const int MaxCost = 84; // maximun posible cost for function with 16 inputs - const int doHigh = iThres / 100, iEnumThres = iThres % 100; + int nWords = Abc_TtWordNum(nVars); + unsigned fExac = 0, fHash = 1 << 29; + static word pCopy[1024]; + Abc_TgMan_t tgMan, tgManCopy; + int iCost; + const int MaxCost = 84; // maximun posible cost for function with 16 inputs + const int doHigh = iThres / 100, iEnumThres = iThres % 100; + // handle constant + if ( nVars == 0 ) { + Abc_TtClear( pTruth, nWords ); + return 0; + } + + Abc_TtVerifySmallTruth(pTruth, nVars); #ifdef CANON_VERIFY - Abc_TtCopy(gpVerCopy, pTruth, nWords, 0); + Abc_TtCopy(gpVerCopy, pTruth, nWords, 0); #endif - assert(nVars <= 16); - if (p && Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash; - Abc_TginitMan(&tgMan, pTruth, nVars); - Abc_TgCreateGroups(&tgMan); - if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash; - Abc_TgPurgeSymmetry(&tgMan, doHigh); - - Abc_TgExpendSymmetry(&tgMan, tgMan.pPerm, pCanonPerm); - Abc_TgImplementPerm(&tgMan, pCanonPerm); - assert(Abc_TgCannonVerify(&tgMan)); - - if (p == NULL) { - if (iEnumThres > MaxCost || Abc_TgEnumerationCost(&tgMan) < iEnumThres) { - Abc_TgManCopy(&tgManCopy, pCopy, &tgMan); - Abc_TgFullEnumeration(&tgManCopy, &tgMan); - } - else - Abc_TgSimpleEnumeration(&tgMan); - } - else { - iCost = Abc_TgEnumerationCost(&tgMan); - if (iCost < iEnumThres) fExac = 1U << 30; - if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash + fExac; - Abc_TgManCopy(&tgManCopy, pCopy, &tgMan); - Abc_TgSimpleEnumeration(&tgMan); - if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash + fExac; - if (fExac) { - Abc_TgManCopy(&tgMan, pTruth, &tgManCopy); - Abc_TgFullEnumeration(&tgManCopy, &tgMan); - } - Abc_TtHieRetrieveOrInsert(p, -1, pTruth, pTruth); - } - memcpy(pCanonPerm, tgMan.pPermT, sizeof(char) * nVars); + assert(nVars <= 16); + if (p && Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash; + Abc_TginitMan(&tgMan, pTruth, nVars); + Abc_TgCreateGroups(&tgMan); + if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash; + Abc_TgPurgeSymmetry(&tgMan, doHigh); + + Abc_TgExpendSymmetry(&tgMan, tgMan.pPerm, pCanonPerm); + Abc_TgImplementPerm(&tgMan, pCanonPerm); + assert(Abc_TgCannonVerify(&tgMan)); + + if (p == NULL) { + if (iEnumThres > MaxCost || Abc_TgEnumerationCost(&tgMan) < iEnumThres) { + Abc_TgManCopy(&tgManCopy, pCopy, &tgMan); + Abc_TgFullEnumeration(&tgManCopy, &tgMan); + } + else + Abc_TgSimpleEnumeration(&tgMan); + } + else { + iCost = Abc_TgEnumerationCost(&tgMan); + if (iCost < iEnumThres) fExac = 1 << 30; + if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash + fExac; + Abc_TgManCopy(&tgManCopy, pCopy, &tgMan); + Abc_TgSimpleEnumeration(&tgMan); + if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash + fExac; + if (fExac) { + Abc_TgManCopy(&tgMan, pTruth, &tgManCopy); + Abc_TgFullEnumeration(&tgManCopy, &tgMan); + } + Abc_TtHieRetrieveOrInsert(p, -1, pTruth, pTruth); + } + memcpy(pCanonPerm, tgMan.pPermT, sizeof(char) * nVars); #ifdef CANON_VERIFY - if (!Abc_TgCannonVerify(&tgMan)) - printf("Canonical form verification failed!\n"); + if (!Abc_TgCannonVerify(&tgMan)) + printf("Canonical form verification failed!\n"); #endif - return tgMan.uPhase; + return tgMan.uPhase; } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c index dacdb02a..b57ade67 100644 --- a/src/opt/dau/dauNpn.c +++ b/src/opt/dau/dauNpn.c @@ -604,16 +604,8 @@ int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int fflush(stdout); return nNew; } -int Dau_RunNpn( Abc_TtHieMan_t * pMan, word * pTruth, int nVars, char * pCanonPerm ) -{ - typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag); - unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag); - unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres); - if ( nVars < 6 ) - return Abc_TtCanonicizeWrap( Abc_TtCanonicizeAda, NULL, pTruth, nVars, pCanonPerm, 99 ); - else - return Abc_TtCanonicizeWrap( Abc_TtCanonicizeAda, pMan, pTruth, nVars, pCanonPerm, 99 ); -} + + int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars0, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk ) { @@ -621,7 +613,7 @@ int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInp char Perm[16] = {0}; int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs ); //unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 ); - unsigned Phase = Dau_RunNpn( pMan, pCur, nInputs, Perm ); + unsigned Phase = Abc_TtCanonicizeWrap( Abc_TtCanonicizeAda, pMan, pCur, nVarsNew, Perm, 99 ); int nEntries = Vec_MemEntryNum(vTtMem); int Entry = Vec_MemHashInsert( vTtMem, pCur ); if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new @@ -639,7 +631,7 @@ void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fR { abctime clk = Abc_Clock(); int nWords = Abc_TtWordNum(nInputs); word nSteps = 0; - Abc_TtHieMan_t * pMan = Abc_TtHieManStart( nInputs, 5 ); + Abc_TtHieMan_t * pMan = Abc_TtHieManStart( nInputs, 5 ); Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 16 ); Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 ); int v, u, k, m, n, Entry, nNew, Limit[32] = {1, 2}; @@ -809,7 +801,7 @@ void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fR Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); //Dau_DumpFuncs( vTtMem, vNodSup, nVars, nNodeMax ); //Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n ); - Abc_TtHieManStop( pMan ); + Abc_TtHieManStop( pMan ); Vec_MemHashFree( vTtMem ); Vec_MemFreeP( &vTtMem ); Vec_IntFree( vNodSup ); -- cgit v1.2.3