/**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 ABC__aig__kit__cloud_h
#define ABC__aig__kit__cloud_h
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <time.h>
#include "src/misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
#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_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)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s))
#define cloudHashCudd3(f,g,h,s) (((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s))
// node complementation (using node)
#define Cloud_Regular(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01)) // get the regular node (w/o bubble)
#define Cloud_Not(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ 01)) // complement the node
#define Cloud_NotCond(p,c) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c))) // complement the node conditionally
#define Cloud_IsComplement(p) ((int)(((ABC_PTRUINT_T)(p)) & 01)) // 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): (0))
#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))
#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))
// 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)
////////////////////////////////////////////////////////////////////////
/// 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 );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////