Version abc50822

4 files changed, 1008 insertions, 3 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 92e631ad..d298a204 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -216,6 +216,10 @@ extern unsigned    Extra_TruthCanonNPN( unsigned uTruth, int nVars );
 extern void        Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
 extern void        Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax );
 /* permutation mapping */
+extern unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase );
+extern unsigned    Extra_TruthPerm5One( unsigned uTruth, int Phase );
+extern void        Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes );
+/* precomputing tables for permutation mapping */
 extern void **     Extra_ArrayAlloc( int nCols, int nRows, int Size );
 extern unsigned short ** Extra_TruthPerm43();
 extern unsigned ** Extra_TruthPerm53();
@@ -223,6 +227,11 @@ extern unsigned ** Extra_TruthPerm54();
 /* for independence from CUDD */
 extern unsigned int Cudd_PrimeCopy( unsigned int  p );
 
+/*=== extraUtilCanon.c ========================================================*/
+
+/* fast computation of N-canoninical form up to 6 inputs */
+extern int         Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes );
+
 /*=== extraUtilProgress.c ================================================================*/
 
 typedef struct ProgressBarStruct ProgressBar;
diff --git a/src/misc/extra/extraUtilCanon.c b/src/misc/extra/extraUtilCanon.c
new file mode 100644
index 00000000..9d4e5b5d
--- /dev/null
+++ b/src/misc/extra/extraUtilCanon.c
@@ -0,0 +1,699 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilMisc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Computing canonical forms of Boolean functions using truth tables.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+static unsigned s_Truths3[256];
+static char s_Phases3[256][9];
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag );
+
+/**AutomaticEnd***************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the N-canonical form of the Boolean function up to 6 inputs.]
+
+  Description [The N-canonical form is defined as the truth table with 
+  the minimum integer value. This function exhaustively enumerates 
+  through the complete set of 2^N phase assignments.
+  Returns pointers to the static storage to the truth table and phases. 
+  This data should be used before the function is called again.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes )
+{
+    static unsigned uTruthStore6[2];
+    int RetValue;
+    assert( nVarsMax <= 6 );
+    assert( nVarsReal <= nVarsMax );
+    RetValue = Extra_TruthCanonN_rec( nVarsReal <= 3? 3: nVarsReal, (unsigned char *)pt, pptRes, ppfRes, 0 );
+    if ( nVarsMax == 6 && nVarsReal < nVarsMax )
+    {
+        uTruthStore6[0] = **pptRes;
+        uTruthStore6[1] = **pptRes;
+        *pptRes = uTruthStore6;
+    }
+    return RetValue;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Recursive implementation of the above.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag )
+{
+    static unsigned uTruthStore[7][2][2];
+    static char uPhaseStore[7][2][64];
+
+    unsigned char * pt0, * pt1;
+    unsigned * ptRes0, * ptRes1, * ptRes;
+    unsigned uInit0, uInit1, uTruth0, uTruth1, uTemp;
+    char * pfRes0, * pfRes1, * pfRes;
+    int nf0, nf1, nfRes, i, nVarsN;
+
+    // table lookup for three vars
+    if ( nVars == 3 )
+    {
+        *pptRes = &s_Truths3[*pt];
+        *ppfRes = s_Phases3[*pt]+1;
+        return s_Phases3[*pt][0];
+    }
+
+    // number of vars for the next call
+    nVarsN = nVars-1;
+    // truth table for the next call
+    pt0 = pt;
+    pt1 = pt + (1 << nVarsN) / 8;
+    // 5-var truth tables for this call
+    uInit0 = *((unsigned *)pt0);
+    uInit1 = *((unsigned *)pt1);
+    if ( nVarsN == 3 )
+    {
+        uInit0 &= 0xFF;
+        uInit1 &= 0xFF;
+        uInit0 = (uInit0 << 24) | (uInit0 << 16) | (uInit0 << 8) | uInit0;
+        uInit1 = (uInit1 << 24) | (uInit1 << 16) | (uInit1 << 8) | uInit1;
+    }
+    else if ( nVarsN == 4 )
+    {
+        uInit0 &= 0xFFFF;
+        uInit1 &= 0xFFFF;
+        uInit0 = (uInit0 << 16) | uInit0;
+        uInit1 = (uInit1 << 16) | uInit1;
+    }
+
+    // storage for truth tables and phases
+    ptRes  = uTruthStore[nVars][Flag];
+    pfRes  = uPhaseStore[nVars][Flag];
+
+    // solve trivial cases
+    if ( uInit1 == 0 )
+    {
+        nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
+        uTruth1 = uInit1;
+        uTruth0 = *ptRes0;
+        nfRes   = 0;
+        for ( i = 0; i < nf0; i++ )
+            pfRes[nfRes++] = pfRes0[i];
+        goto finish;
+    }
+    if ( uInit0 == 0 )
+    {
+        nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
+        uTruth1 = uInit0;
+        uTruth0 = *ptRes1;
+        nfRes   = 0;
+        for ( i = 0; i < nf1; i++ )
+            pfRes[nfRes++] = pfRes1[i] | (1<<nVarsN);
+        goto finish;
+    }
+
+    if ( uInit1 == 0xFFFFFFFF )
+    {
+        nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
+        uTruth1 = *ptRes0;
+        uTruth0 = uInit1;
+        nfRes   = 0;
+        for ( i = 0; i < nf0; i++ )
+            pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+        goto finish;
+    }
+    if ( uInit0 == 0xFFFFFFFF )
+    {
+        nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
+        uTruth1 = *ptRes1;
+        uTruth0 = uInit0;
+        nfRes   = 0;
+        for ( i = 0; i < nf1; i++ )
+            pfRes[nfRes++] = pfRes1[i];
+        goto finish;
+    }
+
+    // solve the problem for cofactors
+    nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
+    nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
+
+    // combine the result
+    if ( *ptRes1 < *ptRes0 )
+    {
+        uTruth0 = 0xFFFFFFFF;
+        nfRes   = 0;
+        for ( i = 0; i < nf1; i++ )
+        {
+            uTemp = Extra_TruthPolarize( uInit0, pfRes1[i], nVarsN );
+            if ( uTruth0 > uTemp )
+            {
+                nfRes          = 0;
+                uTruth0        = uTemp;
+                pfRes[nfRes++] = pfRes1[i];
+            }
+            else if ( uTruth0 == uTemp ) 
+                pfRes[nfRes++] = pfRes1[i];
+        }
+        uTruth1 = *ptRes1;
+    }
+    else if ( *ptRes1 > *ptRes0 )
+    {
+        uTruth0 = 0xFFFFFFFF;
+        nfRes   = 0;
+        for ( i = 0; i < nf0; i++ )
+        {
+            uTemp = Extra_TruthPolarize( uInit1, pfRes0[i], nVarsN );
+            if ( uTruth0 > uTemp )
+            {
+                nfRes          = 0;
+                uTruth0        = uTemp;
+                pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+            }
+            else if ( uTruth0 == uTemp ) 
+                pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+        }
+        uTruth1 = *ptRes0;
+    }
+    else 
+    {
+        assert( nf0 == nf1 );
+        nfRes = 0; 
+        for ( i = 0; i < nf1; i++ )
+            pfRes[nfRes++] = pfRes1[i];
+        for ( i = 0; i < nf0; i++ )
+            pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+        uTruth0 = Extra_TruthPolarize( uInit0, pfRes1[0], nVarsN );
+        uTruth1 = *ptRes0;
+    }
+
+finish :
+    if ( nVarsN == 3 )
+    {
+        uTruth0 &= 0xFF;
+        uTruth1 &= 0xFF;
+        uTemp = (uTruth1 << 8) | uTruth0;
+        *ptRes = (uTemp << 16) | uTemp;
+    }
+    else if ( nVarsN == 4 )
+    {
+        uTruth0 &= 0xFFFF;
+        uTruth1 &= 0xFFFF;
+        *ptRes = (uTruth1 << 16) | uTruth0;
+    }
+    else if ( nVarsN == 5 )
+    {
+        *(ptRes+0) = uTruth0;
+        *(ptRes+1) = uTruth1;
+    }
+
+    *pptRes = ptRes;
+    *ppfRes = pfRes;
+    return nfRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_Var3Print()
+{
+    extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
+
+    unsigned * uCanons;
+    char ** uPhases;
+    char * pCounters;
+    int i, k;
+
+    Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
+
+    for ( i = 0; i < 256; i++ )
+    {
+        if ( i % 8 == 0 )
+            printf( "\n" );
+        Extra_PrintHex( stdout, uCanons[i], 5 ); 
+        printf( ", " );
+    }
+    printf( "\n" );
+
+    for ( i = 0; i < 256; i++ )
+    {
+        printf( "%3d */  { %2d,   ", i, pCounters[i] );
+        for ( k = 0; k < pCounters[i]; k++ )            
+            printf( "%s%d", k? ", ":"", uPhases[i][k] );
+        printf( " }\n" );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_Var3Test()
+{
+    extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
+
+    unsigned * uCanons;
+    char ** uPhases;
+    char * pCounters;
+    int i;
+    unsigned * ptRes;
+    char * pfRes;
+    unsigned uTruth;
+    int Count;
+
+    Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
+
+    for ( i = 0; i < 256; i++ )
+    {
+        uTruth = i;
+        Count =  Extra_TruthCanonFastN( 5, 3, &uTruth, &ptRes, &pfRes );
+        if ( *ptRes != uCanons[i] || Count != pCounters[i] )
+        {
+            int k = 0;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_Var4Test()
+{
+    extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int PhaseMax );
+
+    unsigned short * uCanons;
+    char ** uPhases;
+    char * pCounters;
+    int i, k;
+    unsigned * ptRes;
+    char * pfRes;
+    unsigned uTruth;
+    int Count;
+
+    Extra_Truth4VarN( &uCanons, &uPhases, &pCounters, 16 );
+
+    for ( i = 0; i < 256*256; i++ )
+    {
+        uTruth = i;
+        Count =  Extra_TruthCanonFastN( 5, 4, &uTruth, &ptRes, &pfRes );
+        if ( (*ptRes & 0xFFFF) != uCanons[i] || Count != pCounters[i] )
+        {
+            int k = 0;
+        }
+        for ( k = 0; k < Count; k++ )
+            if ( uPhases[i][k] != pfRes[k] )
+            {
+                int v = 0;
+            }
+    }
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+static unsigned s_Truths3[256] = 
+{
+    0x00000000, 0x01010101, 0x01010101, 0x03030303, 0x01010101, 0x05050505, 0x06060606, 0x07070707,
+    0x01010101, 0x06060606, 0x05050505, 0x07070707, 0x03030303, 0x07070707, 0x07070707, 0x0f0f0f0f,
+    0x01010101, 0x11111111, 0x12121212, 0x13131313, 0x14141414, 0x15151515, 0x16161616, 0x17171717,
+    0x18181818, 0x19191919, 0x1a1a1a1a, 0x1b1b1b1b, 0x1c1c1c1c, 0x1d1d1d1d, 0x1e1e1e1e, 0x1f1f1f1f,
+    0x01010101, 0x12121212, 0x11111111, 0x13131313, 0x18181818, 0x1a1a1a1a, 0x19191919, 0x1b1b1b1b,
+    0x14141414, 0x16161616, 0x15151515, 0x17171717, 0x1c1c1c1c, 0x1e1e1e1e, 0x1d1d1d1d, 0x1f1f1f1f,
+    0x03030303, 0x13131313, 0x13131313, 0x33333333, 0x1c1c1c1c, 0x35353535, 0x36363636, 0x37373737,
+    0x1c1c1c1c, 0x36363636, 0x35353535, 0x37373737, 0x3c3c3c3c, 0x3d3d3d3d, 0x3d3d3d3d, 0x3f3f3f3f,
+    0x01010101, 0x14141414, 0x18181818, 0x1c1c1c1c, 0x11111111, 0x15151515, 0x19191919, 0x1d1d1d1d,
+    0x12121212, 0x16161616, 0x1a1a1a1a, 0x1e1e1e1e, 0x13131313, 0x17171717, 0x1b1b1b1b, 0x1f1f1f1f,
+    0x05050505, 0x15151515, 0x1a1a1a1a, 0x35353535, 0x15151515, 0x55555555, 0x56565656, 0x57575757,
+    0x1a1a1a1a, 0x56565656, 0x5a5a5a5a, 0x5b5b5b5b, 0x35353535, 0x57575757, 0x5b5b5b5b, 0x5f5f5f5f,
+    0x06060606, 0x16161616, 0x19191919, 0x36363636, 0x19191919, 0x56565656, 0x66666666, 0x67676767,
+    0x16161616, 0x69696969, 0x56565656, 0x6b6b6b6b, 0x36363636, 0x6b6b6b6b, 0x67676767, 0x6f6f6f6f,
+    0x07070707, 0x17171717, 0x1b1b1b1b, 0x37373737, 0x1d1d1d1d, 0x57575757, 0x67676767, 0x77777777,
+    0x1e1e1e1e, 0x6b6b6b6b, 0x5b5b5b5b, 0x7b7b7b7b, 0x3d3d3d3d, 0x7d7d7d7d, 0x7e7e7e7e, 0x7f7f7f7f,
+    0x01010101, 0x18181818, 0x14141414, 0x1c1c1c1c, 0x12121212, 0x1a1a1a1a, 0x16161616, 0x1e1e1e1e,
+    0x11111111, 0x19191919, 0x15151515, 0x1d1d1d1d, 0x13131313, 0x1b1b1b1b, 0x17171717, 0x1f1f1f1f,
+    0x06060606, 0x19191919, 0x16161616, 0x36363636, 0x16161616, 0x56565656, 0x69696969, 0x6b6b6b6b,
+    0x19191919, 0x66666666, 0x56565656, 0x67676767, 0x36363636, 0x67676767, 0x6b6b6b6b, 0x6f6f6f6f,
+    0x05050505, 0x1a1a1a1a, 0x15151515, 0x35353535, 0x1a1a1a1a, 0x5a5a5a5a, 0x56565656, 0x5b5b5b5b,
+    0x15151515, 0x56565656, 0x55555555, 0x57575757, 0x35353535, 0x5b5b5b5b, 0x57575757, 0x5f5f5f5f,
+    0x07070707, 0x1b1b1b1b, 0x17171717, 0x37373737, 0x1e1e1e1e, 0x5b5b5b5b, 0x6b6b6b6b, 0x7b7b7b7b,
+    0x1d1d1d1d, 0x67676767, 0x57575757, 0x77777777, 0x3d3d3d3d, 0x7e7e7e7e, 0x7d7d7d7d, 0x7f7f7f7f,
+    0x03030303, 0x1c1c1c1c, 0x1c1c1c1c, 0x3c3c3c3c, 0x13131313, 0x35353535, 0x36363636, 0x3d3d3d3d,
+    0x13131313, 0x36363636, 0x35353535, 0x3d3d3d3d, 0x33333333, 0x37373737, 0x37373737, 0x3f3f3f3f,
+    0x07070707, 0x1d1d1d1d, 0x1e1e1e1e, 0x3d3d3d3d, 0x17171717, 0x57575757, 0x6b6b6b6b, 0x7d7d7d7d,
+    0x1b1b1b1b, 0x67676767, 0x5b5b5b5b, 0x7e7e7e7e, 0x37373737, 0x77777777, 0x7b7b7b7b, 0x7f7f7f7f,
+    0x07070707, 0x1e1e1e1e, 0x1d1d1d1d, 0x3d3d3d3d, 0x1b1b1b1b, 0x5b5b5b5b, 0x67676767, 0x7e7e7e7e,
+    0x17171717, 0x6b6b6b6b, 0x57575757, 0x7d7d7d7d, 0x37373737, 0x7b7b7b7b, 0x77777777, 0x7f7f7f7f,
+    0x0f0f0f0f, 0x1f1f1f1f, 0x1f1f1f1f, 0x3f3f3f3f, 0x1f1f1f1f, 0x5f5f5f5f, 0x6f6f6f6f, 0x7f7f7f7f,
+    0x1f1f1f1f, 0x6f6f6f6f, 0x5f5f5f5f, 0x7f7f7f7f, 0x3f3f3f3f, 0x7f7f7f7f, 0x7f7f7f7f, 0xffffffff
+};
+
+static char s_Phases3[256][9] = 
+{
+/*   0 */  {  8,   0, 1, 2, 3, 4, 5, 6, 7 }, 
+/*   1 */  {  1,   0 }, 
+/*   2 */  {  1,   1 }, 
+/*   3 */  {  2,   0, 1 }, 
+/*   4 */  {  1,   2 }, 
+/*   5 */  {  2,   0, 2 }, 
+/*   6 */  {  2,   0, 3 }, 
+/*   7 */  {  1,   0 }, 
+/*   8 */  {  1,   3 }, 
+/*   9 */  {  2,   1, 2 }, 
+/*  10 */  {  2,   1, 3 }, 
+/*  11 */  {  1,   1 }, 
+/*  12 */  {  2,   2, 3 }, 
+/*  13 */  {  1,   2 }, 
+/*  14 */  {  1,   3 }, 
+/*  15 */  {  4,   0, 1, 2, 3 }, 
+/*  16 */  {  1,   4 }, 
+/*  17 */  {  2,   0, 4 }, 
+/*  18 */  {  2,   0, 5 }, 
+/*  19 */  {  1,   0 }, 
+/*  20 */  {  2,   0, 6 }, 
+/*  21 */  {  1,   0 }, 
+/*  22 */  {  1,   0 }, 
+/*  23 */  {  1,   0 }, 
+/*  24 */  {  2,   0, 7 }, 
+/*  25 */  {  1,   0 }, 
+/*  26 */  {  1,   0 }, 
+/*  27 */  {  1,   0 }, 
+/*  28 */  {  1,   0 }, 
+/*  29 */  {  1,   0 }, 
+/*  30 */  {  1,   0 }, 
+/*  31 */  {  1,   0 }, 
+/*  32 */  {  1,   5 }, 
+/*  33 */  {  2,   1, 4 }, 
+/*  34 */  {  2,   1, 5 }, 
+/*  35 */  {  1,   1 }, 
+/*  36 */  {  2,   1, 6 }, 
+/*  37 */  {  1,   1 }, 
+/*  38 */  {  1,   1 }, 
+/*  39 */  {  1,   1 }, 
+/*  40 */  {  2,   1, 7 }, 
+/*  41 */  {  1,   1 }, 
+/*  42 */  {  1,   1 }, 
+/*  43 */  {  1,   1 }, 
+/*  44 */  {  1,   1 }, 
+/*  45 */  {  1,   1 }, 
+/*  46 */  {  1,   1 }, 
+/*  47 */  {  1,   1 }, 
+/*  48 */  {  2,   4, 5 }, 
+/*  49 */  {  1,   4 }, 
+/*  50 */  {  1,   5 }, 
+/*  51 */  {  4,   0, 1, 4, 5 }, 
+/*  52 */  {  1,   6 }, 
+/*  53 */  {  1,   0 }, 
+/*  54 */  {  1,   0 }, 
+/*  55 */  {  1,   0 }, 
+/*  56 */  {  1,   7 }, 
+/*  57 */  {  1,   1 }, 
+/*  58 */  {  1,   1 }, 
+/*  59 */  {  1,   1 }, 
+/*  60 */  {  4,   0, 1, 6, 7 }, 
+/*  61 */  {  1,   0 }, 
+/*  62 */  {  1,   1 }, 
+/*  63 */  {  2,   0, 1 }, 
+/*  64 */  {  1,   6 }, 
+/*  65 */  {  2,   2, 4 }, 
+/*  66 */  {  2,   2, 5 }, 
+/*  67 */  {  1,   2 }, 
+/*  68 */  {  2,   2, 6 }, 
+/*  69 */  {  1,   2 }, 
+/*  70 */  {  1,   2 }, 
+/*  71 */  {  1,   2 }, 
+/*  72 */  {  2,   2, 7 }, 
+/*  73 */  {  1,   2 }, 
+/*  74 */  {  1,   2 }, 
+/*  75 */  {  1,   2 }, 
+/*  76 */  {  1,   2 }, 
+/*  77 */  {  1,   2 }, 
+/*  78 */  {  1,   2 }, 
+/*  79 */  {  1,   2 }, 
+/*  80 */  {  2,   4, 6 }, 
+/*  81 */  {  1,   4 }, 
+/*  82 */  {  1,   5 }, 
+/*  83 */  {  1,   4 }, 
+/*  84 */  {  1,   6 }, 
+/*  85 */  {  4,   0, 2, 4, 6 }, 
+/*  86 */  {  1,   0 }, 
+/*  87 */  {  1,   0 }, 
+/*  88 */  {  1,   7 }, 
+/*  89 */  {  1,   2 }, 
+/*  90 */  {  4,   0, 2, 5, 7 }, 
+/*  91 */  {  1,   0 }, 
+/*  92 */  {  1,   6 }, 
+/*  93 */  {  1,   2 }, 
+/*  94 */  {  1,   2 }, 
+/*  95 */  {  2,   0, 2 }, 
+/*  96 */  {  2,   4, 7 }, 
+/*  97 */  {  1,   4 }, 
+/*  98 */  {  1,   5 }, 
+/*  99 */  {  1,   4 }, 
+/* 100 */  {  1,   6 }, 
+/* 101 */  {  1,   4 }, 
+/* 102 */  {  4,   0, 3, 4, 7 }, 
+/* 103 */  {  1,   0 }, 
+/* 104 */  {  1,   7 }, 
+/* 105 */  {  4,   0, 3, 5, 6 }, 
+/* 106 */  {  1,   7 }, 
+/* 107 */  {  1,   0 }, 
+/* 108 */  {  1,   7 }, 
+/* 109 */  {  1,   3 }, 
+/* 110 */  {  1,   3 }, 
+/* 111 */  {  2,   0, 3 }, 
+/* 112 */  {  1,   4 }, 
+/* 113 */  {  1,   4 }, 
+/* 114 */  {  1,   5 }, 
+/* 115 */  {  1,   4 }, 
+/* 116 */  {  1,   6 }, 
+/* 117 */  {  1,   4 }, 
+/* 118 */  {  1,   4 }, 
+/* 119 */  {  2,   0, 4 }, 
+/* 120 */  {  1,   7 }, 
+/* 121 */  {  1,   5 }, 
+/* 122 */  {  1,   5 }, 
+/* 123 */  {  2,   0, 5 }, 
+/* 124 */  {  1,   6 }, 
+/* 125 */  {  2,   0, 6 }, 
+/* 126 */  {  2,   0, 7 }, 
+/* 127 */  {  1,   0 }, 
+/* 128 */  {  1,   7 }, 
+/* 129 */  {  2,   3, 4 }, 
+/* 130 */  {  2,   3, 5 }, 
+/* 131 */  {  1,   3 }, 
+/* 132 */  {  2,   3, 6 }, 
+/* 133 */  {  1,   3 }, 
+/* 134 */  {  1,   3 }, 
+/* 135 */  {  1,   3 }, 
+/* 136 */  {  2,   3, 7 }, 
+/* 137 */  {  1,   3 }, 
+/* 138 */  {  1,   3 }, 
+/* 139 */  {  1,   3 }, 
+/* 140 */  {  1,   3 }, 
+/* 141 */  {  1,   3 }, 
+/* 142 */  {  1,   3 }, 
+/* 143 */  {  1,   3 }, 
+/* 144 */  {  2,   5, 6 }, 
+/* 145 */  {  1,   4 }, 
+/* 146 */  {  1,   5 }, 
+/* 147 */  {  1,   5 }, 
+/* 148 */  {  1,   6 }, 
+/* 149 */  {  1,   6 }, 
+/* 150 */  {  4,   1, 2, 4, 7 }, 
+/* 151 */  {  1,   1 }, 
+/* 152 */  {  1,   7 }, 
+/* 153 */  {  4,   1, 2, 5, 6 }, 
+/* 154 */  {  1,   5 }, 
+/* 155 */  {  1,   1 }, 
+/* 156 */  {  1,   6 }, 
+/* 157 */  {  1,   2 }, 
+/* 158 */  {  1,   2 }, 
+/* 159 */  {  2,   1, 2 }, 
+/* 160 */  {  2,   5, 7 }, 
+/* 161 */  {  1,   4 }, 
+/* 162 */  {  1,   5 }, 
+/* 163 */  {  1,   5 }, 
+/* 164 */  {  1,   6 }, 
+/* 165 */  {  4,   1, 3, 4, 6 }, 
+/* 166 */  {  1,   3 }, 
+/* 167 */  {  1,   1 }, 
+/* 168 */  {  1,   7 }, 
+/* 169 */  {  1,   1 }, 
+/* 170 */  {  4,   1, 3, 5, 7 }, 
+/* 171 */  {  1,   1 }, 
+/* 172 */  {  1,   7 }, 
+/* 173 */  {  1,   3 }, 
+/* 174 */  {  1,   3 }, 
+/* 175 */  {  2,   1, 3 }, 
+/* 176 */  {  1,   5 }, 
+/* 177 */  {  1,   4 }, 
+/* 178 */  {  1,   5 }, 
+/* 179 */  {  1,   5 }, 
+/* 180 */  {  1,   6 }, 
+/* 181 */  {  1,   4 }, 
+/* 182 */  {  1,   4 }, 
+/* 183 */  {  2,   1, 4 }, 
+/* 184 */  {  1,   7 }, 
+/* 185 */  {  1,   5 }, 
+/* 186 */  {  1,   5 }, 
+/* 187 */  {  2,   1, 5 }, 
+/* 188 */  {  1,   7 }, 
+/* 189 */  {  2,   1, 6 }, 
+/* 190 */  {  2,   1, 7 }, 
+/* 191 */  {  1,   1 }, 
+/* 192 */  {  2,   6, 7 }, 
+/* 193 */  {  1,   4 }, 
+/* 194 */  {  1,   5 }, 
+/* 195 */  {  4,   2, 3, 4, 5 }, 
+/* 196 */  {  1,   6 }, 
+/* 197 */  {  1,   2 }, 
+/* 198 */  {  1,   3 }, 
+/* 199 */  {  1,   2 }, 
+/* 200 */  {  1,   7 }, 
+/* 201 */  {  1,   2 }, 
+/* 202 */  {  1,   3 }, 
+/* 203 */  {  1,   3 }, 
+/* 204 */  {  4,   2, 3, 6, 7 }, 
+/* 205 */  {  1,   2 }, 
+/* 206 */  {  1,   3 }, 
+/* 207 */  {  2,   2, 3 }, 
+/* 208 */  {  1,   6 }, 
+/* 209 */  {  1,   4 }, 
+/* 210 */  {  1,   5 }, 
+/* 211 */  {  1,   4 }, 
+/* 212 */  {  1,   6 }, 
+/* 213 */  {  1,   6 }, 
+/* 214 */  {  1,   7 }, 
+/* 215 */  {  2,   2, 4 }, 
+/* 216 */  {  1,   7 }, 
+/* 217 */  {  1,   6 }, 
+/* 218 */  {  1,   7 }, 
+/* 219 */  {  2,   2, 5 }, 
+/* 220 */  {  1,   6 }, 
+/* 221 */  {  2,   2, 6 }, 
+/* 222 */  {  2,   2, 7 }, 
+/* 223 */  {  1,   2 }, 
+/* 224 */  {  1,   7 }, 
+/* 225 */  {  1,   4 }, 
+/* 226 */  {  1,   5 }, 
+/* 227 */  {  1,   5 }, 
+/* 228 */  {  1,   6 }, 
+/* 229 */  {  1,   6 }, 
+/* 230 */  {  1,   7 }, 
+/* 231 */  {  2,   3, 4 }, 
+/* 232 */  {  1,   7 }, 
+/* 233 */  {  1,   6 }, 
+/* 234 */  {  1,   7 }, 
+/* 235 */  {  2,   3, 5 }, 
+/* 236 */  {  1,   7 }, 
+/* 237 */  {  2,   3, 6 }, 
+/* 238 */  {  2,   3, 7 }, 
+/* 239 */  {  1,   3 }, 
+/* 240 */  {  4,   4, 5, 6, 7 }, 
+/* 241 */  {  1,   4 }, 
+/* 242 */  {  1,   5 }, 
+/* 243 */  {  2,   4, 5 }, 
+/* 244 */  {  1,   6 }, 
+/* 245 */  {  2,   4, 6 }, 
+/* 246 */  {  2,   4, 7 }, 
+/* 247 */  {  1,   4 }, 
+/* 248 */  {  1,   7 }, 
+/* 249 */  {  2,   5, 6 }, 
+/* 250 */  {  2,   5, 7 }, 
+/* 251 */  {  1,   5 }, 
+/* 252 */  {  2,   6, 7 }, 
+/* 253 */  {  1,   6 }, 
+/* 254 */  {  1,   7 }, 
+/* 255 */  {  8,   0, 1, 2, 3, 4, 5, 6, 7 }
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 2767498b..a12fbce4 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -429,8 +429,6 @@ unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
             uCof1 >>= Shift;
             uTruth = uCof0 | uCof1;
         }
-    if ( nVars < 5 )
-        uTruth &= ((~0) >> (32-nMints));
     return uTruth;
 }
 
@@ -752,6 +750,74 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
   SeeAlso     []
 
 ***********************************************************************/
+void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters )
+{
+    int nPhasesMax = 8;
+    unsigned * uCanons;
+    unsigned uTruth, uPhase, uTruth32;
+    char ** uPhases, * pCounters;
+    int nFuncs, nClasses, i;
+
+    nFuncs  = (1 << 8);
+    uCanons = ALLOC( unsigned, nFuncs );
+    memset( uCanons, 0, sizeof(unsigned) * nFuncs );
+    pCounters = ALLOC( char, nFuncs );
+    memset( pCounters, 0, sizeof(char) * nFuncs );
+    uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
+    nClasses = 0;
+    for ( uTruth = 0; uTruth < (unsigned)nFuncs; uTruth++ )
+    {
+        // skip already assigned
+        uTruth32 = ((uTruth << 24) | (uTruth << 16) | (uTruth << 8) | uTruth);
+        if ( uCanons[uTruth] )
+        {
+            assert( uTruth32 > uCanons[uTruth] );
+            continue;
+        }
+        nClasses++;
+        for ( i = 0; i < 8; i++ )
+        {
+            uPhase = Extra_TruthPolarize( uTruth, i, 3 );
+            if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
+            {
+                uCanons[uPhase]    = uTruth32;
+                uPhases[uPhase][0] = i;
+                pCounters[uPhase]  = 1;
+            }
+            else
+            {
+                assert( uCanons[uPhase] == uTruth32 );
+                if ( pCounters[uPhase] < nPhasesMax )
+                    uPhases[uPhase][ pCounters[uPhase]++ ] = i;
+            }
+        }
+    }
+    if ( puCanons ) 
+        *puCanons = uCanons;
+    else
+        free( uCanons );
+    if ( puPhases ) 
+        *puPhases = uPhases;
+    else
+        free( uPhases );
+    if ( ppCounters ) 
+        *ppCounters = pCounters;
+    else
+        free( pCounters );
+    printf( "The number of 3N-classes = %d.\n", nClasses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes NPN canonical forms for 4-variable functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax )
 {
     unsigned short * uCanons;
@@ -778,7 +844,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
         for ( i = 0; i < 16; i++ )
         {
             uPhase = Extra_TruthPolarize( uTruth, i, 4 );
-            if ( uCanons[uPhase] == 0 )
+            if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
             {
                 uCanons[uPhase]    = uTruth;
                 uPhases[uPhase][0] = i;
@@ -804,6 +870,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
         *ppCounters = pCounters;
     else
         free( pCounters );
+    printf( "The number of 4N-classes = %d.\n", nClasses );
 }
 
 /**Function*************************************************************
@@ -1005,6 +1072,208 @@ unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes a phase of the 3-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes )
+{
+    // cases
+    static unsigned Cases[64] = {
+        0,          // 000000  - skip
+        0,          // 000001  - skip
+        0xCCCCCCCC, // 000010  - single var
+        0,          // 000011  - skip
+        0xF0F0F0F0, // 000100  - single var
+        1,          // 000101
+        1,          // 000110
+        0,          // 000111  - skip
+        0xFF00FF00, // 001000  - single var
+        1,          // 001001
+        1,          // 001010
+        1,          // 001011
+        1,          // 001100
+        1,          // 001101
+        1,          // 001110
+        0,          // 001111  - skip
+        0xFFFF0000, // 010000  - skip
+        1,          // 010001
+        1,          // 010010
+        1,          // 010011
+        1,          // 010100
+        1,          // 010101
+        1,          // 010110
+        1,          // 010111  - four var
+        1,          // 011000
+        1,          // 011001
+        1,          // 011010
+        1,          // 011011  - four var
+        1,          // 011100
+        1,          // 011101  - four var
+        1,          // 011110  - four var
+        0,          // 011111  - skip
+        0xFFFFFFFF, // 100000  - single var
+        1,          // 100001 
+        1,          // 100010  
+        1,          // 100011  
+        1,          // 100100  
+        1,          // 100101
+        1,          // 100110
+        1,          // 100111  
+        1,          // 101000  
+        1,          // 101001
+        1,          // 101010
+        1,          // 101011
+        1,          // 101100
+        1,          // 101101
+        1,          // 101110
+        1,          // 101111  
+        1,          // 110000  
+        1,          // 110001
+        1,          // 110010
+        1,          // 110011
+        1,          // 110100
+        1,          // 110101
+        1,          // 110110
+        1,          // 110111  
+        1,          // 111000
+        1,          // 111001
+        1,          // 111010
+        1,          // 111011  
+        1,          // 111100
+        1,          // 111101  
+        1,          // 111110  
+        0           // 111111  - skip
+    };
+    // permutations
+    static int Perms[64][6] = {
+        { 0, 0, 0, 0, 0, 0 }, // 000000  - skip
+        { 0, 0, 0, 0, 0, 0 }, // 000001  - skip
+        { 0, 0, 0, 0, 0, 0 }, // 000010  - single var
+        { 0, 0, 0, 0, 0, 0 }, // 000011  - skip
+        { 0, 0, 0, 0, 0, 0 }, // 000100  - single var
+        { 0, 2, 1, 3, 4, 5 }, // 000101
+        { 2, 0, 1, 3, 4, 5 }, // 000110
+        { 0, 0, 0, 0, 0, 0 }, // 000111  - skip
+        { 0, 0, 0, 0, 0, 0 }, // 001000  - single var
+        { 0, 2, 3, 1, 4, 5 }, // 001001
+        { 2, 0, 3, 1, 4, 5 }, // 001010
+        { 0, 1, 3, 2, 4, 5 }, // 001011
+        { 2, 3, 0, 1, 4, 5 }, // 001100
+        { 0, 3, 1, 2, 4, 5 }, // 001101
+        { 3, 0, 1, 2, 4, 5 }, // 001110
+        { 0, 0, 0, 0, 0, 0 }, // 001111  - skip
+        { 0, 0, 0, 0, 0, 0 }, // 010000  - skip
+        { 0, 4, 2, 3, 1, 5 }, // 010001
+        { 4, 0, 2, 3, 1, 5 }, // 010010
+        { 0, 1, 3, 4, 2, 5 }, // 010011
+        { 2, 3, 0, 4, 1, 5 }, // 010100
+        { 0, 3, 1, 4, 2, 5 }, // 010101
+        { 3, 0, 1, 4, 2, 5 }, // 010110
+        { 0, 1, 2, 4, 3, 5 }, // 010111  - four var
+        { 2, 3, 4, 0, 1, 5 }, // 011000
+        { 0, 3, 4, 1, 2, 5 }, // 011001
+        { 3, 0, 4, 1, 2, 5 }, // 011010
+        { 0, 1, 4, 2, 3, 5 }, // 011011  - four var
+        { 3, 4, 0, 1, 2, 5 }, // 011100
+        { 0, 4, 1, 2, 3, 5 }, // 011101  - four var
+        { 4, 0, 1, 2, 3, 5 }, // 011110  - four var
+        { 0, 0, 0, 0, 0, 0 }, // 011111  - skip
+        { 0, 0, 0, 0, 0, 0 }, // 100000  - single var
+        { 0, 2, 3, 4, 5, 1 }, // 100001 
+        { 2, 0, 3, 4, 5, 1 }, // 100010  
+        { 0, 1, 3, 4, 5, 2 }, // 100011  
+        { 2, 3, 0, 4, 5, 1 }, // 100100  
+        { 0, 3, 1, 4, 5, 2 }, // 100101
+        { 3, 0, 1, 4, 5, 2 }, // 100110
+        { 0, 1, 2, 4, 5, 3 }, // 100111  
+        { 2, 3, 4, 0, 5, 1 }, // 101000  
+        { 0, 3, 4, 1, 5, 2 }, // 101001
+        { 3, 0, 4, 1, 5, 2 }, // 101010
+        { 0, 1, 4, 2, 5, 3 }, // 101011
+        { 3, 4, 0, 1, 5, 2 }, // 101100
+        { 0, 4, 1, 2, 5, 3 }, // 101101
+        { 4, 0, 1, 2, 5, 3 }, // 101110
+        { 0, 1, 2, 3, 5, 4 }, // 101111  
+        { 2, 3, 4, 5, 0, 1 }, // 110000  
+        { 0, 3, 4, 5, 1, 2 }, // 110001
+        { 3, 0, 4, 5, 1, 2 }, // 110010
+        { 0, 1, 4, 5, 2, 3 }, // 110011
+        { 3, 4, 0, 5, 1, 2 }, // 110100
+        { 0, 4, 1, 5, 2, 3 }, // 110101
+        { 4, 0, 1, 5, 2, 3 }, // 110110
+        { 0, 1, 2, 5, 3, 4 }, // 110111  
+        { 3, 4, 5, 0, 1, 2 }, // 111000
+        { 0, 4, 5, 1, 2, 3 }, // 111001
+        { 4, 0, 5, 1, 2, 3 }, // 111010
+        { 0, 1, 5, 2, 3, 4 }, // 111011  
+        { 4, 5, 0, 1, 2, 3 }, // 111100
+        { 0, 5, 1, 2, 3, 4 }, // 111101  
+        { 5, 0, 1, 2, 3, 4 }, // 111110  
+        { 0, 0, 0, 0, 0, 0 }  // 111111  - skip
+    };
+    int i, k, iRes;
+    assert( Phase >= 0 && Phase < 64 );
+    if ( Cases[Phase] == 0 )
+    {
+        uTruthRes[0] = uTruth[0];
+        uTruthRes[1] = uTruth[1];
+        return;
+    }
+    if ( Cases[Phase] > 1 )
+    {
+        if ( Phase == 32 )
+        {
+            uTruthRes[0] = 0x00000000;
+            uTruthRes[1] = 0xFFFFFFFF;
+        }
+        else
+        {
+            uTruthRes[0] = Cases[Phase];
+            uTruthRes[1] = Cases[Phase];
+        }
+        return;
+    }
+    uTruthRes[0] = 0;
+    uTruthRes[1] = 0;
+    for ( i = 0; i < 64; i++ )
+    {
+        if ( i < 32 )
+        {
+            if ( uTruth[0] & (1 << i) )
+            {
+                for ( iRes = 0, k = 0; k < 6; k++ )
+                    if ( i & (1 << Perms[Phase][k]) )
+                        iRes |= (1 << k);
+                if ( iRes < 32 )
+                    uTruthRes[0] |= (1 << iRes);
+                else
+                    uTruthRes[1] |= (1 << (iRes-32));
+            }
+        }
+        else
+        {
+            if ( uTruth[1] & (1 << (i-32)) )
+            {
+                for ( iRes = 0, k = 0; k < 6; k++ )
+                    if ( i & (1 << Perms[Phase][k]) )
+                        iRes |= (1 << k);
+                if ( iRes < 32 )
+                    uTruthRes[0] |= (1 << iRes);
+                else
+                    uTruthRes[1] |= (1 << (iRes-32));
+            }
+        }
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocated lookup table for truth table permutation.]
 
   Description []
@@ -1085,6 +1354,33 @@ unsigned ** Extra_TruthPerm54()
 
 /**Function*************************************************************
 
+  Synopsis    [Allocated lookup table for truth table permutation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned ** Extra_TruthPerm63()
+{
+    unsigned ** pTable;
+    unsigned uTruth[2];
+    int i, k;
+    pTable = (unsigned **)Extra_ArrayAlloc( 256, 64, 8 );
+    for ( i = 0; i < 256; i++ )
+    {
+        uTruth[0] = (i << 24) | (i << 16) | (i << 8) | i;
+        uTruth[1] = uTruth[0];
+        for ( k = 0; k < 64; k++ )
+            Extra_TruthPerm6One( uTruth, k, &pTable[i][k] );
+    }
+    return pTable;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the smallest prime larger than the number.]
 
   Description []
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index bfc9d0ad..3098a23c 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/misc/extra/extraUtilBdd.c \
     src/misc/extra/extraUtilBitMatrix.c \
+    src/misc/extra/extraUtilCanon.c \
     src/misc/extra/extraUtilFile.c \
     src/misc/extra/extraUtilMemory.c \
     src/misc/extra/extraUtilMisc.c \