Version abc80130

7 files changed, 0 insertions, 1066 deletions

diff --git a/src/aig/bdc/bdc.h b/src/aig/bdc/bdc.h
deleted file mode 100644
index 71875edb..00000000
--- a/src/aig/bdc/bdc.h
+++ /dev/null
@@ -1,73 +0,0 @@
-/**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 __BDC_H__
-#define __BDC_H__
- 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-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
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      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 nNodesLimit );
-
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
deleted file mode 100644
index 157927b1..00000000
--- a/src/aig/bdc/bdcCore.c
+++ /dev/null
@@ -1,189 +0,0 @@
-/**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"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocate resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
-{
-    Bdc_Man_t * p;
-    unsigned * pData;
-    int i, k, nBits;
-    p = ALLOC( Bdc_Man_t, 1 );
-    memset( p, 0, sizeof(Bdc_Man_t) );
-    assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
-    p->pPars = pPars;
-    p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
-    p->nDivsLimit = 200;
-    p->nNodesLimit = 0; // will be set later
-    // memory
-    p->vMemory = Vec_IntStart( 1 << 16 );
-    // internal nodes
-    p->nNodesAlloc = 512;
-    p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
-    // set up hash table
-    p->nTableSize = (1 << p->pPars->nVarsMax);
-    p->pTable = 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_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords );
-    // set elementary truth tables
-    nBits = (1 << pPars->nVarsMax);
-    Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars );
-    for ( k = 0; k < pPars->nVarsMax; k++ )
-    {
-        pData = Vec_PtrEntry( p->vTruths, k+1 );
-        Kit_TruthClear( pData, p->nVars );
-        for ( i = 0; i < nBits; i++ )
-            if ( i & (1 << k) )
-                pData[i>>5] |= (1 << (i&31));
-    }
-    p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 );
-    p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 );
-    p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 );
-    p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 );
-    // 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 )
-{
-    Vec_IntFree( p->vMemory );
-    Vec_IntFree( p->vSpots );
-    Vec_PtrFree( p->vTruths );
-    free( p->pNodes );
-    free( p->pTable );
-    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 = p->nNodesNew = 0;
-    for ( i = 0; i <= p->pPars->nVarsMax; i++ )
-    {
-        pNode = Bdc_FunNew( p );
-        pNode->Type = BDC_TYPE_PI;
-        pNode->puFunc = Vec_PtrEntry( p->vTruths, i );
-        pNode->uSupp = i? (1 << (i-1)) : 0;
-        Bdc_TableAdd( p, pNode );
-    }
-    // add the divisors
-    Vec_PtrForEachEntry( 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;
-    }
-}
-
-/**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;
-    // set current manager parameters
-    p->nVars = nVars;
-    p->nWords = Kit_TruthWordNum( nVars );
-    Bdc_ManPrepare( p, vDivs );
-    p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc;
-    // copy the function
-    Bdc_IsfStart( p, pIsf );
-    Bdc_IsfClean( pIsf );
-    pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
-    Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
-    Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
-    // call decomposition
-    Bdc_SuppMinimize( p, pIsf );
-    p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
-    if ( p->pRoot == NULL )
-        return -1;
-    return p->nNodesNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c
deleted file mode 100644
index 747fcb14..00000000
--- a/src/aig/bdc/bdcDec.c
+++ /dev/null
@@ -1,461 +0,0 @@
-/**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"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR );
-static int        Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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 )
-{
-    Bdc_Fun_t * pFunc;
-    Bdc_Isf_t IsfL, * pIsfL = &IsfL;
-    Bdc_Isf_t IsfB, * pIsfR = &IsfB;
-    // check computed results
-    if ( pFunc = Bdc_TableLookup( p, pIsf ) )
-        return pFunc;
-    // decide on the decomposition type
-    pFunc = Bdc_FunNew( p );
-    if ( pFunc == NULL )
-        return NULL;
-    pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
-    // decompose the left branch
-    pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL );
-    if ( pFunc->pFan0 == NULL )
-        return NULL;
-    // decompose the right branch
-    if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) )
-    {
-        p->nNodes--;
-        return pFunc->pFan0;
-    }
-    pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL );
-    if ( pFunc->pFan1 == NULL )
-        return NULL;
-    // compute the function of node
-    pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
-    if ( pFunc->Type == BDC_TYPE_AND )
-        Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
-    else if ( pFunc->Type == BDC_TYPE_OR )
-        Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
-    else 
-        assert( 0 );
-    // verify correctness
-    assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) );
-    // convert from OR to AND
-    if ( pFunc->Type == BDC_TYPE_OR )
-    {
-        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);
-    }
-    Bdc_TableAdd( p, Bdc_Regular(pFunc) );
-    return pFunc;
-}
-
-/**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, unsigned * puTruth, Bdc_Type_t Type )
-{
-    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->uSupp ); 
-        Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); 
-        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_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
-        Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); 
-        Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); 
-        assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
-        return Kit_TruthIsConst0(pIsfR->puOn, 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->uSupp = (1 << Beg);
-                pIsfR->uSupp = (1 << End);
-                pIsfL->Var = Beg;
-                pIsfR->Var = 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, VarBest, Cost, VarCostBest = 0;
-
-    for ( v = 0; v < p->nVars; v++ )
-    {
-        Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
-//        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 )
-        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->Var = VarBest;
-
-//        assert( pL->Q != b0 );
-//        assert( pL->R != b0 );
-//        assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
-
-        // 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 uSuppRem;
-    int v, nLeftVars = 1, nRightVars = 1; 
-    // clean the var sets
-    Bdc_IsfClean( pIsfL );
-    Bdc_IsfClean( pIsfR );
-    // 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_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var ); 
-    Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var );
-    // go through the remaining variables
-    uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp;
-    assert( Kit_WordCountOnes(uSuppRem) > 0 );
-    for ( v = 0; v < p->nVars; v++ )
-    {
-        if ( (uSuppRem & (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->uSupp |= (1 << v);
-                nLeftVars++;
-            }
-//            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->uSupp |= (1 << v);
-                nRightVars++;
-            }
-        }
-        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->uSupp |= (1 << v);
-                nRightVars++;
-            }
-//            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->uSupp |= (1 << v);
-                nLeftVars++;
-            }
-        }
-    }
-
-    // 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->uSupp );
-    Kit_TruthCopy( pIsfL->puOff, p->puTemp2, 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->uSupp );
-    Kit_TruthCopy( pIsfR->puOff, p->puTemp1, 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) );
-
-    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 CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR;
-
-    Bdc_IsfClean( p->pIsfOL );
-    Bdc_IsfClean( p->pIsfOR );
-    Bdc_IsfClean( p->pIsfAL );
-    Bdc_IsfClean( p->pIsfAR );
-
-    // perform OR decomposition
-    CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
-
-    // perform AND decomposition
-    Bdc_IsfNot( pIsf );
-    CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
-    Bdc_IsfNot( pIsf );
-    Bdc_IsfNot( p->pIsfAL );
-    Bdc_IsfNot( p->pIsfAR );
-
-    // check the hash table
-    Bdc_SuppMinimize( p, p->pIsfOL );
-    CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
-    Bdc_SuppMinimize( p, p->pIsfOR );
-    CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
-    Bdc_SuppMinimize( p, p->pIsfAL );
-    CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
-    Bdc_SuppMinimize( p, p->pIsfAR );
-    CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
-
-    // check if there is any reuse for the components
-    if ( CostOrL + CostOrR < CostAndL + CostAndR )
-    {
-        Bdc_IsfCopy( pIsfL, p->pIsfOL );
-        Bdc_IsfCopy( pIsfR, p->pIsfOR );
-        return BDC_TYPE_OR;
-    }
-    if ( CostOrL + CostOrR > CostAndL + CostAndR )
-    {
-        Bdc_IsfCopy( pIsfL, p->pIsfAL );
-        Bdc_IsfCopy( pIsfR, p->pIsfAR );
-        return BDC_TYPE_AND; 
-    }
-
-    // compare the two-component costs
-    if ( CostOr < CostAnd )
-    {
-        Bdc_IsfCopy( pIsfL, p->pIsfOL );
-        Bdc_IsfCopy( pIsfR, p->pIsfOR );
-        return BDC_TYPE_OR;
-    }
-    return BDC_TYPE_AND;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
deleted file mode 100644
index 9649f870..00000000
--- a/src/aig/bdc/bdcInt.h
+++ /dev/null
@@ -1,150 +0,0 @@
-/**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 __BDC_INT_H__
-#define __BDC_INT_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include "kit.h"
-#include "bdc.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-#define BDC_SCALE 100  // 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,       // 4:  AND-gate
-    BDC_TYPE_OR,        // 5:  OR-gate (temporary)
-    BDC_TYPE_XOR,       // 6:  XOR-gate
-    BDC_TYPE_MUX,       // 7:  MUX-gate
-    BDC_TYPE_OTHER      // 8:  unused
-} Bdc_Type_t;
-
-typedef struct Bdc_Fun_t_ Bdc_Fun_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
-    Bdc_Fun_t *      pFan2;        // 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
-    void *           pCopy;        // the copy field
-};
-
-typedef struct Bdc_Isf_t_ Bdc_Isf_t;
-struct Bdc_Isf_t_
-{
-    int              Var;          // the first variable assigned
-    unsigned         uSupp;        // the current support
-    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              nNodesLimit;  // 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              nNodes;       // the number of nodes used
-    int              nNodesNew;    // the number of nodes used
-    int              nNodesAlloc;  // the number of nodes allocated  
-    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
-};
-
-// working with complemented attributes of objects
-static inline int         Bdc_IsComplement( Bdc_Fun_t * p )             { return (int)((unsigned long)p & (unsigned long)01);              }
-static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )                  { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01);     }
-static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )                      { return (Bdc_Fun_t *)((unsigned long)p ^  (unsigned long)01);     }
-static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )           { return (Bdc_Fun_t *)((unsigned long)p ^  (unsigned long)(c!=0)); }
-
-static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p )                   { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
-static inline void        Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
-static inline void        Bdc_IsfClean( Bdc_Isf_t * p )                 { p->uSupp = 0; p->Var = 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 );
-/*=== 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 void             Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
-extern int              Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c
deleted file mode 100644
index d86a938d..00000000
--- a/src/aig/bdc/bdcTable.c
+++ /dev/null
@@ -1,140 +0,0 @@
-/**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"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Minimizes the support of the ISF.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
-{
-    int v;
-    // 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;
-        // remove the variable
-        Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
-        Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
-        pIsf->uSupp &= ~(1 << v);
-    }
-}
-
-/**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( pIsf->puOff, puTruth, 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 )
-{
-    Bdc_Fun_t * pFunc;
-    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
-        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
-             return pFunc;
-    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                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/bdc/bdc_.c b/src/aig/bdc/bdc_.c
deleted file mode 100644
index 9d0a9462..00000000
--- a/src/aig/bdc/bdc_.c
+++ /dev/null
@@ -1,49 +0,0 @@
-/**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"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/bdc/module.make b/src/aig/bdc/module.make
deleted file mode 100644
index 8697c998..00000000
--- a/src/aig/bdc/module.make
+++ /dev/null
@@ -1,4 +0,0 @@
-SRC +=  src/aig/bdc/bdcCore.c \
-    src/aig/bdc/bdcDec.c \
-    src/aig/bdc/bdcTable.c
-