Experiments with Boolean functions.

3 files changed, 210 insertions, 24 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 820440ac..988aba88 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23108,11 +23108,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fVerbose );
+    extern void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose );
     extern void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose );
-    int c, nInputs = 4, nVars = 4, nNodeMax = 32, fUseTwo = 0, fReduce = 0, fSimple = 0, fDelay = 0, fVerbose = 0;
+    int c, nInputs = 4, nVars = 4, nNodeMax = 32, fUseTwo = 0, fReduce = 0, fSimple = 0, fDelay = 0, fMulti = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SIMtrldvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SIMtrldmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23161,6 +23161,9 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDelay ^= 1;
             break;
+        case 'm':
+            fMulti ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -23178,7 +23181,7 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( -1, "The number of inputs should be 3 <= I <= 5.\n" );
             goto usage;
         }
-        Dtt_EnumerateLf( nVars, nNodeMax, fDelay, fVerbose );
+        Dtt_EnumerateLf( nVars, nNodeMax, fDelay, fMulti, fVerbose );
     }
     else
     {
@@ -23197,15 +23200,16 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: funenum [-SIM num] [-trldvh]\n" );
+    Abc_Print( -2, "usage: funenum [-SIM num] [-trldmvh]\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-I num : the number of inputs of Boolean functions [default = %d]\n", nVars );
     Abc_Print( -2, "\t-M num : the maximum number of 2-input gates [default = %d]\n",       nNodeMax );
-    Abc_Print( -2, "\t-t     : toggle adding combination of two gates [default = %s]\n",    fUseTwo? "yes": "no" );
-    Abc_Print( -2, "\t-r     : toggle reducing the last level [default = %s]\n",            fReduce? "yes": "no" );
-    Abc_Print( -2, "\t-l     : toggle generating L(f) rather than C(f) [default = %s]\n",   fSimple? "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggle generating D(f) rather than C(f) [default = %s]\n",   fDelay? "yes": "no" );
+    Abc_Print( -2, "\t-t     : toggle adding combination of two gates [default = %s]\n",    fUseTwo?  "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle reducing the last level [default = %s]\n",            fReduce?  "yes": "no" );
+    Abc_Print( -2, "\t-l     : toggle generating L(f) rather than C(f) [default = %s]\n",   fSimple?  "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle generating D(f) rather than C(f) [default = %s]\n",   fDelay?   "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle generating multiplicity statistics [default = %s]\n", fMulti?   "yes": "no" );
     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;
diff --git a/src/bdd/extrab/extraBddMisc.c b/src/bdd/extrab/extraBddMisc.c
index 335f6754..42003864 100644
--- a/src/bdd/extrab/extraBddMisc.c
+++ b/src/bdd/extrab/extraBddMisc.c
@@ -2723,8 +2723,8 @@ DdNode * Extra_bddTuples(
         if ( K > nVars )
             return NULL;
 
-        /* the second argument in the recursive call stannds for <n>;
-        /* reate the first argument, which stands for <k> 
+        /* the second argument in the recursive call stands for <n>;
+         * create the first argument, which stands for <k> 
          * as when we are talking about the tuple of <k> out of <n> */
         for ( i = 0; i < nVars-K; i++ )
             VarsK = cuddT( VarsK );
diff --git a/src/opt/dau/dauNpn2.c b/src/opt/dau/dauNpn2.c
index b02aa794..68fdc457 100644
--- a/src/opt/dau/dauNpn2.c
+++ b/src/opt/dau/dauNpn2.c
@@ -46,10 +46,17 @@ struct Dtt_Man_t_
     Vec_Int_t *    vTemp;          // temporary
     Vec_Int_t *    vTemp2;         // temporary
     unsigned       FunMask;        // function mask
+    unsigned       CmpMask;        // function mask
     unsigned       BinMask;        // hash mask
     unsigned *     pBins;          // hash bins
     Vec_Int_t *    vUsedBins;      // used bins
     int            Counts[32];     // node counts
+    int            nClasses;       // count of classes
+    unsigned *     pTable;         // mapping of funcs into their classes
+    int *          pNodes;         // the number of nodes in min-node network
+    int *          pTimes;         // the number of different min-node networks
+    char *         pVisited;       // visited classes
+    Vec_Int_t *    vVisited;       // the number of visited classes
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -67,7 +74,97 @@ struct Dtt_Man_t_
   SeeAlso     []
 
 ***********************************************************************/
-Dtt_Man_t * Dtt_ManAlloc( int nVars )
+unsigned * Dau_ReadFile2( char * pFileName, int nSizeW )
+{
+    abctime clk = Abc_Clock();
+    FILE * pFile = fopen( pFileName, "rb" );
+    unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW);
+    int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
+    RetValue = 0;
+    if ( pFile )
+    {
+        printf( "Finished reading file \"%s\".\n", pFileName );
+        fclose( pFile );
+    }
+    else
+        printf( "Cannot open input file \"%s\".\n", pFileName );
+    Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
+    return p;
+}
+void Dtt_ManRenum( int nVars, unsigned * pTable, int * pnClasses )
+{
+    unsigned i, Limit = 1 << ((1 << nVars)-1), Count = 0;
+    for ( i = 0; i < Limit; i++ )
+        if ( pTable[i] == i )
+            pTable[i] = Count++;
+        else 
+        {
+            assert( pTable[i] < i );
+            pTable[i] = pTable[pTable[i]];
+        }
+    printf( "The total number of NPN classes = %d.\n", Count );
+    *pnClasses = Count;
+}
+unsigned * Dtt_ManLoadClasses( int nVars, int * pnClasses )
+{
+    unsigned * pTable = NULL;
+    if ( nVars == 4 )
+        pTable = Dau_ReadFile2( "tableW14.data", 1 << 14 );
+    else if ( nVars == 5 )
+        pTable = Dau_ReadFile2( "tableW30.data", 1 << 30 );
+    else assert( 0 );
+    Dtt_ManRenum( nVars, pTable, pnClasses );
+    return pTable;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dtt_ManAddVisited( Dtt_Man_t * p, unsigned Truth2, int n )
+{
+    unsigned Truth = Truth2 & p->CmpMask ? ~Truth2 : Truth2;
+    unsigned Class = p->pTable[Truth & p->FunMask];
+    assert( Class < (unsigned)p->nClasses );
+    if ( p->pNodes[Class] < n )
+        return;
+    assert( p->pNodes[Class] == n );
+    if ( p->pVisited[Class] )
+        return;
+    p->pVisited[Class] = 1;
+    Vec_IntPush( p->vVisited, Class );
+}
+void Dtt_ManProcessVisited( Dtt_Man_t * p )
+{
+    int i, Class;
+    Vec_IntForEachEntry( p->vVisited, Class, i )
+    {
+        assert( p->pVisited[Class] );
+        p->pVisited[Class] = 0;
+        p->pTimes[Class]++;
+    }
+    Vec_IntClear( p->vVisited );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dtt_Man_t * Dtt_ManAlloc( int nVars, int fMulti )
 {
     Dtt_Man_t * p = ABC_CALLOC( Dtt_Man_t, 1 );
     p->nVars      = nVars;
@@ -84,14 +181,26 @@ Dtt_Man_t * Dtt_ManAlloc( int nVars )
     p->vFunNodes  = Vec_WecStart( 16 );
     p->vTemp      = Vec_IntAlloc( 4000 );
     p->vTemp2     = Vec_IntAlloc( 4000 );
-    p->FunMask    = nVars == 5 ? ~0 : (nVars == 4 ? 0xFFFF : 0xFF);
+    p->FunMask    = nVars == 5 ?      ~0 : (nVars == 4 ?  0xFFFF :   0xFF);
+    p->CmpMask    = nVars == 5 ? 1 << 31 : (nVars == 4 ? 1 << 15 : 1 << 7);
     p->BinMask    = 0x3FFF;
     p->pBins      = ABC_FALLOC( unsigned, p->BinMask + 1 );
     p->vUsedBins  = Vec_IntAlloc( 4000 );
+    if ( !fMulti ) return p;
+    p->pTable     = Dtt_ManLoadClasses( p->nVars, &p->nClasses );
+    p->pNodes     = ABC_CALLOC( int, p->nClasses );
+    p->pTimes     = ABC_CALLOC( int, p->nClasses );
+    p->pVisited   = ABC_CALLOC( char, p->nClasses );
+    p->vVisited   = Vec_IntAlloc( 1000 );
     return p;
 }
 void Dtt_ManFree( Dtt_Man_t * p )
 {
+    Vec_IntFreeP( &p->vVisited );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p->pNodes );
+    ABC_FREE( p->pTimes );
+    ABC_FREE( p->pVisited );
     Vec_IntFreeP( &p->vFanins );
     Vec_IntFreeP( &p->vTruths );
     Vec_IntFreeP( &p->vConfigs );
@@ -138,14 +247,15 @@ int Dtt_ManCheckHash( Dtt_Man_t * p, unsigned Truth )
 }
 Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
 {
-    int i, k, Entry;
+    int i, k, Entry, Shift = (1 << p->nVars) - 1;
     word tCur = ((word)Truth << 32) | (word)Truth;
     Vec_IntClear( vFuns );
     for ( i = 0; i < p->nPerms; i++ )
     {
         for ( k = 0; k < p->nComps; k++ )
         {
-            unsigned tTemp = (unsigned)(tCur & 1 ? ~tCur : tCur);
+//            unsigned tTemp = (unsigned)(tCur & 1 ? ~tCur : tCur);
+            unsigned tTemp = (unsigned)(tCur & p->CmpMask ? ~tCur : tCur);
             if ( Dtt_ManCheckHash( p, tTemp ) )
                 Vec_IntPush( vFuns, tTemp );
             tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
@@ -174,12 +284,14 @@ Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
 ***********************************************************************/
 static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun )
 {
-    return Abc_TtGetBit( p->pPres, (tFun & p->FunMask) >> 1 );
+    tFun = tFun & p->CmpMask ? ~tFun : tFun;
+    return Abc_TtGetBit( p->pPres, tFun & p->FunMask );
 }
 static inline void Dtt_ManSetFun( Dtt_Man_t * p, unsigned tFun )
 {
-    //assert( !Dtt_ManGetFun(p, (fFun & p->FunMask)) );
-    Abc_TtSetBit( p->pPres, (tFun & p->FunMask) >> 1 );
+    tFun = tFun & p->CmpMask ? ~tFun : tFun;
+    //assert( !Dtt_ManGetFun(p, fFun & p->FunMask );
+    Abc_TtSetBit( p->pPres, tFun & p->FunMask );
 }
 void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, unsigned Truth )
 {
@@ -202,14 +314,23 @@ void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, uns
         Dtt_ManSetFun( p, Min );
     assert( nNodes < 32 );
     p->Counts[nNodes]++;
+
+    if ( p->pTable == NULL )
+        return;
+    Truth = Truth & p->CmpMask ? ~Truth : Truth;
+    Truth &= p->FunMask;
+    assert( p->pNodes[p->pTable[Truth]] == 0 );
+    p->pNodes[p->pTable[Truth]] = n;
 }
-int Dtt_PrintStats( int nNodes, int nVars, Vec_Wec_t * vFunNodes, word nSteps, abctime clk, int fDelay )
+
+int Dtt_PrintStats( int nNodes, int nVars, Vec_Wec_t * vFunNodes, word nSteps, abctime clk, int fDelay, word nMultis )
 {
     int nNew = Vec_IntSize(Vec_WecEntry(vFunNodes, nNodes));
     printf("%c =%2d  |  ",     fDelay ? 'D':'N', nNodes );
     printf("C =%12.0f  |  ",   (double)(iword)nSteps );
     printf("New%d =%10d   ",   nVars, nNew + (int)(nNodes==0) );
     printf("All%d =%10d  |  ", nVars, Vec_WecSizeSize(vFunNodes)+1 );
+    printf("Multi =%10d  |  ", (int)nMultis );
     Abc_PrintTime( 1, "Time",  Abc_Clock() - clk );
     //Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
     fflush(stdout);
@@ -223,10 +344,61 @@ void Dtt_PrintDistrib( Dtt_Man_t * p )
         if ( p->Counts[i] )
             printf( "N = %2d : NPN = %6d\n", i, p->Counts[i] );
 }
-void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fVerbose )
+void Dtt_PrintMulti2( Dtt_Man_t * p )
 {
-    abctime clk = Abc_Clock(); word nSteps = 0;
-    Dtt_Man_t * p = Dtt_ManAlloc( nVars ); int n, i, j;
+    int i, n;
+    for ( n = 0; n <= 7; n++ )
+    {
+        printf( "n=%d : ", n);
+        for ( i = 0; i < p->nClasses; i++ )
+            if ( p->pNodes[i] == n )
+                printf( "%d ", p->pTimes[i] );
+        printf( "\n" );
+    }
+}
+void Dtt_PrintMulti( Dtt_Man_t * p )
+{
+    int i, n, Entry, Count, Prev;
+    for ( n = 0; n < 16; n++ )
+    {
+        Vec_Int_t * vTimes = Vec_IntAlloc( 100 );
+        Vec_Int_t * vUsed  = Vec_IntAlloc( 100 );
+        for ( i = 0; i < p->nClasses; i++ )
+            if ( p->pNodes[i] == n )
+                Vec_IntPush( vTimes, p->pTimes[i] );
+        if ( Vec_IntSize(vTimes) == 0 )
+        {
+            Vec_IntFree(vTimes);
+            Vec_IntFree(vUsed);
+            break;
+        }
+        Vec_IntSort( vTimes, 0 );
+        Count = 1;
+        Prev = Vec_IntEntry( vTimes, 0 );
+        Vec_IntForEachEntryStart( vTimes, Entry, i, 1 )
+            if ( Prev == Entry )
+                Count++;
+            else
+            {
+                assert( Prev < Entry );
+                Vec_IntPushTwo( vUsed, Prev, Count );
+                Count = 1;
+                Prev = Entry;
+            }
+        if ( Count > 0 )
+            Vec_IntPushTwo( vUsed, Prev, Count );
+        printf( "n=%d : ", n);
+        Vec_IntForEachEntryDouble( vUsed, Prev, Entry, i )
+            printf( "%d=%d ", Prev, Entry );
+        printf( "\n" );
+        Vec_IntFree( vTimes );
+        Vec_IntFree( vUsed );
+    }
+}
+void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose )
+{
+    abctime clk = Abc_Clock(); word nSteps = 0, nMultis = 0;
+    Dtt_Man_t * p = Dtt_ManAlloc( nVars, fMulti ); int n, i, j;
     // constant zero class
     Vec_IntPushTwo( p->vFanins, 0, 0 );
     Vec_IntPush( p->vTruths, 0 );
@@ -245,7 +417,7 @@ void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fVerbose )
         Dtt_ManSetFun( p, (unsigned)s_Truths6[i] );
     p->Counts[0] = 2;
     // enumerate
-    Dtt_PrintStats(0, nVars, p->vFunNodes, nSteps, clk, fDelay);
+    Dtt_PrintStats(0, nVars, p->vFunNodes, nSteps, clk, fDelay, 0);
     for ( n = 1; n <= nNodeMax; n++ )
     {
         for ( i = 0, j = n - 1; i < n; i++, j = j - 1 + fDelay ) if ( i <= j )
@@ -274,15 +446,25 @@ void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fVerbose )
                         if ( !Dtt_ManGetFun(p,  TruthJ ^  Truth) )
                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4,  TruthJ ^  Truth );
                         nSteps += 5;
+
+                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ &  Truth, n );
+                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ & ~Truth, n );
+                        if ( p->pTable ) Dtt_ManAddVisited( p, ~TruthJ &  Truth, n );
+                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ |  Truth, n );
+                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ ^  Truth, n );
                     }
+                    nMultis++;
+                    if ( p->pTable ) Dtt_ManProcessVisited( p );
                 }
             }
         }
-        if ( Dtt_PrintStats(n, nVars, p->vFunNodes, nSteps, clk, fDelay) == 0 )
+        if ( Dtt_PrintStats(n, nVars, p->vFunNodes, nSteps, clk, fDelay, nMultis) == 0 )
             break;
     }
     if ( fDelay )
         Dtt_PrintDistrib( p );
+    if ( p->pTable ) 
+        Dtt_PrintMulti( p );
     Dtt_ManFree( p );
 }