#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "misc/util/abc_global.h"

Data Structures
struct	cloudManager

struct	cloudNode

struct	cloudCacheEntry1

struct	cloudCacheEntry2

struct	cloudCacheEntry3

Macros
#define	CLOUD_NODE_BITS 23

#define	CLOUD_CONST_INDEX ((unsigned)0x0fffffff)

#define	CLOUD_MARK_ON ((unsigned)0x10000000)

#define	CLOUD_MARK_OFF ((unsigned)0xefffffff)

#define	cloudHashBuddy2(x, y, s) ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))

#define	cloudHashBuddy3(x, y, z, s) (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1))

#define	DD_P1 12582917

#define	DD_P2 4256249

#define	DD_P3 741457

#define	DD_P4 1618033999

#define	cloudHashCudd2(f, g, s) ((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s))

#define	cloudHashCudd3(f, g, h, s) (((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s))

#define	Cloud_Regular(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01))

#define	Cloud_Not(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ 01))

#define	Cloud_NotCond(p, c) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c)))

#define	Cloud_IsComplement(p) ((int)(((ABC_PTRUINT_T)(p)) & 01))

#define	Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

#define	cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

#define	Cloud_V(p) ((Cloud_Regular(p))->v)

#define	Cloud_E(p) ((Cloud_Regular(p))->e)

#define	Cloud_T(p) ((Cloud_Regular(p))->t)

#define	cloudV(p) ((p)->v)

#define	cloudE(p) ((p)->e)

#define	cloudT(p) ((p)->t)

#define	cloudNodeMark(p) ((p)->v \|= CLOUD_MARK_ON)

#define	cloudNodeUnmark(p) ((p)->v &= CLOUD_MARK_OFF)

#define	cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON))

#define	cloudCacheLookup1(p, sign, f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))

#define	cloudCacheLookup2(p, sign, f, g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))

#define	cloudCacheLookup3(p, sign, f, g, h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))

#define	cloudCacheInsert1(p, sign, f, r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))

#define	cloudCacheInsert2(p, sign, f, g, r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))

#define	cloudCacheInsert3(p, sign, f, g, h, r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r)))

#define	CLOUD_ASSERT(p) assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct cloudManager	CloudManager

typedef unsigned	CloudVar

typedef unsigned	CloudSign

typedef struct cloudNode	CloudNode

typedef struct cloudCacheEntry1	CloudCacheEntry1

typedef struct cloudCacheEntry2	CloudCacheEntry2

typedef struct cloudCacheEntry3	CloudCacheEntry3

Enumerations
enum	CloudOper { CLOUD_OPER_AND, CLOUD_OPER_XOR, CLOUD_OPER_BDIFF, CLOUD_OPER_LEQ }

Functions
CloudManager *	Cloud_Init (int nVars, int nBits)
	FUNCTION DECLARATIONS ///. More...

void	Cloud_Quit (CloudManager *dd)

void	Cloud_Restart (CloudManager *dd)

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

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

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 n)

void	Cloud_bddPrint (CloudManager dd, CloudNode Func)

void	Cloud_bddPrintCube (CloudManager dd, CloudNode Cube)

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

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

void	Cloud_PrintInfo (CloudManager *dd)

void	Cloud_PrintHashTable (CloudManager *dd)

Macro Definition Documentation

#define CLOUD_ASSERT ( p ) assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc)

Definition at line 216 of file cloud.h.

#define CLOUD_CONST_INDEX ((unsigned)0x0fffffff)

Definition at line 169 of file cloud.h.

#define Cloud_E ( p ) ((Cloud_Regular(p))->e)

Definition at line 195 of file cloud.h.

#define Cloud_IsComplement ( p ) ((int)(((ABC_PTRUINT_T)(p)) & 01))

Definition at line 188 of file cloud.h.

#define Cloud_IsConstant ( p ) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

Definition at line 190 of file cloud.h.

#define CLOUD_MARK_OFF ((unsigned)0xefffffff)

Definition at line 171 of file cloud.h.

#define CLOUD_MARK_ON ((unsigned)0x10000000)

Definition at line 170 of file cloud.h.

#define CLOUD_NODE_BITS 23

Definition at line 167 of file cloud.h.

#define Cloud_Not ( p ) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ 01))

Definition at line 186 of file cloud.h.

