cloud.c File Reference

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

Go to the source code of this file.

Functions
static CloudNode *	cloudMakeNode (CloudManager *dd, CloudVar v, CloudNode *t, CloudNode *e)
	FUNCTION DECLARATIONS ///. More...
static void	cloudCacheAllocate (CloudManager *dd, CloudOper oper)
CloudManager *	Cloud_Init (int nVars, int nBits)
	FUNCTION DEFINITIONS ///. More...
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)
static CloudNode *	cloudBddAnd_gate (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)
static void	cloudClearMark (CloudManager *dd, CloudNode *n)
static void	cloudSupport (CloudManager *dd, CloudNode *n, int *support)
CloudNode *	Cloud_Support (CloudManager *dd, CloudNode *n)
int	Cloud_SupportSize (CloudManager *dd, CloudNode *n)
static int	cloudDagSize (CloudManager *dd, CloudNode *n)
int	Cloud_DagSize (CloudManager *dd, CloudNode *n)
static int	Cloud_DagCollect_rec (CloudManager *dd, CloudNode *n, int *pCounter)
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)

Variables
static ABC_NAMESPACE_IMPL_START int	CacheOperNum = 4
static int	CacheLogRatioDefault [4]
static int	CacheSize [4]

Function Documentation

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

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

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

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

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

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

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;

}

static int Cloud_DagCollect_rec ( CloudManager *  dd, CloudNode *  n, int *  pCounter  )

static

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

Synopsis [Performs the recursive step of Cloud_DagSize.]

Description [Performs the recursive step of Cloud_DagSize. Returns the number of nodes in the graph rooted at n.]

SideEffects [None]

Definition at line 741 of file cloud.c.

{
    int tval, eval;
    if ( cloudNodeIsMarked(n) )
        return 0;
    // set visited flag
    cloudNodeMark(n);
    if ( cloudIsConstant(n) )
    {
        dd->ppNodes[(*pCounter)++] = n;
        return 1;
    }
    tval = Cloud_DagCollect_rec( dd, cloudT(n), pCounter );
    eval = Cloud_DagCollect_rec( dd, Cloud_Regular(cloudE(n)), pCounter );
    dd->ppNodes[(*pCounter)++] = n;
    return tval + eval + 1;

}

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;

}

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

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

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

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

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

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

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

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

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

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

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

static CloudNode* cloudBddAnd_gate ( CloudManager *  dd, CloudNode *  f, CloudNode *  g  )

inlinestatic

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

Synopsis [Performs the AND or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file cloud.c.

{
    if ( f <= g )
        return cloudBddAnd(dd,f,g);
    else
        return cloudBddAnd(dd,g,f);
}

void cloudCacheAllocate ( CloudManager *  dd, CloudOper  oper  )

static

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

Synopsis [Internal cache allocation.]

Description []

SideEffects []

SeeAlso []

Definition at line 219 of file cloud.c.

{
    int nCacheEntries = (1 << dd->bitsCache[oper]);

    if ( CacheSize[oper] == 1 )
    {
        dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry1, nCacheEntries );
        dd->nMemUsed     += sizeof(CloudCacheEntry1) * nCacheEntries;
    }
    else if ( CacheSize[oper] == 2 )
    {
        dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry2, nCacheEntries );
        dd->nMemUsed     += sizeof(CloudCacheEntry2) * nCacheEntries;
    }
    else if ( CacheSize[oper] == 3 )
    {
        dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry3, nCacheEntries );
        dd->nMemUsed     += sizeof(CloudCacheEntry3) * nCacheEntries;
    }
}

static void cloudClearMark ( CloudManager *  dd, CloudNode *  n  )

static

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

Synopsis [Performs a DFS from f, clearing the LSB of the next pointers.]

Description []

SideEffects [None]

SeeAlso [cloudSupport cloudDagSize]

Definition at line 569 of file cloud.c.

{
    if ( !cloudNodeIsMarked(n) )
        return;
    // clear visited flag
    cloudNodeUnmark(n);
    if ( cloudIsConstant(n) )
        return;
    cloudClearMark( dd, cloudT(n) );
    cloudClearMark( dd, Cloud_Regular(cloudE(n)) );
}

static int cloudDagSize ( CloudManager *  dd, CloudNode *  n  )

static

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

Synopsis [Performs the recursive step of Cloud_DagSize.]

Description [Performs the recursive step of Cloud_DagSize. Returns the number of nodes in the graph rooted at n.]

SideEffects [None]

Definition at line 694 of file cloud.c.

{
    int tval, eval;
    if ( cloudNodeIsMarked(n) )
        return 0;
    // set visited flag
    cloudNodeMark(n);
    if ( cloudIsConstant(n) )
        return 1;
    tval = cloudDagSize( dd, cloudT(n) );
    eval = cloudDagSize( dd, Cloud_Regular(cloudE(n)) );
    return tval + eval + 1;

}

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

static

FUNCTION DECLARATIONS ///.

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 283 of file cloud.c.

{
    CloudNode * entryUnique;

    CLOUD_ASSERT(t); 
    CLOUD_ASSERT(e);

    assert( ((int)v) >= 0 && ((int)v) < dd->nVars );  // the variable must be in the range
    assert( v < Cloud_V(t) && v < Cloud_V(e) );       // variable should be above in the order
    assert( !Cloud_IsComplement(t) );                 // the THEN edge must not be complemented

    // make sure we are not searching for the constant node
    assert( t && e );

    // get the unique entry
    entryUnique = dd->tUnique + cloudHashCudd3(v, t, e, dd->shiftUnique);
    while ( entryUnique->s == dd->nSignCur )
    {
        // compare the node
        if ( entryUnique->v == v && entryUnique->t == t && entryUnique->e == e )
        { // the node is found
            dd->nUniqueHits++;
            return entryUnique;  // returns the node
        }
        // increment the hash value modulus the hash table size
        if ( ++entryUnique - dd->tUnique == dd->nNodesAlloc )
            entryUnique = dd->tUnique + 1;
        // increment the number of steps through the table
        dd->nUniqueSteps++;
    }
    dd->nUniqueMisses++;

    // check if the new node can be created
    if ( ++dd->nNodesCur == dd->nNodesLimit ) 
    { // initiate the restart
        printf( "Cloud needs restart!\n" );
//      fflush( stdout );
//      exit(1);
        return NULL;
    }
    // create the node
    entryUnique->s   = dd->nSignCur;
    entryUnique->v   = v;
    entryUnique->t   = t;
    entryUnique->e   = e;
    return entryUnique;  // returns the node
}

static void cloudSupport ( CloudManager *  dd, CloudNode *  n, int *  support  )

static

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

Synopsis [Performs the recursive step of Cloud_Support.]

Description [Performs the recursive step of Cloud_Support. Performs a DFS from f. The support is accumulated in supp as a side effect. Uses the LSB of the then pointer as visited flag.]

SideEffects [None]

SeeAlso []

Definition at line 594 of file cloud.c.

{
    if ( cloudIsConstant(n) || cloudNodeIsMarked(n) )
        return;
    // set visited flag
    cloudNodeMark(n);
    support[cloudV(n)] = 1;
    cloudSupport( dd, cloudT(n), support );
    cloudSupport( dd, Cloud_Regular(cloudE(n)), support );
}

Variable Documentation

int CacheLogRatioDefault[4]

static

Initial value:

= {
    2, 
    8, 
    8, 
    8  
}

Definition at line 29 of file cloud.c.

ABC_NAMESPACE_IMPL_START int CacheOperNum = 4

static

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

FileName [cloudCore.c]

PackageName [Fast application-specific BDD package.]

Synopsis [The package core.]

Author [Alan Mishchenko alanm.nosp@m.i@ec.nosp@m.e.pdx.nosp@m..edu]

Affiliation [ECE Department. Portland State University, Portland, Oregon.]

Date [Ver. 1.0. Started - June 10, 2002.]

Revision [

Id:

cloudCore.c,v 1.0 2002/06/10 03:00:00 alanmi Exp

]

Definition at line 26 of file cloud.c.

int CacheSize[4]

static

Initial value:

= {
    2, 
    2, 
    2, 
    2  
}

Definition at line 37 of file cloud.c.