Adding command 'testdec'.

6 files changed, 630 insertions, 22 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index efbc888c..74fe7fc2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4811,7 +4811,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_DecTest( char * pFileName, int DecType );
+    extern int Abc_DecTest( char * pFileName, int DecType, int fVerbose );
     char * pFileName;
     int c;
     int fVerbose = 0;
@@ -4849,17 +4849,17 @@ int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the testbench
-    Abc_DecTest( pFileName, DecType );
+    Abc_DecTest( pFileName, DecType, fVerbose );
     return 0;
 
 usage:
     Abc_Print( -2, "usage: testdec [-A <num>] [-vh] <file_name>\n" );
     Abc_Print( -2, "\t           testbench for Boolean decomposition algorithms\n" );
-    Abc_Print( -2, "\t-A <num> : number of decomposition algorithm [default = %d]\n", DecType );
-    Abc_Print( -2, "\t      0  : none (just read the input file)\n" );
-    Abc_Print( -2, "\t      1  : algebraic factoring applied to ISOP\n" );
-    Abc_Print( -2, "\t      2  : bi-decomposition with cofactoring\n" );
-    Abc_Print( -2, "\t      3  : disjoint-support decomposition\n" );
+    Abc_Print( -2, "\t-A <num> : decomposition algorithm [default = %d]\n", DecType );
+    Abc_Print( -2, "\t               0: none (reading and writing the file)\n" );
+    Abc_Print( -2, "\t               1: algebraic factoring applied to ISOP\n" );
+    Abc_Print( -2, "\t               2: bi-decomposition with cofactoring\n" );
+    Abc_Print( -2, "\t               3: disjoint-support decomposition with cofactoring\n" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 916866ad..8f0d1df8 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -18,7 +18,12 @@
 
 ***********************************************************************/
 
-#include "base/abc/abc.h"
+#include "misc/extra/extra.h"
+#include "misc/vec/vec.h"
+
+#include "bool/bdc/bdc.h"
+#include "bool/dec/dec.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,10 +38,460 @@ ABC_NAMESPACE_IMPL_START
 // 2 - bi-decomposition
 // 3 - DSD
 
+// data-structure to store a bunch of truth tables
+typedef struct Abc_TtStore_t_  Abc_TtStore_t;
+struct Abc_TtStore_t_ 
+{
+    int      nVars;
+    int      nwords;
+    int      nFuncs;
+    word **  pFuncs;
+};
+
+// read/write/flip i-th bit of a bit string table:
+static inline int     Abc_TruthGetBit( word * p, int i )         { return (int)(p[i>>6] >> (i & 63)) & 1;        }
+static inline void    Abc_TruthSetBit( word * p, int i )         { p[i>>6] |= (((word)1)<<(i & 63));             }
+static inline void    Abc_TruthXorBit( word * p, int i )         { p[i>>6] ^= (((word)1)<<(i & 63));             }
+
+// read/write k-th digit d of a hexadecimal number:
+static inline int     Abc_TruthGetHex( word * p, int k )         { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15;  }
+static inline void    Abc_TruthSetHex( word * p, int k, int d )  { p[k>>4] |= (((word)d)<<((k<<2) & 63));        }
+static inline void    Abc_TruthXorHex( word * p, int k, int d )  { p[k>>4] ^= (((word)d)<<((k<<2) & 63));        }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+// read one hex character
+static inline int  Abc_TruthReadHexDigit( char HexChar )
+{
+    if ( HexChar >= '0' && HexChar <= '9' )
+        return HexChar - '0';
+    if ( HexChar >= 'A' && HexChar <= 'F' )
+        return HexChar - 'A' + 10;
+    if ( HexChar >= 'a' && HexChar <= 'f' )
+        return HexChar - 'a' + 10;
+    assert( 0 ); // not a hexadecimal symbol
+    return -1; // return value which makes no sense
+}
+
+// write one hex character
+static inline void Abc_TruthWriteHexDigit( FILE * pFile, int HexDigit )
+{
+    assert( HexDigit >= 0 && HexDigit < 16 );
+    if ( HexDigit < 10 )
+        fprintf( pFile, "%d", HexDigit );
+    else
+        fprintf( pFile, "%c", 'A' + HexDigit-10 );
+}
+
+// read one truth table in hexadecimal
+void Abc_TruthReadHex( word * pTruth, char * pString, int nVars )
+{
+    int nwords = (nVars < 7)? 1 : (1 << (nVars-6));
+    int k, Digit, nDigits = (nwords << 4);
+    char EndSymbol;
+    // skip the first 2 symbols if they are "0x"
+    if ( pString[0] == '0' && pString[1] == 'x' )
+        pString += 2;
+    // get the last symbol
+    EndSymbol = pString[nDigits];
+    // the end symbol of the TT (the one immediately following hex digits)
+    // should be one of the following: space, a new-line, or a zero-terminator
+    // (note that on Windows symbols '\r' can be inserted before each '\n')
+    assert( EndSymbol == ' ' || EndSymbol == '\n' || EndSymbol == '\r' || EndSymbol == '\0' );
+    // read hexadecimal digits in the reverse order
+    // (the last symbol in the string is the least significant digit)
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = Abc_TruthReadHexDigit( pString[nDigits - 1 - k] );
+        assert( Digit >= 0 && Digit < 16 );
+        Abc_TruthSetHex( pTruth, k, Digit );
+    }
+}
+
+// write one truth table in hexadecimal (do not add end-of-line!)
+void Abc_TruthWriteHex( FILE * pFile, word * pTruth, int nVars )
+{
+    int nDigits, Digit, k;
+    // write hexadecimal digits in the reverse order
+    // (the last symbol in the string is the least significant digit)
+    nDigits = (1 << (nVars-2));
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = Abc_TruthGetHex( pTruth, nDigits - 1 - k );
+        assert( Digit >= 0 && Digit < 16 );
+        Abc_TruthWriteHexDigit( pFile, Digit );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate/Deallocate storage for truth tables..]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_TtStore_t * Abc_TruthStoreAlloc( int nVars, int nFuncs )
+{
+    Abc_TtStore_t * p;
+    int i;
+    p = (Abc_TtStore_t *)malloc( sizeof(Abc_TtStore_t) );
+    p->nVars  =  nVars;
+    p->nwords = (nVars < 7) ? 1 : (1 << (nVars-6));
+    p->nFuncs =  nFuncs;
+    // alloc array of 'nFuncs' pointers to truth tables
+    p->pFuncs = (word **)malloc( sizeof(word *) * p->nFuncs );
+    // alloc storage for 'nFuncs' truth tables as one chunk of memory
+    p->pFuncs[0] = (word *)calloc( sizeof(word), p->nFuncs * p->nwords );
+    // split it up into individual truth tables
+    for ( i = 1; i < p->nFuncs; i++ )
+        p->pFuncs[i] = p->pFuncs[i-1] + p->nwords;
+    return p;
+}
+void Abc_TruthStoreFree( Abc_TtStore_t * p )
+{
+    free( p->pFuncs[0] );
+    free( p->pFuncs );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read file contents.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_FileRead( char * pFileName )
+{
+    FILE * pFile;
+    char * pBuffer;
+    int nFileSize;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = (char *)malloc( nFileSize + 3 );
+    fread( pBuffer, nFileSize, 1, pFile );
+    // add several empty lines at the end
+    // (these will be used to signal the end of parsing)
+    pBuffer[ nFileSize + 0] = '\n';
+    pBuffer[ nFileSize + 1] = '\n';
+    // terminate the string with '\0'
+    pBuffer[ nFileSize + 2] = '\0';
+    fclose( pFile );
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the number of variables by reading the first line.]
+
+  Description [Determine the number of functions by counting the lines.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthGetParams( char * pFileName, int * pnVars, int * pnTruths )
+{
+    char * pContents;
+    int i, nVars, nLines;
+    // prepare the output 
+    if ( pnVars )
+        *pnVars = 0;
+    if ( pnTruths )
+        *pnTruths = 0;
+    // read data from file
+    pContents = Abc_FileRead( pFileName );
+    if ( pContents == NULL )
+        return;
+    // count the number of symbols before the first space or new-line
+    // (note that on Windows symbols '\r' can be inserted before each '\n')
+    for ( i = 0; pContents[i]; i++ )
+        if ( pContents[i] == ' ' || pContents[i] == '\n' || pContents[i] == '\r' )
+            break;
+    if ( pContents[i] == 0 )
+        printf( "Strange, the input file does not have spaces and new-lines...\n" );
+
+    // acount for the fact that truth tables may have "0x" at the beginning of each line
+    if ( pContents[0] == '0' && pContents[1] == 'x' )
+        i = i - 2;
+
+    // determine the number of variables
+    for ( nVars = 0; nVars < 32; nVars++ )
+        if ( 4 * i == (1 << nVars) ) // the number of bits equal to the size of truth table
+            break;
+    if ( nVars < 2 || nVars > 16 )
+    {
+        printf( "Does not look like the input file contains truth tables...\n" );
+        return;
+    }
+    if ( pnVars )
+        *pnVars = nVars;
+
+    // determine the number of functions by counting the lines
+    nLines = 0;
+    for ( i = 0; pContents[i]; i++ )
+        nLines += (pContents[i] == '\n');
+    if ( pnTruths )
+        *pnTruths = nLines;
+    ABC_FREE( pContents );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthStoreRead( char * pFileName, Abc_TtStore_t * p )
+{
+    char * pContents;
+    int i, nLines;
+    pContents = Abc_FileRead( pFileName );
+    if ( pContents == NULL )
+        return;
+    // here it is assumed (without checking!) that each line of the file 
+    // begins with a string of hexadecimal chars followed by space
+
+    // the file will be read till the first empty line (pContents[i] == '\n')
+    // (note that Abc_FileRead() added several empty lines at the end of the file contents)
+    for ( nLines = i = 0; pContents[i] != '\n'; )
+    {
+        // read one line
+        Abc_TruthReadHex( p->pFuncs[nLines++], &pContents[i], p->nVars );
+        // skip till after the end-of-line symbol
+        // (note that end-of-line symbol is also skipped)
+        while ( pContents[i++] != '\n' );
+    }
+    // adjust the number of functions read 
+    // (we may have allocated more storage because some lines in the file were empty)
+    assert( p->nFuncs >= nLines );
+    p->nFuncs = nLines;
+    ABC_FREE( pContents );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write truth tables into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthStoreWrite( char * pFileName, Abc_TtStore_t * p )
+{
+    FILE * pFile;
+    int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars );
+        fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from input file and write them into output file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthStoreTest( char * pFileName )
+{ 
+    Abc_TtStore_t * p;
+    char * pFileInput  = pFileName;
+    char * pFileOutput = "out.txt";
+    int nVars, nTruths;
+
+    // figure out how many truth table and how many variables
+    Abc_TruthGetParams( pFileInput, &nVars, &nTruths );
+    if ( nVars < 2 || nVars > 16 || nTruths == 0 )
+        return;
+
+    // allocate data-structure
+    p = Abc_TruthStoreAlloc( nVars, nTruths );
+
+    // read info from file
+    Abc_TruthStoreRead( pFileInput, p );
+
+    // write into another file
+    Abc_TruthStoreWrite( pFileOutput, p );
+
+    // delete data-structure
+    Abc_TruthStoreFree( p );
+    printf( "Input file \"%s\" was copied into output file \"%s\".\n", pFileInput, pFileOutput );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Apply decomposition to the truth table.]
+
+  Description [Returns the number of AIG nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
+{
+    clock_t clk = clock();
+    int i, nNodes = 0;
+
+    char * pAlgoName = NULL;
+    if ( DecType == 1 )
+        pAlgoName = "factoring";
+    else if ( DecType == 2 )
+        pAlgoName = "bi-decomp";
+    else if ( DecType == 3 )
+        pAlgoName = "DSD";
+
+    if ( pAlgoName )
+        printf( "Applying %-10s to %8d func%s of %2d vars...  ",  
+            pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars );
+    if ( fVerbose )
+        printf( "\n" );
+
+    if ( DecType == 1 )
+    {
+        // perform algebraic factoring and count AIG nodes
+        Dec_Graph_t * pFForm;
+        Vec_Int_t * vCover;
+        Vec_Str_t * vStr;
+        char * pSopStr;
+        vStr = Vec_StrAlloc( 10000 );
+        vCover = Vec_IntAlloc( 1 << 16 );
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            pSopStr = Kit_PlaFromTruthNew( (unsigned *)p->pFuncs[i], p->nVars, vCover, vStr );
+            pFForm = Dec_Factor( pSopStr );
+            nNodes += Dec_GraphNodeNum( pFForm );
+            if ( fVerbose )
+                Dec_GraphPrint( stdout, pFForm, NULL, NULL );
+            Dec_GraphFree( pFForm );
+        }
+        Vec_IntFree( vCover );
+        Vec_StrFree( vStr );
+    }
+    else if ( DecType == 2 )
+    {
+        // perform bi-decomposition and count AIG nodes
+        Bdc_Man_t * pManDec;
+        Bdc_Par_t Pars = {0}, * pPars = &Pars;
+        pPars->nVarsMax = p->nVars;
+        pManDec = Bdc_ManAlloc( pPars );
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d :      ", i );
+            Bdc_ManDecompose( pManDec, (unsigned *)p->pFuncs[i], NULL, p->nVars, NULL, 1000 );
+            nNodes += Bdc_ManAndNum( pManDec );
+            if ( fVerbose )
+                Bdc_ManDecPrint( pManDec );
+        }
+        Bdc_ManFree( pManDec );
+    }
+    else if ( DecType == 3 )
+    {
+        // perform disjoint-support decomposition and count AIG nodes
+        // (non-DSD blocks are decomposed into 2:1 MUXes, each counting as 3 AIG nodes)
+        Kit_DsdNtk_t * pNtk;
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d :      ", i );
+            pNtk = Kit_DsdDecomposeMux( (unsigned *)p->pFuncs[i], p->nVars, 3 );
+            if ( fVerbose )
+                Kit_DsdPrintExpanded( pNtk ), printf( "\n" );
+            nNodes += Kit_DsdCountAigNodes( pNtk );
+            Kit_DsdNtkFree( pNtk );
+        }
+    }
+    else assert( 0 );
+
+    printf( "AIG nodes =%9d  ", nNodes );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Apply decomposition to truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthDecTest( char * pFileName, int DecType, int fVerbose )
+{
+    Abc_TtStore_t * p;
+    int nVars, nTruths;
+
+    // figure out how many truth tables and how many variables
+    Abc_TruthGetParams( pFileName, &nVars, &nTruths );
+    if ( nVars < 2 || nVars > 16 || nTruths == 0 )
+        return;
+
+    // allocate data-structure
+    p = Abc_TruthStoreAlloc( nVars, nTruths );
+
+    // read info from file
+    Abc_TruthStoreRead( pFileName, p );
+
+    // consider functions from the file
+    Abc_TruthDecPerform( p, DecType, fVerbose );
+
+    // delete data-structure
+    Abc_TruthStoreFree( p );
+//    printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName );
+}
+
 
 /**Function*************************************************************
 
@@ -49,14 +504,20 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_DecTest( char * pFileName, int DecType )
+int Abc_DecTest( char * pFileName, int DecType, int fVerbose )
 {
-    printf( "Trying to read file \"%s\".\n", pFileName );
+    if ( fVerbose )
+        printf( "Using truth tables from file \"%s\"...\n", pFileName );
+    if ( DecType == 0 )
+        Abc_TruthStoreTest( pFileName );
+    else if ( DecType >= 1 && DecType <= 3 )
+        Abc_TruthDecTest( pFileName, DecType, fVerbose );
+    else
+        printf( "Unknown decomposition type value (%d).\n", DecType );
     fflush( stdout );
     return 0;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h
index a7572fe8..bd0f7d7d 100644
--- a/src/bool/bdc/bdc.h
+++ b/src/bool/bdc/bdc.h
@@ -67,10 +67,12 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )    { return (Bdc_F
 /*=== bdcCore.c ==========================================================*/
 extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
 extern void        Bdc_ManFree( Bdc_Man_t * p );
+extern void        Bdc_ManDecPrint( Bdc_Man_t * p );
 extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
 extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i );
 extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p );
 extern int         Bdc_ManNodeNum( Bdc_Man_t * p );
+extern int         Bdc_ManAndNum( Bdc_Man_t * p );
 extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p );
 extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p );
 extern void *      Bdc_FuncCopy( Bdc_Fun_t * p );
diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c
index fb318e0d..a810146d 100644
--- a/src/bool/bdc/bdcCore.c
+++ b/src/bool/bdc/bdcCore.c
@@ -46,6 +46,7 @@ ABC_NAMESPACE_IMPL_START
 Bdc_Fun_t *  Bdc_ManFunc( Bdc_Man_t * p, int i )               { return Bdc_FunWithId(p, i); }
 Bdc_Fun_t *  Bdc_ManRoot( Bdc_Man_t * p )                      { return p->pRoot;            }
 int          Bdc_ManNodeNum( Bdc_Man_t * p )                   { return p->nNodes;           }
+int          Bdc_ManAndNum( Bdc_Man_t * p )                    { return p->nNodes-p->nVars-1;}
 Bdc_Fun_t *  Bdc_FuncFanin0( Bdc_Fun_t * p )                   { return p->pFan0;            }
 Bdc_Fun_t *  Bdc_FuncFanin1( Bdc_Fun_t * p )                   { return p->pFan1;            }
 void *       Bdc_FuncCopy( Bdc_Fun_t * p )                     { return p->pCopy;            }
@@ -186,7 +187,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
 
 /**Function*************************************************************
 
-  Synopsis    [Clears the manager.]
+  Synopsis    [Prints bi-decomposition in a simple format.]
 
   Description []
                
@@ -195,7 +196,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
   SeeAlso     []
 
 ***********************************************************************/
