diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abcNpn.c | 11 | ||||
-rw-r--r-- | src/bool/lucky/luckySimple.c | 119 | ||||
-rw-r--r-- | src/opt/dau/dauCanon.c | 119 |
3 files changed, 230 insertions, 19 deletions
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c index e667a074..8335edda 100644 --- a/src/base/abci/abcNpn.c +++ b/src/base/abci/abcNpn.c @@ -181,7 +181,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) char pCanonPerm[16]; unsigned uCanonPhase=0; abctime clk = Abc_Clock(); - int i, nClasses = -1; + int i; char * pAlgoName = NULL; if ( NpnType == 0 ) @@ -293,27 +293,28 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) } else if ( NpnType == 7 ) { - extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm ); + extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int fExact ); extern Abc_TtMan_t * Abc_TtManStart( int nVars ); extern void Abc_TtManStop( Abc_TtMan_t * p ); extern int Abc_TtManNumClasses( Abc_TtMan_t * p ); + int fExact = 0; Abc_TtMan_t * pMan = Abc_TtManStart( p->nVars ); for ( i = 0; i < p->nFuncs; i++ ) { if ( fVerbose ) printf( "%7d : ", i ); - uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm ); + uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm, fExact ); if ( fVerbose ) // Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" ); printf( "\n" ); } - nClasses = Abc_TtManNumClasses( pMan ); + // nClasses = Abc_TtManNumClasses( pMan ); Abc_TtManStop( pMan ); } else assert( 0 ); clk = Abc_Clock() - clk; - printf( "Classes =%9d ", nClasses == -1 ? Abc_TruthNpnCountUnique(p) : nClasses ); + printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) ); Abc_PrintTime( 1, "Time", clk ); } diff --git a/src/bool/lucky/luckySimple.c b/src/bool/lucky/luckySimple.c index f9128f3f..0660c0ad 100644 --- a/src/bool/lucky/luckySimple.c +++ b/src/bool/lucky/luckySimple.c @@ -148,6 +148,11 @@ static inline void minWord3(word* a, word* b, word* minimal, int nVars) if (memCompare(b, minimal, nVars) <= 0) Kit_TruthCopy_64bit( minimal, b, nVars ); } +static inline void minWord1(word* a, word* minimal, int nVars) +{ + if (memCompare(a, minimal, nVars) <= 0) + Kit_TruthCopy_64bit( minimal, a, nVars ); +} void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars) { int i,j=0; @@ -179,5 +184,119 @@ void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars) Kit_TruthCopy_64bit( x, minimal, nVars ); } +/** + * pGroups: we assume that the variables are merged into adjacent groups, + * the size of each group is stored in pGroups + * nGroups: the number of groups + * + * pis: we compute all permInfos from 0 to nVars (incl.) + */ +void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput) +{ + /* variables */ + int i, j, o, nn; + permInfo* pi; + + /* reorder groups and calculate group offsets */ + int offset[nGroups]; + o = 0; + j = 0; + + for ( i = 0; i < nGroups; ++i ) + { + offset[j] = o; + o += pGroups[j]; + ++j; + } + + if ( fFlipOutput ) + { + /* keep regular and inverted version of x */ + Kit_TruthCopy_64bit( pAux, x, nVars ); + Kit_TruthNot_64bit( x, nVars ); + + minWord(x, pAux, minimal, nVars); + } + else + { + Kit_TruthCopy_64bit( minimal, x, nVars ); + } + + /* iterate through all combinations of pGroups using mixed radix enumeration */ + nn = ( nGroups << 1 ) + 1; + int a[nn]; + int c[nn]; + int m[nn]; + + /* fill a and m arrays */ + m[0] = 2; + for ( i = 1; i <= nGroups; ++i ) { m[i] = pis[pGroups[i - 1]]->totalFlips + 1; } + for ( i = 1; i <= nGroups; ++i ) { m[nGroups + i] = pis[pGroups[i - 1]]->totalSwaps + 1; } + for ( i = 0; i < nn; ++i ) { a[i] = c[i] = 0; } + + while ( 1 ) + { + /* consider all flips */ + for ( i = 1; i <= nGroups; ++i ) + { + if ( !c[i] ) { continue; } + if ( !fFlipInput && pGroups[i - 1] == 1 ) { continue; } + + pi = pis[pGroups[i - 1]]; + j = a[i] == 0 ? 0 : pi->totalFlips - a[i]; + + Kit_TruthChangePhase_64bit(x, nVars, offset[i - 1] + pi->flipArray[j]); + if ( fFlipOutput ) + { + Kit_TruthChangePhase_64bit(pAux, nVars, offset[i - 1] + pi->flipArray[j]); + minWord3(x, pAux, minimal, nVars); + } + else + { + minWord1(x, minimal, nVars); + } + } + + /* consider all swaps */ + for ( i = 1; i <= nGroups; ++i ) + { + if ( !c[nGroups + i] ) { continue; } + if ( pGroups[i - 1] == 1 ) { continue; } + + pi = pis[pGroups[i - 1]]; + if ( a[nGroups + i] == pi->totalSwaps ) + { + j = 0; + } + else + { + j = pi->swapArray[pi->totalSwaps - a[nGroups + i] - 1]; + } + Kit_TruthSwapAdjacentVars_64bit(x, nVars, offset[i - 1] + j); + if ( fFlipOutput ) + { + Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, offset[i - 1] + j); + minWord3(x, pAux, minimal, nVars); + } + else + { + minWord1(x, minimal, nVars); + } + } + + /* update a's */ + memset(c, 0, sizeof(int) * nn); + j = nn - 1; + while ( a[j] == m[j] - 1 ) { c[j] = 1; a[j--] = 0; } + + /* done? */ + if ( j == 0 ) { break; } + + c[j] = 1; + a[j]++; + } + + Kit_TruthCopy_64bit( x, minimal, nVars ); +} ABC_NAMESPACE_IMPL_END diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c index 4fd8361c..c6ac8288 100644 --- a/src/opt/dau/dauCanon.c +++ b/src/opt/dau/dauCanon.c @@ -21,6 +21,7 @@ #include "dauInt.h" #include "misc/util/utilTruth.h" #include "misc/vec/vecMem.h" +#include "bool/lucky/lucky.h" ABC_NAMESPACE_IMPL_START @@ -1053,13 +1054,32 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars ) SeeAlso [] ***********************************************************************/ -#define TT_NUM_TABLES 4 +#define TT_NUM_TABLES 5 struct Abc_TtMan_t_ { Vec_Mem_t * vTtMem[TT_NUM_TABLES]; // truth table memory and hash tables + Vec_Int_t ** vRepres; // pointers to the representatives from the last hierarchical level }; +Vec_Int_t ** Abc_TtRepresStart() { + Vec_Int_t ** vRepres = ABC_ALLOC(Vec_Int_t *, TT_NUM_TABLES - 1); + int i; + // create a list of pointers for each level of the hierarchy + for (i = 0; i < (TT_NUM_TABLES - 1); i++) { + vRepres[i] = Vec_IntAlloc(1); + } + return vRepres; +} + +void Abc_TtRepresStop(Vec_Int_t ** vRepres) { + int i; + for (i = 0; i < (TT_NUM_TABLES - 1); i++) { + Vec_IntFree(vRepres[i]); + } + ABC_FREE( vRepres ); +} + Abc_TtMan_t * Abc_TtManStart( int nVars ) { Abc_TtMan_t * p = ABC_CALLOC( Abc_TtMan_t, 1 ); @@ -1069,6 +1089,7 @@ Abc_TtMan_t * Abc_TtManStart( int nVars ) p->vTtMem[i] = Vec_MemAlloc( nWords, 12 ); Vec_MemHashAlloc( p->vTtMem[i], 10000 ); } + p->vRepres = Abc_TtRepresStart(); return p; } void Abc_TtManStop( Abc_TtMan_t * p ) @@ -1079,6 +1100,7 @@ void Abc_TtManStop( Abc_TtMan_t * p ) Vec_MemHashFree( p->vTtMem[i] ); Vec_MemFreeP( &p->vTtMem[i] ); } + Abc_TtRepresStop(p->vRepres); ABC_FREE( p ); } int Abc_TtManNumClasses( Abc_TtMan_t * p ) @@ -1086,7 +1108,7 @@ int Abc_TtManNumClasses( Abc_TtMan_t * p ) return Vec_MemEntryNum( p->vTtMem[TT_NUM_TABLES-1] ); } -unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm ) +unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact ) { int fNaive = 1; int pStore[17]; @@ -1095,6 +1117,9 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha int nOnes, nWords = Abc_TtWordNum( nVars ); int i, k, truthId; int * pSpot; + int vTruthId[TT_NUM_TABLES-1]; + int fLevelFound; + word * pRepTruth; assert( nVars <= 16 ); Abc_TtCopy( pTruth, pTruthInit, nWords, 0 ); @@ -1112,9 +1137,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha } // check cache pSpot = Vec_MemHashLookup( p->vTtMem[0], pTruth ); - if ( *pSpot != -1 ) - return 0; - truthId = Vec_MemHashInsert( p->vTtMem[0], pTruth ); + if ( *pSpot != -1 ) { + fLevelFound = 0; + goto end_repres; + } + vTruthId[0] = Vec_MemHashInsert( p->vTtMem[0], pTruth ); // normalize phase Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); @@ -1129,9 +1156,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha } // check cache pSpot = Vec_MemHashLookup( p->vTtMem[1], pTruth ); - if ( *pSpot != -1 ) - return 0; - truthId = Vec_MemHashInsert( p->vTtMem[1], pTruth ); + if ( *pSpot != -1 ) { + fLevelFound = 1; + goto end_repres; + } + vTruthId[1] = Vec_MemHashInsert( p->vTtMem[1], pTruth ); // normalize permutation { @@ -1156,9 +1185,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha } // check cache pSpot = Vec_MemHashLookup( p->vTtMem[2], pTruth ); - if ( *pSpot != -1 ) - return 0; - truthId = Vec_MemHashInsert( p->vTtMem[2], pTruth ); + if ( *pSpot != -1 ) { + fLevelFound = 2; + goto end_repres; + } + vTruthId[2] = Vec_MemHashInsert( p->vTtMem[2], pTruth ); // iterate TT permutations for tied variables for ( k = 0; k < 5; k++ ) @@ -1178,9 +1209,69 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha } // check cache pSpot = Vec_MemHashLookup( p->vTtMem[3], pTruth ); - if ( *pSpot != -1 ) - return 0; - truthId = Vec_MemHashInsert( p->vTtMem[3], pTruth ); + if ( *pSpot != -1 ) { + fLevelFound = 3; + goto end_repres; + } + vTruthId[3] = Vec_MemHashInsert( p->vTtMem[3], pTruth ); + + // perform exact NPN using groups + if ( fExact ) { + extern void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput); + word pAuxWord[1024], pAuxWord1[1024]; + int pGroups[nVars]; + int nGroups = 0; + // get groups + pGroups[0] = 0; + for (i = 0; i < nVars - 1; i++) { + if (pStore[i] == pStore[i + 1]) { + pGroups[nGroups]++; + } else { + pGroups[nGroups]++; + nGroups++; + pGroups[nGroups] = 0; + } + } + pGroups[nGroups]++; + nGroups++; + + // compute permInfo from 0 to nVars (incl.) + permInfo * pis[nVars+1]; + for (i = 0; i <= nVars; i++) { + pis[i] = setPermInfoPtr(i); + } + + // do the exact matching + if (nOnes == nWords * 32) /* balanced output */ + simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 1, 1); + else if (pStore[0] != pStore[1] && pStore[0] == (nOnes - pStore[0])) /* balanced singleton input */ + simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 1); + else + simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 0); + + // cleanup + for (i = 0; i <= nVars; i++) { + freePermInfoPtr(pis[i]); + } + } + // check cache + pSpot = Vec_MemHashLookup( p->vTtMem[4], pTruth ); + fLevelFound = 4; + if ( *pSpot != -1 ) { + goto end_repres; + } + *pSpot = Vec_MemHashInsert( p->vTtMem[4], pTruth ); + +end_repres: + // return the class representative + if(fLevelFound < (TT_NUM_TABLES - 1)) + truthId = Vec_IntEntry(p->vRepres[fLevelFound], *pSpot); + else truthId = *pSpot; + for(i = 0; i < fLevelFound; i++) + Vec_IntSetEntry(p->vRepres[i], vTruthId[i], truthId); + pRepTruth = Vec_MemReadEntry(p->vTtMem[TT_NUM_TABLES-1], truthId); + Abc_TtCopy( pTruthInit, pRepTruth, nWords, 0 ); + return 0; } |