extraBddUnate.c File Reference

#include "extraBdd.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Extra_UnateInfo_t *	Extra_UnateComputeFast (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_zddUnateInfoCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode *	Extra_zddGetSingletonsBoth (DdManager *dd, DdNode *bVars)
Extra_UnateInfo_t *	Extra_UnateInfoAllocate (int nVars)
void	Extra_UnateInfoDissolve (Extra_UnateInfo_t *p)
void	Extra_UnateInfoPrint (Extra_UnateInfo_t *p)
Extra_UnateInfo_t *	Extra_UnateInfoCreateFromZdd (DdManager *dd, DdNode *zPairs, DdNode *bSupp)
Extra_UnateInfo_t *	Extra_UnateComputeSlow (DdManager *dd, DdNode *bFunc)
int	Extra_bddCheckUnateNaive (DdManager *dd, DdNode *bF, int iVar)
DdNode *	extraZddUnateInfoCompute (DdManager *dd, DdNode *bFunc, DdNode *bVars)
DdNode *	extraZddGetSingletonsBoth (DdManager *dd, DdNode *bVars)

Function Documentation

int Extra_bddCheckUnateNaive	(	DdManager *	dd,
		DdNode *	bF,
		int	iVar
	)

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

Synopsis [Checks if the two variables are symmetric.]

Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.]

SideEffects []

SeeAlso []

Definition at line 338 of file extraBddUnate.c.

{
    DdNode * bCof0, * bCof1;
    int Res;

    assert( iVar < dd->size );

    bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) );  Cudd_Ref( bCof0 );
    bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) );            Cudd_Ref( bCof1 );

    if ( Cudd_bddLeq( dd, bCof0, bCof1 ) )
        Res = 1;
    else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) )
        Res =-1;
    else
        Res = 0;

    Cudd_RecursiveDeref( dd, bCof0 );
    Cudd_RecursiveDeref( dd, bCof1 );
    return Res;
} /* end of Extra_bddCheckUnateNaive */

ABC_NAMESPACE_IMPL_START Extra_UnateInfo_t* Extra_UnateComputeFast	(	DdManager *	dd,
		DdNode *	bFunc
	)

CFile****************************************************************

FileName [extraBddUnate.c]

PackageName [extra]

Synopsis [Efficient methods to compute the information about unate variables using an algorithm that is conceptually similar to the algorithm for two-variable symmetry computation presented in: A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. Transactions on CAD, Nov. 2003.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id:

extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes the classical symmetry information for the function.]

Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.]

SideEffects [If the ZDD variables are not derived from BDD variables with multiplicity 2, this function may derive them in a wrong way.]

SeeAlso []

Definition at line 73 of file extraBddUnate.c.

{
    DdNode * bSupp;
    DdNode * zRes;
    Extra_UnateInfo_t * p;

    bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
    zRes  = Extra_zddUnateInfoCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );

    p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp );

    Cudd_RecursiveDeref( dd, bSupp );
    Cudd_RecursiveDerefZdd( dd, zRes );

    return p;

} /* end of Extra_UnateInfoCompute */

Extra_UnateInfo_t* Extra_UnateComputeSlow	(	DdManager *	dd,
		DdNode *	bFunc
	)

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

Synopsis [Computes the classical unateness information for the function.]

Description [Uses the naive way of comparing cofactors.]

SideEffects []

SeeAlso []

Definition at line 293 of file extraBddUnate.c.

{
    int nSuppSize;
    DdNode * bSupp, * bTemp;
    Extra_UnateInfo_t * p;
    int i, Res;

    // compute the support
    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
    nSuppSize = Extra_bddSuppSize( dd, bSupp );
//printf( "Support = %d. ", nSuppSize );
//Extra_bddPrint( dd, bSupp );
//printf( "%d ", nSuppSize );

    // allocate the storage for symmetry info
    p = Extra_UnateInfoAllocate( nSuppSize );

    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index );
        p->pVars[i].iVar = bTemp->index;
        if ( Res == -1 )
            p->pVars[i].Neg = 1;
        else if ( Res == 1 )
            p->pVars[i].Pos = 1;
        p->nUnate += (Res != 0);
    }
    Cudd_RecursiveDeref( dd, bSupp );
    return p;

} /* end of Extra_UnateComputeSlow */

Extra_UnateInfo_t* Extra_UnateInfoAllocate

(

int

nVars

)

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

Synopsis [Allocates unateness information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file extraBddUnate.c.

{
    Extra_UnateInfo_t * p;
    // allocate and clean the storage for unateness info
    p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
    memset( p, 0, sizeof(Extra_UnateInfo_t) );
    p->nVars     = nVars;
    p->pVars     = ABC_ALLOC( Extra_UnateVar_t, nVars );  
    memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
    return p;
} /* end of Extra_UnateInfoAllocate */

Extra_UnateInfo_t* Extra_UnateInfoCreateFromZdd	(	DdManager *	dd,
		DdNode *	zPairs,
		DdNode *	bSupp
	)

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

Synopsis [Creates the symmetry information structure from ZDD.]

Description [ZDD representation of symmetries is the set of cubes, each of which has two variables in the positive polarity. These variables correspond to the symmetric variable pair.]

SideEffects []

SeeAlso []

Definition at line 227 of file extraBddUnate.c.

{
    Extra_UnateInfo_t * p;
    DdNode * bTemp, * zSet, * zCube, * zTemp;
    int * pMapVars2Nums;
    int i, nSuppSize;

    nSuppSize = Extra_bddSuppSize( dd, bSupp );

    // allocate and clean the storage for symmetry info
    p = Extra_UnateInfoAllocate( nSuppSize );

    // allocate the storage for the temporary map
    pMapVars2Nums = ABC_ALLOC( int, dd->size );
    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );

    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        p->pVars[i].iVar = bTemp->index;
        pMapVars2Nums[bTemp->index] = i;
    }

    // write the symmetry info into the structure
    zSet = zPairs;   Cudd_Ref( zSet );
//    Cudd_zddPrintCover( dd, zPairs );    printf( "\n" );
    while ( zSet != z0 )
    {
        // get the next cube
        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );

        // add this var to the data structure
        assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 );
        if ( zCube->index & 1 ) // neg
            p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1;
        else
            p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1;
        // count the unate vars
        p->nUnate++;

        // update the cuver and deref the cube
        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zCube );

    } // for each cube 
    Cudd_RecursiveDerefZdd( dd, zSet );
    ABC_FREE( pMapVars2Nums );
    return p;

} /* end of Extra_UnateInfoCreateFromZdd */

void Extra_UnateInfoDissolve

(

Extra_UnateInfo_t *

p

)

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

Synopsis [Deallocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file extraBddUnate.c.

{
    ABC_FREE( p->pVars );
    ABC_FREE( p );
} /* end of Extra_UnateInfoDissolve */

void Extra_UnateInfoPrint

(

Extra_UnateInfo_t *

p

)

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

Synopsis [Allocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file extraBddUnate.c.

{
    char * pBuffer;
    int i;
    pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
    memset( pBuffer, ' ', p->nVarsMax );
    pBuffer[p->nVarsMax] = 0;
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pVars[i].Neg )
            pBuffer[ p->pVars[i].iVar ] = 'n';
        else if ( p->pVars[i].Pos )
            pBuffer[ p->pVars[i].iVar ] = 'p';
        else
            pBuffer[ p->pVars[i].iVar ] = '.';
    printf( "%s\n", pBuffer );
    ABC_FREE( pBuffer );
} /* end of Extra_UnateInfoPrint */

DdNode* Extra_zddGetSingletonsBoth	(	DdManager *	dd,
		DdNode *	bVars
	)

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

Synopsis [Converts a set of variables into a set of singleton subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file extraBddUnate.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddGetSingletonsBoth( dd, bVars );
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddGetSingletonsBoth */

DdNode* Extra_zddUnateInfoCompute	(	DdManager *	dd,
		DdNode *	bF,
		DdNode *	bVars
	)

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

Synopsis [Computes the classical symmetry information as a ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file extraBddUnate.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddUnateInfoCompute( dd, bF, bVars );
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddUnateInfoCompute */

DdNode* extraZddGetSingletonsBoth	(	DdManager *	dd,
		DdNode *	bVars
	)

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

Synopsis [Performs a recursive step of Extra_zddGetSingletons.]

Description [Returns the set of ZDD singletons, containing those pos/neg polarity ZDD variables that correspond to the BDD variables in bVars.]

SideEffects []

SeeAlso []

Definition at line 570 of file extraBddUnate.c.

{
    DdNode * zRes;

    if ( bVars == b1 )
        return z1;

    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) )
        return zRes;
    else
    {
        DdNode * zTemp, * zPlus;          

        // solve subproblem
        zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) );
        if ( zRes == NULL ) 
            return NULL;
        cuddRef( zRes );

        
        // create the negative singleton
        zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );

        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
        

        // create the positive singleton
        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );

        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );

        cuddDeref( zRes );
        cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSingletonsBoth */

DdNode* extraZddUnateInfoCompute	(	DdManager *	dd,
		DdNode *	bFunc,
		DdNode *	bVars
	)

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

Synopsis [Performs a recursive step of Extra_UnateInfoCompute.]

Description [Returns the set of symmetric variable pairs represented as a set of two-literal ZDD cubes. Both variables always appear in the positive polarity in the cubes. This function works without building new BDD nodes. Some relatively small number of ZDD nodes may be built to ensure proper bookkeeping of the symmetry information.]

SideEffects []

SeeAlso []

Definition at line 385 of file extraBddUnate.c.

{
    DdNode * zRes;
    DdNode * bFR = Cudd_Regular(bFunc); 

    if ( cuddIsConstant(bFR) )
    {
        if ( cuddIsConstant(bVars) )
            return z0;
        return extraZddGetSingletonsBoth( dd, bVars );
    }
    assert( bVars != b1 );

    if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) )
        return zRes;
    else
    {
        DdNode * zRes0, * zRes1;
        DdNode * zTemp, * zPlus;             
        DdNode * bF0, * bF1;             
        DdNode * bVarsNew;
        int nVarsExtra;
        int LevelF;
        int AddVar;

        // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
        // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
        // count how many extra vars are there in bVars
        nVarsExtra = 0;
        LevelF = dd->perm[bFR->index];
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
            nVarsExtra++; 
        // the indexes (level) of variables should be synchronized now
        assert( bFR->index == bVarsNew->index );

        // cofactor the function
        if ( bFR != bFunc ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }

        // solve subproblems
        zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) );
        if ( zRes0 == NULL )
            return NULL;
        cuddRef( zRes0 );

        // if there is no symmetries in the negative cofactor
        // there is no need to test the positive cofactor
        if ( zRes0 == z0 )
            zRes = zRes0;  // zRes takes reference
        else
        {
            zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );

            // only those variables are pair-wise symmetric 
            // that are pair-wise symmetric in both cofactors
            // therefore, intersect the solutions
            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
        }

        // consider the current top-most variable
        AddVar = -1;
        if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos
            AddVar = 0;
        else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg
            AddVar = 1;
        if ( AddVar >= 0 )
        {
            // create the singleton
            zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );

            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        // only zRes is referenced at this point

        // if we skipped some variables, these variables cannot be symmetric with
        // any variables that are currently in the support of bF, but they can be 
        // symmetric with the variables that are in bVars but not in the support of bF
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
        {
            // create the negative singleton
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );

            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        

            // create the positive singleton
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );

            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        cuddDeref( zRes );

        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes);
        return zRes;
    }
} /* end of extraZddUnateInfoCompute */