src/opt/fxu/fxuReduce.c

Go to the documentation of this file.

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


static int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] );


int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax )
{
    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, CutOffQuant;
    int iPair, iQuant, k, c;
    int clk = clock();
    char * pSopCover;
    int nFanins;

    assert( nPairsMax < nPairsTotal );

    // allocate storage for counter of diffs
    pnLitsDiff = ALLOC( 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 = 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 );

    // allocate storage for counters of cube pairs by difference
    pnPairCounters = ALLOC( int, 2 * nBitsMax );
    memset( pnPairCounters, 0, sizeof(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 )
    {
        printf( "The SOPs of the nodes are not cube-free. Run \"bdd; sop\" before \"fx\".\n" );
        return 0;
    }
    if ( pnPairCounters[1] != 0 )
    {
        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;
        }
    }
    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 = 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 );
    FREE( pnLitsDiff );
//PRT( "Preprocess", clock() - clk );
    return 1;
}


int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] )
{
    char * pCube1, * pCube2;
    int nOnes, nCubePairs, nFanins, v;
    nCubePairs = 0;
    nFanins = Abc_SopGetVarNum(pCover);
    Abc_SopForEachCube( pCover, nFanins, pCube1 )
    Abc_SopForEachCube( pCube1, nFanins, pCube2 )
    {
        if ( pCube1 == pCube2 )
            continue;
        nOnes = 0;
        for ( v = 0; v < nFanins; v++ )
            nOnes += (pCube1[v] != pCube2[v]);
        pDiffs[nCubePairs++] = nOnes;
    }
    return 1;
}

---