summaryrefslogtreecommitdiffstats
path: root/src/bool/kit/cloud.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bool/kit/cloud.c')
-rw-r--r--src/bool/kit/cloud.c993
1 files changed, 993 insertions, 0 deletions
diff --git a/src/bool/kit/cloud.c b/src/bool/kit/cloud.c
new file mode 100644
index 00000000..1ab53c00
--- /dev/null
+++ b/src/bool/kit/cloud.c
@@ -0,0 +1,993 @@
+/**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 <string.h>
+#include "cloud.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+// 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 = 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 = clock();
+ dd->tUnique = ABC_CALLOC( CloudNode, dd->nNodesAlloc );
+ dd->nMemUsed += sizeof(CloudNode) * dd->nNodesAlloc;
+clk2 = 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;
+};
+
+/**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;
+ 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 );
+}
+
+/**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 *)ABC_CALLOC( CloudCacheEntry1, nCacheEntries );
+ dd->nMemUsed += sizeof(CloudCacheEntry1) * nCacheEntries;
+ }
+ else if ( CacheSize[oper] == 2 )
+ {
+ dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry2, nCacheEntries );
+ dd->nMemUsed += sizeof(CloudCacheEntry2) * nCacheEntries;
+ }
+ else if ( CacheSize[oper] == 3 )
+ {
+ dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_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 != NULL )
+ 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 NULL;
+ }
+ // 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 != NULL )
+ {
+ 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 == NULL )
+ return NULL;
+
+ if ( fnv <= gnv )
+ e = cloudBddAnd( dd, fnv, gnv );
+ else
+ e = cloudBddAnd( dd, gnv, fnv );
+
+ if ( e == NULL )
+ return NULL;
+
+ if ( t == e )
+ r = t;
+ else
+ {
+ if ( Cloud_IsComplement(t) )
+ {
+ r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
+ if ( r == NULL )
+ return NULL;
+ r = Cloud_Not(r);
+ }
+ else
+ {
+ r = cloudMakeNode( dd, var, t, e );
+ if ( r == NULL )
+ return NULL;
+ }
+ }
+ 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) == 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 );
+}
+
+/**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) == 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;
+}
+
+/**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) == 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 );
+ t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) );
+ if ( t0 == NULL )
+ return NULL;
+ t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
+ if ( t1 == NULL )
+ return NULL;
+ 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 = 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;
+}
+
+/**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 = 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;
+}
+
+
+/**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 = ABC_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 == 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;
+}
+
+/**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 == 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" );
+}
+
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:26:26 +0000