Version abc70909

7 files changed, 1929 insertions, 27 deletions

diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c
new file mode 100644
index 00000000..6e6691f0
--- /dev/null
+++ b/src/aig/kit/cloud.c
@@ -0,0 +1,987 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h
new file mode 100644
index 00000000..ac9d45f4
--- /dev/null
+++ b/src/aig/kit/cloud.h
@@ -0,0 +1,269 @@
+/**CFile****************************************************************
+
+  FileName    [cloud.h]
+
+  PackageName [Fast application-specific BDD package.]
+
+  Synopsis    [Interface of the package.]
+
+  Author      [Alan Mishchenko <alanmi@ece.pdx.edu>]
+  
+  Affiliation [ECE Department. Portland State University, Portland, Oregon.]
+
+  Date        [Ver. 1.0. Started - June 10, 2002.]
+
+  Revision    [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CLOUD_H__
+#define __CLOUD_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <time.h>
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+////////////////////////////////////////////////////////////////////////
+//  n |  2^n ||  n |    2^n ||  n |        2^n ||  n |           2^n  //
+//====================================================================//
+//  1 |    2 ||  9 |    512 || 17 |    131,072 || 25 |    33,554,432  //
+//  2 |    4 || 10 |  1,024 || 18 |    262,144 || 26 |    67,108,864  // 
+//  3 |    8 || 11 |  2,048 || 19 |    524,288 || 27 |   134,217,728  //
+//  4 |   16 || 12 |  4,096 || 20 |  1,048,576 || 28 |   268,435,456  //
+//  5 |   32 || 13 |  8,192 || 21 |  2,097,152 || 29 |   536,870,912  //
+//  6 |   64 || 14 | 16,384 || 22 |  4,194,304 || 30 | 1,073,741,824  //
+//  7 |  128 || 15 | 32,768 || 23 |  8,388,608 || 31 | 2,147,483,648  //
+//  8 |  256 || 16 | 65,536 || 24 | 16,777,216 || 32 | 4,294,967,296  //
+////////////////////////////////////////////////////////////////////////
+
+// data structure typedefs
+typedef struct cloudManager       CloudManager;
+typedef unsigned                  CloudVar;
+typedef unsigned                  CloudSign;
+typedef struct cloudNode          CloudNode;
+typedef struct cloudCacheEntry1   CloudCacheEntry1;
+typedef struct cloudCacheEntry2   CloudCacheEntry2;
+typedef struct cloudCacheEntry3   CloudCacheEntry3;
+
+// operation codes used to set up the cache
+typedef enum { 
+    CLOUD_OPER_AND, 
+    CLOUD_OPER_XOR, 
+    CLOUD_OPER_BDIFF, 
+    CLOUD_OPER_LEQ 
+} CloudOper;
+
+/*
+// 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] = {
+    4, // 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 
+};
+*/
+
+// data structure definitions
+struct cloudManager            // the fast bdd manager     
+{
+    // variables
+    int nVars;                 // the number of variables allocated
+    // bits
+    int bitsNode;              // the number of bits used for the node
+    int bitsCache[4];          // default: bitsNode - CacheSizeRatio[i]
+    // shifts
+    int shiftUnique;           // 8*sizeof(unsigned) - (bitsNode + 1)
+    int shiftCache[4];         // 8*sizeof(unsigned) -  bitsCache[i]
+    // nodes 
+    int nNodesAlloc;           // 2 ^ (bitsNode + 1)
+    int nNodesLimit;           // 2 ^  bitsNode
+    int nNodesCur;             // the current number of nodes (including const1 and vars)
+    // signature
+    CloudSign nSignCur;
+
+    // statistics
+    int nMemUsed;              // memory usage in bytes
+    // cache stats
+    int nUniqueHits;           // hits in the unique table
+    int nUniqueMisses;         // misses in the unique table
+    int nCacheHits;            // hits in the caches
+    int nCacheMisses;          // misses in the caches
+    // the number of steps through the hash table
+    int nUniqueSteps;
+
+    // tables
+    CloudNode * tUnique;       // the unique table to store BDD nodes
+
+    // special nodes
+    CloudNode * pNodeStart;    // the pointer to the first node
+    CloudNode * pNodeEnd;      // the pointer to the first node out of the table
+
+    // constants and variables
+    CloudNode *  one;          // the one function
+    CloudNode *  zero;         // the zero function
+    CloudNode ** vars;         // the elementary variables
+
+    // temporary storage for nodes
+    CloudNode ** ppNodes;
+
+    // caches
+    CloudCacheEntry2 * tCaches[20];    // caches
+};
+
+struct cloudNode   // representation of the node in the unique table
+{
+    CloudSign   s;         // signature
+    CloudVar    v;         // variable
+    CloudNode * e;         // negative cofactor
+    CloudNode * t;         // positive cofactor
+};
+struct cloudCacheEntry1  // one-argument cache
+{
+    CloudSign   s;         // signature
+    CloudNode * a;         // argument 1
+    CloudNode * r;         // result
+};
+struct cloudCacheEntry2  // the two-argument cache
+{
+    CloudSign   s;         // signature
+    CloudNode * a;
+    CloudNode * b;
+    CloudNode * r;
+};
+struct cloudCacheEntry3  // the three-argument cache
+{
+    CloudSign   s;         // signature
+    CloudNode * a;
+    CloudNode * b;
+    CloudNode * c;
+    CloudNode * r;
+};
+
+
+// parameters
+#define CLOUD_NODE_BITS              23
+#define CLOUD_ONE                    ((unsigned)0x00000001)
+#define CLOUD_NOT_ONE                ((unsigned)0xfffffffe)
+#define CLOUD_VOID                   ((unsigned)0x00000000)
+
+#define CLOUD_CONST_INDEX            ((unsigned)0x0fffffff)
+#define CLOUD_MARK_ON                ((unsigned)0x10000000)
+#define CLOUD_MARK_OFF               ((unsigned)0xefffffff)
+
+// hash functions a la Buddy
+#define cloudHashBuddy2(x,y,s)       ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))
+#define cloudHashBuddy3(x,y,z,s)     (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1))
+// hash functions a la Cudd
+#define DD_P1                           12582917
+#define DD_P2                         4256249
+#define DD_P3                         741457
+#define DD_P4                         1618033999
+#define cloudHashCudd2(f,g,s)        ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
+#define cloudHashCudd3(f,g,h,s)      (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s))
+
+// node complementation (using node)
+#define Cloud_Regular(p)             ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble)
+#define Cloud_Not(p)                 ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE))     // complement the node
+#define Cloud_NotCond(p,c)           (((int)(c))? Cloud_Not(p):(p))                  // complement the node conditionally
+#define Cloud_IsComplement(p)        ((int)(((unsigned)(p)) & CLOUD_ONE))            // check if complemented
+// checking constants (using node)
+#define Cloud_IsConstant(p)          (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
+#define cloudIsConstant(p)           (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
+
+// retrieving values from the node (using node structure)
+#define Cloud_V(p)                   ((Cloud_Regular(p))->v)
+#define Cloud_E(p)                   ((Cloud_Regular(p))->e)
+#define Cloud_T(p)                   ((Cloud_Regular(p))->t)
+// retrieving values from the regular node (using node structure)
+#define cloudV(p)                    ((p)->v)
+#define cloudE(p)                    ((p)->e)
+#define cloudT(p)                    ((p)->t)
+// marking/unmarking (using node structure)
+#define cloudNodeMark(p)             ((p)->v       |= CLOUD_MARK_ON)
+#define cloudNodeUnmark(p)           ((p)->v       &= CLOUD_MARK_OFF)
+#define cloudNodeIsMarked(p)         ((int)((p)->v &  CLOUD_MARK_ON))
+
+// cache lookups and inserts (using node)
+#define cloudCacheLookup1(p,sign,f)     (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID))
+#define cloudCacheLookup2(p,sign,f,g)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID))
+#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID))
+// cache inserts
+#define cloudCacheInsert1(p,sign,f,r)     (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))
+#define cloudCacheInsert2(p,sign,f,g,r)   (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))
+#define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r)))
+
+//#define CLOUD_ASSERT(p)              (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd))
+#define CLOUD_ASSERT(p)            assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc)
+
+// utility macros
+#ifndef ALLOC
+#define ALLOC(type, num)           ((type *) malloc(sizeof(type) * (num)))
+#endif
+
+#ifndef CALLOC
+#define CALLOC(type, num)           ((type *) calloc((num), sizeof(type)))
+#endif
+
+#ifndef FREE
+#define FREE(obj)                   ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#endif
+
+#ifndef PRT
+#define PRT(a,t)                   fprintf( stdout, "%s = ", (a)); printf( "%.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       FUNCTION DECLARATIONS                      ///
+////////////////////////////////////////////////////////////////////////
+// starting/stopping 
+extern CloudManager * Cloud_Init( int nVars, int nBits );
+extern void           Cloud_Quit( CloudManager * dd );
+extern void           Cloud_Restart( CloudManager * dd );
+extern void           Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size );
+extern CloudNode *    Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
+// support and node count
+extern CloudNode *    Cloud_Support( CloudManager * dd, CloudNode * n );
+extern int            Cloud_SupportSize( CloudManager * dd, CloudNode * n );
+extern int            Cloud_DagSize( CloudManager * dd, CloudNode * n );
+extern int            Cloud_DagCollect( CloudManager * dd, CloudNode * n );
+extern int            Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn );
+// cubes
+extern CloudNode *    Cloud_GetOneCube( CloudManager * dd, CloudNode * n );
+extern void           Cloud_bddPrint( CloudManager * dd, CloudNode * Func );
+extern void           Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube );
+// operations
+extern CloudNode *    Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g );
+extern CloudNode *    Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g );
+// stats 
+extern void           Cloud_PrintInfo( CloudManager * dd );
+extern void           Cloud_PrintHashTable( CloudManager * dd );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                            END OF FILE                           ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 2ad9a6f0..06a93cf0 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -36,6 +36,7 @@ extern "C" {
 #include <time.h>
 #include "vec.h"
 #include "extra.h"
+#include "cloud.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -133,6 +134,10 @@ struct Kit_DsdMan_t_
     int            nWords;          // the number of words in TTs
     Vec_Ptr_t *    vTtElems;        // elementary truth tables
     Vec_Ptr_t *    vTtNodes;        // the node truth tables
+    // BDD representation
+    CloudManager * dd;              // BDD package
+    Vec_Ptr_t *    vTtBdds;         // the node truth tables
+    Vec_Int_t *    vNodes;          // temporary array for BDD nodes
 };
 
 static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
