Version abc80130

1 files changed, 0 insertions, 987 deletions

diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c
deleted file mode 100644
index 6e6691f0..00000000
--- a/src/aig/kit/cloud.c
+++ /dev/null
@@ -1,987 +0,0 @@
-/**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
-        printf( "Cloud needs restart!\n" );
-//        fflush( stdout );
-//        exit(1);
-        return CLOUD_VOID;
-    }
-    // create the node
-    entryUnique->s   = dd->nSignCur;
-    entryUnique->v   = v;
-    entryUnique->t   = t;
-    entryUnique->e   = e;
-    return entryUnique;  // returns the node
-}
-
-
-/**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 )
-        printf( "Constant 0." );
-    else if ( Func == dd->one )
-        printf( "Constant 1." );
-    else
-    {
-        while ( 1 )
-        {
-            Cube = Cloud_GetOneCube( dd, Func );
-            if ( Cube == CLOUD_VOID || Cube == dd->zero )
-                break;
-            if ( fFirst )       fFirst = 0;
-            else                printf( " + " );
-            Cloud_bddPrintCube( dd, Cube );
-            Func = Cloud_bddAnd( dd, Func, Cloud_Not(Cube) );
-        } 
-    }
-    printf( "\n" );
-}
-
-/**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 );
-            printf( "[%d]'", cloudV(bCube) );
-            bCube = bCube0;
-        }
-        else
-        {
-            assert( bCube1 != dd->zero );
-            printf( "[%d]", cloudV(bCube) );
-            bCube = bCube1;
-        }
-    }
-}
-
-
-/**Function********************************************************************
-
-  Synopsis    [Prints info.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-void Cloud_PrintInfo( CloudManager * dd )
-{
-    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 );
-}
-
-/**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 )
-            printf( "-" );
-        else
-            printf( "+" );
-    printf( "\n" );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-