summaryrefslogtreecommitdiff
path: root/src/opt/dau
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/dau')
-rw-r--r--src/opt/dau/dau.h7
-rw-r--r--src/opt/dau/dauCanon.c1475
-rw-r--r--src/opt/dau/dauGia.c4
-rw-r--r--src/opt/dau/dauNpn.c707
-rw-r--r--src/opt/dau/dauNpn2.c507
-rw-r--r--src/opt/dau/module.make1
6 files changed, 1868 insertions, 833 deletions
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 260d8c7..82e9b83 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 ///
@@ -80,6 +81,12 @@ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPe
extern unsigned Abc_TtCanonicizePerm( word * pTruth, int nVars, char * pCanonPerm );
extern unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars );
extern int Abc_TtCountOnesInCofsSimple( word * pTruth, int nVars, int * pStore );
+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 918c7ce..357da50 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,83 +1165,92 @@ 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;
assert( nVars <= 16 );
- Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
+ // handle constant
+ if ( nVars == 0 )
+ {
+ Abc_TtClear( pTruthInit, nWords );
+ return 0;
+ }
+
+ //Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
for ( i = 0; i < nVars; i++ )
pCanonPerm[i] = i;
@@ -1258,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
{
@@ -1282,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++ )
@@ -1301,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 ) {
@@ -1343,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;
}
@@ -1362,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)
@@ -1402,59 +1422,58 @@ 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
}
@@ -1472,44 +1491,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
}
@@ -1527,84 +1546,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*************************************************************
@@ -1623,33 +1642,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*************************************************************
@@ -1658,7 +1677,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 []
@@ -1668,53 +1687,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*************************************************************
@@ -1731,135 +1750,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);
}
@@ -1876,130 +1895,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*************************************************************
@@ -2016,194 +2035,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/dauGia.c b/src/opt/dau/dauGia.c
index 424ec53..eebfa9a 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -449,6 +449,10 @@ int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t *
Abc_TtCopy( pTruthCopy, pTruth, Abc_TtWordNum(Vec_IntSize(vLeaves)), 0 );
m_Calls++;
assert( Vec_IntSize(vLeaves) <= DAU_DSD_MAX_VAR );
+ if ( Vec_IntSize(vLeaves) == 0 )
+ return (int)(pTruth[0] & 1);
+ if ( Vec_IntSize(vLeaves) == 1 )
+ return Abc_LitNotCond( Vec_IntEntry(vLeaves, 0), (int)(pTruth[0] & 1) );
// collect delay information
if ( fDelayBalance && fUseMuxes )
{
diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c
index d8c1911..b57ade6 100644
--- a/src/opt/dau/dauNpn.c
+++ b/src/opt/dau/dauNpn.c
@@ -21,6 +21,7 @@
#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
+#include "bool/lucky/lucky.h"
ABC_NAMESPACE_IMPL_START
@@ -122,6 +123,7 @@ void Dau_TruthEnum()
{
FILE * pFile = fopen( pFileName, "wb" );
int RetValue = fwrite( pTable, 8, nSizeW, pFile );
+ RetValue = 0;
fclose( pFile );
ABC_FREE( pTable );
}
@@ -144,31 +146,42 @@ unsigned * Dau_ReadFile( char * pFileName, int nSizeW )
abctime clk = Abc_Clock();
FILE * pFile = fopen( pFileName, "rb" );
unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW);
- int RetValue = fread( p, sizeof(word), nSizeW, pFile );
- fclose( pFile );
+ int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
+ RetValue = 0;
+ if ( pFile )
+ {
+ printf( "Finished reading file \"%s\".\n", pFileName );
+ fclose( pFile );
+ }
+ else
+ printf( "Cannot open input file \"%s\".\n", pFileName );
Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
return p;
}
-void Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns )
+int Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns, Vec_Int_t * vNpns_ )
{
int Digit = (1 << nVars)-1;
word tMask = Abc_Tt6Mask( 1 << nVars );
word tNorm = (tCur >> Digit) & 1 ? ~tCur : tCur;
unsigned t = (unsigned)(tNorm & tMask);
- unsigned tRep = pTable[t];
- unsigned tRep2 = pTable[tRep & 0x7FFFFFFF];
+ unsigned tRep = pTable[t] & 0x7FFFFFFF;
+ unsigned tRep2 = pTable[tRep];
assert( ((tNorm >> Digit) & 1) == 0 );
if ( (tRep2 >> 31) == 0 ) // first time
{
Vec_IntPush( vNpns, tRep2 );
- pTable[tRep & 0x7FFFFFFF] = tRep2 | (1 << 31);
+ if ( Abc_TtSupportSize(&tCur, nVars) < nVars )
+ Vec_IntPush( vNpns_, tRep2 );
+ pTable[tRep] = tRep2 | (1 << 31);
+ return tRep2;
}
-
+ return 0;
}
void Dau_NetworkEnum()
{
abctime clk = Abc_Clock();
int Limit = 2;
+ int UseTwo = 0;
#ifdef USE4VARS
int nVars = 4;
int nSizeW = 1 << 14;
@@ -178,146 +191,626 @@ void Dau_NetworkEnum()
int nSizeW = 1 << 30;
char * pFileName = "tableW30.data";
#endif
- unsigned * pTable = Dau_ReadFile( pFileName, nSizeW );
- Vec_Int_t * vNpns = Vec_IntAlloc( 1000 );
- int i, v, g, k, m, Entry, Count = 1, iPrev = 0, iLast = 1;
+ unsigned * pTable = Dau_ReadFile( pFileName, nSizeW );
+ Vec_Wec_t * vNpns = Vec_WecStart( 32 );
+ Vec_Wec_t * vNpns_ = Vec_WecStart( 32 );
+ int i, v, u, g, k, m, n, Res, Entry;
unsigned Inv = (unsigned)Abc_Tt6Mask(1 << (nVars-1));
+ // create constant function and buffer/inverter function
pTable[0] |= (1 << 31);
pTable[Inv] |= (1 << 31);
- Vec_IntPushTwo( vNpns, 0, Inv );
- Vec_IntForEachEntryStart( vNpns, Entry, i, 1 )
+ Vec_IntPushTwo( Vec_WecEntry(vNpns, 0), 0, Inv );
+ Vec_IntPushTwo( Vec_WecEntry(vNpns_, 0), 0, Inv );
+ printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
+ 0, Vec_IntSize(Vec_WecEntry(vNpns, 0)), Vec_WecSizeSize(vNpns),
+ Vec_IntSize(Vec_WecEntry(vNpns_, 0)), Vec_WecSizeSize(vNpns_) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ // numerate other functions based on how many nodes they have
+ for ( n = 1; n < 32; n++ )
{
- word uTruth = (((word)Entry) << 32) | (word)Entry;
- int nSupp = Abc_TtSupportSize( &uTruth, nVars );
- //printf( "Exploring function %4d with %d vars: ", i, nSupp );
- //printf( " %04x\n", (int)uTruth );
- //Dau_DsdPrintFromTruth( &uTruth, 4 );
- for ( v = 0; v < nSupp; v++ )
+ Vec_Int_t * vFuncsN2 = n > 1 ? Vec_WecEntry( vNpns, n-2 ) : NULL;
+ Vec_Int_t * vFuncsN1 = Vec_WecEntry( vNpns, n-1 );
+ Vec_Int_t * vFuncsN = Vec_WecEntry( vNpns, n );
+ Vec_Int_t * vFuncsN_ = Vec_WecEntry( vNpns_,n );
+ Vec_IntForEachEntry( vFuncsN1, Entry, i )
{
- word tGate, tCur;
- word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
- word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
- for ( g = 0; g < Limit; g++ )
+ word uTruth = (((word)Entry) << 32) | (word)Entry;
+ int nSupp = Abc_TtSupportSize( &uTruth, nVars );
+ assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
+ //printf( "Exploring function %4d with %d vars: ", i, nSupp );
+ //printf( " %04x\n", (int)uTruth );
+ //Dau_DsdPrintFromTruth( &uTruth, 4 );
+ for ( v = 0; v < nSupp; v++ )
{
- if ( nSupp < nVars )
+ word tGate, tCur;
+ word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
+ word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
+ for ( g = 0; g < Limit; g++ )
{
- if ( g == 0 )
+ if ( nSupp < nVars )
{
- tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ if ( g == 0 )
+ {
+ tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ }
+ else
+ {
+ tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ }
+ }
+ }
+ for ( g = 0; g < Limit; g++ )
+ {
+ // add one cross bar
+ for ( k = 0; k < nSupp; k++ ) if ( k != v )
+ {
+ if ( g == 0 )
+ {
+ tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ }
+ else
+ {
+ tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ }
}
- else
+ }
+ for ( g = 0; g < Limit; g++ )
+ {
+ // add two cross bars
+ for ( k = 0; k < nSupp; k++ ) if ( k != v )
+ for ( m = k+1; m < nSupp; m++ ) if ( m != v )
{
- tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ if ( g == 0 )
+ {
+ tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ }
+ else
+ {
+ tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ }
}
}
}
- for ( g = 0; g < Limit; g++ )
+ }
+ if ( UseTwo && vFuncsN2 )
+ Vec_IntForEachEntry( vFuncsN2, Entry, i )
+ {
+ word uTruth = (((word)Entry) << 32) | (word)Entry;
+ int nSupp = Abc_TtSupportSize( &uTruth, nVars );
+ assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
+ //printf( "Exploring function %4d with %d vars: ", i, nSupp );
+ //printf( " %04x\n", (int)uTruth );
+ //Dau_DsdPrintFromTruth( &uTruth, 4 );
+ for ( v = 0; v < nSupp; v++ )
+// for ( u = v+1; u < nSupp; u++ ) if ( u != v )
+ for ( u = 0; u < nSupp; u++ ) if ( u != v )
{
+ word tGate1, tGate2, tCur;
+ word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
+ word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
+
+ word Cof00 = Abc_Tt6Cofactor0( Cof0, nVars-1-u );
+ word Cof01 = Abc_Tt6Cofactor1( Cof0, nVars-1-u );
+ word Cof10 = Abc_Tt6Cofactor0( Cof1, nVars-1-u );
+ word Cof11 = Abc_Tt6Cofactor1( Cof1, nVars-1-u );
+
+ tGate1 = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-u];
+ tGate2 = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-u];
+
+ Cof0 = (tGate2 & Cof00) | (~tGate2 & Cof01);
+ Cof1 = (tGate2 & Cof10) | (~tGate2 & Cof11);
+
+ tCur = (tGate1 & Cof1) | (~tGate1 & Cof0);
+ Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ if ( Res )
+ printf( "Found function %d\n", Res );
+
+ tCur = (tGate1 & Cof0) | (~tGate1 & Cof1);
+ Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+ if ( Res )
+ printf( "Found function %d\n", Res );
+ }
+ }
+ printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
+ n, Vec_IntSize(vFuncsN), Vec_WecSizeSize(vNpns), Vec_IntSize(vFuncsN_), Vec_WecSizeSize(vNpns_) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ fflush(stdout);
+ if ( Vec_IntSize(vFuncsN) == 0 )
+ break;
+ }
+// printf( "Functions with 7 nodes:\n" );
+// Vec_IntForEachEntry( Vec_WecEntry(vNpns_,7), Entry, i )
+// printf( "%04x ", Entry );
+// printf( "\n" );
+
+ Vec_WecFree( vNpns );
+ Vec_WecFree( vNpns_ );
+ ABC_FREE( pTable );
+ Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+ fflush(stdout);
+}
+void Dau_NetworkEnumTest()
+{
+ //Dau_TruthEnum();
+ Dau_NetworkEnum();
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of symmetric pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dau_CountSymms( word t, int nVars )
+{
+ word Cof0, Cof1;
+ int i, j, nPairs = 0;
+ for ( i = 0; i < nVars; i++ )
+ for ( j = i+1; j < nVars; j++ )
+ nPairs += Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1);
+ return nPairs;
+}
+int Dau_CountSymms2( word t, int nVars )
+{
+ word Cof0, Cof1;
+ int i, j, SymVars = 0;
+ for ( i = 0; i < nVars; i++ )
+ for ( j = i+1; j < nVars; j++ )
+ if ( Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1) )
+ SymVars |= (1 << j);
+ return SymVars;
+}
+int Dau_CountCompl1( word t, int v, int nVars )
+{
+ word tNew = Abc_Tt6Flip(t, v);
+ int k;
+ if ( tNew == ~t )
+ return 1;
+ for ( k = 0; k < nVars; k++ ) if ( k != v )
+ if ( tNew == Abc_Tt6Flip(t, k) )
+ return 1;
+ return 0;
+}
+int Dau_CountCompl( word t, int nVars )
+{
+ int i, nPairs = 0;
+ for ( i = 0; i < nVars; i++ )
+ nPairs += Dau_CountCompl1(t, i, nVars);
+ return nPairs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs exact canonicization of semi-canonical classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Wrd_t * Dau_ExactNpnForClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs )
+{
+ Vec_Wrd_t * vCanons = Vec_WrdStart( Vec_IntSize(vNodSup) );
+ word pAuxWord[1024], pAuxWord1[1024];
+ word uTruth; int i, Entry;
+ permInfo * pi = setPermInfoPtr(nVars);
+ Vec_IntForEachEntry( vNodSup, Entry, i )
+ {
+ if ( (Entry & 0xF) > nVars )
+ continue;
+ uTruth = *Vec_MemReadEntry( vTtMem, i );
+ simpleMinimal(&uTruth, pAuxWord, pAuxWord1, pi, nVars);
+ Vec_WrdWriteEntry( vCanons, i, uTruth );
+ }
+ freePermInfoPtr(pi);
+ return vCanons;
+}
+void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs, int nNodesMax )
+{
+ abctime clk = Abc_Clock(); int n, nTotal = 0;
+ Vec_Wrd_t * vCanons = Dau_ExactNpnForClasses( vTtMem, vNodSup, nVars, nInputs );
+ Vec_Mem_t * vTtMem2 = Vec_MemAlloc( Vec_MemEntrySize(vTtMem), 10 );
+ Vec_MemHashAlloc( vTtMem2, 1<<10 );
+ Abc_PrintTime( 1, "Exact NPN computation time", Abc_Clock() - clk );
+ printf( "Final results:\n" );
+ for ( n = 0; n <= nNodesMax; n++ )
+ {
+ int i, Entry, Entry2, nEntries2, Counter = 0, Counter2 = 0;
+ Vec_IntForEachEntry( vNodSup, Entry, i )
+ {
+ if ( (Entry & 0xF) > nVars || (Entry >> 16) != n )
+ continue;
+ Counter++;
+ nEntries2 = Vec_MemEntryNum(vTtMem2);
+ Entry2 = Vec_MemHashInsert( vTtMem2, Vec_WrdEntryP(vCanons, i) );
+ if ( nEntries2 == Vec_MemEntryNum(vTtMem2) ) // found in the table - not new
+ continue;
+ Counter2++;
+ }
+ nTotal += Counter2;
+ printf( "Nodes = %2d. ", n );
+ printf( "Semi-canonical = %8d. ", Counter );
+ printf( "Canonical = %8d. ", Counter2 );
+ printf( "Total = %8d.", nTotal );
+ printf( "\n" );
+ }
+ Vec_MemHashFree( vTtMem2 );
+ Vec_MemFreeP( &vTtMem2 );
+ Vec_WrdFree( vCanons );
+ fflush(stdout);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Saving hash tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_TablesSave( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
+{
+ FILE * pFile;
+ char FileName[100];
+ int i, nWords = Abc_TtWordNum(nInputs);
+ // NPN classes
+ sprintf( FileName, "npn%d%d.ttd", nInputs, nVars );
+ pFile = fopen( FileName, "wb" );
+ for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
+ fwrite( Vec_MemReadEntry(vTtMem, i), 8, nWords, pFile );
+ fwrite( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile );
+ fclose( pFile );
+// printf( "Dumped files with %10d classes after exploring %10d frontiers.\n",
+// Vec_IntSize(vNodSup), nFronts );
+ printf( "Dumped file \"%s\" with %10d classes after exploring %10d frontiers. ",
+ FileName, Vec_IntSize(vNodSup), nFronts );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ fflush(stdout);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dump functions by the number of nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_DumpFuncs( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nMax )
+{
+ FILE * pFile[20];
+ int Counters[20] = {0};
+ int n, i;
+ assert( nVars == 4 || nVars == 5 );
+ for ( n = 0; n <= nMax; n++ )
+ {
+ char FileName[100];
+ sprintf( FileName, "func%d_min%d.tt", nVars, n );
+ pFile[n] = fopen( FileName, "wb" );
+ }
+ for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
+ {
+ word * pTruth = Vec_MemReadEntry( vTtMem, i );
+ int NodSup = Vec_IntEntry( vNodSup, i );
+ if ( (NodSup & 0xF) != nVars )
+ continue;
+ Counters[NodSup >> 16]++;
+ if ( nVars == 4 )
+ fprintf( pFile[NodSup >> 16], "%04x\n", (int)(0xFFFF & pTruth[0]) );
+ else if ( nVars == 5 )
+ fprintf( pFile[NodSup >> 16], "%08x\n", (int)(0xFFFFFFFF & pTruth[0]) );
+ }
+ for ( n = 0; n <= nMax; n++ )
+ {
+ printf( "Dumped %8d %d-node %d-input functions into file.\n", Counters[n], n, nVars );
+ fclose( pFile[n] );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Function enumeration.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dau_CountFuncs( Vec_Int_t * vNodSup, int iStart, int iStop, int nVars )
+{
+ int i, Entry, Count = 0;
+ Vec_IntForEachEntryStartStop( vNodSup, Entry, i, iStart, iStop )
+ Count += ((Entry & 0xF) <= nVars);
+ return Count;
+}
+int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int iStart, int iStop, word nSteps, int Count2, abctime clk )
+{
+ int nNew;
+ printf("N =%2d | ", nNodes );
+ printf("C =%12.0f ", (double)(iword)nSteps );
+ printf("New%d =%10d ", nInputs, iStop-iStart );
+ printf("All%d =%10d | ", nInputs, iStop );
+ printf("New%d =%8d ", nVars, nNew = Dau_CountFuncs(vNodSup, iStart, iStop, nVars) );
+ printf("All%d =%8d ", nVars, Dau_CountFuncs(vNodSup, 0, iStop, nVars) );
+ printf("Two =%6d ", Count2 );
+ //Abc_PrintTime( 1, "T", Abc_Clock() - clk );
+ Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
+ fflush(stdout);
+ return nNew;
+}
+
+
+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 )
+{
+ int DumpDelta = 1000000;
+ char Perm[16] = {0};
+ int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
+ //unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 );
+ 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
+ return 0;
+ Entry = 0;
+ Phase = 0;
+ // this is a new class
+ Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
+ assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
+ if ( Vec_IntSize(vNodSup) % DumpDelta == 0 )
+ Dau_TablesSave( nInputs, nVars0, vTtMem, vNodSup, nFronts, clk );
+ return 1;
+}
+void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ int nWords = Abc_TtWordNum(nInputs); word nSteps = 0;
+ 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};
+ word Truth[4] = {0};
+ assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 );
+ Vec_MemHashAlloc( vTtMem, 1<<16 );
+ // add constant 0
+ Vec_MemHashInsert( vTtMem, Truth );
+ Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0
+ // add buffer/inverter
+ Abc_TtIthVar( Truth, 0, nInputs );
+ Abc_TtNot( Truth, nWords );
+ Vec_MemHashInsert( vTtMem, Truth );
+ Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1
+ Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, nSteps, 0, clk );
+ // numerate other functions based on how many nodes they have
+ for ( n = 1; n <= nNodeMax; n++ )
+ {
+ int Count2 = 0;
+ int fExpand = !(fReduce && n == nNodeMax);
+ for ( Entry = Limit[n-1]; Entry < Limit[n]; Entry++ )
+ {
+ word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
+ int NodSup = Vec_IntEntry(vNodSup, Entry);
+ int nSupp = 0xF & NodSup;
+ int SymVars = Dau_CountSymms2( pTruth[0], nSupp );
+ assert( n-1 == (NodSup >> 16) );
+ assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
+ //printf( "Exploring function %4d with %d vars: ", i, nSupp );
+ //printf( " %04x\n", (int)uTruth );
+ //Dau_DsdPrintFromTruth( &uTruth, 4 );
+ for ( v = 0; v < nSupp; v++ ) if ( (SymVars & (1 << v)) == 0 )
+ {
+ word tGate, tCur;
+ word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
+ word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
+ // add one extra variable to support
+ if ( nSupp < nInputs && fExpand )
+ {
+ tGate = s_Truths6[v] & s_Truths6[nSupp];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
+
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
+
+
+ tGate = s_Truths6[v] ^ s_Truths6[nSupp];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
+
+ nSteps += 3;
+ }
// add one cross bar
- for ( k = 0; k < nSupp; k++ ) if ( k != v )
+ if ( fExpand )
+ for ( k = 0; k < nSupp; k++ ) if ( k != v && ((SymVars & (1 << k)) == 0 || k == v+1) )
{
- if ( g == 0 )
- {
- tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tGate = s_Truths6[v] & s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tGate = s_Truths6[v] & ~s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
- }
- else
- {
- tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
- }
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
+
+
+ tGate = s_Truths6[v] ^ s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
+
+ nSteps += 5;
}
- }
- for ( g = 0; g < Limit; g++ )
- {
// add two cross bars
- for ( k = 0; k < nSupp; k++ ) if ( k != v )
- for ( m = k+1; m < nSupp; m++ ) if ( m != v )
+ for ( k = 0; k < nSupp; k++ ) if ( k != v )//&& ((SymVars & (1 << k)) == 0) )
+ for ( m = k+1; m < nSupp; m++ ) if ( m != v )//&& ((SymVars & (1 << m)) == 0 || m == k+1) )
{
- if ( g == 0 )
- {
- tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tGate = s_Truths6[m] & s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tGate = s_Truths6[m] & ~s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tGate = ~s_Truths6[m] & s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
+ tGate = ~s_Truths6[m] & ~s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
- tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
- }
- else
- {
- tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
- tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_AddFunction( tCur, nVars, pTable, vNpns );
- }
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
+
+
+ tGate = s_Truths6[m] ^ s_Truths6[k];
+ tCur = (tGate & Cof1) | (~tGate & Cof0);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
+
+ tGate = s_Truths6[m] ^ s_Truths6[k];
+ tCur = (tGate & Cof0) | (~tGate & Cof1);
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
+
+ nSteps += 10;
}
}
- }
- if ( i == iLast )
+ }
+ if ( fUseTwo && n > 2 && fExpand )
+ for ( Entry = Limit[n-2]; Entry < Limit[n-1]; Entry++ )
{
- //printf("Finished %d nodes with %d functions.\n", Count++, Vec_IntSize(vNpns) );
- iPrev = iLast;
- iLast = Vec_IntSize(vNpns)-1;
- printf("Finished %2d nodes with %6d functions out of %6d. ", Count++, iLast - iPrev, Vec_IntSize(vNpns) );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
- fflush(stdout);
+ word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
+ int NodSup = Vec_IntEntry(vNodSup, Entry);
+ int nSupp = 0xF & NodSup; int g1, g2;
+ assert( n-2 == (NodSup >> 16) );
+ assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
+ for ( v = 0; v < nSupp; v++ )
+ for ( u = 0; u < nSupp; u++ ) if ( u != v )
+ {
+ word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
+ word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
+
+ word Cof00 = Abc_Tt6Cofactor0( Cof0, u );
+ word Cof01 = Abc_Tt6Cofactor1( Cof0, u );
+ word Cof10 = Abc_Tt6Cofactor0( Cof1, u );
+ word Cof11 = Abc_Tt6Cofactor1( Cof1, u );
+
+ word tGates[5], tCur;
+ tGates[0] = s_Truths6[v] & s_Truths6[u];
+ tGates[1] = s_Truths6[v] & ~s_Truths6[u];
+ tGates[2] = ~s_Truths6[v] & s_Truths6[u];
+ tGates[3] = s_Truths6[v] | s_Truths6[u];
+ tGates[4] = s_Truths6[v] ^ s_Truths6[u];
+
+ for ( g1 = 0; g1 < 5; g1++ )
+ for ( g2 = g1+1; g2 < 5; g2++ )
+ {
+ Cof0 = (tGates[g1] & Cof01) | (~tGates[g1] & Cof00);
+ Cof1 = (tGates[g1] & Cof11) | (~tGates[g1] & Cof10);
+
+ tCur = (tGates[g2] & Cof1) | (~tGates[g2] & Cof0);
+ Count2 += Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
+ }
+ }
}
+ Limit[n+1] = Vec_IntSize(vNodSup);
+ nNew = Dau_PrintStats( n, nInputs, nVars, vNodSup, Limit[n], Limit[n+1], nSteps, Count2, clk );
+ if ( nNew == 0 )
+ break;
}
- Vec_IntFree( vNpns );
- ABC_FREE( pTable );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Dau_TablesSave( nInputs, nVars, vTtMem, vNodSup, Vec_IntSize(vNodSup), clk );
+ Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+ //Dau_DumpFuncs( vTtMem, vNodSup, nVars, nNodeMax );
+ //Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n );
+ Abc_TtHieManStop( pMan );
+ Vec_MemHashFree( vTtMem );
+ Vec_MemFreeP( &vTtMem );
+ Vec_IntFree( vNodSup );
fflush(stdout);
}
-void Dau_NetworkEnumTest()
-{
- //Dau_TruthEnum();
- Dau_NetworkEnum();
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-
ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/dau/dauNpn2.c b/src/opt/dau/dauNpn2.c
new file mode 100644
index 0000000..bca65ad
--- /dev/null
+++ b/src/opt/dau/dauNpn2.c
@@ -0,0 +1,507 @@
+/**CFile****************************************************************
+
+ FileName [dau.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware unmapping.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: dau.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dauInt.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Dtt_Man_t_ Dtt_Man_t;
+struct Dtt_Man_t_
+{
+ int nVars; // variable number
+ int nPerms; // number of permutations
+ int nComps; // number of complementations
+ int * pPerms; // permutations
+ int * pComps; // complementations
+ word * pPres; // function marks
+ Vec_Int_t * vFanins; // node fanins
+ Vec_Int_t * vTruths; // node truth tables
+ Vec_Int_t * vConfigs; // configurations
+ Vec_Int_t * vClasses; // node NPN classes
+ Vec_Int_t * vTruthNpns; // truth tables of the classes
+ Vec_Wec_t * vFunNodes; // nodes by NPN class
+ Vec_Int_t * vTemp; // temporary
+ Vec_Int_t * vTemp2; // temporary
+ unsigned FunMask; // function mask
+ unsigned CmpMask; // function mask
+ unsigned BinMask; // hash mask
+ unsigned * pBins; // hash bins
+ Vec_Int_t * vUsedBins; // used bins
+ int Counts[32]; // node counts
+ int nClasses; // count of classes
+ unsigned * pTable; // mapping of funcs into their classes
+ int * pNodes; // the number of nodes in min-node network
+ int * pTimes; // the number of different min-node networks
+ char * pVisited; // visited classes
+ Vec_Int_t * vVisited; // the number of visited classes
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Dau_ReadFile2( char * pFileName, int nSizeW )
+{
+ abctime clk = Abc_Clock();
+ FILE * pFile = fopen( pFileName, "rb" );
+ unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW);
+ int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
+ RetValue = 0;
+ if ( pFile )
+ {
+ printf( "Finished reading file \"%s\".\n", pFileName );
+ fclose( pFile );
+ }
+ else
+ printf( "Cannot open input file \"%s\".\n", pFileName );
+ Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
+ return p;
+}
+void Dtt_ManRenum( int nVars, unsigned * pTable, int * pnClasses )
+{
+ unsigned i, Limit = 1 << ((1 << nVars)-1), Count = 0;
+ for ( i = 0; i < Limit; i++ )
+ if ( pTable[i] == i )
+ pTable[i] = Count++;
+ else
+ {
+ assert( pTable[i] < i );
+ pTable[i] = pTable[pTable[i]];
+ }
+ printf( "The total number of NPN classes = %d.\n", Count );
+ *pnClasses = Count;
+}
+unsigned * Dtt_ManLoadClasses( int nVars, int * pnClasses )
+{
+ unsigned * pTable = NULL;
+ if ( nVars == 4 )
+ pTable = Dau_ReadFile2( "tableW14.data", 1 << 14 );
+ else if ( nVars == 5 )
+ pTable = Dau_ReadFile2( "tableW30.data", 1 << 30 );
+ else assert( 0 );
+ Dtt_ManRenum( nVars, pTable, pnClasses );
+ return pTable;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dtt_ManAddVisited( Dtt_Man_t * p, unsigned Truth2, int n )
+{
+ unsigned Truth = Truth2 & p->CmpMask ? ~Truth2 : Truth2;
+ unsigned Class = p->pTable[Truth & p->FunMask];
+ assert( Class < (unsigned)p->nClasses );
+ if ( p->pNodes[Class] < n )
+ return;
+ assert( p->pNodes[Class] == n );
+ if ( p->pVisited[Class] )
+ return;
+ p->pVisited[Class] = 1;
+ Vec_IntPush( p->vVisited, Class );
+}
+void Dtt_ManProcessVisited( Dtt_Man_t * p )
+{
+ int i, Class;
+ Vec_IntForEachEntry( p->vVisited, Class, i )
+ {
+ assert( p->pVisited[Class] );
+ p->pVisited[Class] = 0;
+ p->pTimes[Class]++;
+ }
+ Vec_IntClear( p->vVisited );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dtt_Man_t * Dtt_ManAlloc( int nVars, int fMulti )
+{
+ Dtt_Man_t * p = ABC_CALLOC( Dtt_Man_t, 1 );
+ p->nVars = nVars;
+ p->nPerms = Extra_Factorial( nVars );
+ p->nComps = 1 << nVars;
+ p->pPerms = Extra_PermSchedule( nVars );
+ p->pComps = Extra_GreyCodeSchedule( nVars );
+ p->pPres = ABC_CALLOC( word, 1 << (p->nComps - 7) );
+ p->vFanins = Vec_IntAlloc( 2*617000 );
+ p->vTruths = Vec_IntAlloc( 617000 );
+ p->vConfigs = Vec_IntAlloc( 617000 );
+ p->vClasses = Vec_IntAlloc( 617000 );
+ p->vTruthNpns = Vec_IntAlloc( 617000 );
+ p->vFunNodes = Vec_WecStart( 16 );
+ p->vTemp = Vec_IntAlloc( 4000 );
+ p->vTemp2 = Vec_IntAlloc( 4000 );
+ p->FunMask = nVars == 5 ? ~0 : (nVars == 4 ? 0xFFFF : 0xFF);
+ p->CmpMask = nVars == 5 ? 1 << 31 : (nVars == 4 ? 1 << 15 : 1 << 7);
+ p->BinMask = 0x3FFF;
+ p->pBins = ABC_FALLOC( unsigned, p->BinMask + 1 );
+ p->vUsedBins = Vec_IntAlloc( 4000 );
+ if ( !fMulti ) return p;
+ p->pTable = Dtt_ManLoadClasses( p->nVars, &p->nClasses );
+ p->pNodes = ABC_CALLOC( int, p->nClasses );
+ p->pTimes = ABC_CALLOC( int, p->nClasses );
+ p->pVisited = ABC_CALLOC( char, p->nClasses );
+ p->vVisited = Vec_IntAlloc( 1000 );
+ return p;
+}
+void Dtt_ManFree( Dtt_Man_t * p )
+{
+ Vec_IntFreeP( &p->vVisited );
+ ABC_FREE( p->pTable );
+ ABC_FREE( p->pNodes );
+ ABC_FREE( p->pTimes );
+ ABC_FREE( p->pVisited );
+ Vec_IntFreeP( &p->vFanins );
+ Vec_IntFreeP( &p->vTruths );
+ Vec_IntFreeP( &p->vConfigs );
+ Vec_IntFreeP( &p->vClasses );
+ Vec_IntFreeP( &p->vTruthNpns );
+ Vec_WecFreeP( &p->vFunNodes );
+ Vec_IntFreeP( &p->vTemp );
+ Vec_IntFreeP( &p->vTemp2 );
+ Vec_IntFreeP( &p->vUsedBins );
+ ABC_FREE( p->pPerms );
+ ABC_FREE( p->pComps );
+ ABC_FREE( p->pPres );
+ ABC_FREE( p->pBins );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect representatives of the same class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Dtt_ManHashKey( Dtt_Man_t * p, unsigned Truth )
+{
+ static unsigned s_P[4] = { 1699, 5147, 7103, 8147 };
+ unsigned char * pD = (unsigned char*)&Truth;
+ return pD[0] * s_P[0] + pD[1] * s_P[1] + pD[2] * s_P[2] + pD[3] * s_P[3];
+}
+int Dtt_ManCheckHash( Dtt_Man_t * p, unsigned Truth )
+{
+ unsigned Hash = Dtt_ManHashKey(p, Truth);
+ unsigned * pSpot = p->pBins + (Hash & p->BinMask);
+ for ( ; ~*pSpot; Hash++, pSpot = p->pBins + (Hash & p->BinMask) )
+ if ( *pSpot == Truth ) // equal
+ return 0;
+ Vec_IntPush( p->vUsedBins, pSpot - p->pBins );
+ *pSpot = Truth;
+ return 1;
+}
+Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
+{
+ int i, k, Entry;
+ word tCur = ((word)Truth << 32) | (word)Truth;
+ Vec_IntClear( vFuns );
+ for ( i = 0; i < p->nPerms; i++ )
+ {
+ for ( k = 0; k < p->nComps; k++ )
+ {
+// unsigned tTemp = (unsigned)(tCur & 1 ? ~tCur : tCur);
+ unsigned tTemp = (unsigned)(tCur & p->CmpMask ? ~tCur : tCur);
+ if ( Dtt_ManCheckHash( p, tTemp ) )
+ Vec_IntPush( vFuns, tTemp );
+ tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
+ }
+ tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] );
+ }
+ assert( tCur == (((word)Truth << 32) | (word)Truth) );
+ // clean hash table
+ Vec_IntForEachEntry( p->vUsedBins, Entry, i )
+ p->pBins[Entry] = ~0;
+ Vec_IntClear( p->vUsedBins );
+ //printf( "%d ", Vec_IntSize(vFuns) );
+ return vFuns;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun )
+{
+ tFun = tFun & p->CmpMask ? ~tFun : tFun;
+ return Abc_TtGetBit( p->pPres, tFun & p->FunMask );
+}
+static inline void Dtt_ManSetFun( Dtt_Man_t * p, unsigned tFun )
+{
+ tFun = tFun & p->CmpMask ? ~tFun : tFun;
+ //assert( !Dtt_ManGetFun(p, fFun & p->FunMask );
+ Abc_TtSetBit( p->pPres, tFun & p->FunMask );
+}
+void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, unsigned Truth )
+{
+ Vec_Int_t * vFuncs = Dtt_ManCollect( p, Truth, p->vTemp2 );
+ unsigned Min = Vec_IntFindMin( vFuncs );
+ int i, nObjs = Vec_IntSize(p->vFanins)/2;
+ int nNodesI = 0xF & (Vec_IntEntry(p->vConfigs, FanI) >> 3);
+ int nNodesJ = 0xF & (Vec_IntEntry(p->vConfigs, FanJ) >> 3);
+ int nNodes = nNodesI + nNodesJ + 1;
+ assert( nObjs == Vec_IntSize(p->vTruths) );
+ assert( nObjs == Vec_IntSize(p->vConfigs) );
+ assert( nObjs == Vec_IntSize(p->vClasses) );
+ Vec_WecPush( p->vFunNodes, n, nObjs );
+ Vec_IntPushTwo( p->vFanins, FanI, FanJ );
+ Vec_IntPush( p->vTruths, Truth );
+ Vec_IntPush( p->vConfigs, (nNodes << 3) | Type );
+ Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
+ Vec_IntPush( p->vTruthNpns, Min );
+ Vec_IntForEachEntry( vFuncs, Min, i )
+ Dtt_ManSetFun( p, Min );
+ assert( nNodes < 32 );
+ p->Counts[nNodes]++;
+
+ if ( p->pTable == NULL )
+ return;
+ Truth = Truth & p->CmpMask ? ~Truth : Truth;
+ Truth &= p->FunMask;
+ assert( p->pNodes[p->pTable[Truth]] == 0 );
+ p->pNodes[p->pTable[Truth]] = n;
+}
+
+int Dtt_PrintStats( int nNodes, int nVars, Vec_Wec_t * vFunNodes, word nSteps, abctime clk, int fDelay, word nMultis )
+{
+ int nNew = Vec_IntSize(Vec_WecEntry(vFunNodes, nNodes));
+ printf("%c =%2d | ", fDelay ? 'D':'N', nNodes );
+ printf("C =%12.0f | ", (double)(iword)nSteps );
+ printf("New%d =%10d ", nVars, nNew + (int)(nNodes==0) );
+ printf("All%d =%10d | ", nVars, Vec_WecSizeSize(vFunNodes)+1 );
+ printf("Multi =%10d | ", (int)nMultis );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ //Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
+ fflush(stdout);
+ return nNew;
+}
+void Dtt_PrintDistrib( Dtt_Man_t * p )
+{
+ int i;
+ printf( "NPN classes for each node count (N):\n" );
+ for ( i = 0; i < 32; i++ )
+ if ( p->Counts[i] )
+ printf( "N = %2d : NPN = %6d\n", i, p->Counts[i] );
+}
+void Dtt_PrintMulti2( Dtt_Man_t * p )
+{
+ int i, n;
+ for ( n = 0; n <= 7; n++ )
+ {
+ printf( "n=%d : ", n);
+ for ( i = 0; i < p->nClasses; i++ )
+ if ( p->pNodes[i] == n )
+ printf( "%d ", p->pTimes[i] );
+ printf( "\n" );
+ }
+}
+void Dtt_PrintMulti1( Dtt_Man_t * p )
+{
+ int i, n, Entry, Count, Prev;
+ for ( n = 0; n < 16; n++ )
+ {
+ Vec_Int_t * vTimes = Vec_IntAlloc( 100 );
+ Vec_Int_t * vUsed = Vec_IntAlloc( 100 );
+ for ( i = 0; i < p->nClasses; i++ )
+ if ( p->pNodes[i] == n )
+ Vec_IntPush( vTimes, p->pTimes[i] );
+ if ( Vec_IntSize(vTimes) == 0 )
+ {
+ Vec_IntFree(vTimes);
+ Vec_IntFree(vUsed);
+ break;
+ }
+ Vec_IntSort( vTimes, 0 );
+ Count = 1;
+ Prev = Vec_IntEntry( vTimes, 0 );
+ Vec_IntForEachEntryStart( vTimes, Entry, i, 1 )
+ if ( Prev == Entry )
+ Count++;
+ else
+ {
+ assert( Prev < Entry );
+ Vec_IntPushTwo( vUsed, Prev, Count );
+ Count = 1;
+ Prev = Entry;
+ }
+ if ( Count > 0 )
+ Vec_IntPushTwo( vUsed, Prev, Count );
+ printf( "n=%d : ", n);
+ Vec_IntForEachEntryDouble( vUsed, Prev, Entry, i )
+ printf( "%d=%d ", Prev, Entry );
+ printf( "\n" );
+ Vec_IntFree( vTimes );
+ Vec_IntFree( vUsed );
+ }
+}
+void Dtt_PrintMulti( Dtt_Man_t * p )
+{
+ int n, Counts[13][11] = {{0}};
+ for ( n = 0; n < 13; n++ )
+ {
+ int i, Total = 0, Count = 0;
+ for ( i = 0; i < p->nClasses; i++ )
+ if ( p->pNodes[i] == n )
+ {
+ int Log = Abc_Base2Log(p->pTimes[i]);
+ assert( Log < 11 );
+ if ( p->pTimes[i] < 2 )
+ Counts[n][0]++;
+ else
+ Counts[n][Log]++;
+ Total += p->pTimes[i];
+ Count++;
+ }
+ if ( Count == 0 )
+ break;
+ printf( "n=%2d : ", n );
+ printf( "All = %7d ", Count );
+ printf( "Ave = %6.2f ", 1.0*Total/Count );
+ for ( i = 0; i < 11; i++ )
+ if ( Counts[n][i] )
+ printf( "%6d", Counts[n][i] );
+ else
+ printf( "%6s", "" );
+ printf( "\n" );
+ }
+}
+void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose )
+{
+ abctime clk = Abc_Clock(); word nSteps = 0, nMultis = 0;
+ Dtt_Man_t * p = Dtt_ManAlloc( nVars, fMulti ); int n, i, j;
+ // constant zero class
+ Vec_IntPushTwo( p->vFanins, 0, 0 );
+ Vec_IntPush( p->vTruths, 0 );
+ Vec_IntPush( p->vConfigs, 0 );
+ Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
+ Vec_IntPush( p->vTruthNpns, 0 );
+ Dtt_ManSetFun( p, 0 );
+ // buffer class
+ Vec_WecPush( p->vFunNodes, 0, Vec_IntSize(p->vFanins)/2 );
+ Vec_IntPushTwo( p->vFanins, 0, 0 );
+ Vec_IntPush( p->vTruths, (unsigned)s_Truths6[0] );
+ Vec_IntPush( p->vConfigs, 0 );
+ Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
+ Vec_IntPush( p->vTruthNpns, (unsigned)s_Truths6[0] );
+ for ( i = 0; i < nVars; i++ )
+ Dtt_ManSetFun( p, (unsigned)s_Truths6[i] );
+ p->Counts[0] = 2;
+ // enumerate
+ Dtt_PrintStats(0, nVars, p->vFunNodes, nSteps, clk, fDelay, 0);
+ for ( n = 1; n <= nNodeMax; n++ )
+ {
+ for ( i = 0, j = n - 1; i < n; i++, j = j - 1 + fDelay ) if ( i <= j )
+ {
+ Vec_Int_t * vFaninI = Vec_WecEntry( p->vFunNodes, i );
+ Vec_Int_t * vFaninJ = Vec_WecEntry( p->vFunNodes, j );
+ int k, i0, j0, EntryI, EntryJ;
+ Vec_IntForEachEntry( vFaninI, EntryI, i0 )
+ {
+ unsigned TruthI = Vec_IntEntry(p->vTruths, EntryI);
+ Vec_Int_t * vFuns = Dtt_ManCollect( p, TruthI, p->vTemp );
+ int Start = i == j ? i0 : 0;
+ Vec_IntForEachEntryStart( vFaninJ, EntryJ, j0, Start )
+ {
+ unsigned Truth, TruthJ = Vec_IntEntry(p->vTruths, EntryJ);
+ Vec_IntForEachEntry( vFuns, Truth, k )
+ {
+ if ( !Dtt_ManGetFun(p, TruthJ & Truth) )
+ Dtt_ManAddFunction( p, n, EntryI, EntryJ, 0, TruthJ & Truth );
+ if ( !Dtt_ManGetFun(p, TruthJ & ~Truth) )
+ Dtt_ManAddFunction( p, n, EntryI, EntryJ, 1, TruthJ & ~Truth );
+ if ( !Dtt_ManGetFun(p, ~TruthJ & Truth) )
+ Dtt_ManAddFunction( p, n, EntryI, EntryJ, 2, ~TruthJ & Truth );
+ if ( !Dtt_ManGetFun(p, TruthJ | Truth) )
+ Dtt_ManAddFunction( p, n, EntryI, EntryJ, 3, TruthJ | Truth );
+ if ( !Dtt_ManGetFun(p, TruthJ ^ Truth) )
+ Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4, TruthJ ^ Truth );
+ nSteps += 5;
+
+ if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ & Truth, n );
+ if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ & ~Truth, n );
+ if ( p->pTable ) Dtt_ManAddVisited( p, ~TruthJ & Truth, n );
+ if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ | Truth, n );
+ if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ ^ Truth, n );
+ }
+ nMultis++;
+ if ( p->pTable ) Dtt_ManProcessVisited( p );
+ }
+ }
+ }
+ if ( Dtt_PrintStats(n, nVars, p->vFunNodes, nSteps, clk, fDelay, nMultis) == 0 )
+ break;
+ }
+ if ( fDelay )
+ Dtt_PrintDistrib( p );
+ if ( p->pTable )
+ Dtt_PrintMulti( p );
+ Dtt_ManFree( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make
index efc34a1..5feb104 100644
--- a/src/opt/dau/module.make
+++ b/src/opt/dau/module.make
@@ -8,4 +8,5 @@ SRC += src/opt/dau/dauCanon.c \
src/opt/dau/dauMerge.c \
src/opt/dau/dauNonDsd.c \
src/opt/dau/dauNpn.c \
+ src/opt/dau/dauNpn2.c \
src/opt/dau/dauTree.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-02 18:33:49 +0000