cloud.c

Go to the documentation of this file.

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

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


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

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

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

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

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

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

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
}
 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 
ABC_NAMESPACE_IMPL_END