Experiments with SPFD-based decomposition.

2 files changed, 318 insertions, 99 deletions

diff --git a/src/aig/bdc/bdcSpfd.c b/src/aig/bdc/bdcSpfd.c
index e3f6f2d9..7e2a423f 100644
--- a/src/aig/bdc/bdcSpfd.c
+++ b/src/aig/bdc/bdcSpfd.c
@@ -78,8 +78,22 @@ static inline word Bdc_Cof6( word t, int iVar, int fCof1 )
         return (t &~Truths[iVar]) | ((t &~Truths[iVar]) << (1<<iVar));
 }
 
+int Bdc_SpfdAdjCost( word t )
+{
+    word c0, c1;
+    int v, Cost = 0;
+    for ( v = 0; v < 6; v++ )
+    {
+        c0 = Bdc_Cof6( t, v, 0 );
+        c1 = Bdc_Cof6( t, v, 1 );
+        Cost += Bdc_CountOnes( c0 ^ c1 );
+    }
+    return Cost;
+}
+
 
-extern void Abc_Show6VarFunc( word F0, word F1 );
+extern void  Abc_Show6VarFunc( word F0, word F1 );
+extern word  Aig_ManRandom64( int fReset );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -383,18 +397,94 @@ void Bdc_SpfdDecomposeTest_()
 typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
 struct Bdc_Ent_t_
 {
-    unsigned         iFan0   : 30;
+    unsigned         iFan0   : 29;
     unsigned         fCompl0 :  1;
     unsigned         fCompl  :  1;
-    unsigned         iFan1   : 30;
+    unsigned         fMark0  :  1;
+    unsigned         iFan1   : 29;
     unsigned         fCompl1 :  1;
     unsigned         fExor   :  1;
+    unsigned         fMark1  :  1;
     int              iNext;
     int              iList;
     word             Truth;
 };
 
-#define BDC_TERM 0x3FFFFFFF
+#define BDC_TERM 0x1FFFFFFF
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdMark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
+{
+    if ( pEnt->iFan0 == BDC_TERM )
+        return 0;
+    if ( pEnt->fMark0 )
+        return 0;
+    pEnt->fMark0 = 1;
+    return pEnt->fMark1 + 
+        Bdc_SpfdMark0(p, p + pEnt->iFan0) + 
+        Bdc_SpfdMark0(p, p + pEnt->iFan1);
+}
+int Bdc_SpfdMark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
+{
+    if ( pEnt->iFan0 == BDC_TERM )
+        return 0;
+    if ( pEnt->fMark1 )
+        return 0;
+    pEnt->fMark1 = 1;
+    return pEnt->fMark0 + 
+        Bdc_SpfdMark1(p, p + pEnt->iFan0) + 
+        Bdc_SpfdMark1(p, p + pEnt->iFan1);
+}
+void Bdc_SpfdUnmark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
+{
+    if ( pEnt->iFan0 == BDC_TERM )
+        return;
+    pEnt->fMark0 = 0;
+    Bdc_SpfdUnmark0( p, p + pEnt->iFan0 );
+    Bdc_SpfdUnmark0( p, p + pEnt->iFan1 );
+}
+void Bdc_SpfdUnmark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
+{
+    if ( pEnt->iFan0 == BDC_TERM )
+        return;
+    pEnt->fMark1 = 0;
+    Bdc_SpfdUnmark1( p, p + pEnt->iFan0 );
+    Bdc_SpfdUnmark1( p, p + pEnt->iFan1 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdCheckOverlap( Bdc_Ent_t * p, Bdc_Ent_t * pEnt0, Bdc_Ent_t * pEnt1 )
+{
+    int RetValue;
+    RetValue = Bdc_SpfdMark0( p, pEnt0 );
+    assert( RetValue == 0 );
+    RetValue = Bdc_SpfdMark1( p, pEnt1 );
+    Bdc_SpfdUnmark0( p, pEnt0 );
+    Bdc_SpfdUnmark1( p, pEnt1 );
+    return RetValue;
+}
 
 /**Function*************************************************************
 
@@ -484,20 +574,15 @@ int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t )
 ***********************************************************************/
 Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
 {
-    int nFuncs = 3000000; // the number of functions to compute
-    int nSize  = 2777111; // the hash table size to use
-    int Limit  = 5;
-
-    
-//    int nFuncs = 13000000; // the number of functions to compute
-//    int nSize  = 12582917; // the hash table size to use
-//    int Limit  = 6;
-
-//    int nFuncs =  60000000; // the number of functions to compute
-//    int nSize  =  50331653; // the hash table size to use
+//    int nFuncs = 8000000; // the number of functions to compute
+//    int nSize  = 2777111; // the hash table size to use
 //    int Limit  = 6;
+    
+    int nFuncs = 51000000; // the number of functions to compute
+    int nSize  = 50331653; // the hash table size to use
+    int Limit  = 6;
 
-    int * pPlace, i, n, m, s, fCompl, clk = clock(), clk2;
+    int * pPlace, i, n, m, k, s, fCompl, clk = clock(), clk2;
     Vec_Int_t * vStops;
     Vec_Wrd_t * vTruths;
     Vec_Int_t * vWeights;
@@ -510,11 +595,15 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
     p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) );
     memset( p, 255, sizeof(Bdc_Ent_t) );
     p->iList = 0;
+    for ( q = p; q < p+nFuncs; q++ )
+       q->iList = 0;
     q = p + 1;
     printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
 
-    vTruths = Vec_WrdAlloc( 100 );
-    vWeights = Vec_IntAlloc( 100 );
+    vTruths  = Vec_WrdStart( nFuncs );
+    vWeights = Vec_IntStart( nFuncs );
+    Vec_WrdClear( vTruths );
+    Vec_IntClear( vWeights );
 
     // create elementary vars
     vStops = Vec_IntAlloc( 10 );
@@ -534,22 +623,27 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
     printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
 
     // create gates
-    for ( n = 0; n < 10; n++ )
+    for ( n = 0; n < Limit; n++ )
     {
-        // set the start and stop
-        pBeg1 = p + Vec_IntEntry( vStops, n );
-        pEnd1 = p + Vec_IntEntry( vStops, n+1 );
-
         // try previous
-        for ( m = 0; m < n; m++ )
-        if ( m+n+1 <= Limit )
+        for ( k = 0; k < Limit; k++ )
+        for ( m = 0; m < Limit; m++ )
         {
+            if ( k + m != n || k > m )
+                continue;
+            // set the start and stop
+            pBeg0 = p + Vec_IntEntry( vStops, k );
+            pEnd0 = p + Vec_IntEntry( vStops, k+1 );
+            // set the start and stop
+            pBeg1 = p + Vec_IntEntry( vStops, m );
+            pEnd1 = p + Vec_IntEntry( vStops, m+1 );
+
             clk2 = clock();
-            pBeg0 = p + Vec_IntEntry( vStops, m );
-            pEnd0 = p + Vec_IntEntry( vStops, m+1 );
-            printf( "Trying %6d x %6d.  ", pEnd0-pBeg0, pEnd1-pBeg1 );
+            printf( "Trying %7d  x %7d.  ", pEnd0-pBeg0, pEnd1-pBeg1 );
             for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
             for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
+            if ( k < m || pThis1 > pThis0 )
+//            if ( n < 5 || Bdc_SpfdCheckOverlap(p, pThis0, pThis1) )
             for ( s = 0; s < 5; s++ )
             {
                 t0 = (s&1)      ? ~pThis0->Truth : pThis0->Truth;
@@ -573,84 +667,40 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
                 *pPlace = q-p;
                 q++;
                 Vec_WrdPush( vTruths, t );
-                Vec_IntPush( vWeights, m+n+1 );
+//                Vec_IntPush( vWeights, n == 5 ? n : n+1 );
+                Vec_IntPush( vWeights, n+1 );
                 if ( q-p == nFuncs )
+                {
+                    printf( "Reached limit of %d functions.\n", nFuncs );
                     goto finish;
+                }
             }
-            Vec_IntPush( vStops, q-p );
-            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", m, n, m+n+1, q-p );
+            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", k, m, n+1, q-p );
             Abc_PrintTime( 1, "Time", clock() - clk2 );
         }
-        if ( n+n+1 > Limit )
-            continue;
-
-        // try current
-        clk2 = clock();
-        printf( "Trying %6d x %6d.  ", pEnd1-pBeg1, pEnd1-pBeg1 );
-        for ( pThis0 = pBeg1; pThis0 < pEnd1; pThis0++ )
-        for ( pThis1 = pThis0+1; pThis1 < pEnd1; pThis1++ )
-        for ( s = 0; s < 5; s++ )
-        {
-            t0 = (s&1)      ? ~pThis0->Truth : pThis0->Truth;
-            t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
-            t  = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
-            fCompl = t & 1;
-            if ( fCompl )
-                t = ~t;
-            if ( t == 0 )
-                continue;
-            pPlace = Bdc_SpfdHashLookup( p, nSize, t );
-            if ( pPlace == NULL )
-                continue;
-            q->iFan0   = pThis0-p;
-            q->fCompl0 = s&1;
-            q->iFan1   = pThis1-p;
-            q->fCompl1 = (s>>1)&1;
-            q->fExor   = (s>>2)&1;
-            q->Truth   = t;
-            q->fCompl  = fCompl;
-            *pPlace = q-p;
-            q++;
-            Vec_WrdPush( vTruths, t );
-            Vec_IntPush( vWeights, n+n+1 );
-            if ( q-p == nFuncs )
-                goto finish;
-        }
         Vec_IntPush( vStops, q-p );
-        assert( n || q-p == 82 );
-        printf( "Added %d + %d + 1 = %d. Total = %8d.   ", n, n, n+n+1, q-p );
-        Abc_PrintTime( 1, "Time", clock() - clk2 );
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
 
-/*
-    {
-        FILE * pFile = fopen( "func6var5node.txt", "w" );
-        word t;
-        Vec_WrdSortUnsigned( vTruths );
-        Vec_WrdForEachEntry( vTruths, t, i )
-            Extra_PrintHex( pFile, (unsigned *)&t, 6 ), fprintf( pFile, "\n" );
-        fclose( pFile );
-    }
-*/
+
     {
-        FILE * pFile = fopen( "func6v5n_bin.txt", "wb" );
-//        Vec_WrdSortUnsigned( vTruths );
+        FILE * pFile = fopen( "func6v6n_bin.txt", "wb" );
         fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
         fclose( pFile );
     }
     {
-        FILE * pFile = fopen( "func6v5nW_bin.txt", "wb" );
+        FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" );
         fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
         fclose( pFile );
     }
 
+
 finish:
     Vec_IntFree( vStops );
-//    Vec_WrdFree( vTruths );
     free( p );
 
     *pvWeights = vWeights;
+//    Vec_WrdFree( vTruths );
     return vTruths;
 }
 
@@ -666,7 +716,38 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Wrd_t * Bdc_SpfdReadFiles( Vec_Int_t ** pvWeights )
+Vec_Wrd_t * Bdc_SpfdReadFiles5( Vec_Int_t ** pvWeights )
+{
+    Vec_Int_t * vWeights;
+    Vec_Wrd_t * vDivs;
+    FILE * pFile;
+    
+    vDivs = Vec_WrdStart( 3863759 );
+    pFile = fopen( "func6v5n_bin.txt", "rb" );
+    fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
+    fclose( pFile );
+
+    vWeights = Vec_IntStart( 3863759 );
+    pFile = fopen( "func6v5nW_bin.txt", "rb" );
+    fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
+    fclose( pFile );
+
+    *pvWeights = vWeights;
+    return vDivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Bdc_SpfdReadFiles6( Vec_Int_t ** pvWeights )
 {
     Vec_Int_t * vWeights;
     Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 );
@@ -785,6 +866,8 @@ int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
     word F0 = ~F1;
     word Func;
     int i, Cost = 0;
+    printf( "Trying: " );
+    Extra_PrintHex( stdout, (unsigned *)&t, 6 ); printf( "\n" );
 //    Abc_Show6VarFunc( F0, F1 );   
     for ( i = 0; F0 && F1; i++ )
     {
@@ -795,7 +878,7 @@ int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
 //        Abc_Show6VarFunc( F0, F1 );    
     }
     Cost += (i-1);
-    printf( "Produce solution with cost %d.\n", Cost );
+    printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) );
     return Cost;
 }
 
@@ -813,24 +896,56 @@ int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
 void Bdc_SpfdDecomposeTest()
 {
 //    word t = 0x5052585a0002080a;
+
     word t = 0x9ef7a8d9c7193a0f;
 //    word t = 0x6BFDA276C7193A0F;
 //    word t = 0xA3756AFE0B1DF60B;
 
+//    word t = 0xFEF7AEBFCE80AA0F;
+//    word t = 0x9EF7FDBFC77F6F0F;
+//    word t = 0xDEF7FDFF377F6FFF;
+
+//    word t = 0x345D02736DB390A5; // xor with var 0
+
+//    word t = 0x3EFDA2736D139A0F; // best solution after changes
+
     Vec_Int_t * vWeights;
     Vec_Wrd_t * vDivs;
     word c0, c1, s, tt, ttt, tbest;
     int i, j, k, n, Cost, CostBest = 100000;
     int clk = clock();
 
-    return;
+//    return;
 
-    // vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
-    vDivs = Bdc_SpfdReadFiles( &vWeights );
+    vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
+//    vDivs = Bdc_SpfdReadFiles5( &vWeights );
 
 //    Abc_Show6VarFunc( ~t, t );  
 
-/*
+    // try function
+    tt = t;
+    Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
+    if ( CostBest > Cost )
+    {
+        CostBest = Cost;
+        tbest = tt;
+    }
+    printf( "\n" );
+
+    // try complemented output
+    for ( i = 0; i < 6; i++ )
+    {
+        tt = t ^ Truths[i];
+        Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
+        if ( CostBest > Cost )
+        {
+            CostBest = Cost;
+            tbest = tt;
+        }
+    }
+    printf( "\n" );
+
+    // try complemented input
     for ( i = 0; i < 6; i++ )
     for ( j = 0; j < 6; j++ )
     {
@@ -848,8 +963,8 @@ void Bdc_SpfdDecomposeTest()
             tbest = tt;
         }
     }
-*/
 
+/*
     for ( i = 0; i < 6; i++ )
     for ( j = 0; j < 6; j++ )
     {
@@ -878,7 +993,7 @@ void Bdc_SpfdDecomposeTest()
             }
         }
     }
-
+*/
 
     printf( "Best solution found with cost %d.  ", CostBest );
     Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
@@ -888,6 +1003,111 @@ void Bdc_SpfdDecomposeTest()
     Vec_IntFree( vWeights );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecomposeTest3()
+{
+    int nSizeM = (1 << 26);
+    int nSizeK = (1 << 3);
+    Vec_Wrd_t * v1M;
+    Vec_Wrd_t * v1K;
+    int i, k, Counter, clk;
+//    int EntryM, EntryK;
+    Aig_ManRandom64( 1 );
+
+    v1M = Vec_WrdAlloc( nSizeM );
+    for ( i = 0; i < nSizeM; i++ )
+        Vec_WrdPush( v1M, Aig_ManRandom64(0) );
+
+    v1K = Vec_WrdAlloc( nSizeK );
+    for ( i = 0; i < nSizeK; i++ )
+        Vec_WrdPush( v1K, Aig_ManRandom64(0) );
+
+    clk = clock();
+    Counter = 0;
+    for ( i = 0; i < nSizeM; i++ )
+    for ( k = 0; k < nSizeK; k++ )
+        Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
+//    Vec_WrdForEachEntry( v1M, EntryM, i )
+//    Vec_WrdForEachEntry( v1K, EntryK, k )
+//        Counter += ((EntryM & EntryK) == EntryK);
+
+    printf( "Total = %8d.  ", Counter );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+    clk = clock();
+    Counter = 0;
+    for ( k = 0; k < nSizeK; k++ )
+    for ( i = 0; i < nSizeM; i++ )
+        Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
+    printf( "Total = %8d.  ", Counter );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecomposeTest8()
+{
+//    word t = 0x9ef7a8d9c7193a0f;
+//    word t = 0x9EF7FDBFC77F6F0F;
+    word t = 0x513B57150819050F;
+
+    Vec_Int_t * vWeights;
+    Vec_Wrd_t * vDivs;
+    word Func, FuncBest;
+    int Cost, CostBest = ABC_INFINITY;
+    int i, clk = clock();
+
+//    return;
+
+    vDivs = Bdc_SpfdReadFiles5( &vWeights );
+
+    printf( "Best init = %4d.  ", Bdc_SpfdAdjCost(t) );
+    Extra_PrintHex( stdout, (unsigned *)&t, 6 ); //printf( "\n" );
+    Abc_PrintTime( 1, "  Time", clock() - clk );
+
+    Vec_WrdForEachEntry( vDivs, Func, i )
+    {
+        Cost = Bdc_SpfdAdjCost( t ^ Func );
+        if ( CostBest > Cost )
+        {
+            CostBest = Cost;
+            FuncBest = Func;
+        }
+    }
+
+    printf( "Best cost = %4d.  ", CostBest );
+    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); //printf( "\n" );
+    Abc_PrintTime( 1, "  Time", clock() - clk );
+
+Abc_Show6VarFunc( 0, t );
+Abc_Show6VarFunc( 0, FuncBest );
+Abc_Show6VarFunc( 0, (FuncBest ^ t) );
+
+    FuncBest ^= t;
+    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f2348d34..fd8d4e07 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -860,7 +860,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
         Dar_LibStart();
     }
     {
-        extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
+//        extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
 //        Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 );
     }
 
@@ -881,10 +881,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
         void For_ManFileExperiment();
 //        For_ManFileExperiment();
     }
-    {
-        void Bdc_SpfdDecomposeTest();
-        Bdc_SpfdDecomposeTest();
-    }
 /*
     {
         int i1, i2, i3, i4, i5, i6, N, Counter = 0;
@@ -8843,7 +8839,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_ManStop( pAig );
 }
 */
-
+/*
 {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
     if ( pAbc->pCex && pNtk )
@@ -8855,8 +8851,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_FrameReplaceCex( pAbc, &pNew );
     }
 }
-
-
+*/
+    {
+        void Bdc_SpfdDecomposeTest();
+        Bdc_SpfdDecomposeTest();
+    }
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );