Major restructuring of the code.

8 files changed, 2691 insertions, 0 deletions

diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h
new file mode 100644
index 00000000..6c88857a
--- /dev/null
+++ b/src/bool/bdc/bdc.h
@@ -0,0 +1,92 @@
+/**CFile****************************************************************
+
+  FileName    [bdc.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdc.h,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__bdc__bdc_h
+#define ABC__aig__bdc__bdc_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+ 
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Bdc_Fun_t_ Bdc_Fun_t;
+typedef struct Bdc_Man_t_ Bdc_Man_t;
+typedef struct Bdc_Par_t_ Bdc_Par_t;
+struct Bdc_Par_t_
+{
+    // general parameters
+    int           nVarsMax;      // the maximum support
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
+};
+
+// working with complemented attributes of objects
+static inline int         Bdc_IsComplement( Bdc_Fun_t * p )      { return (int)((ABC_PTRUINT_T)p & (ABC_PTRUINT_T)01);              }
+static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )           { return (Bdc_Fun_t *)((ABC_PTRUINT_T)p & ~(ABC_PTRUINT_T)01);     }
+static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )               { return (Bdc_Fun_t *)((ABC_PTRUINT_T)p ^  (ABC_PTRUINT_T)01);     }
+static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )    { return (Bdc_Fun_t *)((ABC_PTRUINT_T)p ^  (ABC_PTRUINT_T)(c!=0)); }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bdcCore.c ==========================================================*/
+extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
+extern void        Bdc_ManFree( 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 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 );
+extern int         Bdc_FuncCopyInt( Bdc_Fun_t * p );
+extern void        Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy );
+extern void        Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c
new file mode 100644
index 00000000..58324f81
--- /dev/null
+++ b/src/bool/bdc/bdcCore.c
@@ -0,0 +1,314 @@
+/**CFile****************************************************************
+
+  FileName    [bdcCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [The gateway to bi-decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bdcInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Accessing contents of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;           }
+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;            }
+int          Bdc_FuncCopyInt( Bdc_Fun_t * p )                  { return p->iCopy;            }
+void         Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy )    { p->pCopy = pCopy;           }
+void         Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy )    { p->iCopy = iCopy;           }
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
+{
+    Bdc_Man_t * p;
+    p = ABC_ALLOC( Bdc_Man_t, 1 );
+    memset( p, 0, sizeof(Bdc_Man_t) );
+    assert( pPars->nVarsMax > 1 && pPars->nVarsMax < 16 );
+    p->pPars = pPars;
+    p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
+    p->nDivsLimit = 200;
+    // internal nodes
+    p->nNodesAlloc = 512;
+    p->pNodes = ABC_ALLOC( Bdc_Fun_t, p->nNodesAlloc );
+    // memory
+    p->vMemory = Vec_IntStart( 8 * p->nWords * p->nNodesAlloc );
+    Vec_IntClear(p->vMemory);
+    // set up hash table
+    p->nTableSize = (1 << p->pPars->nVarsMax);
+    p->pTable = ABC_ALLOC( Bdc_Fun_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
+    p->vSpots = Vec_IntAlloc( 256 );
+    // truth tables
+    p->vTruths = Vec_PtrAllocTruthTables( p->pPars->nVarsMax );
+    p->puTemp1 = ABC_ALLOC( unsigned, 4 * p->nWords );
+    p->puTemp2 = p->puTemp1 + p->nWords;
+    p->puTemp3 = p->puTemp2 + p->nWords;
+    p->puTemp4 = p->puTemp3 + p->nWords;
+    // start the internal ISFs
+    p->pIsfOL = &p->IsfOL;  Bdc_IsfStart( p, p->pIsfOL );
+    p->pIsfOR = &p->IsfOR;  Bdc_IsfStart( p, p->pIsfOR );
+    p->pIsfAL = &p->IsfAL;  Bdc_IsfStart( p, p->pIsfAL );
+    p->pIsfAR = &p->IsfAR;  Bdc_IsfStart( p, p->pIsfAR );   
+    return p; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManFree( Bdc_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Bi-decomposition stats: Calls = %d.  Nodes = %d. Reuse = %d.\n", 
+            p->numCalls, p->numNodes, p->numReuse );
+        printf( "ANDs = %d.  ORs = %d.  Weak = %d.  Muxes = %d.  Memory = %.2f K\n", 
+            p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) );
+        ABC_PRT( "Cache", p->timeCache );
+        ABC_PRT( "Check", p->timeCheck );
+        ABC_PRT( "Muxes", p->timeMuxes );
+        ABC_PRT( "Supps", p->timeSupps );
+        ABC_PRT( "TOTAL", p->timeTotal );
+    }
+    Vec_IntFree( p->vMemory );
+    Vec_IntFree( p->vSpots );
+    Vec_PtrFree( p->vTruths );
+    ABC_FREE( p->puTemp1 );
+    ABC_FREE( p->pNodes );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
+{
+    unsigned * puTruth;
+    Bdc_Fun_t * pNode;
+    int i;
+    Bdc_TableClear( p );
+    Vec_IntClear( p->vMemory );
+    // add constant 1 and elementary vars
+    p->nNodes = 0;
+    p->nNodesNew = - 1 - p->nVars - (vDivs? Vec_PtrSize(vDivs) : 0);
+    // add constant 1
+    pNode = Bdc_FunNew( p );
+    pNode->Type = BDC_TYPE_CONST1;
+    pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
+    Kit_TruthFill( pNode->puFunc, p->nVars );
+    pNode->uSupp = 0;
+    Bdc_TableAdd( p, pNode );
+    // add variables
+    for ( i = 0; i < p->nVars; i++ )
+    {
+        pNode = Bdc_FunNew( p );
+        pNode->Type = BDC_TYPE_PI;
+        pNode->puFunc = (unsigned *)Vec_PtrEntry( p->vTruths, i );
+        pNode->uSupp = (1 << i);
+        Bdc_TableAdd( p, pNode );
+    }
+    // add the divisors
+    if ( vDivs )
+    Vec_PtrForEachEntry( unsigned *, vDivs, puTruth, i )
+    {
+        pNode = Bdc_FunNew( p );
+        pNode->Type = BDC_TYPE_PI;
+        pNode->puFunc = puTruth;
+        pNode->uSupp = Kit_TruthSupport( puTruth, p->nVars );
+        Bdc_TableAdd( p, pNode );
+        if ( i == p->nDivsLimit )
+            break;
+    }
+    assert( p->nNodesNew == 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManDecPrint( Bdc_Man_t * p )
+{
+    Bdc_Fun_t * pNode;
+    int i;
+    printf( " 0 : Const 1\n" );
+    for ( i = 1; i < p->nNodes; i++ )
+    {
+        printf( " %d : ", i );
+        pNode = p->pNodes + i;
+        if ( pNode->Type == BDC_TYPE_PI )
+            printf( "PI   " );
+        else
+        {
+            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) );
+        printf( "\n" );
+    }
+    printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
+{
+    Bdc_Isf_t Isf, * pIsf = &Isf;
+    int clk = clock();
+    assert( nVars <= p->pPars->nVarsMax );
+    // set current manager parameters
+    p->nVars = nVars;
+    p->nWords = Kit_TruthWordNum( nVars );
+    p->nNodesMax = nNodesMax;
+    Bdc_ManPrepare( p, vDivs );
+    if ( puCare && Kit_TruthIsConst0( puCare, nVars ) )
+    {
+        p->pRoot = Bdc_Not(p->pNodes);
+        return 0;
+    }
+    // copy the function
+    Bdc_IsfStart( p, pIsf );
+    if ( puCare )
+    {
+        Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
+        Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
+    }
+    else
+    {
+        Kit_TruthCopy( pIsf->puOn, puFunc, p->nVars );
+        Kit_TruthNot( pIsf->puOff, puFunc, p->nVars );
+    }
+    Bdc_SuppMinimize( p, pIsf );
+    // call decomposition
+    p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
+    p->timeTotal += clock() - clk;
+    p->numCalls++;
+    p->numNodes += p->nNodesNew;
+    if ( p->pRoot == NULL )
+        return -1;
+    if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) )
+        printf( "Bdc_ManDecompose(): Internal verification failed.\n" );
+//    assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) );
+    return p->nNodesNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManDecomposeTest( unsigned uTruth, int nVars )
+{
+    static int Counter = 0;
+    static int Total = 0;
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    int RetValue;
+//    unsigned uCare = ~0x888f888f;
+    unsigned uCare = ~0;
+//    unsigned uFunc =  0x88888888;
+//    unsigned uFunc =  0xf888f888;
+//    unsigned uFunc =  0x117e117e;
+//    unsigned uFunc =  0x018b018b;
+    unsigned uFunc = uTruth; 
+
+    pPars->nVarsMax = 8;
+    p = Bdc_ManAlloc( pPars );
+    RetValue = Bdc_ManDecompose( p, &uFunc, &uCare, nVars, NULL, 1000 );
+    Total += RetValue;
+    printf( "%5d : Nodes = %5d. Total = %8d.\n", ++Counter, RetValue, Total );
+//    Bdc_ManDecPrint( p );
+    Bdc_ManFree( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bool/bdc/bdcDec.c b/src/bool/bdc/bdcDec.c
new file mode 100644
index 00000000..61f46f17
--- /dev/null
+++ b/src/bool/bdc/bdcDec.c
@@ -0,0 +1,751 @@
+/**CFile****************************************************************
+
+  FileName    [bdcDec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [Decomposition procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bdcInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int v;
+    int clk = 0; // Suppress "might be used uninitialized"
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    // compute support
+    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
+        Kit_TruthSupport( pIsf->puOff, p->nVars );
+    // go through the support variables
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( (pIsf->uSupp & (1 << v)) == 0 )
+            continue;
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
+        Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
+        if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
+            continue;
+//        if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+//            continue;
+        // remove the variable
+        Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
+        Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
+//        Kit_TruthExist( pIsf->puOn, p->nVars, v );
+//        Kit_TruthExist( pIsf->puOff, p->nVars, v );
+        pIsf->uSupp &= ~(1 << v);
+    }
+    if ( p->pPars->fVerbose )
+        p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int v;
+    int clk = 0; // Suppress "might be used uninitialized"
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    // go through the support variables
+    pIsf->uSupp = 0;
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) && 
+             !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
+              continue;
+        if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+        {
+            Kit_TruthExist( pIsf->puOn, p->nVars, v );
+            Kit_TruthExist( pIsf->puOff, p->nVars, v );
+            continue;
+        }
+        pIsf->uSupp |= (1 << v);
+    }
+    if ( p->pPars->fVerbose )
+        p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the ISF of the right after the left was decompoosed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type )
+{
+    unsigned * puTruth = p->puTemp1;
+    // get the truth table of the left branch
+    if ( Bdc_IsComplement(pFunc0) )
+        Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars );
+    // split into parts
+    if ( Type == BDC_TYPE_OR ) 
+    {
+//        Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
+//        Right.R = bdd_exist( R, setRightRes );
+
+//        if ( pR->Q )  Cudd_RecursiveDeref( dd, pR->Q );
+//        if ( pR->R )  Cudd_RecursiveDeref( dd, pR->R );
+//        pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V );    Cudd_Ref( pR->Q );
+//        pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V );                      Cudd_Ref( pR->R );
+
+//        assert( pR->R != b0 );
+//        return (int)( pR->Q == b0 );
+
+        Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
+        Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq ); 
+        Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq ); 
+//        assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
+        assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
+        return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
+    }
+    else if ( Type == BDC_TYPE_AND )
+    {
+//        Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
+//        Right.Q = bdd_exist( Q, setRightRes );
+
+//        if ( pR->Q )  Cudd_RecursiveDeref( dd, pR->Q );
+//        if ( pR->R )  Cudd_RecursiveDeref( dd, pR->R );
+//        pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V );                Cudd_Ref( pR->R );
+//        pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V );                      Cudd_Ref( pR->Q );
+
+//        assert( pR->Q != b0 );
+//        return (int)( pR->R == b0 );
+
+        Kit_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars );
+        Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq ); 
+        Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq ); 
+//        assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
+        assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
+        return Kit_TruthIsConst0(pIsfR->puOff, p->nVars);
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks existence of OR-bidecomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars )
+{
+    assert( nLeftVars > 0 );
+    assert( nRightVars > 0 );
+    // compute the decomposition coefficient
+    if ( nLeftVars >= nRightVars )
+        return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
+    else // if ( nLeftVars < nRightVars )
+        return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks existence of weak OR-bidecomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+    char pVars[16];
+    int v, nVars, Beg, End;
+
+    assert( pIsfL->uSupp == 0 );
+    assert( pIsfR->uSupp == 0 );
+
+    // fill in the variables
+    nVars = 0;
+    for ( v = 0; v < p->nVars; v++ )
+        if ( pIsf->uSupp & (1 << v) )
+            pVars[nVars++] = v;
+
+    // try variable pairs
+    for ( Beg = 0; Beg < nVars; Beg++ )
+    {
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] ); 
+        for ( End = nVars - 1; End > Beg; End-- )
+        {
+            Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] ); 
+            if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
+            {
+                pIsfL->uUniq = (1 << pVars[Beg]);
+                pIsfR->uUniq = (1 << pVars[End]);
+                return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks existence of weak OR-bidecomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+    int v, VarCost;
+  int VarBest = -1; // Suppress "might be used uninitialized"
+  int Cost, VarCostBest = 0;
+
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( (pIsf->uSupp & (1 << v)) == 0 )
+            continue;
+//        if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
+//        Exist = Cudd_bddExistAbstract( dd, pF->R, Var );   Cudd_Ref( Exist );
+//        if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
+
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
+        if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
+        {
+            // measure the cost of this variable
+//            VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
+//            Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var );   Cudd_Ref( Univ );
+//            VarCost = Kit_TruthCountOnes( Univ, p->nVars );
+//            Cudd_RecursiveDeref( dd, Univ );
+
+            Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
+            VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
+            if ( VarCost == 0 )
+                VarCost = 1;
+            if ( VarCostBest < VarCost )
+            {
+                VarCostBest = VarCost;
+                VarBest = v;
+            }
+        }
+    }
+
+    // derive the components for weak-bi-decomposition if the variable is found
+    if ( VarCostBest )
+    {
+//        funQLeftRes = Q & bdd_exist( R, setRightORweak );
+//        Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest );     Cudd_Ref( Temp );
+//        pL->Q = Cudd_bddAnd( dd, pF->Q, Temp );                    Cudd_Ref( pL->Q );
+//        Cudd_RecursiveDeref( dd, Temp );
+
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
+        Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
+
+//        pL->R = pF->R;                                            Cudd_Ref( pL->R );
+//        pL->V = VarBest;                                        Cudd_Ref( pL->V );
+        Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
+        pIsfL->uUniq = (1 << VarBest);
+        pIsfR->uUniq = 0;
+
+//        assert( pL->Q != b0 );
+//        assert( pL->R != b0 );
+//        assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
+//        assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
+
+        // express cost in percents of the covered boolean space
+        Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
+        if ( Cost == 0 )
+            Cost = 1;
+        return Cost;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks existence of OR-bidecomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+    unsigned uSupportRem;
+    int v, nLeftVars = 1, nRightVars = 1; 
+    // clean the var sets
+    Bdc_IsfStart( p, pIsfL );
+    Bdc_IsfStart( p, pIsfR );
+    // check that the support is correct
+    assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) );
+    assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) );
+    // find initial variable sets
+    if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
+        return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
+    // prequantify the variables in the offset
+    Kit_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq ); 
+    Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq );
+    // go through the remaining variables
+    uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq;
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( (uSupportRem & (1 << v)) == 0 )
+            continue;
+        // prequantify this variable
+        Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
+        Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
+        if ( nLeftVars < nRightVars )
+        {
+//            if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
+//            if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
+            if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
+            {
+//                pL->V &= VarNew;
+                pIsfL->uUniq |= (1 << v);
+                nLeftVars++;
+                Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
+            }
+//            else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
+            else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
+            {
+//                pR->V &= VarNew;
+                pIsfR->uUniq |= (1 << v);
+                nRightVars++;
+                Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
+            }
+        }
+        else
+        {
+//            if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
+            if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
+            {
+//                pR->V &= VarNew;
+                pIsfR->uUniq |= (1 << v);
+                nRightVars++;
+                Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
+            }
+//            else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
+            else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
+            {
+//                pL->V &= VarNew;
+                pIsfL->uUniq |= (1 << v);
+                nLeftVars++;
+                Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
+            }
+        }
+    }
+
+    // derive the functions Q and R for the left branch
+//    pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
+//    pL->R = bdd_exist( pF->R, pR->V );
+
+//    Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V );      Cudd_Ref( Temp );
+//    pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
+//    Cudd_RecursiveDeref( dd, Temp );
+//    pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V );     Cudd_Ref( pL->R );
+
+    Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
+    Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uUniq );
+    Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
+
+//    assert( pL->Q != b0 );
+//    assert( pL->R != b0 );
+//    assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
+    assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
+    assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
+//    assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
+
+    // derive the functions Q and R for the right branch
+//    Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V );      Cudd_Ref( Temp );
+//    pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
+//    Cudd_RecursiveDeref( dd, Temp );
+//    pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V );     Cudd_Ref( pR->R );
+
+    Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
+    Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
+    Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
+
+    assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
+    assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
+//    assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
+
+    assert( pIsfL->uUniq );
+    assert( pIsfR->uUniq );
+    return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );        
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one step of bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+    int WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR;
+
+    Bdc_IsfClean( p->pIsfOL );
+    Bdc_IsfClean( p->pIsfOR );
+    Bdc_IsfClean( p->pIsfAL );
+    Bdc_IsfClean( p->pIsfAR );
+
+    // perform OR decomposition
+    WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
+
+    // perform AND decomposition
+    Bdc_IsfNot( pIsf );
+    WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
+    Bdc_IsfNot( pIsf );
+    Bdc_IsfNot( p->pIsfAL );
+    Bdc_IsfNot( p->pIsfAR );
+
+    // check the case when decomposition does not exist
+    if ( WeightOr == 0 && WeightAnd == 0 )
+    {
+        Bdc_IsfCopy( pIsfL, p->pIsfOL );
+        Bdc_IsfCopy( pIsfR, p->pIsfOR );
+        return BDC_TYPE_MUX;
+    }
+    // check the hash table
+    assert( WeightOr || WeightAnd );
+    WeightOrL = WeightOrR = 0;
+    if ( WeightOr )
+    {
+        if ( p->pIsfOL->uUniq )
+        {
+            Bdc_SuppMinimize( p, p->pIsfOL );
+            WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
+        }
+        if ( p->pIsfOR->uUniq )
+        {
+            Bdc_SuppMinimize( p, p->pIsfOR );
+            WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
+        }
+    }
+    WeightAndL = WeightAndR = 0;
+    if ( WeightAnd )
+    {
+        if ( p->pIsfAL->uUniq )
+        {
+            Bdc_SuppMinimize( p, p->pIsfAL );
+            WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
+        }
+        if ( p->pIsfAR->uUniq )
+        {
+            Bdc_SuppMinimize( p, p->pIsfAR );
+            WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
+        }
+    }
+
+    // check if there is any reuse for the components
+    if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
+    {
+        p->numReuse++;
+        p->numOrs++;
+        Bdc_IsfCopy( pIsfL, p->pIsfOL );
+        Bdc_IsfCopy( pIsfR, p->pIsfOR );
+        return BDC_TYPE_OR;
+    }
+    if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
+    {
+        p->numReuse++;
+        p->numAnds++;
+        Bdc_IsfCopy( pIsfL, p->pIsfAL );
+        Bdc_IsfCopy( pIsfR, p->pIsfAR );
+        return BDC_TYPE_AND; 
+    }
+
+    // compare the two-component costs
+    if ( WeightOr > WeightAnd )
+    {
+        if ( WeightOr < BDC_SCALE )
+            p->numWeaks++;
+        p->numOrs++;
+        Bdc_IsfCopy( pIsfL, p->pIsfOL );
+        Bdc_IsfCopy( pIsfR, p->pIsfOR );
+        return BDC_TYPE_OR;
+    }
+    if ( WeightAnd < BDC_SCALE )
+        p->numWeaks++;
+    p->numAnds++;
+    Bdc_IsfCopy( pIsfL, p->pIsfAL );
+    Bdc_IsfCopy( pIsfR, p->pIsfAR );
+    return BDC_TYPE_AND;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find variable that leads to minimum sum of support sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+    int Var, VarMin, nSuppMin, nSuppCur;
+    unsigned uSupp0, uSupp1;
+    int clk = 0; // Suppress "might be used uninitialized"
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    VarMin = -1;
+    nSuppMin = 1000;
+    for ( Var = 0; Var < p->nVars; Var++ )
+    {
+        if ( (pIsf->uSupp & (1 << Var)) == 0 )
+            continue;
+        Kit_TruthCofactor0New( pIsfL->puOn,  pIsf->puOn,  p->nVars, Var );
+        Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var );
+        Kit_TruthCofactor1New( pIsfR->puOn,  pIsf->puOn,  p->nVars, Var );
+        Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var );
+        uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars );
+        uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars );
+        nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1);  
+        if ( nSuppMin > nSuppCur )
+        {
+            nSuppMin = nSuppCur;
+            VarMin = Var;
+            break;
+        }
+    }
+    if ( VarMin >= 0 )
+    {
+        Kit_TruthCofactor0New( pIsfL->puOn,  pIsf->puOn,  p->nVars, VarMin );
+        Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin );
+        Kit_TruthCofactor1New( pIsfR->puOn,  pIsf->puOn,  p->nVars, VarMin );
+        Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin );
+        Bdc_SuppMinimize( p, pIsfL );
+        Bdc_SuppMinimize( p, pIsfR );
+    }
+    if ( p->pPars->fVerbose )
+        p->timeMuxes += clock() - clk;
+    return VarMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc )
+{
+    unsigned * puTruth = p->puTemp1;
+    if ( Bdc_IsComplement(pFunc) )
+        Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars );
+    return Bdc_TableCheckContainment( p, pIsf, puTruth );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type )
+{
+    Bdc_Fun_t * pFunc;
+    pFunc = Bdc_FunNew( p );
+    if ( pFunc == NULL )
+        return NULL;
+    pFunc->Type = Type;
+    pFunc->pFan0 = pFunc0;
+    pFunc->pFan1 = pFunc1;
+    pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
+    // get the truth table of the left branch
+    if ( Bdc_IsComplement(pFunc0) )
+        Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars );
+    // get the truth table of the right branch
+    if ( Bdc_IsComplement(pFunc1) )
+        Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars );
+    // compute the function of node
+    if ( pFunc->Type == BDC_TYPE_AND )
+    {
+        Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
+    }
+    else if ( pFunc->Type == BDC_TYPE_OR )
+    {
+        Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
+        // transform to AND gate
+        pFunc->Type = BDC_TYPE_AND;
+        pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
+        pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
+        Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
+        pFunc = Bdc_Not(pFunc);
+    }
+    else 
+        assert( 0 );
+    // add to table
+    Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars );
+    Bdc_TableAdd( p, Bdc_Regular(pFunc) );
+    return pFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one step of bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+//    int static Counter = 0;
+//    int LocalCounter = Counter++;
+    Bdc_Type_t Type;
+    Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
+    Bdc_Isf_t IsfL, * pIsfL = &IsfL;
+    Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+    int iVar;
+    int clk = 0; // Suppress "might be used uninitialized"
+/*
+printf( "Init function (%d):\n", LocalCounter );
+Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
+Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
+*/
+    // check computed results
+    assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    pFunc = Bdc_TableLookup( p, pIsf );
+    if ( p->pPars->fVerbose )
+        p->timeCache += clock() - clk;
+    if ( pFunc )
+        return pFunc;
+    // decide on the decomposition type
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+    if ( p->pPars->fVerbose )
+        p->timeCheck += clock() - clk;
+    if ( Type == BDC_TYPE_MUX )
+    {
+        if ( p->pPars->fVerbose )
+            clk = clock();
+        iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+        if ( p->pPars->fVerbose )
+            p->timeMuxes += clock() - clk;
+        p->numMuxes++;
+        pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
+        pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
+        if ( pFunc0 == NULL || pFunc1 == NULL )
+            return NULL;
+        pFunc  = Bdc_FunWithId( p, iVar + 1 );
+        pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND );
+        pFunc1 = Bdc_ManCreateGate( p, pFunc,  pFunc1, BDC_TYPE_AND );
+        if ( pFunc0 == NULL || pFunc1 == NULL )
+            return NULL;
+        pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR );
+    }
+    else
+    {
+        pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
+        if ( pFunc0 == NULL )
+            return NULL;
+        // decompose the right branch
+        if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) )
+        {
+            p->nNodesNew--;
+            return pFunc0;
+        }
+        Bdc_SuppMinimize( p, pIsfR );
+        pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
+        if ( pFunc1 == NULL )
+            return NULL;
+        // create new gate
+        pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
+    }
+    return pFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bool/bdc/bdcInt.h b/src/bool/bdc/bdcInt.h
new file mode 100644
index 00000000..05ce20b6
--- /dev/null
+++ b/src/bool/bdc/bdcInt.h
@@ -0,0 +1,165 @@
+/**CFile****************************************************************
+
+  FileName    [bdcInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__bdc__bdcInt_h
+#define ABC__aig__bdc__bdcInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "src/bool/kit/kit.h"
+#include "bdc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+#define BDC_SCALE 1000  // value used to compute the cost
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// network types
+typedef enum { 
+    BDC_TYPE_NONE = 0,  // 0:  unknown
+    BDC_TYPE_CONST1,    // 1:  constant 1
+    BDC_TYPE_PI,        // 2:  primary input
+    BDC_TYPE_AND,       // 3:  AND-gate
+    BDC_TYPE_OR,        // 4:  OR-gate (temporary)
+    BDC_TYPE_XOR,       // 5:  XOR-gate
+    BDC_TYPE_MUX,       // 6:  MUX-gate
+    BDC_TYPE_OTHER      // 7:  unused
+} Bdc_Type_t;
+
+struct Bdc_Fun_t_
+{
+    int              Type;         // Const1, PI, AND, XOR, MUX
+    Bdc_Fun_t *      pFan0;        // fanin of the given node
+    Bdc_Fun_t *      pFan1;        // fanin of the given node
+    unsigned         uSupp;        // bit mask of current support
+    unsigned *       puFunc;       // the function of the node
+    Bdc_Fun_t *      pNext;        // next function with same support
+    union { int      iCopy;        // the literal of the node (AIG)
+    void *           pCopy; };     // the function of the node (BDD or AIG)
+
+};
+
+typedef struct Bdc_Isf_t_ Bdc_Isf_t;
+struct Bdc_Isf_t_
+{
+    unsigned         uSupp;        // the complete support of this component
+    unsigned         uUniq;        // the unique variables of this component
+    unsigned *       puOn;         // on-set
+    unsigned *       puOff;        // off-set
+};
+
+struct Bdc_Man_t_
+{
+    // external parameters
+    Bdc_Par_t *      pPars;        // parameter set
+    int              nVars;        // the number of variables
+    int              nWords;       // the number of words 
+    int              nNodesMax;    // the limit on the number of new nodes
+    int              nDivsLimit;   // the limit on the number of divisors
+    // internal nodes
+    Bdc_Fun_t *      pNodes;       // storage for decomposition nodes
+    int              nNodesAlloc;  // the number of nodes allocated  
+    int              nNodes;       // the number of all nodes created so far
+    int              nNodesNew;    // the number of new AND nodes created so far
+    Bdc_Fun_t *      pRoot;        // the root node
+    // resub candidates
+    Bdc_Fun_t **     pTable;       // hash table of candidates
+    int              nTableSize;   // hash table size (1 << nVarsMax)
+    Vec_Int_t *      vSpots;       // the occupied spots in the table
+    // elementary truth tables 
+    Vec_Ptr_t *      vTruths;      // for const 1 and elementary variables
+    unsigned *       puTemp1;      // temporary truth table
+    unsigned *       puTemp2;      // temporary truth table
+    unsigned *       puTemp3;      // temporary truth table
+    unsigned *       puTemp4;      // temporary truth table
+    // temporary ISFs
+    Bdc_Isf_t * pIsfOL, IsfOL;
+    Bdc_Isf_t * pIsfOR, IsfOR;
+    Bdc_Isf_t * pIsfAL, IsfAL;
+    Bdc_Isf_t * pIsfAR, IsfAR;
+    // internal memory manager
+    Vec_Int_t *      vMemory;      // memory for internal truth tables
+    // statistics
+    int              numCalls;
+    int              numNodes;
+    int              numMuxes;
+    int              numAnds;
+    int              numOrs;
+    int              numWeaks;
+    int              numReuse;
+    // runtime
+    int              timeCache;
+    int              timeCheck;
+    int              timeMuxes;
+    int              timeSupps;
+    int              timeTotal;
+};
+
+static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p )                   { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; }
+static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id )        { assert( Id < p->nNodes ); return p->pNodes + Id; }
+static inline int         Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun )  { return pFun - p->pNodes; }
+static inline void        Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->uSupp = 0; pF->uUniq = 0; pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); assert( pF->puOff && pF->puOn ); }
+static inline void        Bdc_IsfClean( Bdc_Isf_t * p )                 { p->uSupp = 0; p->uUniq = 0;                                      }
+static inline void        Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q )   { Bdc_Isf_t T = *p; *p = *q; *q = T;                               }
+static inline void        Bdc_IsfNot( Bdc_Isf_t * p )                   { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT;    }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bdcDec.c ==========================================================*/
+extern Bdc_Fun_t *      Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern void             Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern int              Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc );
+/*=== bdcTable.c ==========================================================*/
+extern Bdc_Fun_t *      Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern void             Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
+extern void             Bdc_TableClear( Bdc_Man_t * p );
+extern int              Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/bool/bdc/bdcSpfd.c b/src/bool/bdc/bdcSpfd.c
new file mode 100644
index 00000000..83a35c11
--- /dev/null
+++ b/src/bool/bdc/bdcSpfd.c
@@ -0,0 +1,1176 @@
+/**CFile****************************************************************
+
+  FileName    [bdcSpfd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [The gateway to bi-decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bdcInt.h"
+#include "src/aig/aig/aig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Bdc_Nod_t_ Bdc_Nod_t;
+struct Bdc_Nod_t_
+{
+    unsigned         iFan0g :  8;
+    unsigned         iFan0n : 12;
+    unsigned         Type   : 12;  // 0-3 = AND; 4 = XOR
+
+    unsigned         iFan1g :  8;
+    unsigned         iFan1n : 12;
+    unsigned         Weight : 12;
+
+    word             Truth;
+};
+
+static word Truths[6] = {
+    0xAAAAAAAAAAAAAAAA,
+    0xCCCCCCCCCCCCCCCC,
+    0xF0F0F0F0F0F0F0F0,
+    0xFF00FF00FF00FF00,
+    0xFFFF0000FFFF0000,
+    0xFFFFFFFF00000000
+};
+
+static inline int Bdc_CountOnes( word t )
+{
+    t =    (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555);
+    t =    (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333);
+    t =    (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F);
+    t =    (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF);
+    t =    (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF);
+    return (t & 0x00000000FFFFFFFF) +  (t>>32);
+}
+
+static inline int Bdc_CountSpfd( word t, word f )
+{
+    int n00 = Bdc_CountOnes( ~t & ~f );
+    int n01 = Bdc_CountOnes(  t & ~f );
+    int n10 = Bdc_CountOnes( ~t &  f );
+    int n11 = Bdc_CountOnes(  t &  f );
+    return n00 * n11 + n10 * n01;
+}
+
+static inline word Bdc_Cof6( word t, int iVar, int fCof1 )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    if ( fCof1 )
+        return (t & Truths[iVar]) | ((t & Truths[iVar]) >> (1<<iVar));
+    else
+        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 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdPrint_rec( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels )
+{
+    assert( Level > 0 );
+    printf( "(" );
+
+    if ( pNode->Type & 1 )
+        printf( "!" );
+    if ( pNode->iFan0g == 0 )
+        printf( "%c", 'a' + pNode->iFan0n );
+    else
+    {
+        Bdc_Nod_t * pNode0 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan0g);
+        Bdc_SpfdPrint_rec( pNode0 + pNode->iFan0n, pNode->iFan0g, vLevels );
+    }
+
+    if ( pNode->Type & 4 )
+        printf( "+" );
+    else
+        printf( "*" );
+
+    if ( pNode->Type & 2 )
+        printf( "!" );
+    if ( pNode->iFan1g == 0 )
+        printf( "%c", 'a' + pNode->iFan1n );
+    else
+    {
+        Bdc_Nod_t * pNode1 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan1g);
+        Bdc_SpfdPrint_rec( pNode1 + pNode->iFan1n, pNode->iFan1g, vLevels );
+    }
+
+    printf( ")" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels, word Truth )
+{
+    word Diff = Truth ^ pNode->Truth;
+    Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( "   " );
+    Extra_PrintHex( stdout, (unsigned *)&Diff, 6 );         printf( "   " );
+    Bdc_SpfdPrint_rec( pNode, Level, vLevels );
+    printf( "    %d\n", pNode->Weight );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
+{
+    int nSize = nCands * nCands * (nGatesMax + 1) * 5;
+    Vec_Ptr_t * vLevels;
+    Vec_Int_t * vBegs, * vWeight;
+    Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2;
+    int Count0, Count1, * pPerm;
+    int i, j, k, c, n, clk;
+    assert( nGatesMax < (1<<8) );
+    assert( nCands < (1<<12) );
+    assert( (1<<(nVars-1))*(1<<(nVars-1)) < (1<<12) ); // max SPFD
+
+    printf( "Storage size = %d (%d * %d * %d * %d).\n", nSize, nCands, nCands, nGatesMax + 1, 5 );
+
+    printf( "SPFD = %d.\n", Bdc_CountOnes(Truth) * Bdc_CountOnes(~Truth) );
+
+    // consider elementary functions
+    if ( Truth == 0 || Truth == ~0 )
+    {
+        printf( "Function is a constant.\n" );
+        return;
+    }
+    for ( i = 0; i < nVars; i++ )
+        if ( Truth == Truths[i] || Truth == ~Truths[i] )
+        {
+            printf( "Function is an elementary variable.\n" );
+            return;
+        }
+
+    // allocate
+    vLevels = Vec_PtrAlloc( 100 );
+    vBegs = Vec_IntAlloc( 100 );
+    vWeight = Vec_IntAlloc( 100 );
+
+    // initialize elementary variables
+    pNode = ABC_CALLOC( Bdc_Nod_t, nVars );
+    for ( i = 0; i < nVars; i++ )
+        pNode[i].Truth  = Truths[i];
+    for ( i = 0; i < nVars; i++ )
+        pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
+    Vec_PtrPush( vLevels, pNode );
+    Vec_IntPush( vBegs, nVars );
+
+    // the next level
+clk = clock();
+    pNode0 = pNode;
+    pNode  = ABC_CALLOC( Bdc_Nod_t, 5 * nVars * (nVars - 1) / 2 );
+    for ( c = i = 0; i < nVars; i++ )
+    for ( j = i+1; j < nVars; j++ )
+    {
+        pNode[c].Truth =  pNode0[i].Truth &  pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 0;
+        pNode[c].Truth = ~pNode0[i].Truth &  pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 1;
+        pNode[c].Truth =  pNode0[i].Truth & ~pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 2;
+        pNode[c].Truth = ~pNode0[i].Truth & ~pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 3;
+        pNode[c].Truth =  pNode0[i].Truth ^  pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 4;
+    }
+    assert( c == 5 * nVars * (nVars - 1) / 2 );
+    Vec_PtrPush( vLevels, pNode );
+    Vec_IntPush( vBegs, c );
+    for ( i = 0; i < c; i++ )
+    {
+        pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
+//Bdc_SpfdPrint( pNode + i, 1, vLevels );
+        if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
+        {
+            printf( "Function can be implemented using 1 gate.\n" );
+            pNode = NULL;
+            goto cleanup;
+        }
+    }
+printf( "Selected %6d gates on level %2d.   ", c, 1 );
+Abc_PrintTime( 1, "Time", clock() - clk );
+
+
+    // iterate through levels
+    pNode = ABC_CALLOC( Bdc_Nod_t, nSize );
+    for ( n = 2; n <= nGatesMax; n++ )
+    {
+clk = clock();
+        c = 0;
+        pNode1 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, n-1 );
+        Count1 = Vec_IntEntry( vBegs, n-1 );
+        // go through previous levels
+        for ( k = 0; k < n-1; k++ )
+        {
+            pNode0 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, k );
+            Count0 = Vec_IntEntry( vBegs, k );
+            for ( i = 0; i < Count0; i++ )
+            for ( j = 0; j < Count1; j++ )
+            {
+                pNode[c].Truth =  pNode0[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 0;
+                pNode[c].Truth = ~pNode0[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 1;
+                pNode[c].Truth =  pNode0[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 2;
+                pNode[c].Truth = ~pNode0[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 3;
+                pNode[c].Truth =  pNode0[i].Truth ^  pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 4;
+            }
+            assert( c < nSize );
+        }
+        // go through current level
+        for ( i = 0; i < Count1; i++ )
+        for ( j = i+1; j < Count1; j++ )
+        {
+            pNode[c].Truth =  pNode1[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 0;
+            pNode[c].Truth = ~pNode1[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 1;
+            pNode[c].Truth =  pNode1[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 2;
+            pNode[c].Truth = ~pNode1[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 3;
+            pNode[c].Truth =  pNode1[i].Truth ^  pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 4;
+        }
+        assert( c < nSize );
+        // sort
+        Vec_IntClear( vWeight );
+        for ( i = 0; i < c; i++ )
+        {
+            pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
+if ( pNode[i].Weight > 300 )
+Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
+            Vec_IntPush( vWeight, pNode[i].Weight );
+
+            if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
+            {
+                printf( "Function can be implemented using %d gates.\n", n );
+                Bdc_SpfdPrint( pNode + i, n, vLevels, Truth );
+                goto cleanup;
+            }
+        }
+        pPerm = Abc_SortCost( Vec_IntArray(vWeight), c );
+        assert( Vec_IntEntry(vWeight, pPerm[0]) <= Vec_IntEntry(vWeight, pPerm[c-1]) );
+
+        printf( "Best SPFD = %d.\n", Vec_IntEntry(vWeight, pPerm[c-1]) );
+//        for ( i = 0; i < c; i++ )
+//printf( "%d ", Vec_IntEntry(vWeight, pPerm[i]) );
+
+        // choose the best ones
+        pNode2 = ABC_CALLOC( Bdc_Nod_t, nCands );
+        for ( j = 0, i = c-1; i >= 0; i-- )
+        {
+            pNode2[j++] = pNode[pPerm[i]];
+            if ( j == nCands )
+                break;
+        }
+        ABC_FREE( pPerm );
+        Vec_PtrPush( vLevels, pNode2 );
+        Vec_IntPush( vBegs, j );
+
+printf( "Selected %6d gates (out of %6d) on level %2d.   ", j, c, n );
+Abc_PrintTime( 1, "Time", clock() - clk );
+
+        for ( i = 0; i < 10; i++ )
+            Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
+    }
+
+cleanup:
+    ABC_FREE( pNode );
+    Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i )
+        ABC_FREE( pNode );
+    Vec_PtrFree( vLevels );
+    Vec_IntFree( vBegs );
+    Vec_IntFree( vWeight );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecomposeTest_()
+{
+    int fTry = 0;
+//    word T[17];
+//    int i;
+
+//    word Truth    = Truths[0] & ~Truths[3];
+//    word Truth    = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]);
+//    word Truth    = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5]));
+//    word Truth    = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]);
+//    word Truth = 0x9ef7a8d9c7193a0f;  // AAFFAAFF0A0F0A0F
+//    word Truth = 0x34080226CD163000;
+    word Truth = 0x5052585a0002080a;
+    int nVars     =    6;
+    int nCands    =  200;// 75;
+    int nGatesMax =   20;
+
+    if ( fTry )
+    Bdc_SpfdDecompose( Truth, nVars, nCands, nGatesMax );
+/*
+    for ( i = 0; i < 6; i++ )
+        T[i] = Truths[i];
+    T[7]  = 0;
+    T[8]  = ~T[1]  &  T[3];
+    T[9]  = ~T[8]  &  T[0];
+    T[10] =  T[1]  &  T[4];
+    T[11] =  T[10] &  T[2];
+    T[12] =  T[11] &  T[9];
+    T[13] = ~T[0]  &  T[5];
+    T[14] =  T[2]  &  T[13];
+    T[15] = ~T[12] & ~T[14];
+    T[16] = ~T[15];
+//    if ( T[16] != Truth )
+//        printf( "Failed\n" );
+
+    for ( i = 0; i < 17; i++ )
+    {
+//        printf( "%2d = %3d  ", i, Bdc_CountSpfd(T[i], Truth) );
+        printf( "%2d = %3d  ", i, Bdc_CountSpfd(T[i], T[16]) );
+        Extra_PrintBinary( stdout, (unsigned *)&T[i], 64 ); printf( "\n" );
+    }
+//    Extra_PrintBinary( stdout, (unsigned *)&Truth, 64 ); printf( "\n" );
+*/
+}
+
+
+
+
+typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
+struct Bdc_Ent_t_
+{
+    unsigned         iFan0   : 29;
+    unsigned         fCompl0 :  1;
+    unsigned         fCompl  :  1;
+    unsigned         fMark0  :  1;
+    unsigned         iFan1   : 29;
+    unsigned         fCompl1 :  1;
+    unsigned         fExor   :  1;
+    unsigned         fMark1  :  1;
+    int              iNext;
+    int              iList;
+    word             Truth;
+};
+
+#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*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdHashValue( word t, int Size )
+{
+    // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html
+    // 53,
+    // 97,
+    // 193,
+    // 389,
+    // 769,
+    // 1543,
+    // 3079,
+    // 6151,
+    // 12289,
+    // 24593,
+    // 49157,
+    // 98317,
+    // 196613,
+    // 393241,
+    // 786433,
+    // 1572869,
+    // 3145739,
+    // 6291469,
+    // 12582917,
+    // 25165843,
+    // 50331653,
+    // 100663319,
+    // 201326611,
+    // 402653189,
+    // 805306457,
+    // 1610612741,
+    static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
+    unsigned char * s = (unsigned char *)&t;
+    unsigned i, Value = 0;
+    for ( i = 0; i < 8; i++ )
+        Value ^= BigPrimes[i] * s[i];
+    return Value % Size;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t )
+{
+    Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size );
+    if ( pBin->iList == 0 )
+        return &pBin->iList;
+    for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext )
+    {
+        if ( pBin->Truth == t )
+            return NULL;
+        if ( pBin->iNext == 0 )
+            return &pBin->iNext;
+    }
+    assert( 0 );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
+{
+//    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 nFuncs = 250000000; // the number of functions to compute
+    int nSize  = 201326611; // the hash table size to use
+    int Limit  = 6;
+
+    int * pPlace, i, n, m, k, s, fCompl, clk = clock(), clk2;
+    Vec_Int_t * vStops;
+    Vec_Wrd_t * vTruths;
+    Vec_Int_t * vWeights;
+    Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1;
+    word t0, t1, t;
+    assert( nSize <= nFuncs );
+
+    printf( "Allocating %.2f Mb of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) );
+
+    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_WrdStart( nFuncs );
+    vWeights = Vec_IntStart( nFuncs );
+    Vec_WrdClear( vTruths );
+    Vec_IntClear( vWeights );
+
+    // create elementary vars
+    vStops = Vec_IntAlloc( 10 );
+    Vec_IntPush( vStops, 1 );
+    for ( i = 0; i < 6; i++ )
+    {
+        q->iFan0 = BDC_TERM;
+        q->iFan1 = i;
+        q->Truth = Truths[i];
+        pPlace   = Bdc_SpfdHashLookup( p, nSize, q->Truth );
+        *pPlace  = q-p;
+        q++;
+        Vec_WrdPush( vTruths, Truths[i] );
+        Vec_IntPush( vWeights, 0 );
+    }
+    Vec_IntPush( vStops, 7 );
+    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
+
+    // create gates
+    for ( n = 0; n < Limit; n++ )
+    {
+        // try previous
+        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();
+            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;
+                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 == 5 ? n : n+1 );
+                Vec_IntPush( vWeights, n+1 );
+                if ( q-p == nFuncs )
+                {
+                    printf( "Reached limit of %d functions.\n", nFuncs );
+                    goto finish;
+                }
+            }
+            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", k, m, n+1, q-p );
+            Abc_PrintTime( 1, "Time", clock() - clk2 );
+        }
+        Vec_IntPush( vStops, q-p );
+    }
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+
+    {
+        FILE * pFile = fopen( "func6v6n_bin.txt", "wb" );
+        fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
+        fclose( pFile );
+    }
+    {
+        FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" );
+        fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
+        fclose( pFile );
+    }
+
+
+finish:
+    Vec_IntFree( vStops );
+    free( p );
+
+    *pvWeights = vWeights;
+//    Vec_WrdFree( vTruths );
+    return vTruths;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    FILE * pFile = fopen( "func6v6n_bin.txt", "rb" );
+    fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
+    fclose( pFile );
+
+    vWeights = Vec_IntStart( 12776759 );
+    pFile = fopen( "func6v6nW_bin.txt", "rb" );
+    fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
+    fclose( pFile );
+
+    *pvWeights = vWeights;
+    return vDivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights )
+{
+    int Ones = Bdc_CountOnes(f);
+    if ( Ones == 0 )
+        return -1;
+    return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i));
+//    return Bdc_CountOnes(f);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost )
+{
+    word Func, FuncBest;
+    int i, Cost, CostBest = -1, NumBest;
+    Vec_WrdForEachEntry( vDivs, Func, i )
+    {
+        if ( (Func & F0) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = Func;
+                NumBest  = i;
+            }
+        }
+        if ( (Func & F1) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = Func;
+                NumBest  = i;
+            }
+        }
+        if ( (~Func & F0) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = ~Func;
+                NumBest  = i;
+            }
+        }
+        if ( (~Func & F1) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = ~Func;
+                NumBest  = i;
+            }
+        }
+    }
+    (*pCost) += Vec_IntEntry(vWeights, NumBest);
+    assert( CostBest > 0 );
+    printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) );
+    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
+    return FuncBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
+{
+    word F1 = t;
+    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++ )
+    {
+        printf( "*** ITER %2d   ", i );
+        Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost );
+        F0 &= ~Func;
+        F1 &= ~Func;
+//        Abc_Show6VarFunc( F0, F1 );    
+    }
+    Cost += (i-1);
+    printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) );
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecomposeTest44()
+{
+//    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, tbest;
+    int i, j, Cost, CostBest = 100000;
+    int clk = clock();
+
+    return;
+
+//    printf( "%d\n", RAND_MAX );
+
+    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++ )
+    {
+        if ( i == j )
+            continue;
+        c0 = Bdc_Cof6( t, i, 0 );
+        c1 = Bdc_Cof6( t, i, 1 );
+        s  = Truths[i] ^ Truths[j];
+        tt = (~s & c0) | (s & c1);
+
+        Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
+        if ( CostBest > Cost )
+        {
+            CostBest = Cost;
+            tbest = tt;
+        }
+    }
+
+/*
+    for ( i = 0; i < 6; i++ )
+    for ( j = 0; j < 6; j++ )
+    {
+        if ( i == j )
+            continue;
+        c0 = Bdc_Cof6( t, i, 0 );
+        c1 = Bdc_Cof6( t, i, 1 );
+        s  = Truths[i] ^ Truths[j];
+        tt = (~s & c0) | (s & c1);
+
+        for ( k = 0; k < 6; k++ )
+        for ( n = 0; n < 6; n++ )
+        {
+            if ( k == n )
+                continue;
+            c0 = Bdc_Cof6( tt, k, 0 );
+            c1 = Bdc_Cof6( tt, k, 1 );
+            s  = Truths[k] ^ Truths[n];
+            ttt= (~s & c0) | (s & c1);
+
+            Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights );
+            if ( CostBest > Cost )
+            {
+                CostBest = Cost;
+                tbest = ttt;
+            }
+        }
+    }
+*/
+
+    printf( "Best solution found with cost %d.  ", CostBest );
+    Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
+    Abc_PrintTime( 1, "  Time", clock() - clk );
+
+    Vec_WrdFree( vDivs );
+    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" );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecomposeTest()
+{
+  int nSizeM = (1 << 26);  // big array size
+  int nSizeK = (1 << 3);   // small array size
+  Vec_Wrd_t * v1M, * v1K;
+  int EntryM, EntryK;
+  int i, k, Counter, clk;
+
+  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]);
+  Vec_WrdForEachEntry( v1K, EntryK, k )
+  Vec_WrdForEachEntry( v1M, EntryM, i )
+      Counter += ((EntryM & EntryK) == EntryK);
+  printf( "Total = %8d.  ", Counter );
+  Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bool/bdc/bdcTable.c b/src/bool/bdc/bdcTable.c
new file mode 100644
index 00000000..69f35d88
--- /dev/null
+++ b/src/bool/bdc/bdcTable.c
@@ -0,0 +1,134 @@
+/**CFile****************************************************************
+
+  FileName    [bdcTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [Hash table for intermediate nodes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdcTable.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bdcInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks containment of the function in the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth )
+{
+    return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
+         Kit_TruthIsDisjoint( puTruth, pIsf->puOff, p->nVars );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the new entry to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int fDisableCache = 0;
+    Bdc_Fun_t * pFunc;
+    if ( fDisableCache && Kit_WordCountOnes(pIsf->uSupp) > 1 )
+        return NULL;
+    if ( pIsf->uSupp == 0 )
+    {
+        assert( p->pTable[pIsf->uSupp] == p->pNodes );
+        if ( Kit_TruthIsConst1( pIsf->puOn, p->nVars ) )
+            return p->pNodes;
+        assert( Kit_TruthIsConst1( pIsf->puOff, p->nVars ) );
+        return Bdc_Not(p->pNodes);
+    }
+    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
+        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
+             return pFunc;
+    Bdc_IsfNot( pIsf );
+    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
+        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
+        {
+            Bdc_IsfNot( pIsf );
+            return Bdc_Not(pFunc);
+        }
+    Bdc_IsfNot( pIsf );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the new entry to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc )
+{
+    if ( p->pTable[pFunc->uSupp] == NULL )
+        Vec_IntPush( p->vSpots, pFunc->uSupp );
+    pFunc->pNext = p->pTable[pFunc->uSupp];
+    p->pTable[pFunc->uSupp] = pFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the new entry to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_TableClear( Bdc_Man_t * p )
+{
+    int Spot, i;
+    Vec_IntForEachEntry( p->vSpots, Spot, i )
+        p->pTable[Spot] = NULL;
+    Vec_IntClear( p->vSpots );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bool/bdc/bdc_.c b/src/bool/bdc/bdc_.c
new file mode 100644
index 00000000..b29d4f5e
--- /dev/null
+++ b/src/bool/bdc/bdc_.c
@@ -0,0 +1,54 @@
+/**CFile****************************************************************
+
+  FileName    [bdc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bdcInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bool/bdc/module.make b/src/bool/bdc/module.make
new file mode 100644
index 00000000..0bd5084e
--- /dev/null
+++ b/src/bool/bdc/module.make
@@ -0,0 +1,5 @@
+SRC +=  src/bool/bdc/bdcCore.c \
+    src/bool/bdc/bdcDec.c \
+    src/bool/bdc/bdcSpfd.c \
+    src/bool/bdc/bdcTable.c
+