src/aig/kit/cloud.h

Go to the documentation of this file.

#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

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

---