src/aig/kit/cloud.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <time.h>
Include dependency graph for cloud.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  cloudManager
struct  cloudNode
struct  cloudCacheEntry1
struct  cloudCacheEntry2
struct  cloudCacheEntry3

Defines

#define CLOUD_NODE_BITS   23
#define CLOUD_ONE   ((unsigned)0x00000001)
#define CLOUD_NOT_ONE   ((unsigned)0xfffffffe)
#define CLOUD_VOID   ((unsigned)0x00000000)
#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)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
#define cloudHashCudd3(f, g, h, s)   (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s))
#define Cloud_Regular(p)   ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE))
#define Cloud_Not(p)   ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE))
#define Cloud_NotCond(p, c)   (((int)(c))? Cloud_Not(p):(p))
#define Cloud_IsComplement(p)   ((int)(((unsigned)(p)) & CLOUD_ONE))
#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): (CLOUD_VOID))
#define cloudCacheLookup2(p, sign, f, g)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID))
#define cloudCacheLookup3(p, sign, f, g, h)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID))
#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)
#define CALLOC(type, num)   ((type *) calloc((num), sizeof(type)))

Typedefs

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

Define Documentation

#define CALLOC ( type,
num   )     ((type *) calloc((num), sizeof(type)))

Definition at line 224 of file cloud.h.

#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)(((unsigned)(p)) & CLOUD_ONE))

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 164 of file cloud.h.

#define Cloud_Not ( p   )     ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE))

Definition at line 186 of file cloud.h.

#define CLOUD_NOT_ONE   ((unsigned)0xfffffffe)

Definition at line 166 of file cloud.h.

#define Cloud_NotCond ( p,
c   )     (((int)(c))? Cloud_Not(p):(p))

Definition at line 187 of file cloud.h.

#define CLOUD_ONE   ((unsigned)0x00000001)

Definition at line 165 of file cloud.h.

#define Cloud_Regular ( p   )     ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE))

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 CLOUD_VOID   ((unsigned)0x00000000)

Definition at line 167 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): (CLOUD_VOID))

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): (CLOUD_VOID))

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): (CLOUD_VOID))

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)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

Definition at line 181 of file cloud.h.

#define cloudHashCudd3 ( f,
g,
h,
s   )     (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(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 53 of file cloud.h.

typedef struct cloudCacheEntry2 CloudCacheEntry2

Definition at line 54 of file cloud.h.

typedef struct cloudCacheEntry3 CloudCacheEntry3

Definition at line 55 of file cloud.h.

typedef struct cloudManager CloudManager

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

FileName [cloud.h]

PackageName [Fast application-specific BDD package.]

Synopsis [Interface of the package.]

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

]

Definition at line 49 of file cloud.h.

typedef struct cloudNode CloudNode

Definition at line 52 of file cloud.h.

typedef unsigned CloudSign

Definition at line 51 of file cloud.h.

typedef unsigned CloudVar

Definition at line 50 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 58 of file cloud.h.

00058              { 
00059         CLOUD_OPER_AND, 
00060         CLOUD_OPER_XOR, 
00061         CLOUD_OPER_BDIFF, 
00062         CLOUD_OPER_LEQ 
00063 } 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 485 of file cloud.c.

00486 {
00487     if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
00488         return CLOUD_VOID;
00489         CLOUD_ASSERT(f);
00490         CLOUD_ASSERT(g);
00491         if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
00492                 cloudCacheAllocate( dd, CLOUD_OPER_AND );
00493         return cloudBddAnd_gate( dd, f, g );
00494 }

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.

00508 {
00509         CloudNode * res;
00510     if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
00511         return CLOUD_VOID;
00512         CLOUD_ASSERT(f);
00513         CLOUD_ASSERT(g);
00514         if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
00515                 cloudCacheAllocate( dd, CLOUD_OPER_AND );
00516         res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) );
00517         res = Cloud_NotCond( res, res != CLOUD_VOID );
00518         return res;
00519 }

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.

00863 {
00864         CloudNode * Cube;
00865         int fFirst = 1;
00866 
00867         if ( Func == dd->zero )
00868                 printf( "Constant 0." );
00869         else if ( Func == dd->one )
00870                 printf( "Constant 1." );
00871         else
00872         {
00873                 while ( 1 )
00874                 {
00875                         Cube = Cloud_GetOneCube( dd, Func );
00876                         if ( Cube == CLOUD_VOID || Cube == dd->zero )
00877                                 break;
00878                         if ( fFirst )           fFirst = 0;
00879                         else                            printf( " + " );
00880                         Cloud_bddPrintCube( dd, Cube );
00881                         Func = Cloud_bddAnd( dd, Func, Cloud_Not(Cube) );
00882                 } 
00883         }
00884         printf( "\n" );
00885 }

void Cloud_bddPrintCube ( CloudManager *  dd,
CloudNode *  bCube 
)

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

Synopsis [Prints one cube.]

Description []

SideEffects []

Definition at line 896 of file cloud.c.

00897 {
00898         CloudNode * bCube0, * bCube1;
00899 
00900         assert( !Cloud_IsConstant(bCube) );
00901         while ( 1 )
00902         {
00903                 // get the node structure
00904                 if ( Cloud_IsConstant(bCube) )
00905                         break;
00906 
00907                 // cofactor the cube
00908                 if ( Cloud_IsComplement(bCube) )
00909                 {
00910                         bCube0 = Cloud_Not( cloudE(bCube) );
00911                         bCube1 = Cloud_Not( cloudT(bCube) );
00912                 }
00913                 else
00914                 {
00915                         bCube0 = cloudE(bCube);
00916                         bCube1 = cloudT(bCube);
00917                 }
00918 
00919                 if ( bCube0 != dd->zero )
00920                 {
00921                         assert( bCube1 == dd->zero );
00922                         printf( "[%d]'", cloudV(bCube) );
00923                         bCube = bCube0;
00924                 }
00925                 else
00926                 {
00927                         assert( bCube1 != dd->zero );
00928                         printf( "[%d]", cloudV(bCube) );
00929                         bCube = bCube1;
00930                 }
00931         }
00932 }

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.

00192 {
00193         assert( logratio > 0 );            // cache cannot be larger than the unique table 
00194         assert( logratio < dd->bitsNode ); // cache cannot be smaller than 2 entries
00195 
00196         if ( logratio )
00197         {
00198                 dd->bitsCache[oper]  = dd->bitsNode - logratio;
00199                 dd->shiftCache[oper] = 8*sizeof(unsigned) - dd->bitsCache[oper];
00200         }
00201         cloudCacheAllocate( dd, oper );
00202 }

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.

00769 {
00770         int res, Counter = 0;
00771     if ( dd->ppNodes == NULL )
00772         dd->ppNodes = ALLOC( CloudNode *, dd->nNodesLimit );
00773         res = Cloud_DagCollect_rec( dd, Cloud_Regular( n ), &Counter );
00774         cloudClearMark( dd, Cloud_Regular( n ) );
00775     assert( res == Counter );
00776         return res;
00777 
00778 }

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.

00718 {
00719         int res;
00720         res = cloudDagSize( dd, Cloud_Regular( n ) );
00721         cloudClearMark( dd, Cloud_Regular( n ) );
00722         return res;
00723 
00724 }

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.

00814 {
00815         CloudNode * bFunc0, * bFunc1, * res;
00816 
00817         if ( Cloud_IsConstant(bFunc) )
00818                 return bFunc;
00819 
00820         // cofactor
00821         if ( Cloud_IsComplement(bFunc) )
00822         {
00823                 bFunc0 = Cloud_Not( cloudE(bFunc) );
00824                 bFunc1 = Cloud_Not( cloudT(bFunc) );
00825         }
00826         else
00827         {
00828                 bFunc0 = cloudE(bFunc);
00829                 bFunc1 = cloudT(bFunc);
00830         }
00831 
00832         // try to find the cube with the negative literal
00833         res = Cloud_GetOneCube( dd, bFunc0 );
00834         if ( res == CLOUD_VOID )
00835                 return CLOUD_VOID;
00836 
00837         if ( res != dd->zero )
00838         {
00839                 res = Cloud_bddAnd( dd, res, Cloud_Not(dd->vars[Cloud_V(bFunc)]) );
00840         }
00841         else
00842         {
00843                 // try to find the cube with the positive literal
00844                 res = Cloud_GetOneCube( dd, bFunc1 );
00845                 if ( res == CLOUD_VOID )
00846                         return CLOUD_VOID;
00847                 assert( res != dd->zero );
00848                 res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] );
00849         }
00850         return res;
00851 }

CloudManager* Cloud_Init ( int  nVars,
int  nBits 
)

FUNCTION DECLARATIONS ///

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.

00067 {
00068         CloudManager * dd;
00069         int i;
00070         int clk1, clk2;
00071 
00072         assert( nVars <= 100000 );
00073         assert( nBits < 32 );
00074 
00075         // assign the defaults
00076         if ( nBits == 0 )
00077                 nBits = CLOUD_NODE_BITS;
00078 
00079         // start the manager
00080         dd = CALLOC( CloudManager, 1 );
00081         dd->nMemUsed          += sizeof(CloudManager);
00082 
00083         // variables
00084         dd->nVars             = nVars;              // the number of variables allocated
00085         // bits
00086         dd->bitsNode          = nBits;              // the number of bits used for the node
00087         for ( i = 0; i < CacheOperNum; i++ )
00088                 dd->bitsCache[i]  = nBits - CacheLogRatioDefault[i];
00089         // shifts
00090         dd->shiftUnique       = 8*sizeof(unsigned) - (nBits + 1); // gets node index in the hash table
00091         for ( i = 0; i < CacheOperNum; i++ )
00092                 dd->shiftCache[i] = 8*sizeof(unsigned) - dd->bitsCache[i];
00093         // nodes
00094         dd->nNodesAlloc       = (1 << (nBits + 1)); // 2 ^ (nBits + 1)
00095         dd->nNodesLimit       = (1 << nBits);       // 2 ^  nBits
00096 
00097         // unique table
00098 clk1 = clock();
00099         dd->tUnique           = CALLOC( CloudNode, dd->nNodesAlloc );
00100         dd->nMemUsed         += sizeof(CloudNode) * dd->nNodesAlloc;
00101 clk2 = clock();
00102 //PRT( "calloc() time", clk2 - clk1 ); 
00103 
00104         // set up the constant node (the only node that is not in the hash table)
00105         dd->nSignCur          = 1;
00106         dd->tUnique[0].s      = dd->nSignCur;
00107         dd->tUnique[0].v      = CLOUD_CONST_INDEX;
00108         dd->tUnique[0].e      = CLOUD_VOID;
00109         dd->tUnique[0].t      = CLOUD_VOID;
00110         dd->one               = dd->tUnique;
00111         dd->zero              = Cloud_Not(dd->one);
00112         dd->nNodesCur         = 1;
00113 
00114         // special nodes
00115         dd->pNodeStart        = dd->tUnique + 1;
00116         dd->pNodeEnd          = dd->tUnique + dd->nNodesAlloc;
00117 
00118         // set up the elementary variables
00119         dd->vars              = ALLOC( CloudNode *, dd->nVars );
00120         dd->nMemUsed         += sizeof(CloudNode *) * dd->nVars;
00121         for ( i = 0; i < dd->nVars; i++ )
00122                 dd->vars[i]   = cloudMakeNode( dd, i, dd->one, dd->zero );
00123 
00124         return dd;
00125 };

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.

00251 {
00252         CloudNode * pRes;
00253         CLOUD_ASSERT(t); 
00254         CLOUD_ASSERT(e);
00255     assert( v < Cloud_V(t) && v < Cloud_V(e) );       // variable should be above in the order
00256     if ( Cloud_IsComplement(t) )
00257     {
00258         pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) );
00259         if ( pRes != CLOUD_VOID )
00260             pRes = Cloud_Not(pRes);            
00261     }
00262     else
00263         pRes = cloudMakeNode( dd, v, t, e );
00264     return pRes;
00265 }

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.

00972 {
00973         int i;
00974 
00975         for ( i = 0; i < dd->nNodesAlloc; i++ )
00976                 if ( dd->tUnique[i].v == CLOUD_CONST_INDEX )
00977                         printf( "-" );
00978                 else
00979                         printf( "+" );
00980         printf( "\n" );
00981 }

void Cloud_PrintInfo ( CloudManager *  dd  ) 

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

Synopsis [Prints info.]

Description []

SideEffects []

SeeAlso []

Definition at line 946 of file cloud.c.

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

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.

00141 {
00142         int i;
00143     FREE( dd->ppNodes );
00144         free( dd->tUnique ); 
00145         free( dd->vars ); 
00146         for ( i = 0; i < 4; i++ )
00147                 FREE( dd->tCaches[i] );
00148         free( dd ); 
00149 }

void Cloud_Restart ( CloudManager *  dd  ) 

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

Synopsis [Prepares the manager for another run.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file cloud.c.

00163 {
00164     int i;
00165     assert( dd->one->s == dd->nSignCur );
00166     dd->nSignCur++;
00167     dd->one->s++;
00168         for ( i = 0; i < dd->nVars; i++ )
00169                 dd->vars[i]->s++;
00170     dd->nNodesCur = 1 + dd->nVars;
00171 }

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.

00793 {
00794         int res, i;
00795         res = 0;
00796         for ( i = 0; i < nn; i++ )
00797                 res += cloudDagSize( dd, Cloud_Regular( pn[i] ) );
00798         for ( i = 0; i < nn; i++ )
00799                 cloudClearMark( dd, Cloud_Regular( pn[i] ) );
00800         return res;
00801 }

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.

00615 {
00616         CloudNode * res;
00617         int * support, i;
00618 
00619         CLOUD_ASSERT(n);
00620 
00621         // allocate and initialize support array for cloudSupport
00622         support = CALLOC( int, dd->nVars );
00623 
00624         // compute support and clean up markers
00625         cloudSupport( dd, Cloud_Regular(n), support );
00626         cloudClearMark( dd, Cloud_Regular(n) );
00627 
00628         // transform support from array to cube
00629         res = dd->one;
00630         for ( i = dd->nVars - 1; i >= 0; i-- ) // for each level bottom-up 
00631                 if ( support[i] == 1 )
00632                 {
00633                         res = Cloud_bddAnd( dd, res, dd->vars[i] );
00634                         if ( res == CLOUD_VOID )
00635                                 break;
00636                 }
00637         FREE( support );
00638         return res;
00639 }

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.

00655 {
00656         int * support, i, count;
00657 
00658         CLOUD_ASSERT(n);
00659 
00660         // allocate and initialize support array for cloudSupport
00661         support = CALLOC( int, dd->nVars );
00662 
00663         // compute support and clean up markers
00664         cloudSupport( dd, Cloud_Regular(n), support );
00665         cloudClearMark( dd, Cloud_Regular(n) );
00666 
00667         // count support variables
00668         count = 0;
00669         for ( i = 0; i < dd->nVars; i++ )
00670         {
00671                 if ( support[i] == 1 )
00672                         count++;
00673         }
00674 
00675         FREE( support );
00676         return count;
00677 }

Generated on Tue Jan 5 12:18:26 2010 for abc70930 by  doxygen 1.6.1