@@ -431,6 +436,16 @@ static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pI
     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
 }
+static inline void Kit_TruthMuxPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars, int fComp0 )
+{
+    int w;
+    if ( fComp0 )
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
+    else
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
+}
 static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
 {
     unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
@@ -473,11 +488,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
 extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
 extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
+/*=== kitCloud.c ==========================================================*/
+extern CloudNode *     Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars );
+extern unsigned *      Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv );
+extern int             Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes );
+extern int             Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes );
+extern unsigned *      Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes );
+extern void            Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps );
 /*=== kitDsd.c ==========================================================*/
 extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars, int nNodes );
 extern void            Kit_DsdManFree( Kit_DsdMan_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
-extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
+extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
 extern void            Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
 extern void            Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
@@ -485,10 +507,12 @@ extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
+extern Kit_DsdNtk_t *  Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars );
 extern Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
 extern void            Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
 extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
+extern unsigned        Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdGetSupports( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
@@ -548,6 +572,7 @@ extern void            Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, i
 extern void            Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
 extern void            Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
+extern void            Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 );
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern int             Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
diff --git a/src/aig/kit/kitCloud.c b/src/aig/kit/kitCloud.c
new file mode 100644
index 00000000..7b160fea
--- /dev/null
+++ b/src/aig/kit/kitCloud.c
@@ -0,0 +1,368 @@
+/**CFile****************************************************************
+
+  FileName    [kitCloud.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation kit.]
+
+  Synopsis    [Procedures using BDD package CLOUD.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 6, 2006.]
+
+  Revision    [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// internal representation of the function to be decomposed
+typedef struct Kit_Mux_t_ Kit_Mux_t;
+struct Kit_Mux_t_
+{
+    unsigned      v  :  5;          // variable 
+    unsigned      t  : 12;          // then edge
+    unsigned      e  : 12;          // else edge
+    unsigned      c  :  1;          // complemented attr of else edge
+    unsigned      i  :  1;          // complemented attr of top node
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derive BDD from the truth table for 5 variable functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
+{
+    static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    CloudNode * pCof0, * pCof1;
+    unsigned uCof0, uCof1;
+    assert( nVars <= 5 );
+    if ( uTruth == 0 )
+        return dd->zero;
+    if ( uTruth == ~0 )
+        return dd->one;
+    if ( nVars == 1 )
+    {
+        if ( uTruth == uVars[0] )
+            return dd->vars[nVarsAll-1];
+        if ( uTruth == ~uVars[0] )
+            return Cloud_Not(dd->vars[nVarsAll-1]);
+        assert( 0 );
+    }
+//    Count++;
+    assert( nVars > 1 );
+    uCof0 = uTruth & ~uVars[nVars-1];
+    uCof1 = uTruth &  uVars[nVars-1];
+    uCof0 |= uCof0 << (1<<(nVars-1));
+    uCof1 |= uCof1 >> (1<<(nVars-1));
+    if ( uCof0 == uCof1 )
+        return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+    if ( uCof0 == ~uCof1 )
+    {
+        pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+        pCof1 = Cloud_Not( pCof0 );
+    }
+    else
+    {
+        pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+        pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
+    }
+    return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Compute BDD for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
+{
+    CloudNode * pCof0, * pCof1;
+    unsigned * pTruth0, * pTruth1;
+    if ( nVars <= 5 )
+        return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
+    if ( Kit_TruthIsConst0(pTruth, nVars) )
+        return dd->zero;
+    if ( Kit_TruthIsConst1(pTruth, nVars) )
+        return dd->one;
+//    Count++;
+    pTruth0 = pTruth;
+    pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
+    if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
+        return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+    if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
+    {
+        pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+        pCof1 = Cloud_Not( pCof0 );
+    }
+    else
+    {
+        pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+        pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
+    }
+    return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Compute BDD for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
+{
+    CloudNode * pRes;
+    pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
+//    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
+    return pRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Transforms the array of BDDs into the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
+{
+    Kit_Mux_t Mux;
+    int nNodes, i;
+    // collect BDD nodes
+    nNodes = Cloud_DagCollect( dd, pFunc );
+    if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
+        return 0;
+    assert( nNodes == Cloud_DagSize( dd, pFunc ) );
+    assert( nNodes < dd->nNodesLimit );
+    Vec_IntClear( vNodes );
+    Vec_IntPush( vNodes, 0 ); // const1 node
+    dd->ppNodes[0]->s = 0;
+    for ( i = 1; i < nNodes; i++ )
+    {
+        dd->ppNodes[i]->s = i;
+        Mux.v = dd->ppNodes[i]->v;
+        Mux.t = dd->ppNodes[i]->t->s;
+        Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
+        Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); 
+        Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
+        // put the MUX into the array
+        Vec_IntPush( vNodes, *((int *)&Mux) );
+    }
+    assert( Vec_IntSize(vNodes) == nNodes );
+    // reset signatures
+    for ( i = 0; i < nNodes; i++ )
+        dd->ppNodes[i]->s = dd->nSignCur;
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Transforms the array of BDDs into the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
+{
+    CloudNode * pFunc;
+    Cloud_Restart( dd );
+    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
+    Vec_IntClear( vNodes );
+    return Kit_CreateCloud( dd, pFunc, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes composition of truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
+{
+    unsigned * pThis, * pFan0, * pFan1;
+    Kit_Mux_t Mux;
+    int i, Entry;
+    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
+    pThis = Vec_PtrEntry( vStore, 0 );
+    Kit_TruthFill( pThis, nVars );
+    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+        assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
+        pFan0 = Vec_PtrEntry( vStore, Mux.e );
+        pFan1 = Vec_PtrEntry( vStore, Mux.t );
+        pThis = Vec_PtrEntry( vStore, i );
+        Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
+    } 
+    // complement the result
+    if ( Mux.i )
+        Kit_TruthNot( pThis, pThis, nVars );
+    return pThis;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes composition of truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, 
+    unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
+{
+    CloudNode * pFunc;
+    unsigned * pThis, * pFan0, * pFan1;
+    Kit_Mux_t Mux;
+    int i, Entry, RetValue;
+    // derive BDD from truth table
+    Cloud_Restart( dd );
+    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
+    // convert it into nodes
+    RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
+    if ( RetValue == 0 )
+        printf( "Kit_TruthCompose(): Internal failure!!!\n" );
+    // verify the result
+//    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
+//    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
+//        printf( "Failed!\n" );
+    // compute truth table from the BDD
+    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
+    pThis = Vec_PtrEntry( vStore, 0 );
+    Kit_TruthFill( pThis, nVarsAll );
+    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+        pFan0 = Vec_PtrEntry( vStore, Mux.e );
+        pFan1 = Vec_PtrEntry( vStore, Mux.t );
+        pThis = Vec_PtrEntry( vStore, i );
+        Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
+    }
+    // complement the result
+    if ( Mux.i )
+        Kit_TruthNot( pThis, pThis, nVarsAll );
+    return pThis;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Compute BDD for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
+{
+    Kit_Mux_t Mux;
+    unsigned * puSuppAll, * pThis, * pFan0, * pFan1;
+    int i, v, Var, Entry, nSupps;
+    nSupps = 2 * nVars;
+
+    // extend storage
+    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
+        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
+    puSuppAll = Vec_IntArray( vMemory );
+    // clear storage for the const node
+    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
+    // compute supports from nodes
+    Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+        Var = nVars - 1 - Mux.v;
+        pFan0 = puSuppAll + nSupps * Mux.e;
+        pFan1 = puSuppAll + nSupps * Mux.t;
+        pThis = puSuppAll + nSupps * i;
+        for ( v = 0; v < nSupps; v++ )
+            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
+        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
+        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
+        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
+        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
+    }
+    // copy the result
+    memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
+    // compute the inverse
+
+    // extend storage
+    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
+        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
+    puSuppAll = Vec_IntArray( vMemory );
+    // clear storage for the const node
+    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
+    // compute supports from nodes
+    Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+//        Var = nVars - 1 - Mux.v;
+        Var = Mux.v;
+        pFan0 = puSuppAll + nSupps * Mux.e;
+        pFan1 = puSuppAll + nSupps * Mux.t;
+        pThis = puSuppAll + nSupps * i;
+        for ( v = 0; v < nSupps; v++ )
+            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
+        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
+        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
+        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
+        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
+    }
+
+    // merge supports
+    for ( Var = 0; Var < nSupps; Var++ )
+        puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 9c61bb6f..ada4ef09 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -44,10 +44,13 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
     Kit_DsdMan_t * p;
     p = ALLOC( Kit_DsdMan_t, 1 );
     memset( p, 0, sizeof(Kit_DsdMan_t) );
-    p->nVars = nVars;
-    p->nWords = Kit_TruthWordNum( p->nVars );
+    p->nVars    = nVars;
+    p->nWords   = Kit_TruthWordNum( p->nVars );
     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
     p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
+    p->dd       = Cloud_Init( 16, 13 );
+    p->vTtBdds  = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
+    p->vNodes   = Vec_IntAlloc( 512 );
     return p;
 }
 
@@ -64,6 +67,9 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
 ***********************************************************************/
 void Kit_DsdManFree( Kit_DsdMan_t * p )
 {
+    Cloud_Quit( p->dd );
+    Vec_IntFree( p->vNodes );
+    Vec_PtrFree( p->vTtBdds );
     Vec_PtrFree( p->vTtElems );
     Vec_PtrFree( p->vTtNodes );
     free( p );
@@ -315,11 +321,140 @@ void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
+unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
 {
     Kit_DsdObj_t * pObj;
-    unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
-    unsigned i, m, iLit, nMints, fCompl, nPartial = 0;
+    unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
+    unsigned i, iLit, fCompl;
+//    unsigned m, nMints, * pTruthPrime, * pTruthMint; 
+
+    // get the node with this ID
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
+
+    // special case: literal of an internal node
+    if ( pObj == NULL )
+    {
+        assert( Id < pNtk->nVars );
+        return pTruthRes;
+    }
+
+    // constant node
+    if ( pObj->Type == KIT_DSD_CONST1 )
+    {
+        assert( pObj->nFans == 0 );
+        Kit_TruthFill( pTruthRes, pNtk->nVars );
+        return pTruthRes;
+    }
+
+    // elementary variable node
+    if ( pObj->Type == KIT_DSD_VAR )
+    {
+        assert( pObj->nFans == 1 );
+        iLit = pObj->pFans[0];
+        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+        if ( Kit_DsdLitIsCompl(iLit) )
+            Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
+        else
+            Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
+        return pTruthRes;
+    }
+
+    // collect the truth tables of the fanins
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+    // create the truth table
+
+    // simple gates
+    if ( pObj->Type == KIT_DSD_AND )
+    {
+        Kit_TruthFill( pTruthRes, pNtk->nVars );
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
+        return pTruthRes;
+    }
+    if ( pObj->Type == KIT_DSD_XOR )
+    {
+        Kit_TruthClear( pTruthRes, pNtk->nVars );
+        fCompl = 0;
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        {
+            Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
+            fCompl ^= Kit_DsdLitIsCompl(iLit);
+        }
+        if ( fCompl )
+            Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+        return pTruthRes;
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+/*
+    // get the truth table of the prime node
+    pTruthPrime = Kit_DsdObjTruth( pObj );
+    // get storage for the temporary minterm
+    pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
+
+    // go through the minterms
+    nMints = (1 << pObj->nFans);
+    Kit_TruthClear( pTruthRes, pNtk->nVars );
+    for ( m = 0; m < nMints; m++ )
+    {
+        if ( !Kit_TruthHasBit(pTruthPrime, m) )
+            continue;
+        Kit_TruthFill( pTruthMint, pNtk->nVars );
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
+        Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
+    }
+*/
+    pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
+    Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
+    return pTruthRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
+{
+    unsigned * pTruthRes;
+    int i;
+    // assign elementary truth ables
+    assert( pNtk->nVars <= p->nVars );
+    for ( i = 0; i < (int)pNtk->nVars; i++ )
+        Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+    // compute truth table for each node
+    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
+    // complement the truth table if needed
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+    return pTruthRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the DSD node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
+    unsigned i, iLit, fCompl, nPartial = 0;
+//    unsigned m, nMints, * pTruthPrime, * pTruthMint; 
 
     // get the node with this ID
     pObj = Kit_DsdNtkObj( pNtk, Id );
@@ -347,7 +482,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
         assert( pObj->nFans == 1 );
         iLit = pObj->pFans[0];
         assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
-        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+        pTruthFans[0] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
         if ( Kit_DsdLitIsCompl(iLit) )
             Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
         else
@@ -360,7 +495,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     {
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
             if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
-                pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+                pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
             else
             {
                 pTruthFans[i] = NULL;
@@ -370,7 +505,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     else
     {
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
-            pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+            pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
     }
     // create the truth table
 
@@ -410,7 +545,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
         assert( i < pObj->nFans );
         return pTruthFans[i];
     }
-
+/*
     // get the truth table of the prime node
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
@@ -428,6 +563,9 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
             Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
+*/
+    pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
+    Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
 }
 
@@ -442,7 +580,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
+unsigned * Kit_DsdTruthComputeOne( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
 {
     unsigned * pTruthRes;
     int i;
@@ -454,7 +592,7 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
     for ( i = 0; i < (int)pNtk->nVars; i++ )
         Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
     // compute truth table for each node
-    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
+    pTruthRes = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
     // complement the truth table if needed
     if ( Kit_DsdLitIsCompl(pNtk->Root) )
         Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
@@ -475,9 +613,10 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
 unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec )
 {
     Kit_DsdObj_t * pObj;
-    unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
-    unsigned i, m, iLit, nMints, fCompl, uSuppCur, uSuppFan, nPartial;
     int pfBoundSet[16];
+    unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
+    unsigned i, iLit, fCompl, nPartial, uSuppFan, uSuppCur;
+//    unsigned m, nMints, * pTruthPrime, * pTruthMint; 
     assert( uSupp > 0 );
 
     // get the node with this ID
@@ -507,7 +646,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
 
     // if there is no intersection, or full intersection, use simple procedure
     if ( nPartial == 0 || nPartial == pObj->nFans )
-        return Kit_DsdTruthComputeNode_rec( p, pNtk, Id, 0 );
+        return Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Id, 0 );
 
     // if support of the component includes some other variables
     // we need to continue constructing it as usual by the two-function procedure
@@ -520,7 +659,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
             if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) )
                 pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp, iVar, pTruthDec );
             else
-                pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
+                pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
         }
 
         // create composition/decomposition functions
@@ -556,7 +695,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
         // solve the fanins and collect info, which components belong to the bound set
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
         {
-            pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
+            pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
             pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0);
         }
 
