Version abc50819

1 files changed, 383 insertions, 35 deletions

diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index ccd871e4..2767498b 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -246,15 +246,10 @@ char ** Extra_Permutations( int n )
 {
     char Array[50];
     char ** pRes;
-    char * pBuffer;
     int nFact, i;
-    // allocate all memory at once
-    nFact   = Extra_Factorial( n );
-    pBuffer = ALLOC( char, nFact * sizeof(char *) + nFact * n * sizeof(char) );
-    // split the chunk
-    pRes = (char **)pBuffer;
-    for ( i = 0; i < nFact; i++ )
-        pRes[i] = pBuffer + nFact * sizeof(char *) + i * n * sizeof(char);
+    // allocate memory
+    nFact = Extra_Factorial( n );
+    pRes  = (char **)Extra_ArrayAlloc( nFact, n, sizeof(char) );
     // fill in the permutations
     for ( i = 0; i < n; i++ )
         Array[i] = i;
@@ -290,7 +285,7 @@ void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
 {
     char ** pNext;
     int nFactNext;
-    int iTemp, iCur, iLast, p;
+    int iTemp, iCur, iLast, k;
 
     if ( n == 1 )
     {
@@ -314,8 +309,8 @@ void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
         pNext = pRes + (n - 1 - iCur) * nFactNext;
 
         // set the last entry 
-        for ( p = 0; p < nFactNext; p++ )
-            pNext[p][iLast] = Array[iLast];
+        for ( k = 0; k < nFactNext; k++ )
+            pNext[k][iLast] = Array[iLast];
 
         // call recursively for this part
         Extra_Permutations_rec( pNext, nFactNext, n - 1, Array );
@@ -453,12 +448,12 @@ unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
 unsigned Extra_TruthCanonN( unsigned uTruth, int nVars )
 {
     unsigned uTruthMin, uPhase;
-    int nMints, p;
+    int nMints, i;
     nMints    = (1 << nVars);
     uTruthMin = 0xFFFFFFFF;
-    for ( p = 0; p < nMints; p++ )
+    for ( i = 0; i < nMints; i++ )
     {
-        uPhase = Extra_TruthPolarize( uTruth, p, nVars ); 
+        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
         if ( uTruthMin > uPhase )
             uTruthMin = uPhase;
     }
@@ -479,16 +474,16 @@ unsigned Extra_TruthCanonN( unsigned uTruth, int nVars )
 unsigned Extra_TruthCanonNN( unsigned uTruth, int nVars )
 {
     unsigned uTruthMin, uTruthC, uPhase;
-    int nMints, p;
+    int nMints, i;
     nMints    = (1 << nVars);
     uTruthC   = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
     uTruthMin = 0xFFFFFFFF;
-    for ( p = 0; p < nMints; p++ )
+    for ( i = 0; i < nMints; i++ )
     {
-        uPhase = Extra_TruthPolarize( uTruth, p, nVars ); 
+        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
         if ( uTruthMin > uPhase )
             uTruthMin = uPhase;
-        uPhase = Extra_TruthPolarize( uTruthC, p, nVars ); 
+        uPhase = Extra_TruthPolarize( uTruthC, i, nVars ); 
         if ( uTruthMin > uPhase )
             uTruthMin = uPhase;
     }
@@ -555,7 +550,7 @@ unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
     static char ** pPerms = NULL;
 
     unsigned uTruthMin, uPhase, uPerm;
-    int nMints, k, p;
+    int nMints, k, i;
 
     if ( pPerms == NULL )
     {
@@ -573,9 +568,9 @@ unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
 
     nMints    = (1 << nVars);
     uTruthMin = 0xFFFFFFFF;
-    for ( p = 0; p < nMints; p++ )
+    for ( i = 0; i < nMints; i++ )
     {
-        uPhase = Extra_TruthPolarize( uTruth, p, nVars ); 
+        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
         for ( k = 0; k < nPerms; k++ )
         {
             uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
@@ -603,7 +598,7 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
     static char ** pPerms = NULL;
 
     unsigned uTruthMin, uTruthC, uPhase, uPerm;
-    int nMints, k, p;
+    int nMints, k, i;
 
     if ( pPerms == NULL )
     {
@@ -622,16 +617,16 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
     nMints    = (1 << nVars);
     uTruthC   = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
     uTruthMin = 0xFFFFFFFF;
-    for ( p = 0; p < nMints; p++ )
+    for ( i = 0; i < nMints; i++ )
     {
-        uPhase = Extra_TruthPolarize( uTruth, p, nVars ); 
+        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
         for ( k = 0; k < nPerms; k++ )
         {
             uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
             if ( uTruthMin > uPerm )
                 uTruthMin = uPerm;
         }
-        uPhase = Extra_TruthPolarize( uTruthC, p, nVars ); 
+        uPhase = Extra_TruthPolarize( uTruthC, i, nVars ); 
         for ( k = 0; k < nPerms; k++ )
         {
             uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
@@ -653,21 +648,24 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms )
+void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap )
 {
     unsigned short * uCanons;
+    unsigned char * uMap;
     unsigned uTruth, uPhase, uPerm;
     char ** pPerms4, * uPhases, * uPerms;
     int nFuncs, nClasses;
-    int p, k;
+    int i, k;
 
     nFuncs  = (1 << 16);
     uCanons = ALLOC( unsigned short, nFuncs );
     uPhases = ALLOC( char, nFuncs );
     uPerms  = ALLOC( char, nFuncs );
+    uMap    = ALLOC( unsigned char, nFuncs );
     memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
     memset( uPhases, 0, sizeof(char) * nFuncs );
     memset( uPerms,  0, sizeof(char) * nFuncs );
+    memset( uMap,    0, sizeof(unsigned char) * nFuncs );
     pPerms4 = Extra_Permutations( 4 );
 
     nClasses = 1;
@@ -676,41 +674,45 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
     {
         // skip already assigned
         if ( uCanons[uTruth] )
+        {
+            assert( uTruth > uCanons[uTruth] );
+            uMap[uTruth] = uMap[uCanons[uTruth]];
             continue;
-        nClasses++;
-        for ( p = 0; p < 16; p++ )
+        }
+        uMap[uTruth] = nClasses++;
+        for ( i = 0; i < 16; i++ )
         {
-            uPhase = Extra_TruthPolarize( uTruth, p, 4 );
+            uPhase = Extra_TruthPolarize( uTruth, i, 4 );
             for ( k = 0; k < 24; k++ )
             {
                 uPerm = Extra_TruthPermute( uPhase, pPerms4[k], 4, 0 );
                 if ( uCanons[uPerm] == 0 )
                 {
                     uCanons[uPerm] = uTruth;
-                    uPhases[uPerm] = p;
+                    uPhases[uPerm] = i;
                     uPerms[uPerm]  = k;
 
                     uPerm = ~uPerm & 0xFFFF;
                     uCanons[uPerm] = uTruth;
-                    uPhases[uPerm] = p | 16;
+                    uPhases[uPerm] = i | 16;
                     uPerms[uPerm]  = k;
                 }
                 else
                     assert( uCanons[uPerm] == uTruth );
             }
-            uPhase = Extra_TruthPolarize( ~uTruth & 0xFFFF, p, 4 ); 
+            uPhase = Extra_TruthPolarize( ~uTruth & 0xFFFF, i, 4 ); 
             for ( k = 0; k < 24; k++ )
             {
                 uPerm = Extra_TruthPermute( uPhase, pPerms4[k], 4, 0 );
                 if ( uCanons[uPerm] == 0 )
                 {
                     uCanons[uPerm] = uTruth;
-                    uPhases[uPerm] = p;
+                    uPhases[uPerm] = i;
                     uPerms[uPerm]  = k;
 
                     uPerm = ~uPerm & 0xFFFF;
                     uCanons[uPerm] = uTruth;
-                    uPhases[uPerm] = p | 16;
+                    uPhases[uPerm] = i | 16;
                     uPerms[uPerm]  = k;
                 }
                 else
@@ -733,6 +735,352 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
         *puPerms = uPerms;
     else
         free( uPerms );
+    if ( puMap ) 
+        *puMap = uMap;
+    else
+        free( uMap );
+}
+
+/**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;
+    unsigned uTruth, uPhase;
+    char ** uPhases, * pCounters;
+    int nFuncs, nClasses, i;
+
+    nFuncs  = (1 << 16);
+    uCanons = ALLOC( unsigned short, nFuncs );
+    memset( uCanons, 0, sizeof(unsigned short) * 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
+        if ( uCanons[uTruth] )
+        {
+            assert( uTruth > uCanons[uTruth] );
+            continue;
+        }
+        nClasses++;
+        for ( i = 0; i < 16; i++ )
+        {
+            uPhase = Extra_TruthPolarize( uTruth, i, 4 );
+            if ( uCanons[uPhase] == 0 )
+            {
+                uCanons[uPhase]    = uTruth;
+                uPhases[uPhase][0] = i;
+                pCounters[uPhase]  = 1;
+            }
+            else
+            {
+                assert( uCanons[uPhase] == uTruth );
+                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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocated one-memory-chunk array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void ** Extra_ArrayAlloc( int nCols, int nRows, int Size )
+{
+    char ** pRes;
+    char * pBuffer;
+    int i;
+    assert( nCols > 0 && nRows > 0 && Size > 0 );
+    pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
+    pRes = (char **)pBuffer;
+    pRes[0] = pBuffer + nCols * sizeof(void *);
+    for ( i = 1; i < nCols; i++ )
+        pRes[i] = pRes[0] + i * nRows * Size;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a phase of the 3-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase )
+{
+    // cases
+    static unsigned short Cases[16] = {
+        0,      // 0000  - skip
+        0,      // 0001  - skip
+        0xCCCC, // 0010  - single var
+        0,      // 0011  - skip
+        0xF0F0, // 0100  - single var
+        1,      // 0101
+        1,      // 0110
+        0,      // 0111  - skip
+        0xFF00, // 1000  - single var
+        1,      // 1001
+        1,      // 1010
+        1,      // 1011
+        1,      // 1100
+        1,      // 1101
+        1,      // 1110
+        0       // 1111  - skip
+    };
+    // permutations
+    static int Perms[16][4] = {
+        { 0, 0, 0, 0 }, // 0000  - skip
+        { 0, 0, 0, 0 }, // 0001  - skip
+        { 0, 0, 0, 0 }, // 0010  - single var
+        { 0, 0, 0, 0 }, // 0011  - skip
+        { 0, 0, 0, 0 }, // 0100  - single var
+        { 0, 2, 1, 3 }, // 0101
+        { 2, 0, 1, 3 }, // 0110
+        { 0, 0, 0, 0 }, // 0111  - skip
+        { 0, 0, 0, 0 }, // 1000  - single var
+        { 0, 2, 3, 1 }, // 1001
+        { 2, 0, 3, 1 }, // 1010
+        { 0, 1, 3, 2 }, // 1011
+        { 2, 3, 0, 1 }, // 1100
+        { 0, 3, 1, 2 }, // 1101
+        { 3, 0, 1, 2 }, // 1110
+        { 0, 0, 0, 0 }  // 1111  - skip
+    };
+    int i, k, iRes;
+    unsigned uTruthRes;
+    assert( Phase >= 0 && Phase < 16 );
+    if ( Cases[Phase] == 0 )
+        return uTruth;
+    if ( Cases[Phase] > 1 )
+        return Cases[Phase];
+    uTruthRes = 0;
+    for ( i = 0; i < 16; i++ )
+        if ( uTruth & (1 << i) )
+        {
+            for ( iRes = 0, k = 0; k < 4; k++ )
+                if ( i & (1 << Perms[Phase][k]) )
+                    iRes |= (1 << k);
+            uTruthRes |= (1 << iRes);
+        }
+    return uTruthRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a phase of the 3-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase )
+{
+    // cases
+    static unsigned Cases[32] = {
+        0,          // 00000  - skip
+        0,          // 00001  - skip
+        0xCCCCCCCC, // 00010  - single var
+        0,          // 00011  - skip
+        0xF0F0F0F0, // 00100  - single var
+        1,          // 00101
+        1,          // 00110
+        0,          // 00111  - skip
+        0xFF00FF00, // 01000  - single var
+        1,          // 01001
+        1,          // 01010
+        1,          // 01011
+        1,          // 01100
+        1,          // 01101
+        1,          // 01110
+        0,          // 01111  - skip
+        0xFFFF0000, // 10000  - skip
+        1,          // 10001
+        1,          // 10010
+        1,          // 10011
+        1,          // 10100
+        1,          // 10101
+        1,          // 10110
+        1,          // 10111  - four var
+        1,          // 11000
+        1,          // 11001
+        1,          // 11010
+        1,          // 11011  - four var
+        1,          // 11100
+        1,          // 11101  - four var
+        1,          // 11110  - four var
+        0           // 11111  - skip
+    };
+    // permutations
+    static int Perms[32][5] = {
+        { 0, 0, 0, 0, 0 }, // 00000  - skip
+        { 0, 0, 0, 0, 0 }, // 00001  - skip
+        { 0, 0, 0, 0, 0 }, // 00010  - single var
+        { 0, 0, 0, 0, 0 }, // 00011  - skip
+        { 0, 0, 0, 0, 0 }, // 00100  - single var
+        { 0, 2, 1, 3, 4 }, // 00101
+        { 2, 0, 1, 3, 4 }, // 00110
+        { 0, 0, 0, 0, 0 }, // 00111  - skip
+        { 0, 0, 0, 0, 0 }, // 01000  - single var
+        { 0, 2, 3, 1, 4 }, // 01001
+        { 2, 0, 3, 1, 4 }, // 01010
+        { 0, 1, 3, 2, 4 }, // 01011
+        { 2, 3, 0, 1, 4 }, // 01100
+        { 0, 3, 1, 2, 4 }, // 01101
+        { 3, 0, 1, 2, 4 }, // 01110
+        { 0, 0, 0, 0, 0 }, // 01111  - skip
+        { 0, 0, 0, 0, 0 }, // 10000  - single var
+        { 0, 4, 2, 3, 1 }, // 10001
+        { 4, 0, 2, 3, 1 }, // 10010
+        { 0, 1, 3, 4, 2 }, // 10011
+        { 2, 3, 0, 4, 1 }, // 10100
+        { 0, 3, 1, 4, 2 }, // 10101
+        { 3, 0, 1, 4, 2 }, // 10110
+        { 0, 1, 2, 4, 3 }, // 10111  - four var
+        { 2, 3, 4, 0, 1 }, // 11000
+        { 0, 3, 4, 1, 2 }, // 11001
+        { 3, 0, 4, 1, 2 }, // 11010
+        { 0, 1, 4, 2, 3 }, // 11011  - four var
+        { 3, 4, 0, 1, 2 }, // 11100
+        { 0, 4, 1, 2, 3 }, // 11101  - four var
+        { 4, 0, 1, 2, 3 }, // 11110  - four var
+        { 0, 0, 0, 0, 0 }  // 11111  - skip
+    };
+    int i, k, iRes;
+    unsigned uTruthRes;
+    assert( Phase >= 0 && Phase < 32 );
+    if ( Cases[Phase] == 0 )
+        return uTruth;
+    if ( Cases[Phase] > 1 )
+        return Cases[Phase];
+    uTruthRes = 0;
+    for ( i = 0; i < 32; i++ )
+        if ( uTruth & (1 << i) )
+        {
+            for ( iRes = 0, k = 0; k < 5; k++ )
+                if ( i & (1 << Perms[Phase][k]) )
+                    iRes |= (1 << k);
+            uTruthRes |= (1 << iRes);
+        }
+    return uTruthRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocated lookup table for truth table permutation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned short ** Extra_TruthPerm43()
+{
+    unsigned short ** pTable;
+    unsigned uTruth;
+    int i, k;
+    pTable = (unsigned short **)Extra_ArrayAlloc( 256, 16, 2 );
+    for ( i = 0; i < 256; i++ )
+    {
+        uTruth = (i << 8) | i;
+        for ( k = 0; k < 16; k++ )
+            pTable[i][k] = Extra_TruthPerm4One( uTruth, k );
+    }
+    return pTable;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocated lookup table for truth table permutation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned ** Extra_TruthPerm53()
+{
+    unsigned ** pTable;
+    unsigned uTruth;
+    int i, k;
+    pTable = (unsigned **)Extra_ArrayAlloc( 256, 32, 4 );
+    for ( i = 0; i < 256; i++ )
+    {
+        uTruth = (i << 24) | (i << 16) | (i << 8) | i;
+        for ( k = 0; k < 32; k++ )
+            pTable[i][k] = Extra_TruthPerm5One( uTruth, k );
+    }
+    return pTable;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocated lookup table for truth table permutation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned ** Extra_TruthPerm54()
+{
+    unsigned ** pTable;
+    unsigned uTruth;
+    int i;
+    pTable = (unsigned **)Extra_ArrayAlloc( 256*256, 4, 4 );
+    for ( i = 0; i < 256*256; i++ )
+    {
+        uTruth = (i << 16) | i;
+        pTable[i][0] = Extra_TruthPerm5One( uTruth, 31-8 );
+        pTable[i][1] = Extra_TruthPerm5One( uTruth, 31-4 );
+        pTable[i][2] = Extra_TruthPerm5One( uTruth, 31-2 );
+        pTable[i][3] = Extra_TruthPerm5One( uTruth, 31-1 );
+    }
+    return pTable;
 }
 
 /**Function*************************************************************