src/aig/kit/kitSop.c

Go to the documentation of this file.

#include "kit.h"



void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory )
{
    unsigned uCube;
    int i;
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
    // add the cubes
    Vec_IntForEachEntry( vInput, uCube, i )
        Kit_SopPushCube( cResult, uCube );
}

void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nLits, Vec_Int_t * vMemory )
{
    unsigned uCube, uMask = 0;
    int i, nCubes = Vec_IntSize(vInput);
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
    // add the cubes
//    Vec_IntForEachEntry( vInput, uCube, i )
    for ( i = 0; i < nCubes; i++ )
    {
        uCube = Vec_IntEntry( vInput, i );
        uMask = ((uCube | (uCube >> 1)) & 0x55555555);
        uMask |= (uMask << 1);
        Kit_SopPushCube( cResult, uCube ^ uMask );
    }
}

void Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory )
{
    unsigned uCube;
    int i;
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
    // add the cubes
    Kit_SopForEachCube( cSop, uCube, i )
        Kit_SopPushCube( cResult, uCube );
}

void Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit )
{
    unsigned uCube;
    int i, k = 0;
    Kit_SopForEachCube( cSop, uCube, i )
    {
        if ( Kit_CubeHasLit(uCube, iLit) )
            Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
    }
    Kit_SopShrink( cSop, k );
}


void Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
{
    unsigned uCube, uDiv;
    int i;
    // get the only cube
    assert( Kit_SopCubeNum(cDiv) == 1 );
    uDiv = Kit_SopCube(cDiv, 0);
    // allocate covers
    vQuo->nCubes = 0;
    vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
    vRem->nCubes = 0;
    vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
    // sort the cubes
    Kit_SopForEachCube( cSop, uCube, i )
    {
        if ( Kit_CubeContains( uCube, uDiv ) )
            Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
        else
            Kit_SopPushCube( vRem, uCube );
    }
}

void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
{
    unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
    int i, i2, k, k2, nCubesRem;
    assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
    // consider special case
    if ( Kit_SopCubeNum(cDiv) == 1 )
    {
        Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
        return;
    }
    // allocate quotient
    vQuo->nCubes = 0;
    vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
    // for each cube of the cover
    // it either belongs to the quotient or to the remainder
    Kit_SopForEachCube( cSop, uCube, i )
    {
        // skip taken cubes
        if ( Kit_CubeIsMarked(uCube) )
            continue;
        // find a matching cube in the divisor
        uDiv = ~0;
        Kit_SopForEachCube( cDiv, uDiv, k )
            if ( Kit_CubeContains( uCube, uDiv ) )
                break;
        // the cube is not found 
        if ( k == Kit_SopCubeNum(cDiv) )
            continue;
        // the quotient cube exists
        uQuo = Kit_CubeSharp( uCube, uDiv );
        // find corresponding cubes for other cubes of the divisor
        uDiv2 = ~0;
        Kit_SopForEachCube( cDiv, uDiv2, k2 )
        {
            if ( k2 == k )
                continue;
            // find a matching cube
            Kit_SopForEachCube( cSop, uCube2, i2 )
            {
                // skip taken cubes
                if ( Kit_CubeIsMarked(uCube2) )
                    continue;
                // check if the cube can be used
                if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
                    break;
            }
            // the case when the cube is not found
            if ( i2 == Kit_SopCubeNum(cSop) )
                break;
        }
        // we did not find some cubes - continue looking at other cubes
        if ( k2 != Kit_SopCubeNum(cDiv) )
            continue;
        // we found all cubes - add the quotient cube
        Kit_SopPushCube( vQuo, uQuo );

        // mark the first cube
        Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
        // mark other cubes that have this quotient
        Kit_SopForEachCube( cDiv, uDiv2, k2 )
        {
            if ( k2 == k )
                continue;
            // find a matching cube
            Kit_SopForEachCube( cSop, uCube2, i2 )
            {
                // skip taken cubes
                if ( Kit_CubeIsMarked(uCube2) )
                    continue;
                // check if the cube can be used
                if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
                    break;
            }
            assert( i2 < Kit_SopCubeNum(cSop) );
            // the cube is found, mark it 
            // (later we will add all unmarked cubes to the remainder)
            Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
        }
    }
    // determine the number of cubes in the remainder
    nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
    // allocate remainder
    vRem->nCubes = 0;
    vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
    // finally add the remaining unmarked cubes to the remainder 
    // and clean the marked cubes in the cover
    Kit_SopForEachCube( cSop, uCube, i )
    {
        if ( !Kit_CubeIsMarked(uCube) )
        {
            Kit_SopPushCube( vRem, uCube );
            continue;
        }
        Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
    }
    assert( nCubesRem == Kit_SopCubeNum(vRem) );
}

static inline unsigned Kit_SopCommonCube( Kit_Sop_t * cSop )
{
    unsigned uMask, uCube;
    int i;
    uMask = ~(unsigned)0;
    Kit_SopForEachCube( cSop, uCube, i )
        uMask &= uCube;
    return uMask;
}

void Kit_SopMakeCubeFree( Kit_Sop_t * cSop )
{
    unsigned uMask, uCube;
    int i;
    uMask = Kit_SopCommonCube( cSop );
    if ( uMask == 0 )
        return;
    // remove the common cube
    Kit_SopForEachCube( cSop, uCube, i )
        Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
}

int Kit_SopIsCubeFree( Kit_Sop_t * cSop )
{
    return Kit_SopCommonCube( cSop ) == 0;
}

void Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory )
{
    assert( Kit_SopCubeNum(cSop) > 0 );
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, 1 );
    Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
}


int Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits )
{
    unsigned uCube;
    int i, k, nLitsCur;
    // go through each literal
    for ( i = 0; i < nLits; i++ )
    {
        // go through all the cubes
        nLitsCur = 0;
        Kit_SopForEachCube( cSop, uCube, k )
            if ( Kit_CubeHasLit(uCube, i) )
                nLitsCur++;
        if ( nLitsCur > 1 )
            return i;
    }
    return -1;
}

int Kit_SopWorstLiteral( Kit_Sop_t * cSop, int nLits )
{
    unsigned uCube;
    int i, k, iMin, nLitsMin, nLitsCur;
    int fUseFirst = 1;

    // go through each literal
    iMin = -1;
    nLitsMin = 1000000;
    for ( i = 0; i < nLits; i++ )
    {
        // go through all the cubes
        nLitsCur = 0;
        Kit_SopForEachCube( cSop, uCube, k )
            if ( Kit_CubeHasLit(uCube, i) )
                nLitsCur++;
        // skip the literal that does not occur or occurs once
        if ( nLitsCur < 2 )
            continue;
        // check if this is the best literal
        if ( fUseFirst )
        {
            if ( nLitsMin > nLitsCur )
            {
                nLitsMin = nLitsCur;
                iMin = i;
            }
        }
        else
        {
            if ( nLitsMin >= nLitsCur )
            {
                nLitsMin = nLitsCur;
                iMin = i;
            }
        }
    }
    if ( nLitsMin < 1000000 )
        return iMin;
    return -1;
}

int Kit_SopBestLiteral( Kit_Sop_t * cSop, int nLits, unsigned uMask )
{
    unsigned uCube;
    int i, k, iMax, nLitsMax, nLitsCur;
    int fUseFirst = 1;

    // go through each literal
    iMax = -1;
    nLitsMax = -1;
    for ( i = 0; i < nLits; i++ )
    {
        if ( !Kit_CubeHasLit(uMask, i) )
            continue;
        // go through all the cubes
        nLitsCur = 0;
        Kit_SopForEachCube( cSop, uCube, k )
            if ( Kit_CubeHasLit(uCube, i) )
                nLitsCur++;
        // skip the literal that does not occur or occurs once
        if ( nLitsCur < 2 )
            continue;
        // check if this is the best literal
        if ( fUseFirst )
        {
            if ( nLitsMax < nLitsCur )
            {
                nLitsMax = nLitsCur;
                iMax = i;
            }
        }
        else
        {
            if ( nLitsMax <= nLitsCur )
            {
                nLitsMax = nLitsCur;
                iMax = i;
            }
        }
    }
    if ( nLitsMax >= 0 )
        return iMax;
    return -1;
}

void Kit_SopDivisorZeroKernel_rec( Kit_Sop_t * cSop, int nLits )
{
    int iLit;
    // find any literal that occurs at least two times
    iLit = Kit_SopWorstLiteral( cSop, nLits );
    if ( iLit == -1 )
        return;
    // derive the cube-free quotient
    Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
    Kit_SopMakeCubeFree( cSop );             // the same cover
    // call recursively
    Kit_SopDivisorZeroKernel_rec( cSop, nLits );    // the same cover
}

int Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory )
{
    if ( Kit_SopCubeNum(cSop) <= 1 )
        return 0;
    if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
        return 0;
    // duplicate the cover
    Kit_SopDup( cResult, cSop, vMemory );
    // perform the kerneling
    Kit_SopDivisorZeroKernel_rec( cResult, nLits );
    assert( Kit_SopCubeNum(cResult) > 0 );
    return 1;
}


void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory )
{
    int iLitBest;
    // get the best literal
    iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, 1 );
    // set the cube
    Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
}

---