@@ -603,7 +742,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
         // set the corresponding component to be the new variable
         Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar );
     }
-
+/*
     // get the truth table of the prime node
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
@@ -621,6 +760,11 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
             Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
+*/
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        assert( !Kit_DsdLitIsCompl(iLit) );
+    pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
+    Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
 }
 
@@ -647,12 +791,12 @@ unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsign
     if ( (uSupp & uSuppAll) == 0 )
     {
         Kit_TruthClear( pTruthDec, pNtk->nVars );
-        return Kit_DsdTruthCompute( p, pNtk, 0 );
+        return Kit_DsdTruthCompute( p, pNtk );
     }
     // consider special case - support is fully contained
     if ( (uSupp & uSuppAll) == uSuppAll )
     {
-        pTruthRes = Kit_DsdTruthCompute( p, pNtk, 0 );
+        pTruthRes = Kit_DsdTruthCompute( p, pNtk );
         Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars );
         Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
         return pTruthRes;
@@ -684,7 +828,7 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
     Kit_DsdMan_t * p;
     unsigned * pTruth;
     p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
-    pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruth = Kit_DsdTruthCompute( p, pNtk );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
     Kit_DsdManFree( p );
 }
@@ -720,7 +864,7 @@ void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSu
 ***********************************************************************/
 void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
 {
-    unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
+    unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
 /*
     // verification
@@ -836,6 +980,32 @@ int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
     return nSizeMax;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Finds the union of supports of the non-DSD blocks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned i, uSupport = 0;
+//    FREE( pNtk->pSupps );
+    Kit_DsdGetSupports( pNtk );
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        if ( pObj->Type != KIT_DSD_PRIME )
+            continue;
+        uSupport |= Kit_DsdLitSupport( pNtk, Kit_DsdVar2Lit(pObj->Id,0) );
+    }
+    return uSupport;
+}
+
 
 /**Function*************************************************************
 
@@ -1759,6 +1929,26 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 
   Synopsis    [Performs decomposition of the truth table.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pNtk, * pTemp;
+    pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 );
+    pNtk = Kit_DsdExpand( pTemp = pNtk );      
+    Kit_DsdNtkFree( pTemp );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
   Description [Uses MUXes to break-down large prime nodes.]
                
   SideEffects []
@@ -1867,7 +2057,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
 
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
@@ -1892,7 +2082,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
     Kit_DsdMan_t * p;
     unsigned * pTruthC;
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
@@ -1934,7 +2124,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
 //    Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
 //    Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
     if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
@@ -2004,7 +2194,7 @@ void Kit_DsdPrecompute4Vars()
 */
 
         p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
-        pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+        pTruthC = Kit_DsdTruthCompute( p, pNtk );
         if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
             printf( "Verification failed.\n" );
         Kit_DsdManFree( p );
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index d196b455..65389ef9 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -901,6 +901,68 @@ void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int n
 
 /**Function*************************************************************
 
+  Synopsis    [Multiplexes two functions with the given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    if ( fCompl0 == 0 )
+    {
+        Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
+        return;
+    }
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pOut[i]      = ~pCof0[i];
+                pOut[Step+i] = pCof1[Step+i];
+            }
+            pOut += 2*Step;
+            pCof0 += 2*Step;
+            pCof1 += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks symmetry of two variables.]
 
   Description []
@@ -1623,7 +1685,7 @@ char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
 {
     static char pFileName[100];
     FILE * pFile;
-    sprintf( pFileName, "s%03d", nFile );
+    sprintf( pFileName, "tt\\s%04d", nFile );
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "rt " );
     Extra_PrintHexadecimal( pFile, pTruth, nVars );
diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make
index a01690d0..25c8e767 100644
--- a/src/aig/kit/module.make
+++ b/src/aig/kit/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/aig/kit/kitBdd.c \
+    src/aig/kit/kitCloud.c src/aig/kit/cloud.c \
     src/aig/kit/kitDsd.c \
     src/aig/kit/kitFactor.c \
     src/aig/kit/kitGraph.c \