src/aig/kit/cloud.c

Go to the documentation of this file.

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


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

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

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



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

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
}


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

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

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

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



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

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


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

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

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

---