dsdProc.c

Go to the documentation of this file.

 
#include "dsdInt.h"
 
ABC_NAMESPACE_IMPL_START
 
 

 
// the most important procedures
void dsdKernelDecompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs );
static Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * F );
 
// additional procedures
static Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity );
static int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH );
static void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor );
static int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall );
 
// list copying
static void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize );
static void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int Skipped );
 
// debugging procedures
static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE );

 
// the counter of marks
static int s_Mark;
 
// debugging flag
//static int s_Show = 0;
// temporary var used for debugging
static int Depth = 0;
 
static int s_Loops1;
static int s_Loops2;
static int s_Loops3;
static int s_Common;
static int s_CommonNo;
 
static int s_Case4Calls;
static int s_Case4CallsSpecial;
 
//static int s_Case5;
//static int s_Loops2Useless;
 
// statistical variables
static int   s_nDecBlocks;
static int   s_nLiterals;
static int   s_nExorGates; 
static int   s_nReusedBlocks;
static int   s_nCascades;
static int   s_nPrimeBlocks;
 
static int HashSuccess = 0;
static int HashFailure = 0;
 
static int s_CacheEntries;
 


void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs )
{
    DdManager * dd = pDsdMan->dd;
    int i;
    abctime clk;
    Dsd_Node_t * pTemp;
    int SumMaxGateSize = 0;
    int nDecOutputs = 0;
    int nCBFOutputs = 0;
/*
s_Loops1 = 0;
s_Loops2 = 0;
s_Loops3 = 0;
s_Case4Calls = 0;
s_Case4CallsSpecial = 0;
s_Case5 = 0;
s_Loops2Useless = 0;
*/
    // resize the number of roots in the manager
    if ( pDsdMan->nRootsAlloc < nFuncs )
    {
        if ( pDsdMan->nRootsAlloc > 0 )
            ABC_FREE( pDsdMan->pRoots );
        pDsdMan->nRootsAlloc = nFuncs;
        pDsdMan->pRoots = (Dsd_Node_t **) ABC_ALLOC( char, pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
    }
 
    if ( pDsdMan->fVerbose )
        printf( "\nDecomposability statistics for individual outputs:\n" );
 
    // set the counter of decomposition nodes
    s_nDecBlocks = 0;
 
    // perform decomposition for all outputs
    clk = Abc_Clock();
    pDsdMan->nRoots = 0;
    s_nCascades = 0;
    for ( i = 0; i < nFuncs; i++ )
    {
        int nLiteralsPrev;
        int nDecBlocksPrev;
        int nExorGatesPrev;
        int nReusedBlocksPres;
        int nCascades;
        int MaxBlock;
        int nPrimeBlocks;
        abctime clk;
 
        clk = Abc_Clock();
        nLiteralsPrev     = s_nLiterals;
        nDecBlocksPrev    = s_nDecBlocks;
        nExorGatesPrev    = s_nExorGates;
        nReusedBlocksPres = s_nReusedBlocks;
        nPrimeBlocks      = s_nPrimeBlocks;
 
        pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] );
 
        Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock );
        s_nCascades = ddMax( s_nCascades, nCascades );
        pTemp = Dsd_Regular(pDsdMan->pRoots[i]);
        if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) )
            nDecOutputs++;
        if ( MaxBlock < 3 )
            nCBFOutputs++;
        SumMaxGateSize += MaxBlock;
 
        if ( pDsdMan->fVerbose )
        {
            printf("#%02d: ", i );                              
            printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) );                  
            printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) ); 
            printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) ); 
            printf("Max=%3d. ", MaxBlock ); 
            printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres ); 
            printf("Csc=%2d. ", nCascades ); 
            printf("T= %.2f s. ", (float)(Abc_Clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
            printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) ); 
            printf("\n");
            fflush( stdout );
        }
    }
    assert( pDsdMan->nRoots == nFuncs );
 
    if ( pDsdMan->fVerbose )
    {
        printf( "\n" );
        printf( "The cumulative decomposability statistics:\n" );
        printf( "  Total outputs                             = %5d\n", nFuncs );
        printf( "  Decomposable outputs                      = %5d\n", nDecOutputs );
        printf( "  Completely decomposable outputs           = %5d\n", nCBFOutputs );
        printf( "  The sum of max gate sizes                 = %5d\n", SumMaxGateSize );
        printf( "  Shared BDD size                           = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
        printf( "  Decomposition entries                     = %5d\n", st__count( pDsdMan->Table ) );
        printf( "  Pure decomposition time                   =  %.2f sec\n", (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC) );
    }
/*
    printf( "s_Loops1 = %d.\n", s_Loops1 );
    printf( "s_Loops2 = %d.\n", s_Loops2 );
    printf( "s_Loops3 = %d.\n", s_Loops3 );
    printf( "s_Case4Calls = %d.\n", s_Case4Calls );
    printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial );
    printf( "s_Case5 = %d.\n", s_Case5 );
    printf( "s_Loops2Useless = %d.\n", s_Loops2Useless );
*/
}

Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc )
{
    return dsdKernelDecompose_rec( pDsdMan, bFunc );
}

Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 )
{
    DdManager * dd = pDsdMan->dd;
    DdNode * bLow;
    DdNode * bLowR;
    DdNode * bHigh;
 
    int      VarInt;
    DdNode * bVarCur;
    Dsd_Node_t *     pVarCurDE; 
    // works only if var indices start from 0!!!
    DdNode * bSuppNew = NULL, * bTemp;
 
    int fContained;
    int nSuppLH;
    int nSuppL;
    int nSuppH;
 
 
 
    // various decomposition nodes
    Dsd_Node_t * pThis, * pL, * pH, * pLR, * pHR;
 
    Dsd_Node_t * pSmallR, * pLargeR;
    Dsd_Node_t * pTableEntry;
 
 
    // treat the complemented case
    DdNode * bF = Cudd_Regular(bFunc0);
    int  fCompF = (int)(bF != bFunc0);
 
    // check cache
    if ( st__lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) )
    { // the entry is present 
        HashSuccess++;
        return Dsd_NotCond( pTableEntry, fCompF );
    }
    HashFailure++;
    Depth++;
 
    // proceed to consider "four cases"
    // TERMINAL CASES - CASES 1 and 2
    bLow    = cuddE(bF);
    bLowR   = Cudd_Regular(bLow);
    bHigh   = cuddT(bF);
    VarInt    = bF->index;
    bVarCur   = dd->vars[VarInt];
    pVarCurDE = pDsdMan->pInputs[VarInt]; 
    // works only if var indices start from 0!!!
    bSuppNew = NULL;
 
    if ( bLowR->index == CUDD_CONST_INDEX || bHigh->index == CUDD_CONST_INDEX )
    { // one of the cofactors in the constant
        if ( bHigh == b1 )  // bHigh cannot be equal to b0, because then it will be complemented
          if ( bLow == b0 ) // bLow cannot be equal to b1, because then the node will have bLow == bHigh
          // bLow == 0, bHigh == 1, F = x'&0 + x&1 = x
          { // create the elementary variable node
            assert(0); // should be already in the hash table
            pThis = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, s_nDecBlocks++ );
            pThis->pDecs[0] = NULL;
          }
          else // if ( bLow != constant )
          // bLow != const, bHigh == 1, F = x'&bLow + x&1 = bLow + x  --- DSD_NODE_OR(x,bLow)
          {
            pL  = dsdKernelDecompose_rec( pDsdMan, bLow );
            pLR = Dsd_Regular( pL );
            bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
            if ( pLR->Type == DSD_NODE_OR && pL == pLR ) // OR and no complement
            { // add to the components
                pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pL->nDecs+1, s_nDecBlocks++ );
                dsdKernelCopyListPlusOne( pThis, pVarCurDE, pL->pDecs, pL->nDecs );
            }
            else // all other cases
            { // create a new 2-input OR-gate
                pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
                dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
            }
          }
        else // if ( bHigh != const ) // meaning that bLow should be a constant
        {
          pH = dsdKernelDecompose_rec( pDsdMan, bHigh );
          pHR = Dsd_Regular( pH );
          bSuppNew = Cudd_bddAnd( dd, bVarCur, pHR->S ); Cudd_Ref(bSuppNew);
          if ( bLow == b0 )
          // Low == 0, High != 1, F = x'&0+x&High = (x'+High')'--- NOR(x',High')
            if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement
            { // add to the components
              pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ );
              dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs );
              pThis = Dsd_Not(pThis);
            }
            else // all other cases
            { // create a new 2-input NOR gate
              pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
              pH = Dsd_Not(pH);
              dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
              pThis = Dsd_Not(pThis);
            }
          else // if ( bLow == b1 )
          // Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High)
            if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement
            { // add to the components
                pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pH->nDecs+1, s_nDecBlocks++ );
                dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pH->pDecs, pH->nDecs );
            }
            else // all other cases
            { // create a new 2-input OR-gate
                pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
                dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
            }
        }
        goto EXIT;
    }
    // else if ( bLow != const && bHigh != const )
 
    // the case of equal cofactors (up to complementation)
    if ( bLowR == bHigh )
    // Low == G, High == G', F = x'&G + x&G' = (x(+)G) --- EXOR(x,Low)
    {
        pL  = dsdKernelDecompose_rec( pDsdMan, bLow );
        pLR = Dsd_Regular( pL );
        bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
        if ( pLR->Type == DSD_NODE_EXOR ) // complemented or not - does not matter!
        { // add to the components
            pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, pLR->nDecs+1, s_nDecBlocks++ );
            dsdKernelCopyListPlusOne( pThis, pVarCurDE, pLR->pDecs, pLR->nDecs );
            if ( pL != pLR )
                pThis = Dsd_Not( pThis );
        }
        else // all other cases
        { // create a new 2-input EXOR-gate
            pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ );
            if ( pL != pLR ) // complemented
            {
                dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pLR, 1 );
                pThis = Dsd_Not( pThis );
            }
            else // non-complemented
                dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
        }
        goto EXIT;
    }

    // solve subproblems
    pL   = dsdKernelDecompose_rec( pDsdMan, bLow );
    pH   = dsdKernelDecompose_rec( pDsdMan, bHigh );
    pLR  = Dsd_Regular( pL );
    pHR  = Dsd_Regular( pH );
 
    assert( pLR->Type == DSD_NODE_BUF || pLR->Type == DSD_NODE_OR || pLR->Type == DSD_NODE_EXOR || pLR->Type == DSD_NODE_PRIME );
    assert( pHR->Type == DSD_NODE_BUF || pHR->Type == DSD_NODE_OR || pHR->Type == DSD_NODE_EXOR || pHR->Type == DSD_NODE_PRIME );
 
