mvcUtils.c File Reference

#include "mvc.h"

Include dependency graph for mvcUtils.c:

Go to the source code of this file.

Functions
void	Mvc_CoverSupport (Mvc_Cover_t *pCover, Mvc_Cube_t *pSupp)
	FUNCTION DEFINITIONS ///.
void	Mvc_CoverSupportAnd (Mvc_Cover_t *pCover, Mvc_Cube_t *pSupp)
int	Mvc_CoverSupportSizeBinary (Mvc_Cover_t *pCover)
int	Mvc_CoverSupportVarBelongs (Mvc_Cover_t *pCover, int iVar)
void	Mvc_CoverCommonCube (Mvc_Cover_t *pCover, Mvc_Cube_t *pComCube)
int	Mvc_CoverIsCubeFree (Mvc_Cover_t *pCover)
void	Mvc_CoverMakeCubeFree (Mvc_Cover_t *pCover)
Mvc_Cover_t *	Mvc_CoverCommonCubeCover (Mvc_Cover_t *pCover)
int	Mvc_CoverCheckSuppContainment (Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
int	Mvc_CoverSetCubeSizes (Mvc_Cover_t *pCover)
int	Mvc_CoverCountCubePairDiffs (Mvc_Cover_t *pCover, unsigned char pDiffs[])
Mvc_Cover_t *	Mvc_CoverRemap (Mvc_Cover_t *p, int *pVarsRem, int nVarsRem)
void	Mvc_CoverInverse (Mvc_Cover_t *pCover)
Mvc_Cover_t *	Mvc_CoverRemoveDontCareLits (Mvc_Cover_t *pCover)
Mvc_Cover_t *	Mvc_CoverCofactor (Mvc_Cover_t *p, int iValue, int iValueOther)
Mvc_Cover_t *	Mvc_CoverFlipVar (Mvc_Cover_t *p, int iValue0, int iValue1)
Mvc_Cover_t *	Mvc_CoverUnivQuantify (Mvc_Cover_t *p, int iValueA0, int iValueA1, int iValueB0, int iValueB1)
Mvc_Cover_t *	Mvc_CoverTranspose (Mvc_Cover_t *pCover)
int	Mvc_UtilsCheckUnusedZeros (Mvc_Cover_t *pCover)

Function Documentation

Mvc_CoverCheckSuppContainment()

int Mvc_CoverCheckSuppContainment	(	Mvc_Cover_t *	pCover1,
		Mvc_Cover_t *	pCover2 )

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Mvc_CoverCofactor()

Mvc_Cover_t * Mvc_CoverCofactor	(	Mvc_Cover_t *	p,
		int	iValue,
		int	iValueOther )

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 522 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverCommonCube()

void Mvc_CoverCommonCube	(	Mvc_Cover_t *	pCover,
		Mvc_Cube_t *	pComCube )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file mvcUtils.c.

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

Here is the caller graph for this function:

Mvc_CoverCommonCubeCover()

Mvc_Cover_t * Mvc_CoverCommonCubeCover

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverCountCubePairDiffs()

int Mvc_CoverCountCubePairDiffs	(	Mvc_Cover_t *	pCover,
		unsigned char	pDiffs[] )

Function*************************************************************

Synopsis [Counts the cube sizes.]

Description [This procedure works incorrectly on big-endian machines.]

SideEffects []

SeeAlso [] 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 []

Definition at line 345 of file mvcUtils.c.

{
    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);
    nBytes = sizeof(Mvc_CubeWord_t) * pCover->nWords; // big-endian issue
    // 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;
}

Here is the call graph for this function:

Mvc_CoverFlipVar()

Mvc_Cover_t * Mvc_CoverFlipVar	(	Mvc_Cover_t *	p,
		int	iValue0,
		int	iValue1 )

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 550 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverInverse()

void Mvc_CoverInverse

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file mvcUtils.c.

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

Here is the caller graph for this function:

Mvc_CoverIsCubeFree()

int Mvc_CoverIsCubeFree

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverMakeCubeFree()

void Mvc_CoverMakeCubeFree

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file mvcUtils.c.

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

Here is the call graph for this function:

Mvc_CoverRemap()

Mvc_Cover_t * Mvc_CoverRemap	(	Mvc_Cover_t *	p,
		int *	pVarsRem,
		int	nVarsRem )

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 []

Definition at line 404 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverRemoveDontCareLits()

Mvc_Cover_t * Mvc_CoverRemoveDontCareLits

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file mvcUtils.c.

{
    Mvc_Cover_t * pCoverNew;
    Mvc_Cube_t * pCube;
 
    pCoverNew = Mvc_CoverDup( pCover );
    Mvc_CoverForEachCube( pCoverNew, pCube )
        Mvc_CubeBitRemoveDcs( pCube );
    return pCoverNew;
}

Here is the call graph for this function:

Mvc_CoverSetCubeSizes()

int Mvc_CoverSetCubeSizes

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

Synopsis [Counts the cube sizes.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file mvcUtils.c.

{
    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);
    nBytes = sizeof(Mvc_CubeWord_t) * pCover->nWords; // big-endian issue
    // 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;
}

Here is the caller graph for this function:

Mvc_CoverSupport()

void Mvc_CoverSupport	(	Mvc_Cover_t *	pCover,
		Mvc_Cube_t *	pSupp )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file mvcUtils.c.

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

Here is the caller graph for this function:

Mvc_CoverSupportAnd()

void Mvc_CoverSupportAnd	(	Mvc_Cover_t *	pCover,
		Mvc_Cube_t *	pSupp )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file mvcUtils.c.

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

Here is the caller graph for this function:

Mvc_CoverSupportSizeBinary()

int Mvc_CoverSupportSizeBinary

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverSupportVarBelongs()

int Mvc_CoverSupportVarBelongs	(	Mvc_Cover_t *	pCover,
		int	iVar )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverTranspose()

Mvc_Cover_t * Mvc_CoverTranspose

(

Mvc_Cover_t *

pCover

)

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 []

Definition at line 808 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_CoverUnivQuantify()

Mvc_Cover_t * Mvc_CoverUnivQuantify	(	Mvc_Cover_t *	p,
		int	iValueA0,
		int	iValueA1,
		int	iValueB0,
		int	iValueB1 )

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 []

Definition at line 610 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function:

Mvc_UtilsCheckUnusedZeros()

int Mvc_UtilsCheckUnusedZeros

(

Mvc_Cover_t *

pCover

)

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 846 of file mvcUtils.c.

{
    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;
}

Here is the call graph for this function: