src/aig/kit/cloud.c File Reference

#include "cloud.h"

Include dependency graph for cloud.c:

Go to the source code of this file.

Functions
static CloudNode *	cloudMakeNode (CloudManager *dd, CloudVar v, CloudNode *t, CloudNode *e)
static void	cloudCacheAllocate (CloudManager *dd, CloudOper oper)
CloudManager *	Cloud_Init (int nVars, int nBits)
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 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 485 of file cloud.c.

{
    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
        return CLOUD_VOID;
        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 507 of file cloud.c.

{
        CloudNode * res;
    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
        return CLOUD_VOID;
        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 != CLOUD_VOID );
        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 862 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 == CLOUD_VOID || 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 896 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 532 of file cloud.c.

{
        CloudNode * t0, * t1, * r;
    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
        return CLOUD_VOID;
        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 == CLOUD_VOID )
                return CLOUD_VOID;
        t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
        if ( t1 == CLOUD_VOID )
                return CLOUD_VOID;
        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 191 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 768 of file cloud.c.

{
        int res, Counter = 0;
    if ( dd->ppNodes == NULL )
        dd->ppNodes = 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 737 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 717 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 813 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 == CLOUD_VOID )
                return CLOUD_VOID;

        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 == CLOUD_VOID )
                        return CLOUD_VOID;
                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********************************************************************

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

{
        CloudManager * dd;
        int i;
        int clk1, clk2;

        assert( nVars <= 100000 );
        assert( nBits < 32 );

        // assign the defaults
        if ( nBits == 0 )
                nBits = CLOUD_NODE_BITS;

        // start the manager
        dd = 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 = clock();
        dd->tUnique           = CALLOC( CloudNode, dd->nNodesAlloc );
        dd->nMemUsed         += sizeof(CloudNode) * dd->nNodesAlloc;
clk2 = clock();
//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      = CLOUD_VOID;
        dd->tUnique[0].t      = CLOUD_VOID;
        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              = 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 250 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 != CLOUD_VOID )
            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 971 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 946 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 140 of file cloud.c.

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

void Cloud_Restart

(

CloudManager *

dd

)

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

Synopsis [Prepares the manager for another run.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 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 792 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 614 of file cloud.c.

{
        CloudNode * res;
        int * support, i;

        CLOUD_ASSERT(n);

        // allocate and initialize support array for cloudSupport
        support = 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 == CLOUD_VOID )
                                break;
                }
        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 654 of file cloud.c.

{
        int * support, i, count;

        CLOUD_ASSERT(n);

        // allocate and initialize support array for cloudSupport
        support = 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++;
        }

        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 339 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 != CLOUD_VOID )
        {
                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 == CLOUD_VOID )
                return CLOUD_VOID;

        if ( fnv <= gnv )
                e = cloudBddAnd( dd, fnv, gnv );
        else
                e = cloudBddAnd( dd, gnv, fnv );

        if ( e == CLOUD_VOID )
                return CLOUD_VOID;

        if ( t == e )
                r = t;
        else
        {
                if ( Cloud_IsComplement(t) )
                {
                        r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
                        if ( r == CLOUD_VOID )
                                return CLOUD_VOID;
                        r = Cloud_Not(r);
                }
                else
                {
                        r = cloudMakeNode( dd, var, t, e );
                        if ( r == CLOUD_VOID )
                                return CLOUD_VOID;
                }
        }
        cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r );
        return r;
}

static CloudNode* cloudBddAnd_gate	(	CloudManager *	dd,
		CloudNode *	f,
		CloudNode *	g
	)			[inline, static]

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

Synopsis [Performs the AND or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 466 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 215 of file cloud.c.

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

        if ( CacheSize[oper] == 1 )
        {
                dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry1, nCacheEntries );
                dd->nMemUsed     += sizeof(CloudCacheEntry1) * nCacheEntries;
        }
        else if ( CacheSize[oper] == 2 )
        {
                dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry2, nCacheEntries );
                dd->nMemUsed     += sizeof(CloudCacheEntry2) * nCacheEntries;
        }
        else if ( CacheSize[oper] == 3 )
        {
                dd->tCaches[oper] = (CloudCacheEntry2 *)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 565 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 690 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 279 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 CLOUD_VOID;
        }
        // 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 590 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 25 of file cloud.c.

int CacheOperNum = 4 [static]

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

FileName [cloudCore.c]

PackageName [Fast application-specific BDD package.]

Synopsis [The package core.]

Author [Alan Mishchenko <alanmi@ece.pdx.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 22 of file cloud.c.

int CacheSize[4] [static]

Initial value:

 {
        2, 
        2, 
        2, 
        2  
}

Definition at line 33 of file cloud.c.