fxucreate.c

主要进行大规模的电路综合

        // the node should be added
        Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
        // update the first cube
        pCubeFirst = pCubeNext;
    }
}

/**Function*************************************************************

  Synopsis    [Create Mvc covers for one node that has changed.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
{
    Mvc_Cover_t * pMvcCover;
    Mvc_Cube_t * pMvcCube;
    Fxu_Var * pVar;
    Fxu_Cube * pCube;
    Fxu_Lit * pLit;
    int iNum, iNumC, iNodeVar, iValue, iValueFirst;
    int nValues, c, v;
    bool fPosLitIsOdd;


    // mark and collect all the variables involved with these cubes 
    // between pCubeFirst and pCubeNext
    Fxu_MatrixRingVarsStart( p );
    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
        for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
        {
            pVar = pLit->pVar;
            if ( pVar->pOrder == NULL )
            {
                // add this var
                Fxu_MatrixRingVarsAdd( p, pVar );

                // add the related vars
                // get the corresponding node
                iNodeVar = pData->pValue2Node[pVar->iVar];
                // get the number of values of the corresponding node
                iValueFirst = pData->pNode2Value[iNodeVar];
                nValues     = pData->pNode2Value[iNodeVar+1] - pData->pNode2Value[iNodeVar];
                for ( c = 0; c < nValues; c++ )
                {
                    pVar = p->ppVars[iValueFirst + c];
                    if ( pVar->pOrder == NULL )
                        Fxu_MatrixRingVarsAdd( p, pVar );
                }
            }
        }
    Fxu_MatrixRingVarsStop( p );

    // transfer the vars from the list to the array
    p->nVarsTemp = 0;
    Fxu_MatrixForEachVarInRing( p, pVar )
        p->pVarsTemp[ p->nVarsTemp++ ] = pVar;
    Fxu_MatrixRingVarsUnmark( p );

    // sort the variables by their numbers
    qsort( (void *)p->pVarsTemp, p->nVarsTemp, sizeof(Fxu_Var *), 
        (int (*)(const void *, const void *)) Fxu_CreateCoversVarCompare );
    assert( Fxu_CreateCoversVarCompare( p->pVarsTemp, p->pVarsTemp + p->nVarsTemp - 1 ) < 0 );

    // mark the vars with their numbers
    for ( v = 0; v < p->nVarsTemp; v++ )
        p->pVarsTemp[v]->lLits.nItems = v; // hack - reuse lLits.nItems

    // create the covers for this node
    iValueFirst = pData->pNode2Value[iNode];
    nValues     = pData->pNode2Value[iNode+1] - pData->pNode2Value[iNode];

    // get the starting cube of the first cover
    pCube = pCubeFirst;
    for ( v = 0; v < nValues; v++ )
    {
        // get the current value
        iValue = iValueFirst + v;
        // get the variable
        pVar = p->ppVars[iValue];

        // consider default values and constant values
        if ( pVar->pFirst == NULL )
        {
             if ( iValue < pData->nValuesOld && pData->ppCovers[iValue] )
             { // this is the old cover, and it is present
                 // this should be a constant cover
                 assert( Mvc_CoverIsEmpty(pData->ppCovers[iValue]) || 
                         Mvc_CoverIsTautology(pData->ppCovers[iValue]) );
                 // copy the cover (but with the different number of bits
                 pData->ppCoversNew[iValue] = Mvc_CoverAlloc( pData->pManMvc, p->nVarsTemp );
                 // if the original cover is a tau, make this cover a tau too
                 if ( Mvc_CoverIsTautology(pData->ppCovers[iValue]) )
                     Mvc_CoverMakeTautology(pData->ppCoversNew[iValue]);
             }
             else // set the empty cover
                 pData->ppCoversNew[iValue] = NULL;
            continue;
        }

        // start the new Mvc cover
        pMvcCover = Mvc_CoverAlloc( pData->pManMvc, p->nVarsTemp );
        // set the literals according to the selected vars
        Mvc_CoverAllocateArrayLits( pMvcCover );
        for ( c = 0; c < p->nVarsTemp; c++ )
            pMvcCover->pLits[c] = p->pVarsTemp[c]->iVar;

        // determine the polarity of the new literals
        fPosLitIsOdd = -1;
        for ( c = 0; c < p->nVarsTemp; c++ )
            if ( pMvcCover->pLits[c] >= pData->nValuesOld )
            {
                fPosLitIsOdd = ((c & 1) == 0);
                break;
            }

        // add new Mvc cubes to the cover
        for ( c = 0; c < pVar->nCubes; c++ )
        {
            if ( pCube->lLits.nItems )
            { // the cube is not empty
                // create the new Mvc cube
                pMvcCube = Mvc_CubeAlloc( pMvcCover );
                Mvc_CubeBitClean( pMvcCube );
                // insert literals
                for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
                {
                    iNum = pLit->pVar->lLits.nItems;
                    assert( iNum < p->nVarsTemp );

                    if ( pLit->pVar->iVar < pData->nValuesOld )
                        Mvc_CubeBitInsert( pMvcCube, iNum );
                    else
                    {
//                        Mvc_CubeBitInsert( pMvcCube, iNum - 1 );
                        assert( fPosLitIsOdd != -1 );
                        if ( fPosLitIsOdd )
                        {
                            if ( iNum & 1 )
                                iNumC = iNum - 1;
                            else
                                iNumC = iNum + 1;
                        }
                        else
                        {
                            if ( iNum & 1 )
                                iNumC = iNum + 1;
                            else
                                iNumC = iNum - 1;
                        }
                        Mvc_CubeBitInsert( pMvcCube, iNumC );
                    }
                }
                // here we perform the inverse co-singleton transform
                Mvc_CubeBitNot( pMvcCube );
                // add the cube
                Mvc_CoverAddCubeTail( pMvcCover, pMvcCube );
            }
            // scroll to the new cube
            pCube = pCube->pNext;
        }
        // set the new Mvc cover
        pData->ppCoversNew[iValue] = pMvcCover;
    }
    assert( pCube == pCubeNext );
}


/**Function*************************************************************

  Synopsis    [Adds the var to storage.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode )
{
    Fxu_Var * pVar;
    int v, iValueFirst, nValues;

    iValueFirst = pData->pNode2Value[iNode];
    nValues     = pData->pNode2Value[iNode + 1] - pData->pNode2Value[iNode];
    // go through variables until the one with the cube
    for ( v = 0; v < nValues; v++ )
    {
        pVar = p->ppVars[iValueFirst + v];
        if ( pVar->pFirst )
            return pVar->pFirst;
    }
    return NULL;
}

/**Function*************************************************************

  Synopsis    [Compares the vars by their number.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxu_CreateCoversVarCompare( Fxu_Var ** ppV1, Fxu_Var ** ppV2 )
{
    int iVar1 = (*ppV1)->iVar;
    int iVar2 = (*ppV2)->iVar;
    if ( iVar1 < iVar2 )
        return -1;
    if ( iVar1 > iVar2 )
        return 1;
    assert( 0 );
    return 0;
}

/**Function*************************************************************

  Synopsis    [Compares the vars by their number.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
{
    return s_pLits[*ptrX] - s_pLits[*ptrY];
} 

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxu_CreateSCDs( Fxu_Matrix * p, Fxu_Data_t * pData )
{
    Fxu_Var * pVar1;
    Fxu_Var * pVar2, * pVarTemp;
    Fxu_Lit * pLitV, * pLitH;
    int Coin;
    int CounterAll;
    int CounterTest;
    int CounterImp2;
    int CounterImp3;
    int clk;

    CounterAll = 0;
    CounterTest = 0;
    CounterImp2 = 0;
    CounterImp3 = 0;

clk = clock();
    // iterate through the columns in the matrix
    Fxu_MatrixForEachVariable( p, pVar1 )
    {
        // start collecting the affected vars
        Fxu_MatrixRingVarsStart( p );
        // go through all the literals of this variable
        for ( pLitV = pVar1->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
        {
            // for this literal, go through all the horizontal literals
            for ( pLitH = pLitV->pHNext; pLitH; pLitH = pLitH->pHNext )
            {
                // get another variable
                pVar2 = pLitH->pVar;
                CounterAll++;
                // skip the var if it is already used
                if ( pVar2->pOrder )
                    continue;
                // skip the var if it belongs to the same node
                if ( pData->pValue2Node[pVar1->iVar] == pData->pValue2Node[pVar2->iVar] )
                    continue;
                // collect the var
                Fxu_MatrixRingVarsAdd( p, pVar2 );
            }
        }
        // stop collecting the affected vars
        Fxu_MatrixRingVarsStop( p );

        // iterate through the vars
        Fxu_MatrixForEachVarInRing( p, pVar2 )
        {
            CounterTest++;
            // count the coincidence
            Coin = Fxu_SingleCountCoincidence( p, pVar1, pVar2 );
            assert( Coin > 0 );

            if ( Coin > 1 )
                CounterImp2++;
            if ( Coin > 2 )
            {
//                printf( "pair = (%2d, %2d)\n", pVar1->iVar, pVar2->iVar );
                CounterImp3++;
            }
        }
        // unmark the vars
        Fxu_MatrixForEachVarInRingSafe( p, pVar2, pVarTemp )
            pVar2->pOrder = NULL;

        Fxu_MatrixRingVarsReset( p );

    }
    printf( "Total = %5d. Tested = %5d. 2+ = %d. 3+ = %d.\n", 
        CounterAll, CounterTest, CounterImp2, CounterImp3 );

PRT( "Time", clock() - clk );

return 1;
}