/*
if ( Depth == 1 )
{
//  PRK(bLow,pDecTreeTotal->nInputs);
//  PRK(bHigh,pDecTreeTotal->nInputs);
if ( s_Show )
{
    PRD( pL );
    PRD( pH );
}
}
*/
    // compute the new support
    bTemp    = Cudd_bddAnd( dd, pLR->S, pHR->S );   Cudd_Ref( bTemp );
    nSuppL   = Extra_bddSuppSize( dd, pLR->S );
    nSuppH   = Extra_bddSuppSize( dd, pHR->S );
    nSuppLH  = Extra_bddSuppSize( dd, bTemp );
    bSuppNew = Cudd_bddAnd( dd, bTemp, bVarCur );   Cudd_Ref( bSuppNew );
    Cudd_RecursiveDeref( dd, bTemp );
 
 
    // several possibilities are possible
    // (1) support of one component contains another
    // (2) none of the supports is contained in another
    fContained = dsdKernelCheckContainment( pDsdMan, pLR, pHR, &pLargeR, &pSmallR );

    // CASE 3.b One of the cofactors in a constant (OR and EXOR)
    // the support of the larger component should contain the support of the smaller
    // it is possible to have PRIME function in this role
    // for example: F = ITE( a+b, c(+)d, e+f ), F0 = ITE( b, c(+)d, e+f ), F1 = c(+)d
    if ( fContained )
    {
        Dsd_Node_t * pSmall, * pLarge;
        int c, iCompLarge = -1; // the number of the component is Large is equal to the whole of Small; suppress "might be used uninitialized"
        int fLowIsLarge;
 
        DdNode * bFTemp;     // the changed input function
        Dsd_Node_t * pDETemp, * pDENew;
 
        Dsd_Node_t * pComp = NULL;
        int  nComp = -1; // Suppress "might be used uninitialized"
 
        if ( pSmallR == pLR )
        { // Low is Small => High is Large
            pSmall = pL;
            pLarge = pH;
            fLowIsLarge = 0;
        }
        else
        { // vice versa
            pSmall = pH;
            pLarge = pL;
            fLowIsLarge = 1;
        }
 
        // treat the situation when the larger is PRIME
        if ( pLargeR->Type == DSD_NODE_PRIME ) //&& pLargeR->nDecs != pSmallR->nDecs )
        {
            // QUESTION: Is it possible for pLargeR->nDecs > 3 
            // and pSmall contained as one of input in pLarge?
            // Yes, for example F = a'c + a & MUX(b,c',d) = a'c + abc' + ab'd is non-decomposable
            // Consider the function H(a->xy) = F( xy, b, c, d )
            // H0 = H(x=0) = F(0,b,c,d) = c
            // H1 = F(x=1) = F(y,b,c,d) - non-decomposable
            //
            // QUESTION: Is it possible that pLarge is PRIME(3) and pSmall is OR(2),
            // which is not contained in PRIME as one input?
            // Yes, for example F = abcd + b'c'd' + a'c'd' = PRIME(ab, c, d)
            // F(a=0) = c'd' = NOT(OR(a,d))  F(a=1) = bcd + b'c'd' = PRIME(b,c,d)
            // To find decomposition, we have to prove that F(a=1)|b=0 = F(a=0)
 
            // Is it possible that (pLargeR->nDecs == pSmallR->nDecs) and yet this case holds?
            // Yes, consider the function such that F(a=0) = PRIME(a,b+c,d,e) and F(a=1) = OR(b,c,d,e)
            // They have the same number of inputs and it is possible that they will be the cofactors
            // as discribed in the previous example.
 
            // find the component, which when substituted for 0 or 1, produces the desired result
            int g, fFoundComp = -1; // {0,1} depending on whether setting cofactor to 0 or 1 worked out; suppress "might be used uninitialized"
 
            DdNode * bLarge, * bSmall;
            if ( fLowIsLarge )
            {
                bLarge = bLow;
                bSmall = bHigh;
            }
            else
            {
                bLarge = bHigh;
                bSmall = bLow;
            }
 
            for ( g = 0; g < pLargeR->nDecs; g++ )
//          if ( g != c )
            {
                pDETemp = pLargeR->pDecs[g]; // cannot be complemented
                if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) )
                {
                    fFoundComp = 1;
                    break;
                }
 
                s_Loops1++;
 
                if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, Cudd_Not(pDETemp->G), b1 ) )
                {
                    fFoundComp = 0;
                    break;
                }
 
                s_Loops1++;
            }
 
            if ( g != pLargeR->nDecs ) 
            { // decomposition is found
                if ( fFoundComp )
                    if ( fLowIsLarge )
                        bFTemp = Cudd_bddOr( dd, bVarCur, pLargeR->pDecs[g]->G );
                    else
                        bFTemp = Cudd_bddOr( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
                else
                    if ( fLowIsLarge )
                        bFTemp = Cudd_bddAnd( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
                    else
                        bFTemp = Cudd_bddAnd( dd, bVarCur, pLargeR->pDecs[g]->G );
                Cudd_Ref( bFTemp );
 
                pDENew = dsdKernelDecompose_rec( pDsdMan, bFTemp );
                pDENew = Dsd_Regular( pDENew );
                Cudd_RecursiveDeref( dd, bFTemp );
 
                // get the new gate
                pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLargeR->nDecs, s_nDecBlocks++ );
                dsdKernelCopyListPlusOneMinusOne( pThis, pDENew, pLargeR->pDecs, pLargeR->nDecs, g );
                goto EXIT;
            }
        }
 
        // try to find one component in the pLarger that is equal to the whole of pSmaller
        for ( c = 0; c < pLargeR->nDecs; c++ )
            if ( pLargeR->pDecs[c] == pSmall || pLargeR->pDecs[c] == Dsd_Not(pSmall) )
            {
                iCompLarge = c;
                break;
            }
 
        // assign the equal component
        if ( c != pLargeR->nDecs )  // the decomposition is possible!
        { 
            pComp  = pLargeR->pDecs[iCompLarge];
            nComp  = 1;
        }
        else // the decomposition is still possible
        { // for example F = OR(ab,c,d), F(a=0) = OR(c,d), F(a=1) = OR(b,c,d)
            // supp(F0) is contained in supp(F1), Polarity(F(a=0)) == Polarity(F(a=1))
 
            // try to find a group of common components
            if ( pLargeR->Type == pSmallR->Type &&
                (pLargeR->Type == DSD_NODE_EXOR || (pSmallR->Type == DSD_NODE_OR && ((pLarge==pLargeR) == (pSmall==pSmallR)))) )
            {
                Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
                int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH );
                // if all the components of pSmall are contained in pLarge,
                // then the decomposition exists
                if ( nCommon == pSmallR->nDecs )
                {
                    pComp = pSmallR;
                    nComp = pSmallR->nDecs;
                }
            }
        }
 
        if ( pComp ) // the decomposition is possible!
        {
//          Dsd_Node_t * pComp  = pLargeR->pDecs[iCompLarge];
            Dsd_Node_t * pCompR = Dsd_Regular( pComp );
            int fComp1 = (int)( pLarge != pLargeR );
            int fComp2 = (int)( pComp  != pCompR );
            int fComp3 = (int)( pSmall != pSmallR );
 
            DdNode * bFuncComp;  // the function of the given component
            DdNode * bFuncNew;   // the function of the input component
 
            if ( pLargeR->Type == DSD_NODE_OR ) // Figure 4 of Matsunaga's paper
            { 
                // the decomposition exists only if the polarity assignment 
                // along the paths is the same
                if ( (fComp1 ^ fComp2) == fComp3 )
                { // decomposition exists = consider 4 cases
                    // consideration of cases leads to the following conclusion
                    // fComp1 gives the polarity of the resulting DSD_NODE_OR gate
                    // fComp2 gives the polarity of the common component feeding into the DSD_NODE_OR gate
                    //
                    //                  |  fComp1              pL/  |pS
                    //                  <> .........<=>....... <>   |
                    //                  |                     /     |
                    //                [OR]                  [OR]    | fComp3
                    //                /  \  fComp2          / | \   |
                    //              <>    <> .......<=>... /..|..<> | 
                    //             /        \             /   |    \|
                    //          [OR]        [C]          S1   S2    C 
                    //          /  \      .
                    //        <>    \     .
                    //       /       \    .
                    //     [OR]      [x]  .
                    //     /  \           .
                    //    S1   S2         .
                    //
 
 
                    // at this point we have the function F (bFTemp) and the common component C (bFuncComp)
                    // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
                    // we compute the following R = Exist( F - C, supp(C) )
                    bFTemp = (fComp1)? Cudd_Not( bF ): bF;
                    bFuncComp = (fComp2)? Cudd_Not( pCompR->G ): pCompR->G;
                    bFuncNew  = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bFuncComp), pCompR->S ); Cudd_Ref( bFuncNew );
 
                    // there is no need to copy the dec entry list first, because pComp is a component
                    // which will not be destroyed by the recursive call to decomposition
                    pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
                    assert( Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
                    Cudd_RecursiveDeref( dd, bFuncNew );
 
                    // get the new gate
                    if ( nComp == 1 )
                    {
                        pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
                        pThis->pDecs[0] = pDENew;
                        pThis->pDecs[1] = pComp; // takes the complement
                    }
                    else
                    {  // pComp is not complemented
                        pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nComp+1, s_nDecBlocks++ );
                        dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
                    }
                    
                    if ( fComp1 )
                        pThis = Dsd_Not( pThis );
                    goto EXIT;
                }
            }
            else if ( pLargeR->Type == DSD_NODE_EXOR ) // Figure 5 of Matsunaga's paper (with correction)
            { // decomposition always exists = consider 4 cases
 
                // consideration of cases leads to the following conclusion
                // fComp3 gives the COMPLEMENT of the polarity of the resulting EXOR gate
                // (if fComp3 is 0, the EXOR gate is complemented, and vice versa)
                //
                //                  |  fComp1              pL/  |pS
                //                  <> .........<=>....... /....|  fComp3
                //                  |                     /     |
                //                [XOR]                [XOR]    |
                //                /  \  fComp2==0       / | \   |
                //              /     \                /  |  \  | 
                //             /        \             /   |    \|
                //          [OR]        [C]          S1   S2    C 
                //          /  \     .
                //        <>    \    .
                //       /       \   .
                //    [XOR]      [x] .
                //     /  \          .
                //    S1   S2        .
                //
 
                assert( fComp2 == 0 );
                // find the functionality of the lower gates
                bFTemp = (fComp3)? bF: Cudd_Not( bF );
                bFuncNew = Cudd_bddXor( dd, bFTemp, pComp->G );   Cudd_Ref( bFuncNew );
 
                pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
                assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
                Cudd_RecursiveDeref( dd, bFuncNew ); 
 
                // get the new gate
                if ( nComp == 1 )
                {
                    pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ );
                    pThis->pDecs[0] = pDENew;
                    pThis->pDecs[1] = pComp; 
                }
                else
                {  // pComp is not complemented
                    pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nComp+1, s_nDecBlocks++ );
                    dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
                }
 
                if ( !fComp3 )
                    pThis = Dsd_Not( pThis );
                goto EXIT;
            }
        }
    }
 
    // this case was added to fix the trivial bug found November 4, 2002 in Japan
    // by running the example provided by T. Sasao
    if ( nSuppLH == nSuppL + nSuppH ) // the supports of the components are disjoint
    {
        // create a new component of the type ITE( a, pH, pL )
        pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, 3, s_nDecBlocks++ );
        if ( dd->perm[pLR->S->index] < dd->perm[pHR->S->index] ) // pLR is higher in the varible order
        {
            pThis->pDecs[1] = pLR;
            pThis->pDecs[2] = pHR;
        }
        else  // pHR is higher in the varible order
        {
            pThis->pDecs[1] = pHR;
            pThis->pDecs[2] = pLR;
        }
        // add the first component
        pThis->pDecs[0] = pVarCurDE;
        goto EXIT;
    }
 

    // CASE 3.a Neither of the cofactors is a constant (OR, EXOR, PRIME)
    // the component types are identical 
    // and if they are OR, they are either both complemented or both not complemented
    // and if they are PRIME, their dec numbers should be the same
    if ( pLR->Type == pHR->Type && 
         pLR->Type != DSD_NODE_BUF &&           
        (pLR->Type != DSD_NODE_OR    || ( (pL == pLR && pH == pHR) || (pL != pLR && pH != pHR) ) ) &&
        (pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs)  )
    {
        // array to store common comps in pL and pH
        Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
        int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLR, pHR, &pCommon, &pLastDiffL, &pLastDiffH );
        if ( nCommon )
        {
            if ( pLR->Type == DSD_NODE_OR ) // Figure 2 of Matsunaga's paper
            { // at this point we have the function F and the group of common components C
                // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
                // we compute the following R = Exist( F - C, supp(C) )
 
                // compute the sum total of the common components and the union of their supports
                DdNode * bCommF, * bCommS, * bFTemp, * bFuncNew;
                Dsd_Node_t * pDENew;
 
                dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 );
                Cudd_Ref( bCommF );
                Cudd_Ref( bCommS );
                bFTemp = ( pL != pLR )? Cudd_Not(bF): bF;
 
                bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew );
                Cudd_RecursiveDeref( dd, bCommF );
                Cudd_RecursiveDeref( dd, bCommS );
 
                // get the new gate
 
                // copy the components first, then call the decomposition
                // because decomposition will distroy the list used for copying
                pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nCommon + 1, s_nDecBlocks++ );
                dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
 
                // call the decomposition recursively
                pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
//              assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
                Cudd_RecursiveDeref( dd, bFuncNew );
 
                // add the first component
                pThis->pDecs[0] = pDENew;
                
                if ( pL != pLR )
                    pThis = Dsd_Not( pThis );
                goto EXIT;
            }
            else
            if ( pLR->Type == DSD_NODE_EXOR ) // Figure 3 of Matsunaga's paper
            {
                // compute the sum total of the common components and the union of their supports
                DdNode * bCommF, * bFuncNew;
                Dsd_Node_t * pDENew;
                int fCompExor;
 
                dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, 1 );
                Cudd_Ref( bCommF );
 
                bFuncNew = Cudd_bddXor( dd, bF, bCommF ); Cudd_Ref( bFuncNew );
                Cudd_RecursiveDeref( dd, bCommF );
 
                // get the new gate
 
                // copy the components first, then call the decomposition
                // because decomposition will distroy the list used for copying
                pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nCommon + 1, s_nDecBlocks++ );
                dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
 
                // call the decomposition recursively
                pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
                Cudd_RecursiveDeref( dd, bFuncNew );
 
                // remember the fact that it was complemented
                fCompExor = Dsd_IsComplement(pDENew);
                pDENew = Dsd_Regular(pDENew);
 
                // add the first component
                pThis->pDecs[0] = pDENew;
 
    
                if ( fCompExor )
                    pThis = Dsd_Not( pThis );
                goto EXIT;
            }
            else 
            if ( pLR->Type == DSD_NODE_PRIME && (nCommon == pLR->nDecs-1 || nCommon == pLR->nDecs) )
            {
                // for example the function F(a,b,c,d) = ITE(b,c,a(+)d) produces
                // two cofactors F(a=0) = PRIME(b,c,d) and F(a=1) = PRIME(b,c,d)
                // with exactly the same list of common components
 
                Dsd_Node_t * pDENew;
                DdNode * bFuncNew;
                int fCompComp = 0;  // this flag can be {0,1,2}
                // if it is 0 there is no identity
                // if it is 1/2, the cofactored functions are equal in the direct/complemented polarity
 
                if ( nCommon == pLR->nDecs )
                {   // all the components are the same
                    // find the formal input, in which pLow and pHigh differ (if such input exists)
                    int m;
                    Dsd_Node_t * pTempL, * pTempH;
 
                    s_Common++;
                    for ( m = 0; m < pLR->nDecs; m++ )
                    {
                        pTempL = pLR->pDecs[m]; // cannot be complemented
                        pTempH = pHR->pDecs[m]; // cannot be complemented
 
                        if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh,          pTempL->G, Cudd_Not(pTempH->G) ) &&
                             Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pTempL->G),         pTempH->G ) )
                        {
                             pLastDiffL = pTempL;
                             pLastDiffH = pTempH;
                             assert( pLastDiffL == pLastDiffH );
                             fCompComp = 2;
                             break;
                        }
 
                        s_Loops2++;
                        s_Loops2++;
/* 
                        if ( s_Loops2 % 10000  == 0 )
                        {
                            int i;
                            for ( i = 0; i < pLR->nDecs; i++ )
                                printf( " %d(s=%d)", pLR->pDecs[i]->Type,
                                    Extra_bddSuppSize(dd, pLR->pDecs[i]->S) );
                            printf( "\n" );
                        }
*/
 
                    }
//                    if ( pLR->nDecs == Extra_bddSuppSize(dd, pLR->S) )
//                        s_Loops2Useless += pLR->nDecs * 2;
 
                    if ( fCompComp )
                    { // put the equal components into pCommon, so that they could be copied into the new dec entry
                        nCommon = 0;
                        for ( m = 0; m < pLR->nDecs; m++ )
                            if ( pLR->pDecs[m] != pLastDiffL )
                                 pCommon[nCommon++] = pLR->pDecs[m];
                        assert( nCommon == pLR->nDecs-1 );
                    }
                }
                else
                {  // the differing components are known - check that they have compatible PRIME function
 
                    s_CommonNo++;
 
                    // find the numbers of different components
                    assert( pLastDiffL );
                    assert( pLastDiffH );
                    // also, they cannot be complemented, because the decomposition type is PRIME
 
                    if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), Cudd_Not(pLastDiffH->G) ) &&
                         Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh,          pLastDiffL->G,           pLastDiffH->G ) )
                        fCompComp = 1;
                    else if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh,          pLastDiffL->G, Cudd_Not(pLastDiffH->G) ) &&
                              Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G),         pLastDiffH->G ) )
                        fCompComp = 2;
 
                    s_Loops3 += 4;
                }
 
                if ( fCompComp )
                {
                    if ( fCompComp == 1 ) // it is true that bLow(G=0) == bHigh(H=0) && bLow(G=1) == bHigh(H=1)
                        bFuncNew = Cudd_bddIte( dd, bVarCur, pLastDiffH->G, pLastDiffL->G ); 
                    else // it is true that bLow(G=0) == bHigh(H=1) && bLow(G=1) == bHigh(H=0)
                        bFuncNew = Cudd_bddIte( dd, bVarCur, Cudd_Not(pLastDiffH->G), pLastDiffL->G ); 
                    Cudd_Ref( bFuncNew );
 
                    // get the new gate
 
                    // copy the components first, then call the decomposition
                    // because decomposition will distroy the list used for copying
                    pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLR->nDecs, s_nDecBlocks++ );
                    dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
 
                    // create a new component
                    pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
                    Cudd_RecursiveDeref( dd, bFuncNew );
                    // the BDD of the argument function in PRIME decomposition, should be regular
                    pDENew = Dsd_Regular(pDENew);
 
                    // add the first component
                    pThis->pDecs[0] = pDENew;
                    goto EXIT;
                }
            } // end of PRIME type
        } // end of existing common components
    } // end of CASE 3.a
 
// if ( Depth != 1) 
// {
 
//CASE4:
    // CASE 4
    {
    // estimate the number of entries in the list
    int nEntriesMax = pDsdMan->nInputs - dd->perm[VarInt];
 
    // create the new decomposition entry
    int nEntries = 0;
 
    DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init;
    Dsd_Node_t *pHigher = NULL; // Suppress "might be used uninitialized"
        Dsd_Node_t *pLower, * pTemp, * pDENew;
 
 
    int levTopSuppL;
    int levTopSuppH;
    int levTop;
 
    pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, nEntriesMax, s_nDecBlocks++ );
    pThis->pDecs[ nEntries++ ] = pVarCurDE;
    // other entries will be added to this list one-by-one during analysis
 
    // count how many times does it happen that the decomposition entries are
    s_Case4Calls++;
 
    // consider the simplest case: when the supports are equal 
    // and at least one of the components
    // is the PRIME without decompositions, or 
    // when both of them are without decomposition
    if ( (((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) || (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) && pLR->S == pHR->S)  ||
          ((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) && (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) )
    {
 
         s_Case4CallsSpecial++;
         // walk through both supports and create the decomposition list composed of simple entries
         SuppL = pLR->S;
         SuppH = pHR->S;
         do
         {
             // determine levels
             levTopSuppL = cuddI(dd,SuppL->index);
             levTopSuppH = cuddI(dd,SuppH->index);
 
             // skip the topmost variable in both supports
             if ( levTopSuppL <= levTopSuppH )
             {
                 levTop = levTopSuppL;
                 SuppL  = cuddT(SuppL);
             }
             else
                 levTop = levTopSuppH;
 
             if ( levTopSuppH <= levTopSuppL )
                 SuppH = cuddT(SuppH);
 
             // set the new decomposition entry
             pThis->pDecs[ nEntries++ ] = pDsdMan->pInputs[ dd->invperm[levTop] ];
         }
         while ( SuppL != b1 || SuppH != b1 );
    }
    else
    {
 
        // compare two different decomposition lists
        SuppL_init = pLR->S;
        SuppH_init = pHR->S;
        // start references (because these supports will change)
        SuppL = pLR->S;  Cudd_Ref( SuppL );
        SuppH = pHR->S;  Cudd_Ref( SuppH );
        while ( SuppL != b1 || SuppH != b1 )
        {
            // determine the top level in cofactors and
            // whether they have the same top level
            int TopLevL  = cuddI(dd,SuppL->index);
            int TopLevH  = cuddI(dd,SuppH->index);
            int TopLevel = TopLevH;
            int fEqualLevel = 0;
 
            DdNode * bVarTop;
            DdNode * bSuppSubract;
 
 
            if ( TopLevL < TopLevH )
            {
                pHigher = pLR;
                pLower  = pHR;
                TopLevel = TopLevL;
            }
            else if ( TopLevL > TopLevH )
            {
                pHigher = pHR;
                pLower  = pLR;
            }
            else
                fEqualLevel = 1;
            assert( TopLevel != CUDD_CONST_INDEX );
 
 
            // find the currently top variable in the decomposition lists
            bVarTop = dd->vars[dd->invperm[TopLevel]];
 
            if ( !fEqualLevel )
            {
                // find the lower support
                DdNode * bSuppLower = (TopLevL < TopLevH)? SuppH_init: SuppL_init; 
 
                // find the first component in pHigher 
                // whose support does not overlap with supp(Lower) 
                // and remember the previous component
                int fPolarity;          
                Dsd_Node_t * pPrev = NULL;       // the pointer to the component proceeding pCur
                Dsd_Node_t * pCur  = pHigher;    // the first component not contained in supp(Lower)
                while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) )
                {   // get the next component
                    pPrev = pCur;
                    pCur  = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity );
                };
 
                // look for the possibility to subtract more than one component
                if ( pPrev == NULL || pPrev->Type == DSD_NODE_PRIME )
                { // if there is no previous component, or if the previous component is PRIME
                  // there is no way to subtract more than one component
 
                    // add the new decomposition entry (it is already regular)
                    pThis->pDecs[ nEntries++ ] = pCur;
                    // assign the support to be subtracted from both components
                    bSuppSubract = pCur->S;
                }
                else // all other types
                {
                    // go through the decomposition list of pPrev and find components 
                    // whose support does not overlap with supp(Lower) 
 
                    static Dsd_Node_t * pNonOverlap[MAXINPUTS];
                    int i, nNonOverlap = 0;
                    for ( i = 0; i < pPrev->nDecs; i++ )
                    {
                        pTemp = Dsd_Regular( pPrev->pDecs[i] );
                        if ( !Extra_bddSuppOverlapping( dd, pTemp->S, bSuppLower ) )
                            pNonOverlap[ nNonOverlap++ ] = pPrev->pDecs[i];
                    }
                    assert( nNonOverlap > 0 );
 
                    if ( nNonOverlap == 1 )
                    { // one one component was found, which is the original one
                        assert( Dsd_Regular(pNonOverlap[0]) == pCur);
                        // add the new decomposition entry
                        pThis->pDecs[ nEntries++ ] = pCur;
                        // assign the support to be subtracted from both components
                        bSuppSubract = pCur->S;
                    }
                    else // more than one components was found
                    {
                        // find the OR (EXOR) of the non-overlapping components
                        DdNode * bCommF;
                        dsdKernelComputeSumOfComponents( pDsdMan, pNonOverlap, nNonOverlap, &bCommF, NULL, (int)(pPrev->Type==DSD_NODE_EXOR) );
                        Cudd_Ref( bCommF );
 
                        // create a new gated 
                        pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
                        Cudd_RecursiveDeref(dd, bCommF);
                        // make it regular... it must be regular already
                        assert( !Dsd_IsComplement(pDENew) );
 
                        // add the new decomposition entry
                        pThis->pDecs[ nEntries++ ] = pDENew;
                        // assign the support to be subtracted from both components
                        bSuppSubract = pDENew->S;
                    }
                }
                
                // subtract its support from the support of upper component
                if ( TopLevL < TopLevH )
                {
                    SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ); Cudd_Ref( SuppL );
                    Cudd_RecursiveDeref(dd, bTemp);
                }
                else
                {
                    SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ); Cudd_Ref( SuppH );
                    Cudd_RecursiveDeref(dd, bTemp);
                }
            } // end of if ( !fEqualLevel )
            else // if ( fEqualLevel ) -- they have the same top level var
            {
                static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks
                static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks
                int nMarkedLeft = 0;
 
                int fPolarity = 0;
                Dsd_Node_t * pTempL = pLR;
 
                int fPolarityCurH = 0;
                Dsd_Node_t * pPrevH = NULL, * pCurH = pHR;
 
                int fPolarityCurL = 0;
                Dsd_Node_t * pPrevL = NULL, * pCurL = pLR; // = pMarkedLeft[0];
                int index = 1;
 
                // set the new mark
                s_Mark++;
 
                // go over the dec list of pL, mark all components that contain the given variable
                assert( Extra_bddSuppContainVar( dd, pLR->S, bVarTop ) );
                assert( Extra_bddSuppContainVar( dd, pHR->S, bVarTop ) );
                do {
                    pTempL->Mark = s_Mark;
                    pMarkedLeft[ nMarkedLeft ] = pTempL;
                    pMarkedPols[ nMarkedLeft ] = fPolarity;
                    nMarkedLeft++;
                } while ( (pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity )) );
 
                // go over the dec list of pH, and find the component that is marked and the previos one
                // (such component always exists, because they have common variables)
                while ( pCurH->Mark != s_Mark )
                {
                    pPrevH = pCurH;
                    pCurH  = dsdKernelFindContainingComponent( pDsdMan, pCurH, bVarTop, &fPolarityCurH );
                    assert( pCurH );
                }
 
                // go through the first list once again and find 
                // the component proceeding the one marked found in the second list
                while ( pCurL != pCurH )
                {
                    pPrevL = pCurL;
                    pCurL  = pMarkedLeft[index];
                    fPolarityCurL = pMarkedPols[index];
                    index++;
                }
 
                // look for the possibility to subtract more than one component
                if ( !pPrevL || !pPrevH || pPrevL->Type != pPrevH->Type || pPrevL->Type == DSD_NODE_PRIME || fPolarityCurL != fPolarityCurH )
                { // there is no way to extract more than one
                    pThis->pDecs[ nEntries++ ] = pCurH;
                    // assign the support to be subtracted from both components
                    bSuppSubract = pCurH->S;
                }
                else 
                {
                    // find the equal components in two decomposition lists
                    Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
                    int nCommon = dsdKernelFindCommonComponents( pDsdMan, pPrevL, pPrevH, &pCommon, &pLastDiffL, &pLastDiffH );
        
                    if ( nCommon == 0 || nCommon == 1 )
                    { // one one component was found, which is the original one
    //                  assert( Dsd_Regular(pCommon[0]) == pCurL);
                        // add the new decomposition entry
                        pThis->pDecs[ nEntries++ ] = pCurL;
                        // assign the support to be subtracted from both components
                        bSuppSubract = pCurL->S;
                    }
                    else // more than one components was found
                    {
                        // find the OR (EXOR) of the non-overlapping components
                        DdNode * bCommF;
                        dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, (int)(pPrevL->Type==DSD_NODE_EXOR) );
                        Cudd_Ref( bCommF );
 
                        pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
                        assert( !Dsd_IsComplement(pDENew) ); // cannot be complemented because of construction
                        Cudd_RecursiveDeref( dd, bCommF );
 
                        // add the new decomposition entry
                        pThis->pDecs[ nEntries++ ] = pDENew;
 
                        // assign the support to be subtracted from both components
                        bSuppSubract = pDENew->S;
                    }
                }
 
                SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ), Cudd_Ref( SuppL );
                Cudd_RecursiveDeref(dd, bTemp);
 
                SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH );
                Cudd_RecursiveDeref(dd, bTemp);
 
            } // end of if ( fEqualLevel ) 
 
        } // end of decomposition list comparison
        Cudd_RecursiveDeref( dd, SuppL );
        Cudd_RecursiveDeref( dd, SuppH );
 
    }
 
    // check that the estimation of the number of entries was okay
    assert( nEntries <= nEntriesMax );
 
