summaryrefslogtreecommitdiffstats
path: root/src/misc/mvc/mvcUtils.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/mvc/mvcUtils.c')
-rw-r--r--src/misc/mvc/mvcUtils.c868
1 files changed, 0 insertions, 868 deletions
diff --git a/src/misc/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c
deleted file mode 100644
index 4b13b23d..00000000
--- a/src/misc/mvc/mvcUtils.c
+++ /dev/null
@@ -1,868 +0,0 @@
-/**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 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 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 ///
-////////////////////////////////////////////////////////////////////////
-
-