Updating canonical form computation procedures.

3 files changed, 598 insertions, 109 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 475fe7b7..b30970ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6797,6 +6797,9 @@ usage:
     Abc_Print( -2, "\t               6: new phase canonical form\n" );
     Abc_Print( -2, "\t               7: new hierarchical matching\n" );
     Abc_Print( -2, "\t               8: hierarchical matching by XueGong Zhou at Fudan University, Shanghai\n" );
+    Abc_Print( -2, "\t               9: FPL2018 algorithm     by XueGong Zhou at Fudan University, Shanghai\n" );
+    Abc_Print( -2, "\t              10: TRETS algorithm       by XueGong Zhou at Fudan University, Shanghai\n" );
+    Abc_Print( -2, "\t              11: a new exact matching  by XueGong Zhou at Fudan University, Shanghai\n" );
     Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
     Abc_Print( -2, "\t-d       : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" );
     Abc_Print( -2, "\t-b       : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 4f8019b1..ed8125b1 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -185,23 +185,29 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
 
     char * pAlgoName = NULL;
     if ( NpnType == 0 )
-        pAlgoName = "uniqifying         ";
+        pAlgoName = "uniqifying          ";
     else if ( NpnType == 1 )
-        pAlgoName = "exact NPN          ";
+        pAlgoName = "exact NPN           ";
     else if ( NpnType == 2 )
-        pAlgoName = "counting 1s        ";
+        pAlgoName = "counting 1s         ";
     else if ( NpnType == 3 )
-        pAlgoName = "Jake's hybrid fast ";
+        pAlgoName = "Jake's hybrid fast  ";
     else if ( NpnType == 4 )
-        pAlgoName = "Jake's hybrid good ";
+        pAlgoName = "Jake's hybrid good  ";
     else if ( NpnType == 5 )
-        pAlgoName = "new hybrid fast    ";
+        pAlgoName = "new hybrid fast     ";
     else if ( NpnType == 6 )
-        pAlgoName = "new phase flipping ";
+        pAlgoName = "new phase flipping  ";
     else if ( NpnType == 7 )
-        pAlgoName = "new hier. matching ";
+        pAlgoName = "new hier. matching  ";
     else if ( NpnType == 8 )
-        pAlgoName = "new adap. matching ";
+        pAlgoName = "new adap. matching  ";
+    else if ( NpnType == 9 )
+        pAlgoName = "FPL 2018 algorithm  ";
+    else if ( NpnType == 10 )
+        pAlgoName = "TRETS algorithm     ";
+    else if ( NpnType == 11 )
+        pAlgoName = "new exact algorithm ";
 
     assert( p->nVars <= 16 );
     if ( pAlgoName )
@@ -327,6 +333,29 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
         }
 		Abc_TtHieManStop(pMan);
     }
+    else if ( NpnType == 9 || NpnType == 10 || NpnType == 11 )
+    {
+        typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
+        unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
+        unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
+        unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
+		
+		Abc_TtHieMan_t * pMan = Abc_TtHieManStart(p->nVars, 5);
+		for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            if ( NpnType == 9 )
+                uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeAda, pMan, p->pFuncs[i], p->nVars, pCanonPerm,  100); // FPL2018 algorithm
+            else if ( NpnType == 10 )
+                uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeAda, pMan, p->pFuncs[i], p->nVars, pCanonPerm, 1100); // TRETS algorithm
+            else if ( NpnType == 11 )
+                uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeAda, pMan, p->pFuncs[i], p->nVars, pCanonPerm,    0); // the new exact algorithm
+            if ( fVerbose )
+                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
+        }
+		Abc_TtHieManStop(pMan);
+    }
     else assert( 0 );
     clk = Abc_Clock() - clk;
     printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) );
@@ -390,7 +419,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
 {
     if ( fVerbose )
         printf( "Using truth tables from file \"%s\"...\n", pFileName );
-    if ( NpnType >= 0 && NpnType <= 8 )
+    if ( NpnType >= 0 && NpnType <= 11 )
         Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
     else
         printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 739dd373..84813ba6 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -302,7 +302,7 @@ void Abc_TtNormalizeSmallTruth(word * pTruth, int nVars)
     }
 }
 
