cloud.c File Reference

#include <string.h>
#include "cloud.h"

Include dependency graph for cloud.c:

Go to the source code of this file.

Functions
CloudManager *	Cloud_Init (int nVars, int nBits)
	FUNCTION DEFINITIONS ///.
void	Cloud_Quit (CloudManager *dd)
void	Cloud_Restart (CloudManager *dd)
void	Cloud_CacheAllocate (CloudManager *dd, CloudOper oper, int logratio)
CloudNode *	Cloud_MakeNode (CloudManager *dd, CloudVar v, CloudNode *t, CloudNode *e)
CloudNode *	cloudBddAnd (CloudManager *dd, CloudNode *f, CloudNode *g)
CloudNode *	Cloud_bddAnd (CloudManager *dd, CloudNode *f, CloudNode *g)
CloudNode *	Cloud_bddOr (CloudManager *dd, CloudNode *f, CloudNode *g)
CloudNode *	Cloud_bddXor (CloudManager *dd, CloudNode *f, CloudNode *g)
CloudNode *	Cloud_Support (CloudManager *dd, CloudNode *n)
int	Cloud_SupportSize (CloudManager *dd, CloudNode *n)
int	Cloud_DagSize (CloudManager *dd, CloudNode *n)
int	Cloud_DagCollect (CloudManager *dd, CloudNode *n)
int	Cloud_SharingSize (CloudManager *dd, CloudNode **pn, int nn)
CloudNode *	Cloud_GetOneCube (CloudManager *dd, CloudNode *bFunc)
void	Cloud_bddPrint (CloudManager *dd, CloudNode *Func)
void	Cloud_bddPrintCube (CloudManager *dd, CloudNode *bCube)
void	Cloud_PrintInfo (CloudManager *dd)
void	Cloud_PrintHashTable (CloudManager *dd)

Function Documentation

Cloud_bddAnd()

CloudNode * Cloud_bddAnd	(	CloudManager *	dd,
		CloudNode *	f,
		CloudNode *	g )

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

Synopsis [Performs the AND or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 489 of file cloud.c.

{
    if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
        return NULL;
    CLOUD_ASSERT(f);
    CLOUD_ASSERT(g);
    if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
        cloudCacheAllocate( dd, CLOUD_OPER_AND );
    return cloudBddAnd_gate( dd, f, g );
}

Here is the caller graph for this function:

Cloud_bddOr()

CloudNode * Cloud_bddOr	(	CloudManager *	dd,
		CloudNode *	f,
		CloudNode *	g )

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

Synopsis [Performs the OR or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file cloud.c.

{
    CloudNode * res;
    if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
        return NULL;
    CLOUD_ASSERT(f);
    CLOUD_ASSERT(g);
    if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
        cloudCacheAllocate( dd, CLOUD_OPER_AND );
    res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) );
    res = Cloud_NotCond( res, res != NULL );
    return res;
}

Here is the caller graph for this function:

Cloud_bddPrint()

void Cloud_bddPrint	(	CloudManager *	dd,
		CloudNode *	Func )

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

Synopsis [Prints the BDD as a set of disjoint cubes to the standard output.]

Description []

SideEffects []

Definition at line 866 of file cloud.c.

{
    CloudNode * Cube;
    int fFirst = 1;
 
    if ( Func == dd->zero )
        printf( "Constant 0." );
    else if ( Func == dd->one )
        printf( "Constant 1." );
    else
    {
        while ( 1 )
        {
            Cube = Cloud_GetOneCube( dd, Func );
            if ( Cube == NULL || Cube == dd->zero )
                break;
            if ( fFirst )       fFirst = 0;
            else                printf( " + " );
            Cloud_bddPrintCube( dd, Cube );
            Func = Cloud_bddAnd( dd, Func, Cloud_Not(Cube) );
        } 
    }
    printf( "\n" );
}

Here is the call graph for this function:

Cloud_bddPrintCube()

void Cloud_bddPrintCube	(	CloudManager *	dd,
		CloudNode *	bCube )

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

Synopsis [Prints one cube.]

Description []

SideEffects []

Definition at line 900 of file cloud.c.

{
    CloudNode * bCube0, * bCube1;
 
    assert( !Cloud_IsConstant(bCube) );
    while ( 1 )
    {
        // get the node structure
        if ( Cloud_IsConstant(bCube) )
            break;
 
        // cofactor the cube
        if ( Cloud_IsComplement(bCube) )
        {
            bCube0 = Cloud_Not( cloudE(bCube) );
            bCube1 = Cloud_Not( cloudT(bCube) );
        }
        else
        {
            bCube0 = cloudE(bCube);
            bCube1 = cloudT(bCube);
        }
 
        if ( bCube0 != dd->zero )
        {
            assert( bCube1 == dd->zero );
            printf( "[%d]'", cloudV(bCube) );
            bCube = bCube0;
        }
        else
        {
            assert( bCube1 != dd->zero );
            printf( "[%d]", cloudV(bCube) );
            bCube = bCube1;
        }
    }
}

Here is the caller graph for this function:

Cloud_bddXor()

CloudNode * Cloud_bddXor	(	CloudManager *	dd,
		CloudNode *	f,
		CloudNode *	g )

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

Synopsis [Performs the XOR or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 536 of file cloud.c.

{
    CloudNode * t0, * t1, * r;
    if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
        return NULL;
    CLOUD_ASSERT(f);
    CLOUD_ASSERT(g);
    if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
        cloudCacheAllocate( dd, CLOUD_OPER_AND );
    t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) );
    if ( t0 == NULL )
        return NULL;
    t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
    if ( t1 == NULL )
        return NULL;
    r  = Cloud_bddOr( dd, t0, t1 );
    return r;
}

Here is the call graph for this function:

Cloud_CacheAllocate()

void Cloud_CacheAllocate	(	CloudManager *	dd,
		CloudOper	oper,
		int	logratio )

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

Synopsis [This optional function allocates operation cache of the given size.]

Description [Cache for each operation is allocated independently when the first operation of the given type is performed. The user can allocate cache of his/her preferred size by calling Cloud_CacheAllocate before the first operation of the given type is performed, but this call is optional. Argument "logratio" gives the binary logarithm of the ratio of the size of the unique table to that of cache. For example, if "logratio" is equal to 3, and the unique table will be 2^3=8 times larger than cache; so, if unique table is 2^23 = 8,388,608 nodes, the cache size will be 2^3=8 times smaller and equal to 2^20 = 1,048,576 entries.]

SideEffects []

SeeAlso []

Definition at line 195 of file cloud.c.

{
    assert( logratio > 0 );            // cache cannot be larger than the unique table 
    assert( logratio < dd->bitsNode ); // cache cannot be smaller than 2 entries
 
    if ( logratio )
    {
        dd->bitsCache[oper]  = dd->bitsNode - logratio;
        dd->shiftCache[oper] = 8*sizeof(unsigned) - dd->bitsCache[oper];
    }
    cloudCacheAllocate( dd, oper );
}

Cloud_DagCollect()

int Cloud_DagCollect	(	CloudManager *	dd,
		CloudNode *	n )

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

Synopsis [Counts the number of nodes in a DD.]

Description [Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.]

SideEffects []

SeeAlso []

Definition at line 772 of file cloud.c.

{
    int res, Counter = 0;
    if ( dd->ppNodes == NULL )
        dd->ppNodes = ABC_ALLOC( CloudNode *, dd->nNodesLimit );
    res = Cloud_DagCollect_rec( dd, Cloud_Regular( n ), &Counter );
    cloudClearMark( dd, Cloud_Regular( n ) );
    assert( res == Counter );
    return res;
 
}

Here is the caller graph for this function:

Cloud_DagSize()

int Cloud_DagSize	(	CloudManager *	dd,
		CloudNode *	n )

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

Synopsis [Counts the number of nodes in a DD.]

Description [Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.]

SideEffects []

SeeAlso []

Definition at line 721 of file cloud.c.

{
    int res;
    res = cloudDagSize( dd, Cloud_Regular( n ) );
    cloudClearMark( dd, Cloud_Regular( n ) );
    return res;
 
}

Here is the caller graph for this function:

Cloud_GetOneCube()

CloudNode * Cloud_GetOneCube	(	CloudManager *	dd,
		CloudNode *	bFunc )

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

Synopsis [Returns one cube contained in the given BDD.]

Description []

SideEffects []

Definition at line 817 of file cloud.c.

{
    CloudNode * bFunc0, * bFunc1, * res;
 
    if ( Cloud_IsConstant(bFunc) )
        return bFunc;
 
    // cofactor
    if ( Cloud_IsComplement(bFunc) )
    {
        bFunc0 = Cloud_Not( cloudE(bFunc) );
        bFunc1 = Cloud_Not( cloudT(bFunc) );
    }
    else
    {
        bFunc0 = cloudE(bFunc);
        bFunc1 = cloudT(bFunc);
    }
 
    // try to find the cube with the negative literal
    res = Cloud_GetOneCube( dd, bFunc0 );
    if ( res == NULL )
        return NULL;
 
    if ( res != dd->zero )
    {
        res = Cloud_bddAnd( dd, res, Cloud_Not(dd->vars[Cloud_V(bFunc)]) );
    }
    else
    {
        // try to find the cube with the positive literal
        res = Cloud_GetOneCube( dd, bFunc1 );
        if ( res == NULL )
            return NULL;
        assert( res != dd->zero );
        res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] );
    }
    return res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cloud_Init()

CloudManager * Cloud_Init	(	int	nVars,
		int	nBits )

FUNCTION DEFINITIONS ///.

FUNCTION DECLARATIONS ///.

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

Synopsis [Starts the cloud manager.]

Description [The first arguments is the number of elementary variables used. The second arguments is the number of bits of the unsigned integer used to represent nodes in the unique table. If the second argument is 0, the package assumes 23 to represent nodes, which is equivalent to 2^23 = 8,388,608 nodes.]

SideEffects []

SeeAlso []

Definition at line 70 of file cloud.c.

{
    CloudManager * dd;
    int i;
    abctime clk1, clk2;
 
    assert( nVars <= 100000 );
    assert( nBits < 32 );
 
    // assign the defaults
    if ( nBits == 0 )
        nBits = CLOUD_NODE_BITS;
 
    // start the manager
    dd = ABC_CALLOC( CloudManager, 1 );
    dd->nMemUsed          += sizeof(CloudManager);
 
    // variables
    dd->nVars             = nVars;              // the number of variables allocated
    // bits
    dd->bitsNode          = nBits;              // the number of bits used for the node
    for ( i = 0; i < CacheOperNum; i++ )
        dd->bitsCache[i]  = nBits - CacheLogRatioDefault[i];
    // shifts
    dd->shiftUnique       = 8*sizeof(unsigned) - (nBits + 1); // gets node index in the hash table
    for ( i = 0; i < CacheOperNum; i++ )
        dd->shiftCache[i] = 8*sizeof(unsigned) - dd->bitsCache[i];
    // nodes
    dd->nNodesAlloc       = (1 << (nBits + 1)); // 2 ^ (nBits + 1)
    dd->nNodesLimit       = (1 << nBits);       // 2 ^  nBits
 
    // unique table
clk1 = Abc_Clock();
    dd->tUnique           = ABC_CALLOC( CloudNode, dd->nNodesAlloc );
    dd->nMemUsed         += sizeof(CloudNode) * dd->nNodesAlloc;
clk2 = Abc_Clock();
//ABC_PRT( "calloc() time", clk2 - clk1 ); 
 
    // set up the constant node (the only node that is not in the hash table)
    dd->nSignCur          = 1;
    dd->tUnique[0].s      = dd->nSignCur;
    dd->tUnique[0].v      = CLOUD_CONST_INDEX;
    dd->tUnique[0].e      = NULL;
    dd->tUnique[0].t      = NULL;
    dd->one               = dd->tUnique;
    dd->zero              = Cloud_Not(dd->one);
    dd->nNodesCur         = 1;
 
    // special nodes
    dd->pNodeStart        = dd->tUnique + 1;
    dd->pNodeEnd          = dd->tUnique + dd->nNodesAlloc;
 
    // set up the elementary variables
    dd->vars              = ABC_ALLOC( CloudNode *, dd->nVars );
    dd->nMemUsed         += sizeof(CloudNode *) * dd->nVars;
    for ( i = 0; i < dd->nVars; i++ )
        dd->vars[i]   = cloudMakeNode( dd, i, dd->one, dd->zero );
 
    return dd;
};

Here is the caller graph for this function:

Cloud_MakeNode()

CloudNode * Cloud_MakeNode	(	CloudManager *	dd,
		CloudVar	v,
		CloudNode *	t,
		CloudNode *	e )

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

Synopsis [Returns or creates a new node]

Description [Checks the unique table for the existance of the node. If the node is present, returns the node. If the node is absent, creates a new node.]

SideEffects []

SeeAlso []

Definition at line 254 of file cloud.c.

{
    CloudNode * pRes;
    CLOUD_ASSERT(t); 
    CLOUD_ASSERT(e);
    assert( v < Cloud_V(t) && v < Cloud_V(e) );       // variable should be above in the order
    if ( Cloud_IsComplement(t) )
    {
        pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) );
        if ( pRes != NULL )
            pRes = Cloud_Not(pRes);            
    }
    else
        pRes = cloudMakeNode( dd, v, t, e );
    return pRes;
}

Here is the caller graph for this function:

Cloud_PrintHashTable()

void Cloud_PrintHashTable

(

CloudManager *

dd

)

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

Synopsis [Prints the state of the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 975 of file cloud.c.

{
    int i;
 
    for ( i = 0; i < dd->nNodesAlloc; i++ )
        if ( dd->tUnique[i].v == CLOUD_CONST_INDEX )
            printf( "-" );
        else
            printf( "+" );
    printf( "\n" );
}

Cloud_PrintInfo()

void Cloud_PrintInfo

(

CloudManager *

dd

)

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

Synopsis [Prints info.]

Description []

SideEffects []

SeeAlso []

Definition at line 950 of file cloud.c.

{
    if ( dd == NULL ) return;
    printf( "The number of unique table nodes allocated = %12d.\n", dd->nNodesAlloc );
    printf( "The number of unique table nodes present   = %12d.\n", dd->nNodesCur );
    printf( "The number of unique table hits            = %12d.\n", dd->nUniqueHits );
    printf( "The number of unique table misses          = %12d.\n", dd->nUniqueMisses );
    printf( "The number of unique table steps           = %12d.\n", dd->nUniqueSteps );
    printf( "The number of cache hits                   = %12d.\n", dd->nCacheHits );
    printf( "The number of cache misses                 = %12d.\n", dd->nCacheMisses );
    printf( "The current signature                      = %12d.\n", dd->nSignCur );
    printf( "The total memory in use                    = %12d.\n", dd->nMemUsed );
}

Cloud_Quit()

void Cloud_Quit

(

CloudManager *

dd

)

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

Synopsis [Stops the cloud manager.]

Description [The first arguments tells show many elementary variables are used. The second arguments tells how many bits of the unsigned integer are used to represent regular nodes in the unique table.]

SideEffects []

SeeAlso []

Definition at line 144 of file cloud.c.

{
    int i;
    ABC_FREE( dd->ppNodes );
    ABC_FREE( dd->tUnique ); 
    ABC_FREE( dd->vars ); 
    for ( i = 0; i < 4; i++ )
        ABC_FREE( dd->tCaches[i] );
    ABC_FREE( dd ); 
}

Here is the caller graph for this function:

Cloud_Restart()

void Cloud_Restart

(

CloudManager *

dd

)

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

Synopsis [Prepares the manager for another run.]

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file cloud.c.

{
    int i;
    assert( dd->one->s == dd->nSignCur );
    dd->nSignCur++;
    dd->one->s++;
    for ( i = 0; i < dd->nVars; i++ )
        dd->vars[i]->s++;
    dd->nNodesCur = 1 + dd->nVars;
}

Here is the caller graph for this function:

Cloud_SharingSize()

int Cloud_SharingSize	(	CloudManager *	dd,
		CloudNode **	pn,
		int	nn )

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

Synopsis [Counts the number of nodes in an array of DDs.]

Description [Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.]

SideEffects []

SeeAlso []

Definition at line 796 of file cloud.c.

{
    int res, i;
    res = 0;
    for ( i = 0; i < nn; i++ )
        res += cloudDagSize( dd, Cloud_Regular( pn[i] ) );
    for ( i = 0; i < nn; i++ )
        cloudClearMark( dd, Cloud_Regular( pn[i] ) );
    return res;
}

Cloud_Support()

CloudNode * Cloud_Support	(	CloudManager *	dd,
		CloudNode *	n )

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

Synopsis [Finds the variables on which a DD depends.]

Description [Finds the variables on which a DD depends. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 618 of file cloud.c.

{
    CloudNode * res;
    int * support, i;
 
    CLOUD_ASSERT(n);
 
    // allocate and initialize support array for cloudSupport
    support = ABC_CALLOC( int, dd->nVars );
 
    // compute support and clean up markers
    cloudSupport( dd, Cloud_Regular(n), support );
    cloudClearMark( dd, Cloud_Regular(n) );
 
    // transform support from array to cube
    res = dd->one;
    for ( i = dd->nVars - 1; i >= 0; i-- ) // for each level bottom-up 
        if ( support[i] == 1 )
        {
            res = Cloud_bddAnd( dd, res, dd->vars[i] );
            if ( res == NULL )
                break;
        }
    ABC_FREE( support );
    return res;
}

Here is the call graph for this function:

Cloud_SupportSize()

int Cloud_SupportSize	(	CloudManager *	dd,
		CloudNode *	n )

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

Synopsis [Counts the variables on which a DD depends.]

Description [Counts the variables on which a DD depends. Returns the number of the variables if successful; Cloud_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 658 of file cloud.c.

{
    int * support, i, count;
 
    CLOUD_ASSERT(n);
 
    // allocate and initialize support array for cloudSupport
    support = ABC_CALLOC( int, dd->nVars );
 
    // compute support and clean up markers
    cloudSupport( dd, Cloud_Regular(n), support );
    cloudClearMark( dd, Cloud_Regular(n) );
 
    // count support variables
    count = 0;
    for ( i = 0; i < dd->nVars; i++ )
    {
        if ( support[i] == 1 )
            count++;
    }
 
    ABC_FREE( support );
    return count;
}

cloudBddAnd()

CloudNode * cloudBddAnd	(	CloudManager *	dd,
		CloudNode *	f,
		CloudNode *	g )

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

Synopsis [Performs the AND or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 343 of file cloud.c.

{
    CloudNode * F, * G, * r;
    CloudCacheEntry2 * cacheEntry;
    CloudNode * fv, * fnv, * gv, * gnv, * t, * e;
    CloudVar  var;
 
    assert( f <= g );
 
    // terminal cases
    F = Cloud_Regular(f);
    G = Cloud_Regular(g);
    if ( F == G )
    {
        if ( f == g )
            return f;
        else
            return dd->zero;
    }
    if ( F == dd->one )
    {
        if ( f == dd->one )
            return g;
        else
            return f;
    }
 
    // check cache
    cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
//    cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
    r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g );
    if ( r != NULL )
    {
        dd->nCacheHits++;
        return r;
    }
    dd->nCacheMisses++;
 
 
    // compute cofactors
    if ( cloudV(F) <= cloudV(G) )
    {
        var = cloudV(F);
        if ( Cloud_IsComplement(f) )
        {
            fnv = Cloud_Not(cloudE(F));
            fv  = Cloud_Not(cloudT(F));
        }
        else
        {
            fnv = cloudE(F);
            fv  = cloudT(F);
        }
    }
    else
    {
        var = cloudV(G);
        fv  = fnv = f;
    }
 
    if ( cloudV(G) <= cloudV(F) )
    {
        if ( Cloud_IsComplement(g) )
        {
            gnv = Cloud_Not(cloudE(G));
            gv  = Cloud_Not(cloudT(G));
        }
        else
        {
            gnv = cloudE(G);
            gv  = cloudT(G);
        }
    }
    else
    {
        gv = gnv = g;
    }
 
    if ( fv <= gv )
        t = cloudBddAnd( dd, fv, gv );
    else
        t = cloudBddAnd( dd, gv, fv );
 
    if ( t == NULL )
        return NULL;
 
    if ( fnv <= gnv )
        e = cloudBddAnd( dd, fnv, gnv );
    else
        e = cloudBddAnd( dd, gnv, fnv );
 
    if ( e == NULL )
        return NULL;
 
    if ( t == e )
        r = t;
    else
    {
        if ( Cloud_IsComplement(t) )
        {
            r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
            if ( r == NULL )
                return NULL;
            r = Cloud_Not(r);
        }
        else
        {
            r = cloudMakeNode( dd, var, t, e );
            if ( r == NULL )
                return NULL;
        }
    }
    cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r );
    return r;
}

Here is the call graph for this function:

Here is the caller graph for this function: