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

Include dependency graph for cloud.h:

This graph shows which files directly or indirectly include this file:

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

#define	cloudHashBuddy3(x, y, z, s)

#define	DD_P1 12582917

#define	DD_P2 4256249

#define	DD_P3 741457

#define	DD_P4 1618033999

#define	cloudHashCudd2(f, g, s)

#define	cloudHashCudd3(f, g, h, s)

#define	Cloud_Regular(p)

#define	Cloud_Not(p)

#define	Cloud_NotCond(p, c)

#define	Cloud_IsComplement(p)

#define	Cloud_IsConstant(p)

#define	cloudIsConstant(p)

#define	Cloud_V(p)

#define	Cloud_E(p)

#define	Cloud_T(p)

#define	cloudV(p)

#define	cloudE(p)

#define	cloudT(p)

#define	cloudNodeMark(p)

#define	cloudNodeUnmark(p)

#define	cloudNodeIsMarked(p)

#define	cloudCacheLookup1(p, sign, f)

#define	cloudCacheLookup2(p, sign, f, g)

#define	cloudCacheLookup3(p, sign, f, g, h)

#define	cloudCacheInsert1(p, sign, f, r)

#define	cloudCacheInsert2(p, sign, f, g, r)

#define	cloudCacheInsert3(p, sign, f, g, h, r)

#define	CLOUD_ASSERT(p)

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 ///.

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

◆ CLOUD_ASSERT

#define CLOUD_ASSERT ( p )

Value:

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

p

Cube * p

Definition exorList.c:222

assert

#define assert(ex)

Definition util_old.h:213

Definition at line 216 of file cloud.h.

◆ CLOUD_CONST_INDEX

#define CLOUD_CONST_INDEX ((unsigned)0x0fffffff)

Definition at line 169 of file cloud.h.

◆ Cloud_E

#define Cloud_E ( p )

Value:

((Cloud_Regular(p))->e)

Cloud_Regular

#define Cloud_Regular(p)

Definition cloud.h:185

Definition at line 195 of file cloud.h.

◆ Cloud_IsComplement

#define Cloud_IsComplement ( p )

Value:

((int)(((ABC_PTRUINT_T)(p)) & 01))

Definition at line 188 of file cloud.h.

◆ Cloud_IsConstant

#define Cloud_IsConstant ( p )

Value:

(((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

CLOUD_MARK_OFF

#define CLOUD_MARK_OFF

Definition cloud.h:171

CLOUD_CONST_INDEX

#define CLOUD_CONST_INDEX

Definition cloud.h:169

Definition at line 190 of file cloud.h.

◆ CLOUD_MARK_OFF

#define CLOUD_MARK_OFF ((unsigned)0xefffffff)

Definition at line 171 of file cloud.h.

◆ CLOUD_MARK_ON

#define CLOUD_MARK_ON ((unsigned)0x10000000)

Definition at line 170 of file cloud.h.

◆ CLOUD_NODE_BITS

#define CLOUD_NODE_BITS 23

Definition at line 167 of file cloud.h.

◆ Cloud_Not

#define Cloud_Not ( p )

Value:

((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ 01))

CloudNode

struct cloudNode CloudNode

Definition cloud.h:55

Definition at line 186 of file cloud.h.

◆ Cloud_NotCond

#define Cloud_NotCond	(		p,
			c )

Value:

((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c)))

Definition at line 187 of file cloud.h.

◆ Cloud_Regular

#define Cloud_Regular ( p )

Value:

((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01))

Definition at line 185 of file cloud.h.

◆ Cloud_T

#define Cloud_T ( p )

Value:

((Cloud_Regular(p))->t)

Definition at line 196 of file cloud.h.

◆ Cloud_V

#define Cloud_V ( p )

Value:

((Cloud_Regular(p))->v)

Definition at line 194 of file cloud.h.

◆ cloudCacheInsert1

#define cloudCacheInsert1	(	p,
		sign,
		f,
		r )

Value:

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

Definition at line 211 of file cloud.h.

◆ cloudCacheInsert2

#define cloudCacheInsert2	(	p,
		sign,
		f,
		g,
		r )

Value:

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

Definition at line 212 of file cloud.h.

◆ cloudCacheInsert3

#define cloudCacheInsert3	(	p,
		sign,
		f,
		g,
		h,
		r )

Value:

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

Definition at line 213 of file cloud.h.

◆ cloudCacheLookup1

#define cloudCacheLookup1	(	p,
		sign,
		f )

Value:

(((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))

Definition at line 207 of file cloud.h.

◆ cloudCacheLookup2

#define cloudCacheLookup2	(	p,
		sign,
		f,
		g )

Value:

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

Definition at line 208 of file cloud.h.

◆ cloudCacheLookup3

#define cloudCacheLookup3	(	p,
		sign,
		f,
		g,
		h )

Value:

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

Definition at line 209 of file cloud.h.

◆ cloudE

#define cloudE ( p )

Value:

((p)->e)

Definition at line 199 of file cloud.h.

◆ cloudHashBuddy2

#define cloudHashBuddy2	(	x,
		y,
		s )

Value:

((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))

Definition at line 174 of file cloud.h.

◆ cloudHashBuddy3

#define cloudHashBuddy3	(	x,
		y,
		z,
		s )

Value:

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

cloudHashBuddy2

#define cloudHashBuddy2(x, y, s)

Definition cloud.h:174

Definition at line 175 of file cloud.h.

◆ cloudHashCudd2

#define cloudHashCudd2	(	f,
		g,
		s )

Value:

((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s))

DD_P2

#define DD_P2

Definition cloud.h:178

DD_P1

#define DD_P1

Definition cloud.h:177

Definition at line 181 of file cloud.h.

◆ cloudHashCudd3

#define cloudHashCudd3	(	f,
		g,
		h,
		s )

Value:

(((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s))

DD_P3

#define DD_P3

Definition cloud.h:179

Definition at line 182 of file cloud.h.

◆ cloudIsConstant

#define cloudIsConstant ( p )

Value:

(((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

Definition at line 191 of file cloud.h.

◆ cloudNodeIsMarked

#define cloudNodeIsMarked ( p )

Value:

((int)((p)->v & CLOUD_MARK_ON))

CLOUD_MARK_ON

#define CLOUD_MARK_ON

Definition cloud.h:170

Definition at line 204 of file cloud.h.

◆ cloudNodeMark

#define cloudNodeMark ( p )

Value:

((p)->v |= CLOUD_MARK_ON)

Definition at line 202 of file cloud.h.

◆ cloudNodeUnmark

#define cloudNodeUnmark ( p )

Value:

((p)->v &= CLOUD_MARK_OFF)

Definition at line 203 of file cloud.h.

◆ cloudT

#define cloudT ( p )

Value:

((p)->t)

Definition at line 200 of file cloud.h.

◆ cloudV

#define cloudV ( p )

Value:

((p)->v)

Definition at line 198 of file cloud.h.

◆ DD_P1

#define DD_P1 12582917

Definition at line 177 of file cloud.h.

◆ DD_P2

#define DD_P2 4256249

Definition at line 178 of file cloud.h.

◆ DD_P3

#define DD_P3 741457

Definition at line 179 of file cloud.h.

◆ DD_P4

#define DD_P4 1618033999

Definition at line 180 of file cloud.h.

Typedef Documentation

◆ CloudCacheEntry1

typedef struct cloudCacheEntry1 CloudCacheEntry1

Definition at line 56 of file cloud.h.

◆ CloudCacheEntry2

typedef struct cloudCacheEntry2 CloudCacheEntry2

Definition at line 57 of file cloud.h.

◆ CloudCacheEntry3

typedef struct cloudCacheEntry3 CloudCacheEntry3

Definition at line 58 of file cloud.h.

◆ CloudManager

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.

◆ CloudNode

typedef struct cloudNode CloudNode

Definition at line 55 of file cloud.h.

◆ CloudSign

typedef unsigned CloudSign

Definition at line 54 of file cloud.h.

◆ CloudVar

typedef unsigned CloudVar

Definition at line 53 of file cloud.h.

Enumeration Type Documentation

◆ CloudOper

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

◆ Cloud_bddAnd()

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

extern

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

Synopsis [Performs the AND or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 489 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_bddOr()

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

extern

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

Synopsis [Performs the OR or two BDDs]

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_bddPrint()

void Cloud_bddPrint	(	CloudManager *	dd,
		CloudNode *	Func )

extern

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

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

Description []

SideEffects []

Definition at line 866 of file cloud.c.

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

Here is the call graph for this function:

◆ Cloud_bddPrintCube()

void Cloud_bddPrintCube	(	CloudManager *	dd,
		CloudNode *	bCube )

extern

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

Synopsis [Prints one cube.]

Description []

SideEffects []

Definition at line 900 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_CacheAllocate()

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

extern

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

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

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

SideEffects []

SeeAlso []

Definition at line 195 of file cloud.c.

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

◆ Cloud_DagCollect()

int Cloud_DagCollect	(	CloudManager *	dd,
		CloudNode *	n )

extern

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

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

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

SideEffects []

SeeAlso []

Definition at line 772 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_DagSize()

int Cloud_DagSize	(	CloudManager *	dd,
		CloudNode *	n )

extern

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

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

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

SideEffects []

SeeAlso []

Definition at line 721 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_GetOneCube()

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

extern

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

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

Description []

SideEffects []

Definition at line 817 of file cloud.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Cloud_Init()

CloudManager * Cloud_Init	(	int	nVars,
		int	nBits )

extern

FUNCTION DECLARATIONS ///.

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

Synopsis [Starts the cloud manager.]

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

SideEffects []

SeeAlso []

Definition at line 70 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_MakeNode()

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

extern

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

Synopsis [Returns or creates a new node]

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

SideEffects []

SeeAlso []

Definition at line 254 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_PrintHashTable()

void Cloud_PrintHashTable ( CloudManager * dd )

extern

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

Synopsis [Prints the state of the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 975 of file cloud.c.

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

◆ Cloud_PrintInfo()

void Cloud_PrintInfo ( CloudManager * dd )

extern

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

Synopsis [Prints info.]

Description []

SideEffects []

SeeAlso []

Definition at line 950 of file cloud.c.

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

◆ Cloud_Quit()

void Cloud_Quit ( CloudManager * dd )

extern

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

Synopsis [Stops the cloud manager.]

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

SideEffects []

SeeAlso []

Definition at line 144 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_Restart()

void Cloud_Restart ( CloudManager * dd )

extern

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

Synopsis [Prepares the manager for another run.]

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file cloud.c.

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

Here is the caller graph for this function:

◆ Cloud_SharingSize()

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

extern

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

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

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

SideEffects []

SeeAlso []

Definition at line 796 of file cloud.c.

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

◆ Cloud_Support()

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

extern

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

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

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

SideEffects [None]

SeeAlso []

Definition at line 618 of file cloud.c.

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

Here is the call graph for this function:

◆ Cloud_SupportSize()

int Cloud_SupportSize	(	CloudManager *	dd,
		CloudNode *	n )

extern

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

Classes

Macros

Typedefs

Enumerations

Functions

Macro Definition Documentation

◆ CLOUD_ASSERT

◆ CLOUD_CONST_INDEX

◆ Cloud_E

◆ Cloud_IsComplement

◆ Cloud_IsConstant

◆ CLOUD_MARK_OFF

◆ CLOUD_MARK_ON

◆ CLOUD_NODE_BITS

◆ Cloud_Not

◆ Cloud_NotCond

◆ Cloud_Regular

◆ Cloud_T

◆ Cloud_V

◆ cloudCacheInsert1

◆ cloudCacheInsert2

◆ cloudCacheInsert3

◆ cloudCacheLookup1

◆ cloudCacheLookup2

◆ cloudCacheLookup3

◆ cloudE

◆ cloudHashBuddy2

◆ cloudHashBuddy3

◆ cloudHashCudd2

◆ cloudHashCudd3

◆ cloudIsConstant

◆ cloudNodeIsMarked

◆ cloudNodeMark

◆ cloudNodeUnmark

◆ cloudT

◆ cloudV

◆ DD_P1

◆ DD_P2

◆ DD_P3

◆ DD_P4

Typedef Documentation

◆ CloudCacheEntry1

◆ CloudCacheEntry2

◆ CloudCacheEntry3

◆ CloudManager

◆ CloudNode

◆ CloudSign

◆ CloudVar

Enumeration Type Documentation

◆ CloudOper

Function Documentation

◆ Cloud_bddAnd()

◆ Cloud_bddOr()

◆ Cloud_bddPrint()

◆ Cloud_bddPrintCube()

◆ Cloud_CacheAllocate()

◆ Cloud_DagCollect()

◆ Cloud_DagSize()

◆ Cloud_GetOneCube()

◆ Cloud_Init()

◆ Cloud_MakeNode()

◆ Cloud_PrintHashTable()

◆ Cloud_PrintInfo()

◆ Cloud_Quit()

◆ Cloud_Restart()

◆ Cloud_SharingSize()

◆ Cloud_Support()

◆ Cloud_SupportSize()