fxuReduce.c File Reference

#include "base/abc/abc.h"
#include "fxuInt.h"
#include "fxu.h"

Include dependency graph for fxuReduce.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 ///.

Function Documentation

Fxu_PreprocessCubePairs()

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

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: