mvcUtils.c

Go to the documentation of this file.

/**CFile****************************************************************

  FileName    [mvcUtils.c]

  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

  Synopsis    [Various cover handling utilities.]

  Author      [MVSIS Group]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: mvcUtils.c,v 1.7 2003/04/26 20:41:36 alanmi Exp $]

***********************************************************************/

#include "mvc.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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 );


////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}


/**Function*************************************************************

  Synopsis    [Returns 1 if the support of cover2 is contained in the support of cover1.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Counts the cube sizes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Counts the cube sizes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Counts the differences in each cube pair in the cover.]

  Description [Takes the cover (pCover) and the array where the
  diff counters go (pDiffs). The array pDiffs should have as many
  entries as there are different pairs of cubes in the cover: n(n-1)/2.
  Fills out the array pDiffs with the following info: For each cube
  pair, included in the array is the number of literals in both cubes
  after they are made cube ABC_FREE.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}


/**Function*************************************************************

  Synopsis    [Creates a new cover containing some literals of the old cover.]

  Description [Creates the new cover containing the given number (nVarsRem)
  literals of the old cover. All the bits of the new cover are initialized
  to "1". The selected bits from the old cover are copied on top. The numbers
  of the selected bits to copy are given in the array pVarsRem. The i-set
  entry in this array is the index of the bit in the old cover which goes
  to the i-th place in the new cover. If the i-th entry in pVarsRem is -1, 
  it means that the i-th bit does not change (remains composed of all 1's).
  This is a useful feature to speed up remapping covers, which are known
  to depend only on a subset of input variables.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Copies a column from the old cover to the new cover.]

  Description [Copies the column (iColOld) of the old cover (pCoverOld)
  into the column (iColNew) of the new cover (pCoverNew). Assumes that 
  the number of cubes is the same in both covers. Makes no assuptions 
  about the current contents of the column in the new cover.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 );
    }
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    [This function dups the cover and removes DC literals from cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Returns the cofactor w.r.t. to a binary var.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Returns the cover, in which the binary var is complemented.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Returns the cover derived by universal quantification.]

  Description [Returns the cover computed by universal quantification
  as follows: CoverNew = Univ(B) [Cover & (A==B)]. Removes the second 
  binary var from the support (given by values iValueB0 and iValueB1). 
  Leaves the first binary variable (given by values iValueA0 and iValueA1) 
  in the support.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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

/**Function*************************************************************

  Synopsis    [Derives the cofactors of the cover.]

  Description [Derives the cofactors w.r.t. a variable and also cubes
  that do not depend on this variable.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 = ABC_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;
}

/**Function*************************************************************

  Synopsis    [Count the cubes with non-trivial literals with the given value.]

  Description [The data and the cover are given (pData, pCover). Also given 
  are the variable number and the number of a value of this variable.
  This procedure returns the number of cubes having a non-trivial literal
  of this variable that have the given value present.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Creates the expanded cover.]

  Description [The original cover is expanded by adding some variables.
  These variables are the additional variables in pVmNew, compared to
  pCvr->pVm. The resulting cover is the same as the original one, except
  that it contains the additional variables present as full literals
  in every cube.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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

/**Function*************************************************************

  Synopsis    [Transposes the cube cover.]

  Description [Returns the cube cover that looks like a transposed
  matrix, compared to the matrix derived from the original cover.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}

/**Function*************************************************************

  Synopsis    [Checks that the cubes of the cover have 0's in unused bits.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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;
}


////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END