#define Cloud_NotCond	(	p,
		c
	)	((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c)))

Definition at line 187 of file cloud.h.

#define Cloud_Regular ( p ) ((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01))

Definition at line 185 of file cloud.h.

#define Cloud_T ( p ) ((Cloud_Regular(p))->t)

Definition at line 196 of file cloud.h.

#define Cloud_V ( p ) ((Cloud_Regular(p))->v)

Definition at line 194 of file cloud.h.

#define cloudCacheInsert1	(	p,
		sign,
		f,
		r
	)	(((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))

Definition at line 211 of file cloud.h.

#define cloudCacheInsert2	(	p,
		sign,
		f,
		g,
		r
	)	(((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))

Definition at line 212 of file cloud.h.

#define cloudCacheInsert3	(	p,
		sign,
		f,
		g,
		h,
		r
	)	(((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r)))

Definition at line 213 of file cloud.h.

#define cloudCacheLookup1	(	p,
		sign,
		f
	)	(((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))

Definition at line 207 of file cloud.h.

#define cloudCacheLookup2	(	p,
		sign,
		f,
		g
	)	(((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))

Definition at line 208 of file cloud.h.

#define cloudCacheLookup3	(	p,
		sign,
		f,
		g,
		h
	)	(((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))

Definition at line 209 of file cloud.h.

#define cloudE ( p ) ((p)->e)

Definition at line 199 of file cloud.h.

#define cloudHashBuddy2	(	x,
		y,
		s
	)	((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))

Definition at line 174 of file cloud.h.

#define cloudHashBuddy3	(	x,
		y,
		z,
		s
	)	(cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1))

Definition at line 175 of file cloud.h.

#define cloudHashCudd2	(	f,
		g,
		s
	)	((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s))

Definition at line 181 of file cloud.h.

#define cloudHashCudd3	(	f,
		g,
		h,
		s
	)	(((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s))

Definition at line 182 of file cloud.h.

#define cloudIsConstant ( p ) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

Definition at line 191 of file cloud.h.

#define cloudNodeIsMarked ( p ) ((int)((p)->v & CLOUD_MARK_ON))

Definition at line 204 of file cloud.h.

#define cloudNodeMark ( p ) ((p)->v |= CLOUD_MARK_ON)

Definition at line 202 of file cloud.h.

#define cloudNodeUnmark ( p ) ((p)->v &= CLOUD_MARK_OFF)

Definition at line 203 of file cloud.h.

#define cloudT ( p ) ((p)->t)

Definition at line 200 of file cloud.h.

#define cloudV ( p ) ((p)->v)

Definition at line 198 of file cloud.h.

#define DD_P1 12582917

Definition at line 177 of file cloud.h.

#define DD_P2 4256249

Definition at line 178 of file cloud.h.

#define DD_P3 741457

Definition at line 179 of file cloud.h.

#define DD_P4 1618033999

Definition at line 180 of file cloud.h.

Typedef Documentation

typedef struct cloudCacheEntry1 CloudCacheEntry1

Definition at line 56 of file cloud.h.

typedef struct cloudCacheEntry2 CloudCacheEntry2

Definition at line 57 of file cloud.h.

typedef struct cloudCacheEntry3 CloudCacheEntry3

Definition at line 58 of file cloud.h.

typedef typedefABC_NAMESPACE_HEADER_START struct cloudManager CloudManager

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

FileName [cloud.h]

PackageName [Fast application-specific BDD package.]

Synopsis [Interface of the package.]

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:: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp

]

Definition at line 52 of file cloud.h.

typedef struct cloudNode CloudNode

Definition at line 55 of file cloud.h.

typedef unsigned CloudSign

Definition at line 54 of file cloud.h.

typedef unsigned CloudVar

Definition at line 53 of file cloud.h.

Enumeration Type Documentation

enum CloudOper

Enumerator
CLOUD_OPER_AND
CLOUD_OPER_XOR
CLOUD_OPER_BDIFF
CLOUD_OPER_LEQ

Definition at line 61 of file cloud.h.

              { 
     CLOUD_OPER_AND, 
     CLOUD_OPER_XOR, 
     CLOUD_OPER_BDIFF, 
     CLOUD_OPER_LEQ 
 } CloudOper;

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

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

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

Data Structures

Macros

Typedefs

Enumerations

Functions

Macro Definition Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation