fxuCreate.c File Reference

#include "fxuInt.h"
#include "fxu.h"

Include dependency graph for fxuCreate.c:

Go to the source code of this file.

Functions
int	Fxu_PreprocessCubePairs (Fxu_Matrix *p, Vec_Ptr_t *vCovers, int nPairsTotal, int nPairsMax)
	FUNCTION DEFINITIONS ///.
Fxu_Matrix *	Fxu_CreateMatrix (Fxu_Data_t *pData)
	FUNCTION DEFINITIONS ///.
void	Fxu_CreateCovers (Fxu_Matrix *p, Fxu_Data_t *pData)

Function Documentation

Fxu_CreateCovers()

void Fxu_CreateCovers	(	Fxu_Matrix *	p,
		Fxu_Data_t *	pData )

Function*************************************************************

Synopsis [Creates the new array of Sop covers from the sparse matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file fxuCreate.c.

{
    Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
    char * pSopCover;
    int iNode, n;
 
    // get the first cube of the first internal node 
    pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
 
    // go through the internal nodes
    for ( n = 0; n < pData->nNodesOld; n++ )
    if ( (pSopCover = (char *)pData->vSops->pArray[n]) )
    {
        // get the number of this node
        iNode = n;
        // get the next first cube
        pCubeNext = Fxu_CreateCoversFirstCube(  p, pData, iNode + 1 );
        // check if there any new variables in these cubes
        for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
            if ( pCube->lLits.pTail && pCube->lLits.pTail->iVar >= 2 * pData->nNodesOld )
                break;
        if ( pCube != pCubeNext )
            Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
        // update the first cube
        pCubeFirst = pCubeNext;
    }
 
    // add the covers for the extracted nodes
    for ( n = 0; n < pData->nNodesNew; n++ )
    {
        // get the number of this node
        iNode = pData->nNodesOld + n;
        // get the next first cube
        pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
        // the node should be added
        Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
        // update the first cube
        pCubeFirst = pCubeNext;
    }
}

Here is the caller graph for this function:

Fxu_CreateMatrix()

Fxu_Matrix * Fxu_CreateMatrix

(

Fxu_Data_t *

pData

)

FUNCTION DEFINITIONS ///.

DECLARATIONS ///.

Function*************************************************************

Synopsis [Creates the sparse matrix from the array of SOPs.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file fxuCreate.c.

{
    Fxu_Matrix * p;
    Fxu_Var * pVar;
    Fxu_Cube * pCubeFirst, * pCubeNew;
    Fxu_Cube * pCube1, * pCube2;
    Vec_Int_t * vFanins;
    char * pSopCover;
    char * pSopCube;
    int * pOrder, nBitsMax;
    int i, v, c;
    int nCubesTotal;
    int nPairsTotal;
    int nPairsStore;
    int nCubes;
    int iCube, iPair;
    int nFanins;
 
    // collect all sorts of statistics
    nCubesTotal =  0;
    nPairsTotal =  0;
    nPairsStore =  0;
    nBitsMax    = -1; 
    for ( i = 0; i < pData->nNodesOld; i++ )
        if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
        {
            nCubes       = Abc_SopGetCubeNum( pSopCover );
            nFanins      = Abc_SopGetVarNum( pSopCover );
            assert( nFanins > 1 && nCubes > 0 );
 
            nCubesTotal += nCubes;
            nPairsTotal += nCubes * (nCubes - 1) / 2;
            nPairsStore += nCubes * nCubes;
            if ( nBitsMax < nFanins )
                nBitsMax = nFanins;
        }
    if ( nBitsMax <= 0 )
    {
        printf( "The current network does not have SOPs to perform extraction.\n" );
        return NULL;
    }
 
    if ( nPairsStore > 50000000 )
    {
        printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
        return NULL;
    }
 
    // start the matrix
    p = Fxu_MatrixAllocate();
    // create the column labels 
    p->ppVars = ABC_ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
    for ( i = 0; i < 2 * pData->nNodesOld; i++ )
        p->ppVars[i] = Fxu_MatrixAddVar( p );
 
    // allocate storage for all cube pairs at once
    p->pppPairs = ABC_ALLOC( Fxu_Pair **, nCubesTotal + 100 );
    p->ppPairs  = ABC_ALLOC( Fxu_Pair *,  nPairsStore + 100 );
    memset( p->ppPairs, 0, sizeof(Fxu_Pair *) * nPairsStore );
    iCube = 0;
    iPair = 0;
    for ( i = 0; i < pData->nNodesOld; i++ )
        if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
        {
            // get the number of cubes
            nCubes = Abc_SopGetCubeNum( pSopCover );
            // get the new var in the matrix
            pVar = p->ppVars[2*i+1];
            // assign the pair storage
            pVar->nCubes     = nCubes;
            if ( nCubes > 0 )
            {
                pVar->ppPairs    = p->pppPairs + iCube;
                pVar->ppPairs[0] = p->ppPairs  + iPair;
                for ( v = 1; v < nCubes; v++ )
                    pVar->ppPairs[v] = pVar->ppPairs[v-1] + nCubes;
            }
            // update
            iCube += nCubes;
            iPair += nCubes * nCubes;
        }
    assert( iCube == nCubesTotal );
    assert( iPair == nPairsStore );
 
 
    // allocate room for the reordered literals
    pOrder = ABC_ALLOC( int, nBitsMax );
    // create the rows
    for ( i = 0; i < pData->nNodesOld; i++ )
    if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
    {
        // get the new var in the matrix
        pVar = p->ppVars[2*i+1];
        // here we sort the literals of the cover
        // in the increasing order of the numbers of the corresponding nodes
        // because literals should be added to the matrix in this order
        vFanins = (Vec_Int_t *)pData->vFanins->pArray[i];
        s_pLits = vFanins->pArray;
        // start the variable order
        nFanins = Abc_SopGetVarNum( pSopCover );
        for ( v = 0; v < nFanins; v++ )
            pOrder[v] = v;
        // reorder the fanins
        qsort( (void *)pOrder, (size_t)nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
        assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
        // create the corresponding cubes in the matrix
        pCubeFirst = NULL;
        c = 0;
        Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
        {
            // create the cube
            pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
            Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
            if ( pCubeFirst == NULL )
                pCubeFirst = pCubeNew;
            pCubeNew->pFirst = pCubeFirst;
        }
        // set the first cube of this var
        pVar->pFirst = pCubeFirst;
        // create the divisors without preprocessing
        if ( nPairsTotal <= pData->nPairsMax )
        {
            for ( pCube1 = pCubeFirst; pCube1; pCube1 = pCube1->pNext )
                for ( pCube2 = pCube1? pCube1->pNext: NULL; pCube2; pCube2 = pCube2->pNext )
                    Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
        }
    }
    ABC_FREE( pOrder );
 
    // consider the case when cube pairs should be preprocessed
    // before adding them to the set of divisors
//    if ( pData->fVerbose )
//        printf( "The total number of cube pairs is %d.\n", nPairsTotal );
    if ( nPairsTotal > 10000000 )
    {
        printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
        printf( "that the user changes the network by reducing the size of logic node and\n" );
        printf( "consequently the number of cube pairs to be processed by this command.\n" );
        printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
        return NULL;
    }
    if ( nPairsTotal > pData->nPairsMax )
        if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
            return NULL;
//    if ( pData->fVerbose )
//        printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
 
    if ( p->lVars.nItems > 1000000 )
    {
        printf( "The total number of variables is more than 1,000,000.\n" );
        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
        printf( "that the user changes the network by reducing the size of logic node and\n" );
        printf( "consequently the number of cube pairs to be processed by this command.\n" );
        printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
        return NULL;
    }
 
 
    // add the var pairs to the heap
    Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
 
    // print stats
    if ( pData->fVerbose )
    {
        double Density;
        Density = ((double)p->nEntries) / p->lVars.nItems / p->lCubes.nItems;
        fprintf( stdout, "Matrix: [vars x cubes] = [%d x %d]  ",
            p->lVars.nItems, p->lCubes.nItems );
        fprintf( stdout, "Lits = %d  Density = %.5f%%\n", 
            p->nEntries, Density );
        fprintf( stdout, "1-cube divs = %6d. (Total = %6d)  ",  p->lSingles.nItems, p->nSingleTotal );
        fprintf( stdout, "2-cube divs = %6d. (Total = %6d)",  p->nDivsTotal, nPairsTotal );
        fprintf( stdout, "\n" );
    }
//    Fxu_MatrixPrint( stdout, p );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_PreprocessCubePairs()

int Fxu_PreprocessCubePairs ( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax )

extern

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Precomputes the pairs to use for creating two-cube divisors.]

Description [This procedure takes the matrix with variables and cubes allocated (p), the original covers of the nodes (i-sets) and their number (ppCovers,nCovers). The maximum number of pairs to compute and the total number of pairs in existence. This procedure adds to the storage of divisors exactly the given number of pairs (nPairsMax) while taking first those pairs that have the smallest number of literals in their cube-free form.]

SideEffects []

SeeAlso []

Definition at line 53 of file fxuReduce.c.

{
    unsigned char * pnLitsDiff;   // storage for the counters of diff literals
    int * pnPairCounters;         // the counters of pairs for each number of diff literals
    Fxu_Cube * pCubeFirst, * pCubeLast;
    Fxu_Cube * pCube1, * pCube2;
    Fxu_Var * pVar;
    int nCubes, nBitsMax, nSum;
    int CutOffNum = -1, CutOffQuant = -1; // Suppress "might be used uninitialized"
    int iPair, iQuant, k, c;
//    abctime clk = Abc_Clock();
    char * pSopCover;
    int nFanins;
 
    assert( nPairsMax < nPairsTotal );
 
    // allocate storage for counter of diffs
    pnLitsDiff = ABC_FALLOC( unsigned char, nPairsTotal );
    // go through the covers and precompute the distances between the pairs
    iPair    =  0;
    nBitsMax = -1;
    for ( c = 0; c < vCovers->nSize; c++ )
        if ( (pSopCover = (char *)vCovers->pArray[c]) )
        {
            nFanins = Abc_SopGetVarNum(pSopCover);
            // precompute the differences
            Fxu_CountPairDiffs( pSopCover, pnLitsDiff + iPair );
            // update the counter
            nCubes = Abc_SopGetCubeNum( pSopCover );
            iPair += nCubes * (nCubes - 1) / 2;
            if ( nBitsMax < nFanins )
                nBitsMax = nFanins;
        }
    assert( iPair == nPairsTotal );
    if ( nBitsMax == -1 )
        nBitsMax = 0;
 
    // allocate storage for counters of cube pairs by difference
    pnPairCounters = ABC_CALLOC( int, 2 * nBitsMax );
    // count the number of different pairs
    for ( k = 0; k < nPairsTotal; k++ )
        pnPairCounters[ pnLitsDiff[k] ]++;
    // determine what pairs to take starting from the lower
    // so that there would be exactly pPairsMax pairs
    if ( pnPairCounters[0] != 0 )
    {
        ABC_FREE( pnLitsDiff );
        ABC_FREE( pnPairCounters );
        printf( "The SOPs of the nodes contain duplicated cubes. Run \"bdd; sop\" before \"fx\".\n" );
        return 0;
    }
    if ( pnPairCounters[1] != 0 )
    {
        ABC_FREE( pnLitsDiff );
        ABC_FREE( pnPairCounters );
        printf( "The SOPs of the nodes are not SCC-free. Run \"bdd; sop\" before \"fx\".\n" );
        return 0;
    }
    assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
    assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
    nSum = 0;
    for ( k = 0; k < 2 * nBitsMax; k++ )
    {
        nSum += pnPairCounters[k];
        if ( nSum >= nPairsMax )
        {
            CutOffNum   = k;
            CutOffQuant = pnPairCounters[k] - (nSum - nPairsMax);
            break;
        }
    }
    ABC_FREE( pnPairCounters );
 
    // set to 0 all the pairs above the cut-off number and quantity
    iQuant = 0;
    iPair  = 0;
    for ( k = 0; k < nPairsTotal; k++ )
        if ( pnLitsDiff[k] > CutOffNum ) 
            pnLitsDiff[k] = 0;
        else if ( pnLitsDiff[k] == CutOffNum )
        {
            if ( iQuant++ >= CutOffQuant )
                pnLitsDiff[k] = 0;
            else
                iPair++;
        }
        else
            iPair++;
    assert( iPair == nPairsMax );
 
    // collect the corresponding pairs and add the divisors
    iPair = 0;
    for ( c = 0; c < vCovers->nSize; c++ )
        if ( (pSopCover = (char *)vCovers->pArray[c]) )
        {
            // get the var
            pVar = p->ppVars[2*c+1];
            // get the first cube
            pCubeFirst = pVar->pFirst;
            // get the last cube
            pCubeLast = pCubeFirst;
            for ( k = 0; k < pVar->nCubes; k++ )
                pCubeLast = pCubeLast->pNext;
            assert( pCubeLast == NULL || pCubeLast->pVar != pVar );
 
            // go through the cube pairs
            for ( pCube1 = pCubeFirst; pCube1 != pCubeLast; pCube1 = pCube1->pNext )
                for ( pCube2 = pCube1->pNext; pCube2 != pCubeLast; pCube2 = pCube2->pNext )
                    if ( pnLitsDiff[iPair++] )
                    {   // create the divisors for this pair
                        Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
                    }
        }
    assert( iPair == nPairsTotal );
    ABC_FREE( pnLitsDiff );
//ABC_PRT( "Preprocess", Abc_Clock() - clk );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function: