Expriments with functions.

2 files changed, 325 insertions, 0 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5280f5fc..67d361ac 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -317,6 +317,7 @@ static int Abc_CommandPermute                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandUnpermute              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCubeEnum               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPathEnum               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFunEnum                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCec                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1005,6 +1006,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "unpermute",     Abc_CommandUnpermute,        1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "cubeenum",      Abc_CommandCubeEnum,         0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "pathenum",      Abc_CommandPathEnum,         0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "funenum",       Abc_CommandFunEnum,          0 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
@@ -22973,6 +22975,71 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose );
+    int c, nInputs = 4, nVars = 4, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SNvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nInputs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nInputs < 0 )
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVars < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+    Dau_FunctionEnum( nInputs, nVars, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: funenum [-SN num] [-vh]\n" );
+    Abc_Print( -2, "\t         enumerates minimum 2-input-gate implementations\n" );
+    Abc_Print( -2, "\t-S num : the maximum intermediate support size [default = %d]\n", nInputs );
+    Abc_Print( -2, "\t-N num : the number of inputs of Boolean functions [default = %d]\n", nVars );
+    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c
index fb3d5db1..a9fbca10 100644
--- a/src/opt/dau/dauNpn.c
+++ b/src/opt/dau/dauNpn.c
@@ -21,6 +21,7 @@
 #include "dauInt.h"
 #include "misc/util/utilTruth.h"
 #include "misc/extra/extra.h"
+#include "bool/lucky/lucky.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -384,6 +385,263 @@ void Dau_NetworkEnumTest()
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Performs exact canonicization of semi-canonical classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Dau_ExactNpnForClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs )
+{
+    Vec_Wrd_t * vCanons = Vec_WrdStart( Vec_IntSize(vNodSup) );
+    word pAuxWord[1024], pAuxWord1[1024];
+    word uTruth; int i, Entry;
+    permInfo * pi = setPermInfoPtr(nVars);
+    Vec_IntForEachEntry( vNodSup, Entry, i )
+    {
+        if ( (Entry & 0xF) > nVars )
+            continue;
+        uTruth = *Vec_MemReadEntry( vTtMem, i );
+        simpleMinimal(&uTruth, pAuxWord, pAuxWord1, pi, nVars);
+        Vec_WrdWriteEntry( vCanons, i, uTruth );
+    }
+    freePermInfoPtr(pi);
+    return vCanons;
+}
+void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs, int nNodesMax )
+{
+    abctime clk = Abc_Clock(); int n, nTotal = 0;
+    Vec_Wrd_t * vCanons = Dau_ExactNpnForClasses( vTtMem, vNodSup, nVars, nInputs );
+    Vec_Mem_t * vTtMem2  = Vec_MemAlloc( Vec_MemEntrySize(vTtMem), 10 );
+    Vec_MemHashAlloc( vTtMem2, 1<<10 );
+    Abc_PrintTime( 1, "Exact NPN computation time", Abc_Clock() - clk );
+    printf( "Final results:\n" );
+    for ( n = 0; n <= nNodesMax; n++ )
+    {
+        int i, Entry, Entry2, nEntries2, Counter = 0, Counter2 = 0;
+        Vec_IntForEachEntry( vNodSup, Entry, i )
+        {
+            if ( (Entry & 0xF) > nVars || (Entry >> 16) != n )
+                continue;
+            Counter++;
+            nEntries2 = Vec_MemEntryNum(vTtMem2);
+            Entry2 = Vec_MemHashInsert( vTtMem2, Vec_WrdEntryP(vCanons, i) );
+            if ( nEntries2 == Vec_MemEntryNum(vTtMem2) ) // found in the table - not new
+                continue;
+            Counter2++;
+        }
+        nTotal += Counter2;
+        printf( "Nodes = %2d.  ", n );
+        printf( "Semi-canonical = %8d.  ", Counter );
+        printf( "Canonical = %8d.  ", Counter2 );
+        printf( "Total = %8d.", nTotal );
+        printf( "\n" );
+    }
+    Vec_MemHashFree( vTtMem2 );
+    Vec_MemFreeP( &vTtMem2 );
+    Vec_WrdFree( vCanons );
+    fflush(stdout);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Function enumeration.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_CountFuncs( Vec_Int_t * vNodSup, int iStart, int iStop, int nVars )
+{
+    int i, Entry, Count = 0;
+    Vec_IntForEachEntryStartStop( vNodSup, Entry, i, iStart, iStop )
+        Count += ((Entry & 0xF) <= nVars);
+    return Count;
+}
+int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int iStart, int iStop, abctime clk )
+{
+    int nNew;
+    printf("Nodes = %2d.   ",  nNodes );
+    printf("New%d = %8d. ",    nInputs, iStop-iStart );
+    printf("Total%d = %8d.  ", nInputs, iStop );
+    printf("New%d = %8d. ",    nVars, nNew = Dau_CountFuncs(vNodSup, iStart, iStop, nVars) );
+    printf("Total%d = %8d.  ", nVars,        Dau_CountFuncs(vNodSup,      0, iStop, nVars) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    fflush(stdout);
+    return nNew;
+}
+int Dau_InsertFunction( word * pCur, int nNodes, int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup )
+{
+    char Perm[16] = {0};
+    int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
+    unsigned Phase = Abc_TtCanonicize( pCur, nVarsNew, Perm );
+    int nEntries = Vec_MemEntryNum(vTtMem);
+    int Entry = Vec_MemHashInsert( vTtMem, pCur );
+    if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new
+        return 0;
+    // this is a new class
+    Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
+    assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
+    return 1;
+}
+void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    int nWords = Abc_TtWordNum(nInputs);
+    Vec_Mem_t * vTtMem  = Vec_MemAlloc( nWords, 16 );
+    Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 );
+    int v, g, k, m, n, Entry, nNew, iStart = 1, iStop = 2;
+    word Truth[4] = {0};
+    assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 );
+    Vec_MemHashAlloc( vTtMem, 1<<16 );
+    // add constant 0
+    Vec_MemHashInsert( vTtMem, Truth );
+    Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0
+    // add buffer/inverter
+    Abc_TtIthVar( Truth, 0, nInputs );
+    Abc_TtNot( Truth, nWords );
+    Vec_MemHashInsert( vTtMem, Truth );
+    Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1
+    Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, clk );
+    // numerate other functions based on how many nodes they have
+    for ( n = 1; n < 32; n++ )
+    {
+        for ( Entry = iStart; Entry < iStop; Entry++ )
+        {
+            word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
+            int NodSup = Vec_IntEntry(vNodSup, Entry);
+            int nSupp = 0xF & NodSup;
+            assert( n-1 == (NodSup >> 16) );
+            assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
+            //printf( "Exploring function %4d with %d vars: ", i, nSupp );
+            //printf( " %04x\n", (int)uTruth );
+            //Dau_DsdPrintFromTruth( &uTruth, 4 );
+            for ( v = 0; v < nSupp; v++ )
+            {
+                word tGate, tCur;
+                word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
+                word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
+                if ( nSupp < nInputs )
+                {
+                    // add one extra variable to support
+                    for ( g = 0; g < 2; g++ )
+                    {
+                        if ( g == 0 )
+                        {
+                            tGate = s_Truths6[v] & s_Truths6[nSupp];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup );
+                        }
+                        else
+                        {
+                            tGate = s_Truths6[v] ^ s_Truths6[nSupp];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup );
+                        }
+                    }
+                }
+                for ( g = 0; g < 2; g++ )
+                {
+                    // add one cross bar
+                    for ( k = 0; k < nSupp; k++ ) if ( k != v )
+                    {
+                        if ( g == 0 )
+                        {
+                            tGate = s_Truths6[v] & s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tGate = s_Truths6[v] & ~s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+                        }
+                        else
+                        {
+                            tGate = s_Truths6[v] ^ s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+                        }
+                    }
+                }
+                for ( g = 0; g < 2; g++ )
+                {
+                    // add two cross bars
+                    for ( k = 0;   k < nSupp; k++ ) if ( k != v )
+                    for ( m = k+1; m < nSupp; m++ ) if ( m != v )
+                    {
+                        if ( g == 0 )
+                        {
+                            tGate = s_Truths6[m] & s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tGate = s_Truths6[m] & ~s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tGate = ~s_Truths6[m] & s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tGate = ~s_Truths6[m] & ~s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+                        }
+                        else
+                        {
+                            tGate = s_Truths6[m] ^ s_Truths6[k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+                        }
+                    }
+                }
+            }
+        }
+        iStart = iStop; 
+        iStop  = Vec_IntSize(vNodSup);
+        nNew = Dau_PrintStats( n, nInputs, nVars, vNodSup, iStart, iStop, clk );
+        if ( nNew == 0 )
+            break;
+    }
+    Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+    Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n );
+    Vec_MemHashFree( vTtMem );
+    Vec_MemFreeP( &vTtMem );
+    Vec_IntFree( vNodSup );
+    fflush(stdout);
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////