Expriments with functions.

1 files changed, 171 insertions, 109 deletions

diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c
index d8c19111..3683189d 100644
--- a/src/opt/dau/dauNpn.c
+++ b/src/opt/dau/dauNpn.c
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-//#define USE4VARS 1
+#define USE4VARS 1
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -149,26 +149,30 @@ unsigned * Dau_ReadFile( char * pFileName, int nSizeW )
     Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
     return p;
 }
-void Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns )
+int Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns, Vec_Int_t * vNpns_ )
 {
     int Digit  = (1 << nVars)-1;
     word tMask = Abc_Tt6Mask( 1 << nVars );
     word tNorm = (tCur >> Digit) & 1 ? ~tCur : tCur;
     unsigned t = (unsigned)(tNorm & tMask);
-    unsigned tRep = pTable[t];
-    unsigned tRep2 = pTable[tRep & 0x7FFFFFFF];
+    unsigned tRep = pTable[t] & 0x7FFFFFFF;
+    unsigned tRep2 = pTable[tRep];
     assert( ((tNorm >> Digit) & 1) == 0 );
     if ( (tRep2 >> 31) == 0 ) // first time
     {
         Vec_IntPush( vNpns, tRep2 );
-        pTable[tRep & 0x7FFFFFFF] = tRep2 | (1 << 31);
+        if ( Abc_TtSupportSize(&tCur, nVars) < nVars )
+            Vec_IntPush( vNpns_, tRep2 );
+        pTable[tRep] = tRep2 | (1 << 31);
+        return tRep2;
     }
-
+    return 0;
 }
 void Dau_NetworkEnum()
 {
     abctime clk = Abc_Clock();
     int Limit = 2;
+    int UseTwo = 1;
 #ifdef USE4VARS
     int nVars = 4;
     int nSizeW  = 1 << 14;
@@ -178,133 +182,191 @@ void Dau_NetworkEnum()
     int nSizeW  = 1 << 30;
     char * pFileName = "tableW30.data";
 #endif
-    unsigned * pTable = Dau_ReadFile( pFileName, nSizeW );
-    Vec_Int_t * vNpns = Vec_IntAlloc( 1000 );
-    int i, v, g, k, m, Entry, Count = 1, iPrev = 0, iLast = 1;
+    unsigned * pTable  = Dau_ReadFile( pFileName, nSizeW );
+    Vec_Wec_t * vNpns  = Vec_WecStart( 32 );
+    Vec_Wec_t * vNpns_ = Vec_WecStart( 32 );
+    int i, v, u, g, k, m, n, Res, Entry, iPrev = 0, iLast = 1;
     unsigned Inv = (unsigned)Abc_Tt6Mask(1 << (nVars-1));
+    // create constant function and buffer/inverter function
     pTable[0]   |= (1 << 31);
     pTable[Inv] |= (1 << 31);
-    Vec_IntPushTwo( vNpns, 0, Inv );
-    Vec_IntForEachEntryStart( vNpns, Entry, i, 1 )
+    Vec_IntPushTwo( Vec_WecEntry(vNpns,  0), 0, Inv );
+    Vec_IntPushTwo( Vec_WecEntry(vNpns_, 0), 0, Inv );
+    printf("Nodes = %2d.   New = %4d. Total = %6d.   New = %4d. Total = %6d.  ", 
+        0, Vec_IntSize(Vec_WecEntry(vNpns,  0)), Vec_WecSizeSize(vNpns), 
+           Vec_IntSize(Vec_WecEntry(vNpns_, 0)), Vec_WecSizeSize(vNpns_) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    // numerate other functions based on how many nodes they have
+    for ( n = 1; n < 32; n++ )
     {
-        word uTruth = (((word)Entry) << 32) | (word)Entry;
-        int nSupp = Abc_TtSupportSize( &uTruth, nVars );
-        //printf( "Exploring function %4d with %d vars: ", i, nSupp );
-        //printf( " %04x\n", (int)uTruth );
-        //Dau_DsdPrintFromTruth( &uTruth, 4 );
-        for ( v = 0; v < nSupp; v++ )
+        Vec_Int_t * vFuncsN2 = n > 1 ? Vec_WecEntry( vNpns, n-2 ) : NULL;
+        Vec_Int_t * vFuncsN1 = Vec_WecEntry( vNpns, n-1 );
+        Vec_Int_t * vFuncsN  = Vec_WecEntry( vNpns, n   );
+        Vec_Int_t * vFuncsN_ = Vec_WecEntry( vNpns_,n   );
+        Vec_IntForEachEntry( vFuncsN1, Entry, i )
         {
-            word tGate, tCur;
-            word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
-            word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
-            for ( g = 0; g < Limit; g++ )
+            word uTruth = (((word)Entry) << 32) | (word)Entry;
+            int nSupp = Abc_TtSupportSize( &uTruth, nVars );
+            assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-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++ )
             {
-                if ( nSupp < nVars )
+                word tGate, tCur;
+                word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
+                word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
+                for ( g = 0; g < Limit; g++ )
                 {
-                    if ( g == 0 )
-                    {
-                        tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-                    }
-                    else
+                    if ( nSupp < nVars )
                     {
-                        tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
+                        if ( g == 0 )
+                        {
+                            tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                        }
+                        else
+                        {
+                            tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                        }
                     }
                 }
-            }
-            for ( g = 0; g < Limit; g++ )
-            {
-                // add one cross bar
-                for ( k = 0; k < nSupp; k++ ) if ( k != v )
+                for ( g = 0; g < Limit; g++ )
                 {
-                    if ( g == 0 )
+                    // add one cross bar
+                    for ( k = 0; k < nSupp; k++ ) if ( k != v )
                     {
-                        tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-                    }
-                    else
-                    {
-                        tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
+                        if ( g == 0 )
+                        {
+                            tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                        }
+                        else
+                        {
+                            tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                        }
                     }
                 }
-            }
-            for ( g = 0; g < Limit; g++ )
-            {
-                // add two cross bars
-                for ( k = 0;   k < nSupp; k++ ) if ( k != v )
-                for ( m = k+1; m < nSupp; m++ ) if ( m != v )
+                for ( g = 0; g < Limit; g++ )
                 {
-                    if ( g == 0 )
+                    // add two cross bars
+                    for ( k = 0;   k < nSupp; k++ ) if ( k != v )
+                    for ( m = k+1; m < nSupp; m++ ) if ( m != v )
                     {
-                        tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-
-                        tCur  = (tGate & Cof0) | (~tGate & Cof1);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
-                    }
-                    else
-                    {
-                        tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
-                        tCur  = (tGate & Cof1) | (~tGate & Cof0);
-                        Dau_AddFunction( tCur, nVars, pTable, vNpns );
+                        if ( g == 0 )
+                        {
+                            tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+
+                            tCur  = (tGate & Cof0) | (~tGate & Cof1);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                        }
+                        else
+                        {
+                            tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
+                            tCur  = (tGate & Cof1) | (~tGate & Cof0);
+                            Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                        }
                     }
                 }
             }
         }
-        if ( i == iLast )
+        if ( UseTwo && vFuncsN2 )
+        Vec_IntForEachEntry( vFuncsN2, Entry, i )
         {
-            //printf("Finished %d nodes with %d functions.\n", Count++, Vec_IntSize(vNpns) );
-            iPrev = iLast;
-            iLast = Vec_IntSize(vNpns)-1;
-            printf("Finished %2d nodes with %6d functions out of %6d.  ", Count++, iLast - iPrev, Vec_IntSize(vNpns) );
-            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-            fflush(stdout);
+            word uTruth = (((word)Entry) << 32) | (word)Entry;
+            int nSupp = Abc_TtSupportSize( &uTruth, nVars );
+            assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-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++ )
+//            for ( u = v+1; u < nSupp; u++ ) if ( u != v )
+            for ( u = 0; u < nSupp; u++ ) if ( u != v )
+            {
+                word tGate1, tGate2, tCur;
+                word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
+                word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
+
+                word Cof00 = Abc_Tt6Cofactor0( Cof0, nVars-1-u );
+                word Cof01 = Abc_Tt6Cofactor1( Cof0, nVars-1-u );
+                word Cof10 = Abc_Tt6Cofactor0( Cof1, nVars-1-u );
+                word Cof11 = Abc_Tt6Cofactor1( Cof1, nVars-1-u );
+
+                tGate1 = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-u];
+                tGate2 = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-u];
+
+                Cof0  = (tGate2 & Cof00) | (~tGate2 & Cof01);
+                Cof1  = (tGate2 & Cof10) | (~tGate2 & Cof11);
+
+                tCur  = (tGate1 & Cof1)  | (~tGate1 & Cof0);
+                Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                if ( Res )
+                    printf( "Found function %d\n", Res );
+
+                tCur  = (tGate1 & Cof0)  | (~tGate1 & Cof1);
+                Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
+                if ( Res )
+                    printf( "Found function %d\n", Res );
+            }
         }
+        printf("Nodes = %2d.   New = %4d. Total = %6d.   New = %4d. Total = %6d.  ", 
+            n, Vec_IntSize(vFuncsN), Vec_WecSizeSize(vNpns), Vec_IntSize(vFuncsN_), Vec_WecSizeSize(vNpns_) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        fflush(stdout);
+        if ( Vec_IntSize(vFuncsN) == 0 )
+            break;
     }
-    Vec_IntFree( vNpns );
+    printf( "Functions with 7 nodes:\n" );
+    Vec_IntForEachEntry( Vec_WecEntry(vNpns_,7), Entry, i )
+        printf( "%04x ", Entry );
+    printf( "\n" );
+
+    Vec_WecFree( vNpns );
+    Vec_WecFree( vNpns_ );
     ABC_FREE( pTable );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
     fflush(stdout);
 }
 void Dau_NetworkEnumTest()