From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 1 Nov 2010 01:35:04 -0700
Subject: initial commit of public abc

---
 src/misc/extra/extraUtilCanon.c | 767 ++++++++++++++++++++--------------------
 1 file changed, 385 insertions(+), 382 deletions(-)

(limited to 'src/misc/extra/extraUtilCanon.c')

diff --git a/src/misc/extra/extraUtilCanon.c b/src/misc/extra/extraUtilCanon.c
index c9c199d8..99d5dc42 100644
--- a/src/misc/extra/extraUtilCanon.c
+++ b/src/misc/extra/extraUtilCanon.c
@@ -20,6 +20,9 @@
 
 #include "extra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -36,391 +39,44 @@
 /* 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 s_Truths3[256] = 
 {
-    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 [This procedure has a bug, which shows on Solaris.
-  Most likely has something to do with the casts, i.g *((unsigned *)pt0)]
-
-  SeeAlso     []
+    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
+};
 
-***********************************************************************/
-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 = (pt0[0] << 24) | (pt0[0] << 16) | (pt0[0] << 8) | pt0[0];
-        uInit1 = (pt1[0] << 24) | (pt1[0] << 16) | (pt1[0] << 8) | pt1[0];
-    }
-    else if ( nVarsN == 4 )
-    {
-        uInit0 = (pt0[1] << 24) | (pt0[0] << 16) | (pt0[1] << 8) | pt0[0];
-        uInit1 = (pt1[1] << 24) | (pt1[0] << 16) | (pt1[1] << 8) | pt1[0];
-    }
-    else
-    {
-        uInit0 = (pt0[3] << 24) | (pt0[2] << 16) | (pt0[1] << 8) | pt0[0];
-        uInit1 = (pt1[3] << 24) | (pt1[2] << 16) | (pt1[1] << 8) | pt1[0];
-    }
-
-    // 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 );
-    }
-}
-
-/**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;
-    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 );
-    }
-}
-
-/*---------------------------------------------------------------------------*/
-/* 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] = 
+static char s_Phases3[256][9] = 
 {
 /*   0 */  {  8,   0, 1, 2, 3, 4, 5, 6, 7 }, 
 /*   1 */  {  1,   0 }, 
@@ -681,8 +337,355 @@ 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 [This procedure has a bug, which shows on Solaris.
+  Most likely has something to do with the casts, i.g *((unsigned *)pt0)]
+
+  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 = (pt0[0] << 24) | (pt0[0] << 16) | (pt0[0] << 8) | pt0[0];
+        uInit1 = (pt1[0] << 24) | (pt1[0] << 16) | (pt1[0] << 8) | pt1[0];
+    }
+    else if ( nVarsN == 4 )
+    {
+        uInit0 = (pt0[1] << 24) | (pt0[0] << 16) | (pt0[1] << 8) | pt0[0];
+        uInit1 = (pt1[1] << 24) | (pt1[0] << 16) | (pt1[1] << 8) | pt1[0];
+    }
+    else
+    {
+        uInit0 = (pt0[3] << 24) | (pt0[2] << 16) | (pt0[1] << 8) | pt0[0];
+        uInit1 = (pt1[3] << 24) | (pt1[2] << 16) | (pt1[1] << 8) | pt1[0];
+    }
+
+    // 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 );
+    }
+}
+
+/**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;
+    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 );
+    }
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
-- 
cgit v1.2.3