//    if ( nEntries != Extra_bddSuppSize(dd, bSuppNew) )
//        s_Case5++;
 
    // update the number of entries in the new decomposition list
    pThis->nDecs = nEntries;
    }
//}
EXIT:
 
    {
    // if the component created is complemented, it represents a function without complement
    // therefore, as it is, without complement, it should recieve the complemented function
    Dsd_Node_t * pThisR = Dsd_Regular( pThis );
    assert( pThisR->G == NULL );
    assert( pThisR->S == NULL );
 
    if ( pThisR == pThis ) // set regular function
        pThisR->G = bF; 
    else // set complemented function
        pThisR->G = Cudd_Not(bF);    
    Cudd_Ref(bF);           // reference the function in the component
 
    assert( bSuppNew );
    pThisR->S = bSuppNew;   // takes the reference from the new support
    if ( st__insert( pDsdMan->Table, (char*)bF, (char*)pThis ) )
    {
        assert( 0 );
    }
    s_CacheEntries++;
 
 
/*
    if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
    {
        // write the function, for which verification does not work
        cout << endl << "Internal verification failed!"" );
 
        // create the variable mask
        static int s_pVarMask[MAXINPUTS];
        int nInputCounter = 0;
 
        Cudd_SupportArray( dd, bF, s_pVarMask );
        int k; 
        for ( k = 0; k < dd->size; k++ )
            if ( s_pVarMask[k] )
                nInputCounter++;
 
        cout << endl << "The problem function is "" );
 
        DdNode * zNewFunc = Cudd_zddIsopCover( dd, bF, bF ); Cudd_Ref( zNewFunc );
        cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
        Cudd_RecursiveDerefZdd( dd, zNewFunc );
    }
*/
 
    }
 
    Depth--;
    return Dsd_NotCond( pThis, fCompF );
}
 


Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity )
 
{
    Dsd_Node_t * pTemp;
    int i;
 
//  assert( !Dsd_IsComplement( pWhere ) );
//  assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) );
 
    if ( pWhere->nDecs == 1 )
        return NULL;
 
    for( i = 0; i < pWhere->nDecs; i++ )
    {
        pTemp = Dsd_Regular( pWhere->pDecs[i] );
        if ( Extra_bddSuppContainVar( pDsdMan->dd, pTemp->S, Var ) )
        {
            *fPolarity = (int)( pTemp != pWhere->pDecs[i] );
            return pTemp;
        }
    }
    assert( 0 );
    return NULL;
}

int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH )
{
    static Dsd_Node_t * Common[MAXINPUTS];
    int nCommon = 0;
 
    // pointers to the current decomposition entries
    Dsd_Node_t * pLcur;
    Dsd_Node_t * pHcur;
 
    // the pointers to their supports
    DdNode * bSLcur;
    DdNode * bSHcur;
 
    // the top variable in the supports
    int TopVar;
 
    // the indices running through the components
    int iCurL = 0;
    int iCurH = 0;
    while ( iCurL < pL->nDecs && iCurH < pH->nDecs )
    { // both did not run out
 
        pLcur = Dsd_Regular(pL->pDecs[iCurL]);
        pHcur = Dsd_Regular(pH->pDecs[iCurH]);
 
        bSLcur = pLcur->S;
        bSHcur = pHcur->S;
 
        // find out what component is higher in the BDD
        if ( pDsdMan->dd->perm[bSLcur->index] < pDsdMan->dd->perm[bSHcur->index] )
            TopVar = bSLcur->index;
        else
            TopVar = bSHcur->index;
 
        if ( TopVar == bSLcur->index && TopVar == bSHcur->index ) 
        {
            // the components may be equal - should match exactly!
            if ( pL->pDecs[iCurL] == pH->pDecs[iCurH] )
                Common[nCommon++] = pL->pDecs[iCurL];
            else
            {
                *pLastDiffL = pL->pDecs[iCurL];
                *pLastDiffH = pH->pDecs[iCurH];
            }
 
            // skip both
            iCurL++;
            iCurH++;
        }
        else if ( TopVar == bSLcur->index )
        {  // the components cannot be equal
            // skip the top-most one
            *pLastDiffL = pL->pDecs[iCurL++];
        }
        else // if ( TopVar == bSHcur->index )
        {  // the components cannot be equal
            // skip the top-most one
            *pLastDiffH = pH->pDecs[iCurH++];
        }
    }
 
    // if one of the lists still has components, write the first one down
    if ( iCurL < pL->nDecs )
        *pLastDiffL = pL->pDecs[iCurL];
 
    if ( iCurH < pH->nDecs )
        *pLastDiffH = pH->pDecs[iCurH];
 
    // return the pointer to the array
    *pCommon = Common;
    // return the number of common components
    return nCommon;         
}

void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor )
{
    DdManager * dd = pDsdMan->dd;
    DdNode * bF, * bFadd, * bTemp;
        DdNode * bS = NULL; // Suppress "might be used uninitialized"
    Dsd_Node_t * pDE, * pDER;
    int i;
 
    // start the function
    bF = b0; Cudd_Ref( bF );
    // start the support
    if ( pCompS )
        bS = b1, Cudd_Ref( bS );
 
    assert( nCommon > 0 );
    for ( i = 0; i < nCommon; i++ )
    {
        pDE  = pCommon[i];
        pDER = Dsd_Regular( pDE );
        bFadd = (pDE != pDER)? Cudd_Not(pDER->G): pDER->G;
        // add to the function
        if ( fExor )
            bF = Cudd_bddXor( dd, bTemp = bF, bFadd );
        else
            bF = Cudd_bddOr( dd, bTemp = bF, bFadd );
        Cudd_Ref( bF );
        Cudd_RecursiveDeref( dd, bTemp );
        if ( pCompS )
        {
            // add to the support
            bS = Cudd_bddAnd( dd, bTemp = bS, pDER->S );  Cudd_Ref( bS );
            Cudd_RecursiveDeref( dd, bTemp );
        }
    }
    // return the function
    Cudd_Deref( bF );
    *pCompF = bF;
 
    // return the support
    if ( pCompS )
        Cudd_Deref( bS ), *pCompS = bS;
}

int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall )
{
    DdManager * dd = pDsdMan->dd;
    DdNode * bSuppLarge, * bSuppSmall;
    int RetValue;
    
    RetValue = Extra_bddSuppCheckContainment( dd, pL->S, pH->S, &bSuppLarge, &bSuppSmall );
 
    if ( RetValue == 0 ) 
        return 0;
 
    if ( pH->S == bSuppLarge )
    {
        *pLarge = pH;
        *pSmall = pL;
    }
    else // if ( pL->S == bSuppLarge )
    {
        *pLarge = pL;
        *pSmall = pH;
    }
    return 1;
}

void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize )
{
    int i;
    assert( nListSize+1 == p->nDecs );
    p->pDecs[0] = First;
    for( i = 0; i < nListSize; i++ )
        p->pDecs[i+1] = ppList[i];
}

void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int iSkipped )
{
    int i, Counter;
    assert( nListSize == p->nDecs );
    p->pDecs[0] = First;
    for( i = 0, Counter = 1; i < nListSize; i++ )
        if ( i != iSkipped )
            p->pDecs[Counter++] = ppList[i];
}

int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
{
    DdManager * dd = pDsdMan->dd;
    Dsd_Node_t * pR    = Dsd_Regular(pDE);
    int RetValue;
 
    DdNode * bRes;
    if ( pR->Type == DSD_NODE_CONST1 )
        bRes = b1;
    else if ( pR->Type == DSD_NODE_BUF )
        bRes = pR->G;
    else if ( pR->Type == DSD_NODE_OR || pR->Type == DSD_NODE_EXOR )
        dsdKernelComputeSumOfComponents( pDsdMan, pR->pDecs, pR->nDecs, &bRes, NULL, (int)(pR->Type == DSD_NODE_EXOR) );
    else if ( pR->Type == DSD_NODE_PRIME )
    {
        int i;
        static DdNode * bGVars[MAXINPUTS];
        // transform the function of this block, so that it depended on inputs
        // corresponding to the formal inputs
        DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 );  Cudd_Ref( bNewFunc );
 
        // compose this function with the inputs
        // create the elementary permutation
        for ( i = 0; i < dd->size; i++ )
            bGVars[i] = dd->vars[i];
 
        // assign functions to be composed
        for ( i = 0; i < pR->nDecs; i++ )
            bGVars[dd->invperm[i]] = pR->pDecs[i]->G;
 
        // perform the composition
        bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars );      Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bNewFunc );

        RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
        Cudd_Deref( bRes );
    }
    else
    {
        assert(0);
    }
 
    Cudd_Ref( bRes );
    RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
    Cudd_RecursiveDeref( dd, bRes );
    return RetValue;
}

ABC_NAMESPACE_IMPL_END