Version abc50904

1 files changed, 868 insertions, 0 deletions

diff --git a/src/misc/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c
new file mode 100644
index 00000000..3fb57276
--- /dev/null
+++ b/src/misc/mvc/mvcUtils.c
@@ -0,0 +1,868 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 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 = 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                                ///
+////////////////////////////////////////////////////////////////////////
+
+