-static inline void Abc_TtVerifySmallTruth(word * pTruth, int nVars)
+inline void Abc_TtVerifySmallTruth(word * pTruth, int nVars)
 {
 #ifndef NDEBUG
     if (nVars < 6) {
@@ -368,6 +368,80 @@ int Abc_TtCountOnesInCofsSimple( word * pTruth, int nVars, int * pStore )
     return Abc_TtCountOnesInTruth( pTruth, nVars );
 }
 
+// Shifted Cofactor Coefficient
+inline int shiftFunc(int ci)
+//{ return ci * ci; }
+{ return 1 << ci; }
+
+static int Abc_TtScc6(word wTruth, int ck)
+{
+    int i;
+    int sum = 0;
+    if (!wTruth) return 0;
+    for (i = 0; i < 64; i++)
+        if (wTruth & ABC_CONST(0x1) << i) {
+            int ci = Abc_TtBitCount8[i] + ck;
+            sum += shiftFunc(ci);
+        }
+    return sum;
+}
+int Abc_TtScc(word * pTruth, int nVars)
+{
+    int k, nWords = Abc_TtWordNum(nVars);
+    int sum = 0;
+    Abc_TtNormalizeSmallTruth(pTruth, nVars);
+    for (k = 0; k < nWords; k++)
+        sum += Abc_TtScc6(pTruth[k], Abc_TtBitCount16(k));
+    return sum;
+}
+static inline void Abc_TtSccInCofs6(word wTruth, int nVars, int ck, int * pStore)
+{
+    int i, j, v;
+    assert(nVars <= 6);
+    for (v = 0; v < nVars; v++)
+    {
+        int sum = 0;
+        for (i = j = 0; j < 64; j++)
+            if (s_Truths6Neg[v] & ABC_CONST(0x1) << j)
+            {
+                if (wTruth & ABC_CONST(0x1) << j)
+                {
+                    int ci = Abc_TtBitCount8[i] + ck;
+                    sum += shiftFunc(ci);
+                }
+                i++;
+            }
+        pStore[v] += sum;
+    }
+}
+static inline void Abc_TtSccInCofs(word * pTruth, int nVars, int * pStore)
+{
+    int k, v, nWords;
+    int kv[10] = { 0 };
+    memset(pStore, 0, sizeof(int) * nVars);
+    if (nVars <= 6)
+    {
+        Abc_TtNormalizeSmallTruth(pTruth, nVars);
+        Abc_TtSccInCofs6(pTruth[0], nVars, 0, pStore);
+        return;
+    }
+    assert(nVars > 6);
+    nWords = Abc_TtWordNum(nVars);
+    for (k = 0; k < nWords; k++)
+    {
+        // count 1's for the first six variables
+        Abc_TtSccInCofs6(pTruth[k], 6, Abc_TtBitCount16(k), pStore);
+
+        // count 1's for all other variables
+        for (v = 6; v < nVars; v++)
+            if ((k & (1 << (v - 6))) == 0)
+            {
+                pStore[v] += Abc_TtScc6(pTruth[k], Abc_TtBitCount16(kv[v - 6]));
+                kv[v - 6]++;
+            }
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Minterm counting in all cofactors.]
@@ -953,7 +1027,7 @@ int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char *
   SeeAlso     []
 
 ***********************************************************************/
-//#define CANON_VERIFY
+#define CANON_VERIFY
 unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
 {
     int pStoreIn[17];
@@ -1169,6 +1243,8 @@ struct Abc_TtHieMan_t_
     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 * vPhase;
 };
 
 Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels)
@@ -1185,6 +1261,7 @@ Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels)
         Vec_MemHashAlloc(p->vTtMem[i], 10000);
         p->vRepres[i] = Vec_IntAlloc(1);
     }
+    p->vPhase = Vec_IntAlloc(2500);
     return p;
 }
 
@@ -1384,7 +1461,6 @@ 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_
@@ -1394,6 +1470,7 @@ typedef struct Abc_TgMan_t_
     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
+    int fPhased;                        // if the phases of all the variables are determined
     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
@@ -1402,6 +1479,10 @@ typedef struct Abc_TgMan_t_
     // symemtric group attributes
     char symPhase[16];                  // phase type of symemtric groups
     signed char symLink[17];            // singly linked list, indicate the variables in symemtric groups
+
+    int  nAlgorithm;                    // 0: AdjCE,  1: AdjSE,  2: E: Cost-Aware
+    char pFGrps[16];                    // tied groups to be flipped
+    Vec_Int_t * vPhase;                 // candidate phase assignments
 } Abc_TgMan_t;
 
 #if !defined(NDEBUG) && !defined(CANON_VERIFY)
@@ -1439,7 +1520,7 @@ static int Abc_NextPermSwapC(char * pData, signed char * pDir, int size)
     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);
@@ -1456,7 +1537,7 @@ unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word *
     if (Abc_TtCompareRev(pTruth, pTruth2, nWords) <= 0)
         return uCanonPhase1;
     Abc_TtCopy(pTruth, pTruth2, nWords, 0);
-    memcpy(pCanonPerm, pCanonPerm2, (size_t)nVars);
+    memcpy(pCanonPerm, pCanonPerm2, nVars);
     return uCanonPhase2;
 }
 
@@ -1489,21 +1570,62 @@ SeeAlso     []
 
 ***********************************************************************/
 
-static void Abc_TginitMan(Abc_TgMan_t * pMan, word * pTruth, int nVars)
+static void Abc_TgInitMan(Abc_TgMan_t * pMan, word * pTruth, int nVars, int nAlg, Vec_Int_t * vPhase)
 {
     int i;
     pMan->pTruth = pTruth;
-    pMan->nVars = pMan->nGVars = nVars;
     pMan->uPhase = 0;
+    pMan->fPhased = 0;
+    pMan->nVars = pMan->nGVars = nVars;
+    pMan->nGroups = 1;
+    pMan->pGroup[0].iStart = 0;
+    pMan->pGroup[0].nGVars = nVars;
     for (i = 0; i < nVars; i++)
     {
         pMan->pPerm[i] = i;
         pMan->pPermT[i] = i;
         pMan->pPermTRev[i] = i;
         pMan->symPhase[i] = 1;
+        pMan->symLink[i] = -1;
     }
+    pMan->symLink[i] = -1;
+    pMan->nAlgorithm = nAlg;
+    pMan->vPhase = vPhase;
+    Vec_IntClear(vPhase);
 }
 
+static int Abc_TgSplitGroup(Abc_TgMan_t * pMan, TiedGroup * pGrp, int * pCoef)
+{
+    int i, j, n = 0;
+    int nGVars = pGrp->nGVars;
+    char * pVars = pMan->pPerm + pGrp->iStart;
+    int iGrp = pGrp - pMan->pGroup;
+
+    // sort variables
+    for (i = 1; i < nGVars; i++)
+    {
+        int a = pCoef[i]; char aa = pVars[i];
+        for (j = i; j > 0 && pCoef[j - 1] > a; j--)
+            pCoef[j] = pCoef[j - 1], pVars[j] = pVars[j - 1];
+        pCoef[j] = a; pVars[j] = aa;
+    }
+    for (i = 1; i < nGVars; i++)
+        if (pCoef[i] != pCoef[i - 1]) n++;
+    if (n == 0) return 0;
+    memmove(pGrp + n + 1, pGrp + 1, (pMan->nGroups - iGrp - 1) * sizeof(TiedGroup));
+    // group variables
+    for (i = j = 1; i < nGVars; i++)
+    {
+        if (pCoef[i] == pCoef[i - 1]) continue;
+        pGrp[j].iStart = pGrp->iStart + i;
+        pGrp[j - 1].nGVars = pGrp[j].iStart - pGrp[j - 1].iStart;
+        j++;
+    }
+    assert(j == n + 1);
+    pGrp[n].nGVars = pGrp->iStart + i - pGrp[n].iStart;
+    pMan->nGroups += n;
+    return n;
+}
 static inline void Abc_TgManCopy(Abc_TgMan_t* pDst, word* pDstTruth, Abc_TgMan_t* pSrc)
 {
     *pDst = *pSrc;
@@ -1516,13 +1638,13 @@ static 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);
+int Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pDest);
 static void CheckConfig(Abc_TgMan_t * pMan)
 {
 #ifndef NDEBUG
     int i;
     char pPermE[16];
-    Abc_TgExpendSymmetry(pMan, pMan->pPerm, pPermE);
+    Abc_TgExpendSymmetry(pMan, pPermE);
     for (i = 0; i < pMan->nVars; i++)
     {
         assert(pPermE[i] == pMan->pPermT[i]);
@@ -1609,7 +1731,7 @@ static void Abc_TgSwapAdjacentSymGroups(Abc_TgMan_t* pMan, int idx)
     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_TgExpendSymmetry(pMan, pPermNew);
         Abc_TgImplementPerm(pMan, pPermNew);
         return;
     }
@@ -1688,7 +1810,7 @@ SeeAlso     []
 static void Abc_TgCreateGroups(Abc_TgMan_t * pMan)
 {
     int pStore[17];
-    int i, j, nOnes;
+    int i, nOnes;
     int nVars = pMan->nVars, nWords = Abc_TtWordNum(nVars);
     TiedGroup * pGrp = pMan->pGroup;
     assert(nVars <= 16);
@@ -1712,28 +1834,8 @@ static void Abc_TgCreateGroups(Abc_TgMan_t * pMan)
         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;
+    Abc_TgSplitGroup(pMan, pMan->pGroup, pStore);
+    pMan->fPhased = pStore[0] * 2 != nOnes;
 }
 
 /**Function*************************************************************
@@ -1748,13 +1850,14 @@ SeeAlso     []
 
 ***********************************************************************/
 
-static int Abc_TgGroupSymmetry(Abc_TgMan_t * pMan, TiedGroup * pGrp, int doHigh)
+static int Abc_TgGroupSymmetry(Abc_TgMan_t * pMan, TiedGroup * pGrp, int fHigh)
 {
     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;
+    int fPhase = (pGrp == pMan->pGroup) && !pMan->fPhased;
     char * pVars = pMan->pPerm + pGrp->iStart;
     int modified;
 
@@ -1775,9 +1878,9 @@ static int Abc_TgGroupSymmetry(Abc_TgMan_t * pMan, TiedGroup * pGrp, int doHigh)
                 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);
+                    stype[j] = Abc_TtIsSymmetric(pMan->pTruth, pMan->nVars, iVar, jVar, fPhase);
                 else
-                    stype[j] = Abc_TtIsSymmetricHigh(pMan, iVar, jVar, !pGrp->fPhased);
+                    stype[j] = Abc_TtIsSymmetricHigh(pMan, iVar, jVar, fPhase);
             }
             fDone[i] = 1;
             // Merge symmetric groups
@@ -1811,23 +1914,20 @@ static int Abc_TgGroupSymmetry(Abc_TgMan_t * pMan, TiedGroup * pGrp, int doHigh)
             }
         }
 //      if (++order > 3) printf("%d", order);
-    } while (doHigh && modified);
+    } while (fHigh && modified);
 
     return nsym;
 }
 
-static void Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan, int doHigh)
+static void Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan, int fHigh)
 {
     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)
+    if (!pMan->fPhased)
     {
         int iVar = pMan->nVars;
         for (j = 0; j < pMan->pGroup[0].nGVars; j++)
@@ -1845,7 +1945,7 @@ static void Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan, int doHigh)
     }
 
     for (k = 0; k < pMan->nGroups; k++)
-        gcnt[k] += Abc_TgGroupSymmetry(pMan, pMan->pGroup + k, doHigh);
+        gcnt[k] += Abc_TgGroupSymmetry(pMan, pMan->pGroup + k, fHigh);
 
     for (i = 0; i < nVars && pPerm[i] >= 0; i++)
         ;
@@ -1870,17 +1970,65 @@ static void Abc_TgPurgeSymmetry(Abc_TgMan_t * pMan, int doHigh)
     pMan->nGVars -= sum;
 }
 
-void Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pPerm, char * pDest)
+static int Abc_TgExpendSymmetry(Abc_TgMan_t * pMan, char * pDest)
 {
-    int i = 0, j, k;
+    int i = 0, j, k, s;
+    char * pPerm = pMan->pPerm;
     for (j = 0; j < pMan->nGVars; j++)
         for (k = pPerm[j]; k >= 0; k = pMan->symLink[k])
             pDest[i++] = k;
+    s = i;
     for (k = pMan->symLink[pMan->nVars]; k >= 0; k = pMan->symLink[k])
         pDest[i++] = k;
     assert(i == pMan->nVars);
+    return s;
 }
 
+static void Abc_TgResetGroup(Abc_TgMan_t * pMan)
+{
+    int i, j;
+    char * pPerm = pMan->pPerm;
+    char pPermNew[16];
+    int nGVars = pMan->nGVars;
+    for (i = 1; i < nGVars; i++)
+    {
+        char t = pPerm[i];
+        for (j = i; j > 0 && pPerm[j - 1] > t; j--)
+            pPerm[j] = pPerm[j - 1];
+        pPerm[j] = t;
+    }
+    Abc_TgExpendSymmetry(pMan, pPermNew);
+    Abc_TgImplementPerm(pMan, pPermNew);
+    pMan->fPhased = 0;
+    pMan->nGroups = 1;
+    pMan->pGroup->nGVars = nGVars;
+    Vec_IntClear(pMan->vPhase);
+}
+
+static void Abc_TgResetGroup1(Abc_TgMan_t * pMan)
+{
+    int i, j;
+    char pPermNew[16];
+    int nSVars = Abc_TgExpendSymmetry(pMan, pPermNew);
+    for (i = 1; i < nSVars; i++)
+    {
+        char t = pPermNew[i];
+        for (j = i; j > 0 && pPermNew[j - 1] > t; j--)
+            pPermNew[j] = pPermNew[j - 1];
+        pPermNew[j] = t;
+    }
+    Abc_TgImplementPerm(pMan, pPermNew);
+    pMan->fPhased = 0;
+    pMan->nGroups = 1;
+    pMan->nGVars = pMan->pGroup->nGVars = nSVars;
+    for (i = 0; i < pMan->nVars; i++)
+    {
+        pMan->pPerm[i] = pPermNew[i];
+        pMan->symPhase[i] = 1;
+        pMan->symLink[i] = -1;
+    }
+    Vec_IntClear(pMan->vPhase);
+}
 
 /**Function*************************************************************
 
@@ -1893,7 +2041,7 @@ SideEffects []
 SeeAlso     []
 
 ***********************************************************************/
