src/misc/mvc/mvcUtils.c

Go to the documentation of this file.

#include "mvc.h"


static int bit_count[256] = {
  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};


static void Mvc_CoverCopyColumn( Mvc_Cover_t * pCoverOld, Mvc_Cover_t * pCoverNew, int iColOld, int iColNew );



void Mvc_CoverSupport( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp )
{
    Mvc_Cube_t * pCube;
    // clean the support
    Mvc_CubeBitClean( pSupp );
    // collect the support
    Mvc_CoverForEachCube( pCover, pCube )
        Mvc_CubeBitOr( pSupp, pSupp, pCube );
}

void Mvc_CoverSupportAnd( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp )
{
    Mvc_Cube_t * pCube;
    // clean the support
    Mvc_CubeBitFill( pSupp );
    // collect the support
    Mvc_CoverForEachCube( pCover, pCube )
        Mvc_CubeBitAnd( pSupp, pSupp, pCube );
}

int Mvc_CoverSupportSizeBinary( Mvc_Cover_t * pCover )
{
    Mvc_Cube_t * pSupp;
    int Counter, i, v0, v1;
    // compute the support
    pSupp = Mvc_CubeAlloc( pCover );
    Mvc_CoverSupportAnd( pCover, pSupp );
    Counter = pCover->nBits/2;
    for ( i = 0; i < pCover->nBits/2; i++ )
    {
        v0 = Mvc_CubeBitValue( pSupp, 2*i   );
        v1 = Mvc_CubeBitValue( pSupp, 2*i+1 );
        if ( v0 && v1 )
            Counter--;
    }
    Mvc_CubeFree( pCover, pSupp );
    return Counter;
}

int Mvc_CoverSupportVarBelongs( Mvc_Cover_t * pCover, int iVar )
{
    Mvc_Cube_t * pSupp;
    int RetValue, v0, v1;
    // compute the support
    pSupp = Mvc_CubeAlloc( pCover );
    Mvc_CoverSupportAnd( pCover, pSupp );
    v0 = Mvc_CubeBitValue( pSupp, 2*iVar   );
    v1 = Mvc_CubeBitValue( pSupp, 2*iVar+1 );
    RetValue = (int)( !v0 || !v1 );
    Mvc_CubeFree( pCover, pSupp );
    return RetValue;
}

void Mvc_CoverCommonCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pComCube )
{
    Mvc_Cube_t * pCube;
    // clean the support
    Mvc_CubeBitFill( pComCube );
    // collect the support
    Mvc_CoverForEachCube( pCover, pCube )
        Mvc_CubeBitAnd( pComCube, pComCube, pCube );
}

int Mvc_CoverIsCubeFree( Mvc_Cover_t * pCover )
{
    int Result;
    // get the common cube
    Mvc_CoverAllocateMask( pCover );
    Mvc_CoverCommonCube( pCover, pCover->pMask );
    // check whether the common cube is empty
    Mvc_CubeBitEmpty( Result, pCover->pMask );
    return Result;
}

void Mvc_CoverMakeCubeFree( Mvc_Cover_t * pCover )
{
    Mvc_Cube_t * pCube;
    // get the common cube
    Mvc_CoverAllocateMask( pCover );
    Mvc_CoverCommonCube( pCover, pCover->pMask );
    // remove this cube from the cubes in the cover
    Mvc_CoverForEachCube( pCover, pCube )
        Mvc_CubeBitSharp( pCube, pCube, pCover->pMask );
}

Mvc_Cover_t * Mvc_CoverCommonCubeCover( Mvc_Cover_t * pCover )
{
    Mvc_Cover_t * pRes;
    Mvc_Cube_t * pCube;
    // create the new cover
    pRes = Mvc_CoverClone( pCover );
    // get the new cube
    pCube = Mvc_CubeAlloc( pRes );
    // get the common cube
    Mvc_CoverCommonCube( pCover, pCube );
    // add the cube to the cover
    Mvc_CoverAddCubeTail( pRes, pCube );
    return pRes;
}


int Mvc_CoverCheckSuppContainment( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
{
    int Result;
    assert( pCover1->nBits == pCover2->nBits );
    // set the supports
    Mvc_CoverAllocateMask( pCover1 );
    Mvc_CoverSupport( pCover1, pCover1->pMask );
    Mvc_CoverAllocateMask( pCover2 );
    Mvc_CoverSupport( pCover2, pCover2->pMask );
    // check the containment
    Mvc_CubeBitNotImpl( Result, pCover2->pMask, pCover1->pMask );
    return !Result;
}

int Mvc_CoverSetCubeSizes( Mvc_Cover_t * pCover )
{
    Mvc_Cube_t * pCube;
    unsigned char * pByte, * pByteStart, * pByteStop;
    int nBytes, nOnes;

    // get the number of unsigned chars in the cube's bit strings
    nBytes = pCover->nBits / (8 * sizeof(unsigned char)) + (int)(pCover->nBits % (8 * sizeof(unsigned char)) > 0);
    // iterate through the cubes
    Mvc_CoverForEachCube( pCover, pCube )
    {
        // clean the counter of ones
        nOnes = 0;
        // set the starting and stopping positions
        pByteStart = (unsigned char *)pCube->pData;
        pByteStop  = pByteStart + nBytes;
        // iterate through the positions
        for ( pByte = pByteStart; pByte < pByteStop; pByte++ )
            nOnes += bit_count[*pByte];
        // set the nOnes
        Mvc_CubeSetSize( pCube, nOnes );
    }
    return 1;
}

int Mvc_CoverGetCubeSize( Mvc_Cube_t * pCube )
{
    unsigned char * pByte, * pByteStart, * pByteStop;
    int nOnes, nBytes, nBits;
    // get the number of unsigned chars in the cube's bit strings
    nBits = (pCube->iLast + 1) * sizeof(Mvc_CubeWord_t) * 8 - pCube->nUnused;
    nBytes = nBits / (8 * sizeof(unsigned char)) + (int)(nBits % (8 * sizeof(unsigned char)) > 0);
    // clean the counter of ones
    nOnes = 0;
    // set the starting and stopping positions
    pByteStart = (unsigned char *)pCube->pData;
    pByteStop  = pByteStart + nBytes;
    // iterate through the positions
    for ( pByte = pByteStart; pByte < pByteStop; pByte++ )
        nOnes += bit_count[*pByte];
    return nOnes;
}

int Mvc_CoverCountCubePairDiffs( Mvc_Cover_t * pCover, unsigned char pDiffs[] )
{
    Mvc_Cube_t * pCube1;
    Mvc_Cube_t * pCube2;
    Mvc_Cube_t * pMask;
    unsigned char * pByte, * pByteStart, * pByteStop;
    int nBytes, nOnes;
    int nCubePairs;

    // allocate a temporary mask
    pMask = Mvc_CubeAlloc( pCover );
    // get the number of unsigned chars in the cube's bit strings
    nBytes = pCover->nBits / (8 * sizeof(unsigned char)) + (int)(pCover->nBits % (8 * sizeof(unsigned char)) > 0);
    // iterate through the cubes
    nCubePairs = 0;
    Mvc_CoverForEachCube( pCover, pCube1 )
    {
        Mvc_CoverForEachCubeStart( Mvc_CubeReadNext(pCube1), pCube2 )
        {
            // find the bit-wise exor of cubes
            Mvc_CubeBitExor( pMask, pCube1, pCube2 );
            // set the starting and stopping positions
            pByteStart = (unsigned char *)pMask->pData;
            pByteStop  = pByteStart + nBytes;
            // clean the counter of ones
            nOnes = 0;
            // iterate through the positions
            for ( pByte = pByteStart; pByte < pByteStop; pByte++ )
                nOnes += bit_count[*pByte];
            // set the nOnes
            pDiffs[nCubePairs++] = nOnes;
        }
    }
    // deallocate the mask
    Mvc_CubeFree( pCover, pMask );
    return 1;
}


Mvc_Cover_t * Mvc_CoverRemap( Mvc_Cover_t * p, int * pVarsRem, int nVarsRem )
{
    Mvc_Cover_t * pCover;
    Mvc_Cube_t * pCube, * pCubeCopy;
    int i;
    // clone the cover
    pCover = Mvc_CoverAlloc( p->pMem, nVarsRem );
    // copy the cube list
    Mvc_CoverForEachCube( p, pCube )
    {
        pCubeCopy = Mvc_CubeAlloc( pCover );
        //Mvc_CubeBitClean( pCubeCopy );   //changed by wjiang
        Mvc_CubeBitFill( pCubeCopy );      //changed by wjiang
        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
    }
    // copy the corresponding columns
    for ( i = 0; i < nVarsRem; i++ )
    {
        if (pVarsRem[i] < 0) 
            continue;     //added by wjiang
        assert( pVarsRem[i] >= 0 && pVarsRem[i] < p->nBits );
        Mvc_CoverCopyColumn( p, pCover, pVarsRem[i], i );
    }
    return pCover;
}

void Mvc_CoverCopyColumn( Mvc_Cover_t * pCoverOld, Mvc_Cover_t * pCoverNew, 
                         int iColOld, int iColNew )
{
    Mvc_Cube_t * pCubeOld, * pCubeNew;
    int iWordOld, iWordNew, iBitOld, iBitNew;

    assert( Mvc_CoverReadCubeNum(pCoverOld) == Mvc_CoverReadCubeNum(pCoverNew) );

    // get the place of the old and new columns
    iWordOld = Mvc_CubeWhichWord(iColOld);
    iBitOld  = Mvc_CubeWhichBit(iColOld);
    iWordNew = Mvc_CubeWhichWord(iColNew);
    iBitNew  = Mvc_CubeWhichBit(iColNew);

    // go through the cubes of both covers
    pCubeNew = Mvc_CoverReadCubeHead(pCoverNew);
    Mvc_CoverForEachCube( pCoverOld, pCubeOld )
    {
        if ( pCubeOld->pData[iWordOld] & (1<<iBitOld) )
            pCubeNew->pData[iWordNew] |= (1<<iBitNew);
        else
            pCubeNew->pData[iWordNew] &= ~(1<<iBitNew);  // added by wjiang
        pCubeNew = Mvc_CubeReadNext( pCubeNew );
    }
}

void Mvc_CoverInverse( Mvc_Cover_t * pCover )
{
    Mvc_Cube_t * pCube;
    // complement the cubes
    Mvc_CoverForEachCube( pCover, pCube )
        Mvc_CubeBitNot( pCube );
}

Mvc_Cover_t * Mvc_CoverRemoveDontCareLits( Mvc_Cover_t * pCover )
{
    Mvc_Cover_t * pCoverNew;
    Mvc_Cube_t * pCube;

    pCoverNew = Mvc_CoverDup( pCover );
    Mvc_CoverForEachCube( pCoverNew, pCube )
        Mvc_CubeBitRemoveDcs( pCube );
    return pCoverNew;
}

Mvc_Cover_t * Mvc_CoverCofactor( Mvc_Cover_t * p, int iValue, int iValueOther )
{
    Mvc_Cover_t * pCover;
    Mvc_Cube_t * pCube, * pCubeCopy;
    // clone the cover
    pCover = Mvc_CoverClone( p );
    // copy the cube list
    Mvc_CoverForEachCube( p, pCube )
        if ( Mvc_CubeBitValue( pCube, iValue ) )
        {
            pCubeCopy = Mvc_CubeDup( pCover, pCube );
            Mvc_CoverAddCubeTail( pCover, pCubeCopy );
            Mvc_CubeBitInsert( pCubeCopy, iValueOther );
        }
    return pCover;
}

Mvc_Cover_t * Mvc_CoverFlipVar( Mvc_Cover_t * p, int iValue0, int iValue1 )
{
    Mvc_Cover_t * pCover;
    Mvc_Cube_t * pCube, * pCubeCopy;
    int Value0, Value1, Temp;

    assert( iValue0 + 1 == iValue1 ); // should be adjacent

    // clone the cover
    pCover = Mvc_CoverClone( p );
    // copy the cube list
    Mvc_CoverForEachCube( p, pCube )
    {
        pCubeCopy = Mvc_CubeDup( pCover, pCube );
        Mvc_CoverAddCubeTail( pCover, pCubeCopy );

        // get the bits
        Value0 = Mvc_CubeBitValue( pCubeCopy, iValue0 );
        Value1 = Mvc_CubeBitValue( pCubeCopy, iValue1 );

        // if both bits are one, nothing to swap
        if ( Value0 && Value1 )
            continue;
        // cannot be both zero because they belong to the same var
        assert( Value0 || Value1 ); 

        // swap the bits
        Temp   = Value0;
        Value0 = Value1;
        Value1 = Temp;

        // set the bits after the swap
        if ( Value0 )
            Mvc_CubeBitInsert( pCubeCopy, iValue0 );
        else
            Mvc_CubeBitRemove( pCubeCopy, iValue0 );

        if ( Value1 )
            Mvc_CubeBitInsert( pCubeCopy, iValue1 );
        else
            Mvc_CubeBitRemove( pCubeCopy, iValue1 );
    }
    return pCover;
}

Mvc_Cover_t * Mvc_CoverUnivQuantify( Mvc_Cover_t * p, 
    int iValueA0, int iValueA1, int iValueB0, int iValueB1 )
{
    Mvc_Cover_t * pCover;
    Mvc_Cube_t * pCube, * pCubeCopy;
    int ValueA0, ValueA1, ValueB0, ValueB1;

    // clone the cover
    pCover = Mvc_CoverClone( p );
    // copy the cube list
    Mvc_CoverForEachCube( p, pCube )
    {
        // get the bits
        ValueA0 = Mvc_CubeBitValue( pCube, iValueA0 );
        ValueA1 = Mvc_CubeBitValue( pCube, iValueA1 );
        ValueB0 = Mvc_CubeBitValue( pCube, iValueB0 );
        ValueB1 = Mvc_CubeBitValue( pCube, iValueB1 );

        // cannot be both zero because they belong to the same var
        assert( ValueA0 || ValueA1 ); 
        assert( ValueB0 || ValueB1 ); 

        // if the values of this var are different, do not add the cube
        if ( ValueA0 != ValueB0 && ValueA1 != ValueB1 )
            continue;

        // create the cube
        pCubeCopy = Mvc_CubeDup( pCover, pCube );
        Mvc_CoverAddCubeTail( pCover, pCubeCopy );

        // insert 1's into for the first var, if both have this value
        if ( ValueA0 && ValueB0 )
            Mvc_CubeBitInsert( pCubeCopy, iValueA0 );
        else
            Mvc_CubeBitRemove( pCubeCopy, iValueA0 );

        if ( ValueA1 && ValueB1 )
            Mvc_CubeBitInsert( pCubeCopy, iValueA1 );
        else
            Mvc_CubeBitRemove( pCubeCopy, iValueA1 );
            
        // insert 1's into for the second var (the cover does not depend on it)
        Mvc_CubeBitInsert( pCubeCopy, iValueB0 );
        Mvc_CubeBitInsert( pCubeCopy, iValueB1 );
    }
    return pCover;
}

#if 0

Mvc_Cover_t ** Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar )
{
    Mvc_Cover_t ** ppCofs;
    Mvc_Cube_t * pCube, * pCubeNew;
    int i, nValues, iValueFirst, Res;

    // start the covers for cofactors
    iValueFirst = Vm_VarMapReadValuesFirst(pData->pVm, iVar);
    nValues = Vm_VarMapReadValues(pData->pVm, iVar);
    ppCofs = ALLOC( Mvc_Cover_t *, nValues + 1 );
    for ( i = 0; i <= nValues; i++ )
        ppCofs[i] = Mvc_CoverClone( pCover );

    // go through the cubes
    Mvc_CoverForEachCube( pCover, pCube )
    {
        // if the literal if a full literal, add it to last "cofactor"
        Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] );
        if ( Res )
        {
            pCubeNew = Mvc_CubeDup(pCover, pCube);
            Mvc_CoverAddCubeTail( ppCofs[nValues], pCubeNew );
            continue;
        }

        // otherwise, add it to separate values
        for ( i = 0; i < nValues; i++ )
            if ( Mvc_CubeBitValue( pCube, iValueFirst + i ) )
            {
                pCubeNew = Mvc_CubeDup(pCover, pCube);
                Mvc_CubeBitOr( pCubeNew, pCubeNew, pData->ppMasks[iVar] );
                Mvc_CoverAddCubeTail( ppCofs[i], pCubeNew );
            }
    }
    return ppCofs;
}

int Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue )
{
    Mvc_Cube_t * pCube;
    int iValueFirst, Res, Counter;

    Counter = 0;
    iValueFirst = Vm_VarMapReadValuesFirst( pData->pVm, iVar );
    Mvc_CoverForEachCube( pCover, pCube )
    {
        // check if the given literal is the full literal
        Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] );
        if ( Res )
            continue;
        // this literal is not a full literal; check if it has this value
        Counter += Mvc_CubeBitValue( pCube, iValueFirst + iValue );
    }
    return Counter;
}

Mvc_Cover_t * Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew )
{
    Mvc_Cover_t * pCoverNew;
    Mvc_Cube_t * pCube, * pCubeNew;
    int i, iLast, iLastNew;

    // create the new cover
    pCoverNew = Mvc_CoverAlloc( pCover->pMem, Vm_VarMapReadValuesInNum(pVmNew) );

    // get the cube composed of extra bits
    Mvc_CoverAllocateMask( pCoverNew );
    Mvc_CubeBitClean( pCoverNew->pMask );
    for ( i = pCover->nBits; i < pCoverNew->nBits; i++ )
        Mvc_CubeBitInsert( pCoverNew->pMask, i );

    // get the indexes of the last words in both covers
    iLast    = pCover->nWords?    pCover->nWords - 1: 0;
    iLastNew = pCoverNew->nWords? pCoverNew->nWords - 1: 0;

    // create the cubes of the new cover
    Mvc_CoverForEachCube( pCover, pCube )
    {
        pCubeNew = Mvc_CubeAlloc( pCoverNew );
        Mvc_CubeBitClean( pCubeNew );
        // copy the bits (cannot immediately use Mvc_CubeBitCopy, 
        // because covers have different numbers of bits)
        Mvc_CubeSetLast( pCubeNew, iLast );
        Mvc_CubeBitCopy( pCubeNew, pCube );
        Mvc_CubeSetLast( pCubeNew, iLastNew );
        // add the extra bits
        Mvc_CubeBitOr( pCubeNew, pCubeNew, pCoverNew->pMask );
        // add the cube to the new cover
        Mvc_CoverAddCubeTail( pCoverNew, pCubeNew );
    }
    return pCoverNew;
}