-void Bdc_ManDecPrint( Bdc_Man_t * p )
+void Bdc_ManDecPrintSimple( Bdc_Man_t * p )
 {
     Bdc_Fun_t * pNode;
     int i;
@@ -211,7 +212,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
             printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) );
             printf( " %s%d   ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) );
         }
-        Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
+//        Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
         printf( "\n" );
     }
     printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
@@ -219,6 +220,65 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints bi-decomposition recursively.]
+
+  Description [This procedure prints bi-decomposition as a factored form.
+  In doing so, logic sharing, if present, will be replicated several times.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManDecPrint_rec( Bdc_Man_t * p, Bdc_Fun_t * pNode )
+{
+    if ( pNode->Type == BDC_TYPE_PI )
+        printf( "%c", 'a' + Bdc_FunId(p,pNode) - 1 );
+    else if ( pNode->Type == BDC_TYPE_AND )
+    {
+        Bdc_Fun_t * pNode0 = Bdc_FuncFanin0( pNode );
+        Bdc_Fun_t * pNode1 = Bdc_FuncFanin1( pNode );
+
+        if ( Bdc_IsComplement(pNode0) )
+            printf( "!" );
+        if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
+            printf( "(" );
+        Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode0) );
+        if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
+            printf( ")" );
+
+        if ( Bdc_IsComplement(pNode1) )
+            printf( "!" );
+        if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
+            printf( "(" );
+        Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode1) );
+        if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
+            printf( ")" );
+    }
+    else assert( 0 );
+}
+void Bdc_ManDecPrint( Bdc_Man_t * p )
+{
+    Bdc_Fun_t * pRoot = Bdc_Regular(p->pRoot);
+
+    printf( "F = " );
+    if ( pRoot->Type == BDC_TYPE_CONST1 ) // constant 0
+        printf( "Constant %d", !Bdc_IsComplement(p->pRoot) );
+    else if ( pRoot->Type == BDC_TYPE_PI ) // literal
+        printf( "%s%d", Bdc_IsComplement(p->pRoot) ? "!" : "", Bdc_FunId(p,pRoot)-1 );
+    else
+    {
+        if ( Bdc_IsComplement(p->pRoot) )
+            printf( "!(" );
+        Bdc_ManDecPrint_rec( p, pRoot );
+        if ( Bdc_IsComplement(p->pRoot) )
+            printf( ")" );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs decomposition of one function.]
 
   Description []
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index dfee532e..8151f1d2 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -112,17 +112,17 @@ struct Kit_DsdObj_t_
     unsigned       Offset     : 8;  // offset to the truth table
     unsigned       nRefs      : 8;  // offset to the truth table
     unsigned       nFans      : 6;  // the number of fanins of this node
-    unsigned char  pFans[0];        // the fanin literals
+    unsigned short pFans[0];        // the fanin literals
 };
 
 // DSD network
 typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
 struct Kit_DsdNtk_t_
 {
-    unsigned char  nVars;           // at most 16 (perhaps 18?)
-    unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
-    unsigned char  nNodes;          // the number of nodes
-    unsigned char  Root;            // the root of the tree
+    unsigned short nVars;           // at most 16 (perhaps 18?)
+    unsigned short nNodesAlloc;     // the number of allocated nodes (at most nVars)
+    unsigned short nNodes;          // the number of nodes
+    unsigned short Root;            // the root of the tree
     unsigned *     pMem;            // memory for the truth tables (memory manager?)
     unsigned *     pSupps;          // supports of the nodes
     Kit_DsdObj_t** pNodes;          // the nodes
@@ -142,7 +142,7 @@ struct Kit_DsdMan_t_
     Vec_Int_t *    vNodes;          // temporary array for BDD nodes
 };
  
-static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
+static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 1) + ((nFans & 1) > 0);                    }
 static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
 static inline int             Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
 static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )      { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
@@ -538,6 +538,7 @@ extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
 extern Kit_DsdObj_t *  Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
+extern int             Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdGetSupports( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c
index 3df16d8c..d026afbc 100644
--- a/src/bool/kit/kitDsd.c
+++ b/src/bool/kit/kitDsd.c
@@ -1485,7 +1485,7 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, unsigned piLitsRes[] )
+void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] )
 {
     int nSuppSizes[16], Priority[16], pOrder[16];
     int i, k, iVarBest, SuppMax, PrioMax;
@@ -1827,6 +1827,90 @@ int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned iLit, i, RetValue;
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    if ( pObj == NULL )
+        return 0;
+    if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR )
+        return 0;
+    if ( pObj->nFans < 2 ) // why this happens? - need to figure out
+        return 0; 
+    assert( pObj->nFans > 1 );
+    if ( pObj->Type == KIT_DSD_AND )
+        RetValue = ((int)pObj->nFans - 1);
+    else if ( pObj->Type == KIT_DSD_XOR )
+        RetValue = ((int)pObj->nFans - 1) * 3;
+    else if ( pObj->Type == KIT_DSD_PRIME )
+    {
+        // assuming MUX decomposition
+        assert( (int)pObj->nFans == 3 );
+        RetValue = 3;
+    }
+    else assert( 0 );
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk )
+{
+    return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj;
+    int i, Counter = 0;
+    for ( i = 0; i < pNtk->nNodes; i++ )
+    {
+        pObj = pNtk->pNodes[i];
+        if ( pObj->Type == KIT_DSD_AND )
+            Counter += ((int)pObj->nFans - 1);
+        else if ( pObj->Type == KIT_DSD_XOR )
+            Counter += ((int)pObj->nFans - 1) * 3;
+        else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition
+            Counter += 3;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
 
   Description []
@@ -1883,7 +1967,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux )
+void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux )
 {
     Kit_DsdObj_t * pRes, * pRes0, * pRes1;
     int nWords = Kit_TruthWordNum(pObj->nFans);