-static int Abc_TgSymGroupPerm(Abc_TgMan_t* pMan, int idx, TiedGroup* pTGrp)
+static int Abc_TgSymGroupPerm(Abc_TgMan_t* pMan, int idx, int fSwapOnly)
 {
     word* pTruth = pMan->pTruth;
     static word pCopy[1024];
@@ -1901,7 +2049,6 @@ static int Abc_TgSymGroupPerm(Abc_TgMan_t* pMan, int idx, TiedGroup* pTGrp)
     int Config = 0;
     int nWords = Abc_TtWordNum(pMan->nVars);
     Abc_TgMan_t tgManCopy, tgManBest;
-    int fSwapOnly = pTGrp->fPhased;
 
     CheckConfig(pMan);
     if (fSwapOnly)
@@ -2005,10 +2152,10 @@ static void Abc_TgSimpleEnumeration(Abc_TgMan_t * pMan)
         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]);
+                fChanges |= Abc_TgSymGroupPerm(pMan, i, pGid[i] > 0 || pMan->fPhased);
         for (i = 1; i < pMan->nGVars - 1; i++)
             if (pGid[i] == pGid[i + 1])
-                fChanges |= Abc_TgSymGroupPerm(pMan, i, pMan->pGroup + pGid[i]);
+                fChanges |= Abc_TgSymGroupPerm(pMan, i, pGid[i] > 0 || pMan->fPhased);
 
         for (i = pMan->nVars - 1; i >= 0; i--)
             if (pMan->symPhase[i])
@@ -2032,36 +2179,6 @@ 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)
 {
@@ -2126,18 +2243,17 @@ static int grayFlip(unsigned a)
 
 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)
+    if (Abc_TtCompareRev(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;
+    int i, j, n = pMan->pGroup->nGVars;
 
     Abc_TgSaveBest(pMan, pBest);
-    if (pGrp->fPhased) return;
+    if (pMan->fPhased) return;
 
     // sort by symPhase
     for (i = 0; i < n; i++)
@@ -2155,18 +2271,298 @@ static void Abc_TgPhaseEnumeration(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
     }
 }
 
-static void Abc_TgFullEnumeration(Abc_TgMan_t * pWork, Abc_TgMan_t * pBest)
+/**Function*************************************************************
+
+Synopsis    [Hybrid exact canonical form computation.]
+
+Description []
+
+SideEffects []
+
+SeeAlso     []
+
+***********************************************************************/
+static void Abc_TgCalcScc(Abc_TgMan_t * pMan, int * pOut, int fSort)
 {
-//  static word pCopy[1024];
-//  Abc_TgMan_t tgManCopy;
-//  Abc_TgManCopy(&tgManCopy, pCopy, pMan);
+    int i, j, k;
+    TiedGroup * pGrp;
+
+    Abc_TtSccInCofs(pMan->pTruth, pMan->nVars, pOut);
+
+    for (i = j = 0; j < pMan->nGVars; j++)
+    {
+        pOut[j] = pOut[i];
+        for (k = pMan->pPerm[j]; k >= 0; k = pMan->symLink[k])
+        {
+            i++;
+            assert(pMan->symLink[k] < 0 || pOut[j] == pOut[i]);
+        }
+    }
+    if (!fSort) return;
+
+    for (pGrp = pMan->pGroup; pGrp < pMan->pGroup + pMan->nGroups; pGrp++)
+    {
+        int vb = pGrp->iStart, ve = vb + pGrp->nGVars;
+        for (i = vb + 1; i < ve; i++)
+        {
+            int a = pOut[i];
+            for (j = i; j > vb && pOut[j - 1] > a; j--)
+                pOut[j] = pOut[j - 1];
+            pOut[j] = a;
+        }
+    }
+}
+
+static void Abc_TgSplitGroupsByScc(Abc_TgMan_t * pMan)
+{
+    int pScc[16];
+    char pPermT[16];
+    TiedGroup * pGrp;
+
+    Abc_TgCalcScc(pMan, pScc, 0);
+    for (pGrp = pMan->pGroup; pGrp < pMan->pGroup + pMan->nGroups; pGrp++)
+        pGrp += Abc_TgSplitGroup(pMan, pGrp, pScc + pGrp->iStart);
+
+    Abc_TgExpendSymmetry(pMan, pPermT);
+    Abc_TgImplementPerm(pMan, pPermT);
+    assert(Abc_TgCannonVerify(pMan));
+}
 
-    Abc_TgFirstPermutation(pWork);
-    do Abc_TgPhaseEnumeration(pWork, pBest);
-    while (Abc_TgNextPermutation(pWork));
+static int Abc_TgCompareCoef(int * pIn1, int * pIn2, int n)
+{
+    int i;
+    for (i = 0; i < n; i++)
+        if (pIn1[i] != pIn2[i])
+            return (pIn1[i] < pIn2[i]) ? -1 : 1;
+    return 0;
+}
+
+// log2(n!)*100
+static const int log2fn[17] = { 0, 0, 100, 258, 458, 691, 949, 1230, 1530, 1847, 2179, 2525, 2884, 3254, 3634, 4025, 4425 };
+static int Abc_TgPermCostScc(Abc_TgMan_t * pMan, int *pScc)
+{
+    int i, j, k, cost = 0;
+
+    for (i = k = 0; i < pMan->nGroups; i++)
+    {
+        int n = pMan->pGroup[i].nGVars;
+        int d = 1;
+        for (j = 1, k++; j < n; j++, k++)
+            if (pScc[k] == pScc[k - 1]) d++;
+            else {
+                cost += log2fn[d];
+                d = 1;
+            }
+        cost += log2fn[d];
+    }
+    return cost;
+}
+
+static void Abc_TgPermEnumerationScc(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
+{
+    static word pCopy[1024];
+    Abc_TgMan_t tgManCopy;
+    Abc_TgManCopy(&tgManCopy, pCopy, pMan);
+    if (pMan->nAlgorithm > 1)
+        Abc_TgSplitGroupsByScc(&tgManCopy);
+    Abc_TgFirstPermutation(&tgManCopy);
+    do {
+        Abc_TgSaveBest(&tgManCopy, pBest);
+    } while (Abc_TgNextPermutation(&tgManCopy));
+}
+
+static void Abc_TgReorderFGrps(Abc_TgMan_t * pMan)
+{
+    char * pFGrps = pMan->pFGrps;
+    int i, j, n = pMan->fPhased ? 0 : pMan->pGroup->nGVars;
+
+    // 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;
+    }
+}
+
+static int ilog2(int n)
+{
+    int i;
+    for (i = 0; n /= 2; i++)
+        ;
+    return i;
+}
+
+typedef struct Abc_SccCost_t_ {
+    int cNeg, cPhase, cPerm;
+} Abc_SccCost_t;
+
+static Abc_SccCost_t Abc_TgRecordPhase(Abc_TgMan_t * pMan, int mode)
+{
+    Vec_Int_t * vPhase = pMan->vPhase;
+    int i, j, n = pMan->pGroup->nGVars;
+    int nStart = mode == 0 ? 1 : 0;
+    int nCoefs = pMan->nGVars + 2 - nStart;
+    int pScc[18], pMinScc[18];
+    Abc_SccCost_t ret;
+
+    if (pMan->fPhased)
+    {
+        ret.cNeg = 0;
+        ret.cPhase = 0;
+        Abc_TgCalcScc(pMan, pScc + 2, 1);
+        ret.cPerm = Abc_TgPermCostScc(pMan, pScc + 2);
+        return ret;
+    }
+
+    Abc_TgReorderFGrps(pMan);
+    pMinScc[1] = Abc_TtScc(pMan->pTruth, pMan->nVars);
+    Abc_TgCalcScc(pMan, pMinScc + 2, 1);
+    pMinScc[0] = mode == 0 ? 0 : Abc_TgPermCostScc(pMan, pMinScc + 2);
+    Vec_IntPush(vPhase, 0);
+    for (i = 0; (j = grayFlip(i)) < n; i++)
+    {
+        Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[j]);
+        pScc[1] = Abc_TtScc(pMan->pTruth, pMan->nVars);
+        if (mode == 0 && pScc[1] > pMinScc[1]) continue;
+        Abc_TgCalcScc(pMan, pScc + 2, 1);
+        if (mode > 0)
+            pScc[0] = Abc_TgPermCostScc(pMan, pScc + 2);
+        if (Abc_TgCompareCoef(pScc + nStart, pMinScc + nStart, nCoefs) < 0)
+        {
+            memcpy(pMinScc + nStart, pScc + nStart, nCoefs * sizeof(int));
+            Vec_IntClear(vPhase);
+        }
+        if (Abc_TgCompareCoef(pScc + nStart, pMinScc + nStart, nCoefs) == 0)
+            Vec_IntPush(vPhase, grayCode(i+1));
+    }
+    Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[n - 1]);
+
+    ret.cNeg = n;
+    ret.cPhase = ilog2(Vec_IntSize(vPhase));
+    ret.cPerm = Abc_TgPermCostScc(pMan, pMinScc + 2);
+    return ret;
+}
+
+static int Abc_TgRecordPhase1(Abc_TgMan_t * pMan)   // for AdjSE
+{
+    Vec_Int_t * vPhase = pMan->vPhase;
+    int i, j, n = pMan->pGroup->nGVars;
+    int nCoefs = pMan->nGVars + 2;
+    int nScc, nMinScc;
+
+    assert (Vec_IntSize(vPhase) == 0);
+    if (pMan->fPhased) return 0;
+
+    Abc_TgReorderFGrps(pMan);
+    nMinScc = Abc_TtScc(pMan->pTruth, pMan->nVars);
+    Vec_IntPush(vPhase, 0);
+    for (i = 0; (j = grayFlip(i)) < n; i++)
+    {
+        Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[j]);
+        nScc = Abc_TtScc(pMan->pTruth, pMan->nVars);
+        if (nScc > nMinScc) continue;
+        if (nScc < nMinScc)
+        {
+            nMinScc = nScc;
+            Vec_IntClear(vPhase);
+        }
+        Vec_IntPush(vPhase, grayCode(i + 1));
+    }
+
+    Abc_TgFlipSymGroupByVar(pMan, pMan->pFGrps[n - 1]);
+    return ilog2(Vec_IntSize(vPhase));
+}
+
+static void Abc_TgPhaseEnumerationScc(Abc_TgMan_t * pMan, Abc_TgMan_t * pBest)
+{
+    Vec_Int_t * vPhase = pMan->vPhase;
+    int i, j, n = pMan->pGroup->nGVars;
+    int ph0 = 0, ph, flp;
+    static word pCopy[1024];
+    Abc_TgMan_t tgManCopy;
+
+    if (pMan->fPhased)
+    {
+        Abc_TgPermEnumerationScc(pMan, pBest);
+        return;
+    }
+
+    Abc_TgManCopy(&tgManCopy, pCopy, pMan);
+    Vec_IntForEachEntry(vPhase, ph, i)
+    {
+        flp = ph ^ ph0;
+        for (j = 0; j < n; j++)
+            if (flp & (1 << j))
+                Abc_TgFlipSymGroupByVar(&tgManCopy, pMan->pFGrps[j]);
+        ph0 = ph;
+        Abc_TgPermEnumerationScc(&tgManCopy, pBest);
+    }
+}
+
+static void Abc_TgFullEnumeration(Abc_TgMan_t * pWork, Abc_TgMan_t * pBest)
+{
+    if (pWork->nAlgorithm > 0)
+    {
+        Abc_TtFill(pBest->pTruth, Abc_TtWordNum(pBest->nVars));
+        Abc_TgPhaseEnumerationScc(pWork, pBest);
+    }
+    else 
+    {
+        Abc_TgFirstPermutation(pWork);
+        do Abc_TgPhaseEnumeration(pWork, pBest);
+        while (Abc_TgNextPermutation(pWork));
+    }
     pBest->uPhase |= 1 << 30;
 }
 
+// runtime cost for Abc_TgRecordPhase (mode = 1)
+static inline double Abc_SccPhaseCost(Abc_TgMan_t * pMan)
+{
+    return pMan->nVars * 0.997 + pMan->nGVars * 1.043 - 15.9;
+}
+
+// runtime cost for Abc_TgFullEnumeration
+static inline double Abc_SccEnumCost(Abc_TgMan_t * pMan, Abc_SccCost_t c)
+{
+    switch (pMan->nAlgorithm)
+    {
+        case 0: return pMan->nVars + c.cPhase * 1.09 + c.cPerm * 0.01144;
+        case 1: return pMan->nVars + c.cPhase * 0.855 + c.cPerm * 0.00797;
+        case 2: return pMan->nVars * 0.94 + c.cPhase * 0.885 + c.cPerm * 0.00855 - 20.59;
+    }
+    return 0;
+}
+
+static int Abc_TgEnumerationCost(Abc_TgMan_t * pMan)
+{
+    int i;
+    Abc_SccCost_t c = { 0,0,0 };
+    if (pMan->nGroups == 0) return 0;
+
+    for (i = 0; i < pMan->nGroups; i++)
+        c.cPerm += log2fn[pMan->pGroup[i].nGVars];
+
+    c.cPhase = pMan->fPhased ? 0
+             : pMan->nAlgorithm == 0 ? pMan->pGroup->nGVars
+             : Abc_TgRecordPhase1(pMan);
+
+    // coefficients computed by linear regression
+    return Abc_SccEnumCost(pMan, c) + 0.5;
+}
+
+/**Function*************************************************************
+
+Synopsis    [Adaptive heuristic/exact canonical form computation.]
+
+Description []
+
+SideEffects []
+
+SeeAlso     []
+
+***********************************************************************/
 unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres)
 {
     int nWords = Abc_TtWordNum(nVars);
@@ -2174,8 +2570,9 @@ unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char
     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;
+    const int MaxCost = 84;  // maximun posible cost for function with 16 inputs
+    const int nAlg = iThres >= 1000 ? 1 : 0;
+    const int fHigh = (iThres % 1000) >= 100, nEnumThres = iThres % 100;
 
     // handle constant
     if ( nVars == 0 ) {
@@ -2189,18 +2586,20 @@ unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char
 #endif
 
     assert(nVars <= 16);
+    assert(!(nAlg && p == NULL));
     if (p && Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash;
-    Abc_TginitMan(&tgMan, pTruth, nVars);
+    Abc_TgInitMan(&tgMan, pTruth, nVars, nAlg, p ? p->vPhase : NULL);
     Abc_TgCreateGroups(&tgMan);
     if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash;
-    Abc_TgPurgeSymmetry(&tgMan, doHigh);
+    Abc_TgPurgeSymmetry(&tgMan, fHigh);
 
-    Abc_TgExpendSymmetry(&tgMan, tgMan.pPerm, pCanonPerm);
+    Abc_TgExpendSymmetry(&tgMan, pCanonPerm);
     Abc_TgImplementPerm(&tgMan, pCanonPerm);
     assert(Abc_TgCannonVerify(&tgMan));
 
-    if (p == NULL) {
-        if (iEnumThres > MaxCost || Abc_TgEnumerationCost(&tgMan) < iEnumThres) {
+    iCost = Abc_TgEnumerationCost(&tgMan);
+    if (p == NULL || p->nLastLevel == 0) {
+        if (nEnumThres > MaxCost || iCost < nEnumThres) {
             Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
             Abc_TgFullEnumeration(&tgManCopy, &tgMan);
         }
@@ -2208,8 +2607,7 @@ unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char
             Abc_TgSimpleEnumeration(&tgMan);
     }
     else {
-        iCost = Abc_TgEnumerationCost(&tgMan);
-        if (iCost < iEnumThres) fExac = 1 << 30;
+        if (nEnumThres > MaxCost || iCost < nEnumThres) fExac = 1 << 30;
         if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash + fExac;
         Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
         Abc_TgSimpleEnumeration(&tgMan);
@@ -2229,6 +2627,65 @@ unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char
     return tgMan.uPhase;
 }
 
+unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres)
+{
+    int nWords = Abc_TtWordNum(nVars);
+    unsigned fHard = 0, fHash = 1 << 29;
+    static word pCopy[1024];
+    Abc_TgMan_t tgMan, tgManCopy;
+    Abc_SccCost_t sc;
+
+    // handle constant
+    if (nVars == 0) {
+        Abc_TtClear(pTruth, nWords);
+        return 0;
+    }
+
+    Abc_TtVerifySmallTruth(pTruth, nVars);
+#ifdef CANON_VERIFY
+    Abc_TtCopy(gpVerCopy, pTruth, nWords, 0);
+#endif
+
+    assert(nVars <= 16);
+    assert(p != NULL);
+    if (Abc_TtHieRetrieveOrInsert(p, -5, pTruth, pTruth) > 0) return fHash;
+    Abc_TgInitMan(&tgMan, pTruth, nVars, 2, p->vPhase);
+
+    Abc_TgCreateGroups(&tgMan);
+    if (p && Abc_TtHieRetrieveOrInsert(p, -4, pTruth, pTruth) > 0) return fHash;
+    Abc_TgPurgeSymmetry(&tgMan, 1);
+
+    Abc_TgExpendSymmetry(&tgMan, pCanonPerm);
+    Abc_TgImplementPerm(&tgMan, pCanonPerm);
+    assert(Abc_TgCannonVerify(&tgMan));
+
+    if (Abc_TtHieRetrieveOrInsert(p, -3, pTruth, pTruth) > 0) return fHash;
+    Abc_TgManCopy(&tgManCopy, pCopy, &tgMan);
+    Abc_TgSimpleEnumeration(&tgMan);
+    if (Abc_TtHieRetrieveOrInsert(p, -2, pTruth, pTruth) > 0) return fHash;
+    Abc_TgManCopy(&tgMan, pTruth, &tgManCopy);
+    Abc_TtFill(pTruth, nWords);
+
+    assert(Abc_TgCannonVerify(&tgManCopy));
+    sc = Abc_TgRecordPhase(&tgManCopy, 0);
+    if (Abc_SccEnumCost(&tgManCopy, sc) > Abc_SccPhaseCost(&tgManCopy))
+    {
+        Abc_TgResetGroup(&tgManCopy);
+        sc = Abc_TgRecordPhase(&tgManCopy, 1);
+        fHard = 1 << 28;
+    }
+    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 | fHard;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////