Adding new NPN code developed by XueGong Zhou at Fudan University.

2 files changed, 1069 insertions, 137 deletions

diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 1fa22494..f392a98f 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -59,7 +59,7 @@ typedef enum {
 } Dau_DsdType_t;
 
 typedef struct Dss_Man_t_ Dss_Man_t;
-typedef struct Abc_TtMan_t_ Abc_TtMan_t;
+typedef struct Abc_TtHieMan_t_ Abc_TtHieMan_t;
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 4bc0f9c5..c471fb18 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -22,6 +22,7 @@
 #include "misc/util/utilTruth.h"
 #include "misc/vec/vecMem.h"
 #include "bool/lucky/lucky.h"
+#include <math.h>
 
 ABC_NAMESPACE_IMPL_START
 
@@ -40,6 +41,90 @@ static word s_CMasks6[5] = {
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Compares Cof0 and Cof1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
+{
+    if ( nWords == 1 )
+    {
+        word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
+        word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
+        if ( Cof0 != Cof1 )
+            return Cof0 < Cof1 ? -1 : 1;
+        return 0;
+    }
+	if ( iVar <= 5 )
+	{
+        word Cof0, Cof1;
+		int w, shift = (1 << iVar);
+		for ( w = 0; w < nWords; w++ )
+        {
+            Cof0 = pTruth[w] & s_Truths6Neg[iVar];
+            Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
+            if ( Cof0 != Cof1 )
+                return Cof0 < Cof1 ? -1 : 1;
+        }
+        return 0;
+	}
+	// if ( iVar > 5 )
+	{
+        word * pLimit = pTruth + nWords;
+		int i, iStep = Abc_TtWordNum(iVar);
+        assert( nWords >= 2 );
+		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 )
+{
+    if ( nWords == 1 )
+    {
+        word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
+        word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
+        if ( Cof0 != Cof1 )
+            return Cof0 < Cof1 ? -1 : 1;
+        return 0;
+    }
+	if ( iVar <= 5 )
+	{
+        word Cof0, Cof1;
+		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];
+            if ( Cof0 != Cof1 )
+                return Cof0 < Cof1 ? -1 : 1;
+        }
+        return 0;
+	}
+	// if ( iVar > 5 )
+	{
+        word * pLimit = pTruth + nWords;
+		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-- )
+                if ( pLimit[i] != pLimit[i + iStep] )
+                    return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
+        return 0;
+	}	
+}
+*/
 
 /**Function*************************************************************
 
@@ -57,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*************************************************************
@@ -110,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];
@@ -122,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 )
 {
@@ -158,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];
@@ -170,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*************************************************************
@@ -207,10 +292,21 @@ static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar,
   SeeAlso     []
 
 ***********************************************************************/
+#define DO_SMALL_TRUTHTABLE 0
+
+inline void Abc_TtNormalizeSmallTruth(word * pTruth, int nVars)
+{
+#if DO_SMALL_TRUTHTABLE
+	if (nVars < 6)
+		*pTruth &= (1ULL << (1 << nVars)) - 1;
+#endif
+}
+
 static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
 {   
     int nWords = Abc_TtWordNum( nVars );
     int k, Counter = 0;
+    Abc_TtNormalizeSmallTruth(pTruth, nVars);
     for ( k = 0; k < nWords; k++ )
         if ( pTruth[k] )
             Counter += Abc_TtCountOnes( pTruth[k] );
@@ -222,6 +318,7 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore
     int i, k, Counter, nWords;
     if ( nVars <= 6 )
     {
+        Abc_TtNormalizeSmallTruth(pTruth, nVars);
         for ( i = 0; i < nVars; i++ )
             pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
         return;
@@ -972,72 +1069,84 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-#define TT_NUM_TABLES 5
+#define TT_MAX_LEVELS 5
 
-struct Abc_TtMan_t_
+struct Abc_TtHieMan_t_
 {
-    Vec_Mem_t *   vTtMem[TT_NUM_TABLES];   // truth table memory and hash tables
-    Vec_Int_t **  vRepres;                 // pointers to the representatives from the last hierarchical level
+	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];
 };
 
-Vec_Int_t ** Abc_TtRepresStart() {
-    Vec_Int_t ** vRepres = ABC_ALLOC(Vec_Int_t *, TT_NUM_TABLES - 1);
-    int i;
-    // create a list of pointers for each level of the hierarchy
-    for (i = 0; i < (TT_NUM_TABLES - 1); i++) {
-        vRepres[i] = Vec_IntAlloc(1);
-    }
-    return vRepres;
-}
-
-void Abc_TtRepresStop(Vec_Int_t ** vRepres) {
-    int i;
-    for (i = 0; i < (TT_NUM_TABLES - 1); i++) {
-        Vec_IntFree(vRepres[i]);
-    }
-    ABC_FREE( vRepres );
-}
-
-Abc_TtMan_t * Abc_TtManStart( int nVars )
+Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels)
 {
-    Abc_TtMan_t * p = ABC_CALLOC( Abc_TtMan_t, 1 );
-    int i, nWords = Abc_TtWordNum( nVars );
-    for ( i = 0; i < TT_NUM_TABLES; i++ )
-    {
-        p->vTtMem[i] = Vec_MemAlloc( nWords, 12 );
-        Vec_MemHashAlloc( p->vTtMem[i], 10000 );
-    }
-    p->vRepres = Abc_TtRepresStart();
-    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_TtManStop( Abc_TtMan_t * p )
+
+void Abc_TtHieManStop(Abc_TtHieMan_t * p)
 {
-    int i;
-    for ( i = 0; i < TT_NUM_TABLES; i++ )
-    {
-        Vec_MemHashFree( p->vTtMem[i] );
-        Vec_MemFreeP( &p->vTtMem[i] );
-    }
-    Abc_TtRepresStop(p->vRepres);
-    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_TtManNumClasses( Abc_TtMan_t * p )
+
+int Abc_TtHieRetrieveOrInsert(Abc_TtHieMan_t * p, int level, word * pTruth, word * pResult)
 {
-    return Vec_MemEntryNum( p->vTtMem[TT_NUM_TABLES-1] );
+	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;
 }
 
-unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact )
+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];
     unsigned uCanonPhase = 0;
     int nOnes, nWords = Abc_TtWordNum( nVars );
-    int i, k, truthId;
-    int * pSpot;
-    int vTruthId[TT_NUM_TABLES-1];
-    int fLevelFound;
-    word * pRepTruth;
+    int i, k;
     assert( nVars <= 16 );
 
     Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
@@ -1054,12 +1163,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
         uCanonPhase |= (1 << nVars);
     }
     // check cache
-    pSpot = Vec_MemHashLookup( p->vTtMem[0], pTruth );
-    if ( *pSpot != -1 ) {
-        fLevelFound = 0;
-        goto end_repres;
-    }
-    vTruthId[0] = Vec_MemHashInsert( p->vTtMem[0], pTruth );
+    if (Abc_TtHieRetrieveOrInsert(p, 0, pTruth, pTruthInit) > 0) return 0;
 
     // normalize phase
     Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
@@ -1073,12 +1177,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
         pStore[i] = nOnes - pStore[i]; 
     }
     // check cache
-    pSpot = Vec_MemHashLookup( p->vTtMem[1], pTruth );
-    if ( *pSpot != -1 ) {
-        fLevelFound = 1;
-        goto end_repres;
-    }
-    vTruthId[1] = Vec_MemHashInsert( p->vTtMem[1], pTruth );
+	if (Abc_TtHieRetrieveOrInsert(p, 1, pTruth, pTruthInit) > 0) return 0;
 
     // normalize permutation
     {
@@ -1102,12 +1201,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
         }
     }
     // check cache
-    pSpot = Vec_MemHashLookup( p->vTtMem[2], pTruth );
-    if ( *pSpot != -1 ) {
-        fLevelFound = 2;
-        goto end_repres;
-    }
-    vTruthId[2] = Vec_MemHashInsert( p->vTtMem[2], pTruth );
+	if (Abc_TtHieRetrieveOrInsert(p, 2, pTruth, pTruthInit) > 0) return 0;
 
     // iterate TT permutations for tied variables
     for ( k = 0; k < 5; k++ )
@@ -1126,12 +1220,7 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
             break;
     }
     // check cache
-    pSpot = Vec_MemHashLookup( p->vTtMem[3], pTruth );
-    if ( *pSpot != -1 ) {
-        fLevelFound = 3;
-        goto end_repres;
-    }
-    vTruthId[3] = Vec_MemHashInsert( p->vTtMem[3], pTruth );
+	if (Abc_TtHieRetrieveOrInsert(p, 3, pTruth, pTruthInit) > 0) return 0;
 
     // perform exact NPN using groups
     if ( fExact ) {
@@ -1172,27 +1261,870 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
             freePermInfoPtr(pis[i]);
         }
     }
-    // check cache
-    pSpot = Vec_MemHashLookup( p->vTtMem[4], pTruth );
-    fLevelFound = 4;
-    if ( *pSpot != -1 ) {
-        goto end_repres;
-    }
-    *pSpot = Vec_MemHashInsert( p->vTtMem[4], pTruth );
-
-end_repres:
-    // return the class representative
-    if(fLevelFound < (TT_NUM_TABLES - 1))
-        truthId = Vec_IntEntry(p->vRepres[fLevelFound], *pSpot);
-    else truthId = *pSpot;
-    for(i = 0; i < fLevelFound; i++)
-        Vec_IntSetEntry(p->vRepres[i], vTruthId[i], truthId);
-    pRepTruth = Vec_MemReadEntry(p->vTtMem[TT_NUM_TABLES-1], truthId);
-    Abc_TtCopy( pTruthInit, pRepTruth, nWords, 0 );
-
+    // update cache
+	Abc_TtHieRetrieveOrInsert(p, 4, pTruth, pTruthInit);
     return 0;
 }
 
+
+/**Function*************************************************************
+
+Synopsis    [Adaptive exact/semi-canonical form computation.]
+
+Description []
+
+SideEffects []
+
+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
+} 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
+} Abc_TgMan_t;
+
+#if !defined(NDEBUG) && !defined(CANON_VERIFY)
+#define CANON_VERIFY
+#endif
+/**Function*************************************************************
+
+Synopsis    [Utilities.]
+
+Description []
+
+SideEffects []
+
+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;
+}
+
+
+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;
+}
+
+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);
+#else
+	return 1;
+#endif
+}
+
+/**Function*************************************************************
+
+Synopsis    [Tied group management.]
+
+Description []
+
+SideEffects []
+
+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;
+	}
+}
+
+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;
+}
+
+inline int Abc_TgCannonVerify(Abc_TgMan_t* pMan)
+{
+	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[pMan->pPermT[i]] == i);
+	}
+	assert(Abc_TgCannonVerify(pMan));
+#endif
+}
+
+/**Function*************************************************************
+
+Synopsis    [Truthtable manipulation.]
+
+Description []
+
+SideEffects []
+
+SeeAlso     []
+
+***********************************************************************/
+
+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;
+}
+
+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);
+}
+
+inline void Abc_TgFlipSymGroup(Abc_TgMan_t* pMan, int idx)
+{
+	Abc_TgFlipSymGroupByVar(pMan, pMan->pPerm[idx]);
+}
+
+inline void Abc_TgClearSymGroupPhase(Abc_TgMan_t* pMan, int iVar)
+{
+	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[pPerm[i]] = i;
+	for (i = 0; i < nVars; i++)
+		pPerm[i] = pRev[pPermDest[i]];
+	for (i = 0; i < nVars; i++)
+		pRev[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[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));
+}
+
+/**Function*************************************************************
+
+Synopsis    [semmetry of two variables.]
+
+Description []
+
+SideEffects []
+
+SeeAlso     []
+
+***********************************************************************/
+
+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);
+}
+
+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);
+}
+
+/**Function*************************************************************
+
+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. ]
+
+SideEffects []
+
+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;
+}
+
+/**Function*************************************************************
+
+Synopsis    [Group symmetric variables.]
+
+Description []
+
+SideEffects []
+
+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, order = 0;
+
+	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;
+}
+
+static 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);
+}
+
+
+/**Function*************************************************************
+
+Synopsis    [Semi-canonical form computation.]
+
+Description [simple config enumeration]
+
+SideEffects []
+
+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;
+}
+
+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 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));
+}
+
+/**Function*************************************************************
+
+Synopsis    [Exact canonical form computation.]
+
+Description [full config enumeration]
+
+SideEffects []
+
+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;
+}
+
+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;
+}
+
+static void Abc_TgFirstPermutation(Abc_TgMan_t * pMan)
+{
+	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));
+	}
+#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;
+}
+
+inline unsigned grayCode(unsigned a) { return a ^ (a >> 1); }
+
+static int grayFlip(unsigned a, int n)
+{
+	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;
+}
+
+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);
+}
+
+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[pFGrps[j-1]] > pMan->symPhase[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);
+	}
+}
+
+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;
+}
+
+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;
+
+#ifdef CANON_VERIFY
+	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);
+
+#ifdef CANON_VERIFY
+	if (!Abc_TgCannonVerify(&tgMan))
+		printf("Canonical form verification failed!\n");
+#endif
+	return tgMan.uPhase;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////