/**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 $]

***********************************************************************/

#include "cloud.h"

// the number of operators using cache
static int CacheOperNum = 4;

// the ratio of cache size to the unique table size for each operator
static int CacheLogRatioDefault[4] = {
	2, // CLOUD_OPER_AND, 
	8, // CLOUD_OPER_XOR, 
	8, // CLOUD_OPER_BDIFF, 
	8  // CLOUD_OPER_LEQ 
};

// the ratio of cache size to the unique table size for each operator
static int CacheSize[4] = {
	2, // CLOUD_OPER_AND, 
	2, // CLOUD_OPER_XOR, 
	2, // CLOUD_OPER_BDIFF, 
	2  // CLOUD_OPER_LEQ 
};

////////////////////////////////////////////////////////////////////////
///                       FUNCTION DECLARATIONS                      ///
////////////////////////////////////////////////////////////////////////

// static functions
static CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
static void        cloudCacheAllocate( CloudManager * dd, CloudOper oper );

////////////////////////////////////////////////////////////////////////
///                       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     []

******************************************************************************/
CloudManager * Cloud_Init( int nVars, int nBits )
{
	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;
};

/**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     []

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

/**Function********************************************************************

  Synopsis    [Prepares the manager for another run.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
void Cloud_Restart( CloudManager * dd )
{
    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;
}

/**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     []

******************************************************************************/
void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int logratio )
{
	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 );
}

/**Function********************************************************************

  Synopsis    [Internal cache allocation.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
void cloudCacheAllocate( CloudManager * dd, CloudOper oper )
{
	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;
	}
}



/**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     []

******************************************************************************/
CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
{
	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;
}

/**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     []

******************************************************************************/
CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
{
	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
		fprintf(outStream,  "Cloud needs restart!\n" );
//		fflush( outStream );
//		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
}


/**Function********************************************************************

  Synopsis    [Performs the AND or two BDDs]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
{
	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;
}

/**Function********************************************************************

  Synopsis    [Performs the AND or two BDDs]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, CloudNode * g )
{
	if ( f <= g )
		return cloudBddAnd(dd,f,g);
	else
		return cloudBddAnd(dd,g,f);
}

/**Function********************************************************************

  Synopsis    [Performs the AND or two BDDs]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
{
    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 );
}

/**Function********************************************************************

  Synopsis    [Performs the OR or two BDDs]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
{
	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;
}

/**Function********************************************************************

  Synopsis    [Performs the XOR or two BDDs]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g )
{
	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;
}



/**Function********************************************************************

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

  Description []

  SideEffects [None]

  SeeAlso     [cloudSupport cloudDagSize]

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

/**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     []

******************************************************************************/
static void cloudSupport( CloudManager * dd, CloudNode * n, int * support )
{
	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 );
}

/**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     []

******************************************************************************/
CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n )
{
	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;
}

/**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     []

******************************************************************************/
int Cloud_SupportSize( CloudManager * dd, CloudNode * n )
{
	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;
}


/**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]

******************************************************************************/
static int cloudDagSize( CloudManager * dd, CloudNode * n )
{
	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;

}

/**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     []

******************************************************************************/
int Cloud_DagSize( CloudManager * dd, CloudNode * n )
{
	int res;
	res = cloudDagSize( dd, Cloud_Regular( n ) );
	cloudClearMark( dd, Cloud_Regular( n ) );
	return res;

}


/**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]

******************************************************************************/
static int Cloud_DagCollect_rec( CloudManager * dd, CloudNode * n, int * pCounter )
{
	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;

}

/**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     []

******************************************************************************/
int Cloud_DagCollect( CloudManager * dd, CloudNode * n )
{
	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;

}

/**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     []

******************************************************************************/
int Cloud_SharingSize( CloudManager * dd, CloudNode ** pn, int nn )
{
	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;
}


/**Function********************************************************************

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

  Description []

  SideEffects []

******************************************************************************/
CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
{
	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;
}

/**Function********************************************************************

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

  Description []

  SideEffects []

******************************************************************************/
void Cloud_bddPrint( CloudManager * dd, CloudNode * Func )
{
	CloudNode * Cube;
	int fFirst = 1;

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

/**Function********************************************************************

  Synopsis    [Prints one cube.]

  Description []

  SideEffects []

******************************************************************************/
void Cloud_bddPrintCube( CloudManager * dd, CloudNode * bCube )
{
	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 );
			fprintf(outStream,  "[%d]'", cloudV(bCube) );
			bCube = bCube0;
		}
		else
		{
			assert( bCube1 != dd->zero );
			fprintf(outStream,  "[%d]", cloudV(bCube) );
			bCube = bCube1;
		}
	}
}


/**Function********************************************************************

  Synopsis    [Prints info.]

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function********************************************************************

  Synopsis    [Prints the state of the hash table.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void Cloud_PrintHashTable( CloudManager * dd )
{
	int i;

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


////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////