#endif

Mvc_Cover_t * Mvc_CoverTranspose( Mvc_Cover_t * pCover )
{
    Mvc_Cover_t * pRes;
    Mvc_Cube_t * pCubeRes, * pCube;
    int nWord, nBit, i, iCube;

    pRes = Mvc_CoverAlloc( pCover->pMem, Mvc_CoverReadCubeNum(pCover) );
    for ( i = 0; i < pCover->nBits; i++ )
    {
        // get the word and bit of this literal
        nWord = Mvc_CubeWhichWord(i);
        nBit  = Mvc_CubeWhichBit(i);
        // get the transposed cube
        pCubeRes = Mvc_CubeAlloc( pRes );
        Mvc_CubeBitClean( pCubeRes );
        iCube = 0;
        Mvc_CoverForEachCube( pCover, pCube )
        {
            if ( pCube->pData[nWord] & (1<<nBit) )
                Mvc_CubeBitInsert( pCubeRes, iCube );
            iCube++;
        }
        Mvc_CoverAddCubeTail( pRes, pCubeRes ); 
    }
    return pRes;
}

int Mvc_UtilsCheckUnusedZeros( Mvc_Cover_t * pCover )
{
    unsigned Unsigned;
    Mvc_Cube_t * pCube;
    int nCubes;

    nCubes = 0;
    Mvc_CoverForEachCube( pCover, pCube )
    {
        if ( pCube->nUnused == 0 )
            continue;

        Unsigned = ( pCube->pData[pCube->iLast] & 
                    (BITS_FULL << (32-pCube->nUnused)) );
        if( Unsigned )
        {
            printf( "Cube %2d out of %2d contains dirty bits.\n", nCubes, 
                Mvc_CoverReadCubeNum(pCover) );
        }
        nCubes++;
    }
    return 1;
}

---