glu-2.2: src/calBdd/calInt.h Source File

00001 
00039 #ifndef _CALINT
00040 #define _CALINT
00041 
00042 #include "cal.h"
00043 
00044 /* Make sure variable argument lists work */
00045 #if HAVE_STDARG_H
00046 #  include <stdarg.h>
00047 #else
00048 #  if HAVE_VARARGS_H
00049 #    include <varargs.h>
00050 #  else
00051 #    error "Need to have HAVE_STDARG_H or HAVE_VARARGS_H defined for variable arguments"
00052 #  endif
00053 #endif
00054 
00055 
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Constant declarations                                                     */
00059 /*---------------------------------------------------------------------------*/
00060 /* Begin Performance Related Constants */
00061 
00062 /* Garbage collection and reordering related constants */
00063 /* The following constants could significantly affect the
00064    performance of the package */ 
00065 
00066 
00067 #define CAL_MIN_GC_LIMIT 10000 /* minimum number of nodes in the unique table
00068                                   before performing garbage collection. It can
00069                                   be overridden by user define node limit */
00070 
00071 
00072 
00073 
00074 #define CAL_REPACK_AFTER_GC_THRESHOLD 0.75 /* If the number of nodes fall below
00075                                            this factor after garbage
00076                                            collection, repacking should be
00077                                            done */ 
00078 /* A note about repacking after garbage collection: Since repacking
00079 ** moves the node pointers, it is important that "user" does not have
00080 ** access to internal node pointers during such times. If for some
00081 ** purposes the node handle is needed and also there is a possibility of
00082 ** garbage collection being invoked, this field (repackAfterGCThreshold) of
00083 ** the bdd manager should be set to 0.
00084 */
00085 
00086 #define CAL_TABLE_REPACK_THRESHOLD 0.9 /* If the page utility of a unique
00087                                             table (for some id) goes below this, repacking
00088                                             would be done */ 
00089 
00090 #define CAL_BDD_REORDER_THRESHOLD 10000 /* Don't perform reordering below these
00091                                            many nodes */
00092 
00093 #define CAL_NUM_PAGES_THRESHOLD 3
00094 
00095 #define CAL_NUM_FORWARDED_NODES_LIMIT 50000 /* maximum number of forwarded nodes 
00096                                                allowed during BF reordering */
00097 
00098 #define CAL_GC_CHECK 100       /* garbage collection check performed after
00099                                   addition of every GC_CHECK number of nodes to
00100                                   the unique table */
00101 
00102 /* End Performance Related Constants */
00103 
00104 /* Memory Management related constants */
00105 #define NODE_SIZE sizeof(CalBddNode_t)          /* sizeof(CalBddNode_t) */
00106 
00107 #ifndef PAGE_SIZE
00108 #  define PAGE_SIZE 4096        /* size of a virtual memory page */
00109 #endif
00110 #ifndef LG_PAGE_SIZE
00111 #  define LG_PAGE_SIZE 12       /* log2 of the page size */
00112 #endif
00113 
00114 #define NUM_NODES_PER_PAGE (PAGE_SIZE/NODE_SIZE)
00115 
00116 #define MAX_NUM_SEGMENTS 32 
00117 #define NUM_PAGES_PER_SEGMENT 64 /* We start with grabbing 64 pages at a time */
00118 #define MIN_NUM_PAGES_PER_SEGMENT 4
00119 #define MAX_NUM_PAGES 10
00120 
00121 #define MIN_REC_SIZE CAL_ALLOC_ALIGNMENT
00122 #define MAX_REC_SIZE (sizeof(CalHashTable_t)) /* size of hash table */
00123 #define NUM_REC_MGRS (((MAX_REC_SIZE-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT)+1)
00124 
00125 
00126 
00127 
00128 /* true / false */
00129 #ifndef TRUE
00130 #define TRUE 1
00131 #endif
00132 #ifndef FALSE
00133 #define FALSE 0
00134 #endif
00135 
00136 
00137 
00138 
00139 /* Error Codes */
00140 #define CAL_BDD_OK 0
00141 #define CAL_BDD_OVERFLOWED 1
00142 
00143 /* bdd variable id and index related constants */
00144 #define CAL_BDD_NULL_ID ((unsigned short) ((1 << 8*sizeof(unsigned short)) - 1))
00145 #define CAL_BDD_CONST_ID 0
00146 #define CAL_MAX_VAR_ID ((unsigned short) (CAL_BDD_NULL_ID - 1))
00147 #define CAL_BDD_NULL_INDEX (unsigned short) ((1 << 8*sizeof(unsigned short)) - 1)
00148 #define CAL_BDD_CONST_INDEX CAL_BDD_NULL_INDEX
00149 #define CAL_MAX_VAR_INDEX (CAL_BDD_NULL_INDEX - 1)
00150 #define CAL_MAX_REF_COUNT (unsigned short)((1 << 8*sizeof(char)) - 1)
00151 #define CAL_INFINITY (1 << 20)
00152 
00153 /* Pipeline related constants */
00154 #define MAX_INSERT_DEPTH 256
00155 #define PIPELINE_EXECUTION_DEPTH 1
00156 #define DEFAULT_DEPTH 4
00157 #define DEFAULT_MAX_DEPTH 6
00158 
00159 
00160 #define FORWARD_FLAG 0     /* Flag used to identify redundant nodes */
00161 
00162 
00163 /* Hash table management related constants. */
00164 #define HASH_TABLE_DEFAULT_MAX_DENSITY 5
00165 #define HASH_TABLE_DEFAULT_SIZE_INDEX 8
00166 #define HASH_TABLE_DEFAULT_NUM_BINS TABLE_SIZE(HASH_TABLE_DEFAULT_SIZE_INDEX)
00167 #define HASH_TABLE_DEFAULT_MAX_CAPACITY HASH_TABLE_DEFAULT_NUM_BINS*HASH_TABLE_DEFAULT_MAX_DENSITY
00168 extern unsigned long calPrimes[];
00169 
00170 #define USE_POWER_OF_2
00171 #ifdef  USE_POWER_OF_2
00172 #define TABLE_SIZE(sizeIndex) (1<<sizeIndex)
00173 #else
00174 #define TABLE_SIZE(sizeIndex) (calPrimes[sizeIndex])
00175 #endif
00176 
00177 
00178 /* Codes to be used in cache table */
00179 #define  CAL_OP_INVALID 0x0000
00180 #define  CAL_OP_OR 0x1000
00181 #define  CAL_OP_AND 0x2000
00182 #define  CAL_OP_NAND 0x3000
00183 #define  CAL_OP_QUANT 0x4000
00184 #define  CAL_OP_REL_PROD 0x5000
00185 #define  CAL_OP_COMPOSE 0x6000
00186 #define  CAL_OP_SUBST 0x7000
00187 #define  CAL_OP_VAR_SUBSTITUTE 0x8000
00188 
00189 #define  CAL_LARGE_BDD (1<<19) /* For smaller BDDs, we would
00190                                   use depth-first exist and forall routines */
00191 
00192 
00193 /*---------------------------------------------------------------------------*/
00194 /* Type declarations                                                         */
00195 /*---------------------------------------------------------------------------*/
00196 typedef struct Cal_BddStruct Cal_Bdd_t;
00197 typedef struct CalBddNodeStruct CalBddNode_t;
00198 typedef unsigned short Cal_BddRefCount_t;
00199 typedef struct CalPageManagerStruct CalPageManager_t;
00200 typedef struct CalNodeManagerStruct CalNodeManager_t;
00201 typedef struct CalListStruct CalList_t;
00202 typedef struct CalHashTableStruct CalHashTable_t;
00203 typedef struct CalHashTableStruct *CalReqQueForId_t;
00204 typedef struct CalHashTableStruct CalReqQueForIdAtDepth_t;
00205 typedef struct CalAssociationStruct CalAssociation_t;
00206 typedef struct CalBddNodeStruct CalRequestNode_t;
00207 typedef struct Cal_BddStruct CalRequest_t;
00208 typedef struct CalCacheTableStruct CalCacheTable_t;
00209 typedef int (*CalBddNodeToIndexFn_t)(CalBddNode_t*, Cal_BddId_t);
00210 typedef unsigned long CalAddress_t;
00211 typedef struct Cal_BlockStruct Cal_Block_t;
00212 
00213 struct Cal_BddStruct {
00214   Cal_BddId_t bddId;      /* variable id */
00215   CalBddNode_t *bddNode;  /* pointer to the bdd node */
00216 };
00217 
00218 typedef int (*CalOpProc_t) (Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t, Cal_Bdd_t *); 
00219 typedef int (*CalOpProc1_t) (Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t *); 
00220 
00221 
00222 /*---------------------------------------------------------------------------*/
00223 /* Stucture declarations                                                     */
00224 /*---------------------------------------------------------------------------*/
00225 
00226 enum CalPipeStateEnum { READY, CREATE, UPDATE };
00227 typedef enum CalPipeStateEnum CalPipeState_t;
00228 
00229 struct CalNodeManagerStruct{
00230   CalPageManager_t *pageManager;
00231   CalBddNode_t *freeNodeList;
00232   int numPages;
00233   int maxNumPages;
00234   CalAddress_t **pageList;
00235 };
00236 
00237 struct CalPageManagerStruct {
00238   CalAddress_t *freePageList;
00239   CalAddress_t **pageSegmentArray; /* Array of pointers to segments */
00240   int *numPagesArray; /* Number of pages in each segment */
00241   int numSegments;
00242   int totalNumPages; /* Total number of pages = sum of elements of numPagesArray */
00243   int numPagesPerSegment;
00244   int maxNumSegments;
00245 };
00246 
00247 struct CalBddNodeStruct {
00248   CalBddNode_t *nextBddNode; /* Attn: CalPageManagerFreePage overwrites this field of the node. Hence need to be aware of the consequences if the order of the fields is changed */
00249 
00250   CalBddNode_t *thenBddNode;
00251   CalBddNode_t *elseBddNode;
00252   Cal_BddId_t thenBddId;
00253   Cal_BddId_t elseBddId;
00254 };
00255 
00256 struct CalHashTableStruct {
00257   int sizeIndex;
00258   long numBins;
00259   long maxCapacity;
00260   CalBddNode_t **bins;
00261   Cal_BddId_t bddId;
00262   CalNodeManager_t *nodeManager;
00263   CalBddNode_t *requestNodeList;
00264  /* The following two fields are added to improve the performance of hash table clean up.*/
00265   CalBddNode_t startNode;
00266   CalBddNode_t *endNode;
00267   long numEntries;
00268 };
00269 
00270 struct CalAssociationStruct {
00271   Cal_Bdd_t *varAssociation;
00272   int lastBddIndex;
00273   int id;
00274   int refCount;
00275   CalAssociation_t *next;
00276 };
00277 
00278 struct Cal_BlockStruct
00279 {
00280   long numChildren;
00281   Cal_Block_t **children;
00282   int reorderable;
00283   long firstIndex;
00284   long lastIndex;
00285 };
00286 
00287 /* Cal_BddManager_t - manages the BDD nodes */
00288 struct Cal_BddManagerStruct {
00289 
00290   int numVars; /*
00291                 * Number of BDD variables present in the manager. This does
00292                 * not include the constant. The maximum number of variables 
00293                 * manager can have is CAL_MAX_VAR_ID (as opposed to
00294                 CAL_MAX_VAR_ID+1, id "0" being used for constant).
00295                 * CAL_MAX_VAR_ID = (((1 << 16) - 1) -1 )
00296                 */
00297   int maxNumVars; /* Maximum number of variables which can be created without
00298                      reallocating memory */
00299 
00300   Cal_Bdd_t *varBdds; /* Array of Cal_Bdd_t's. Cal_Bdd_t[i] is the BDD
00301                          corresponding to variable with id "i". */
00302   
00303   /* memory management */
00304   CalPageManager_t *pageManager1;  /* manages memory pages */
00305   CalPageManager_t *pageManager2;  /* manages memory pages */
00306   CalNodeManager_t **nodeManagerArray; /*
00307                                         * nodeManagerArray[i] is the node
00308                                         * manager for the variable with id = i.
00309                                         */     
00310   /* special nodes */
00311   Cal_Bdd_t bddOne; /* Constant: Id = 0; Index = CAL_MAX_INDEX */
00312   Cal_Bdd_t bddZero;
00313   Cal_Bdd_t bddNull;
00314   CalBddNode_t *userOneBdd;
00315   CalBddNode_t *userZeroBdd;
00316 
00317   Cal_BddId_t *indexToId; /*
00318                            * Table mapping index to id. If there are n
00319                            * variables, then this table has n entries from
00320                            * 0 to n-1 (indexToId[0] through indexToId[n-1]).
00321                            */
00322   Cal_BddIndex_t *idToIndex; /*
00323                               * Table mapping id to index:
00324                               * idToIndex[0] = CAL_MAX_INDEX
00325                               * If there are n variables in the manager, then
00326                               * corresponding to these variables this table
00327                               * has entries from 1 to n (idToIndex[1] through
00328                               * idToIndex[n]).
00329                               */
00330   
00331   CalHashTable_t **uniqueTable; /* uniqueTable[i] is the unique table for the
00332                                  * variable id " i". Unique table for an id is
00333                                  * a hash table of the nodes with that
00334                                  * variable id.
00335                                  */
00336   CalCacheTable_t *cacheTable; /* Computed table */
00337 
00338   /* Special functions */
00339   void (*TransformFn) (Cal_BddManager_t*, CalAddress_t, CalAddress_t,
00340        CalAddress_t*, CalAddress_t*, Cal_Pointer_t);
00341   Cal_Pointer_t transformEnv;
00342 
00343   /* logic operation management */
00344   CalHashTable_t ***reqQue;     /* reqQue[depth][id] is the hash table of
00345                                  * requests corresponding to variable id "id"
00346                                  * and the request depth "depth".
00347                                  */
00348                                
00349   /* Pipeline related information */
00350   int depth;
00351   int maxDepth;
00352   CalPipeState_t pipelineState;
00353   CalOpProc_t pipelineFn;
00354   int pipelineDepth;
00355   int currentPipelineDepth;
00356   CalRequestNode_t **requestNodeArray;/* Used for pipelined operations. */
00357   CalRequestNode_t *userProvisionalNodeList;   /* List of user BDD nodes
00358                                                   pointing to provisional
00359                                                   BDDs */
00360   CalRequestNode_t **requestNodeListArray;
00361   
00362 
00363   /* garbage collection related information */
00364   unsigned long numNodes;
00365   unsigned long numPeakNodes;
00366   unsigned long numNodesFreed;
00367   int gcCheck;
00368   unsigned long uniqueTableGCLimit;
00369   int  numGC;
00370   int gcMode;
00371   unsigned long nodeLimit;
00372   int overflow;
00373   float repackAfterGCThreshold;
00374   
00375 
00376   /* Association related stuff */
00377   CalAssociation_t *currentAssociation;
00378   CalAssociation_t *associationList;
00379   CalAssociation_t *tempAssociation;
00380   unsigned short tempOpCode; /* To store the id of temporary associations. */
00381   
00382   /* Variable reordering related stuff */
00383   long *interact; /* Interaction matrix */
00384   int dynamicReorderingEnableFlag;
00385   int reorderMethod;
00386   int reorderTechnique;
00387   long numForwardedNodes;
00388   int numReorderings;
00389   long maxNumVarsSiftedPerReordering;
00390   long numSwaps;
00391   long numTrivialSwaps;
00392   long maxNumSwapsPerReordering;
00393   double maxSiftingGrowth;
00394   long reorderingThreshold;
00395   long maxForwardedNodes;
00396   float tableRepackThreshold;
00397   Cal_Block superBlock; /* Variable blocks */
00398 
00399 
00400   void *hooks;
00401   int debugFlag;
00402 
00403   
00404 };
00405 
00406 
00407 /*---------------------------------------------------------------------------*/
00408 /* Variable declarations                                                     */
00409 /*---------------------------------------------------------------------------*/
00410 #ifdef COMPUTE_MEMORY_OVERHEAD
00411 long calNumEntriesAfterReduce, calNumEntriesAfterApply;
00412 double calAfterReduceToAfterApplyNodesRatio, calAfterReduceToUniqueTableNodesRatio;
00413 #endif
00414 
00415 /*---------------------------------------------------------------------------*/
00416 /* Macro declarations                                                        */
00417 /*---------------------------------------------------------------------------*/ 
00418 
00419 
00420 #define CalNodeManagerAllocNode(nodeManager, node)                          \
00421 {                                                                           \
00422   if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){                 \
00423     node = nodeManager->freeNodeList;                                       \
00424     nodeManager->freeNodeList = ((CalBddNode_t *)(node))->nextBddNode;      \
00425     Cal_Assert(!((CalAddress_t)nodeManager->freeNodeList & 0xf));\
00426   }                                                                         \
00427   else{                                                                     \
00428     CalBddNode_t *_freeNodeList, *_nextNode, *_node;                        \
00429     _freeNodeList =                                                         \
00430         (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager);  \
00431     for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0;       \
00432         _node != _freeNodeList; _nextNode = _node--){                       \
00433       _node->nextBddNode = _nextNode;                                       \
00434     }                                                                       \
00435     nodeManager->freeNodeList = _freeNodeList + 1;                          \
00436     node = _node;                                                           \
00437     if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
00438       (nodeManager)->maxNumPages *= 2;                                      \
00439       (nodeManager)->pageList =                                            \
00440           Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
00441                          (nodeManager)->maxNumPages);                       \
00442     }                                                                       \
00443     (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
00444   }                                                                         \
00445   ((CalBddNode_t *)(node))->nextBddNode = 0;                                \
00446   ((CalBddNode_t *)(node))->thenBddId = 0;                                  \
00447   ((CalBddNode_t *)(node))->elseBddId = 0;                                  \
00448   ((CalBddNode_t *)(node))->thenBddNode = 0;                                \
00449   ((CalBddNode_t *)(node))->elseBddNode = 0;                                \
00450 }
00451 
00452 #define CalNodeManagerFreeNode(nodeManager, node) \
00453 { \
00454   (node)->nextBddNode = (nodeManager)->freeNodeList; \
00455   (nodeManager)->freeNodeList = node; \
00456 }
00457 #define CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd, next, node) \
00458 { \
00459   if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){ \
00460     node = nodeManager->freeNodeList; \
00461     nodeManager->freeNodeList = ((CalBddNode_t *)(node))->nextBddNode; \
00462     Cal_Assert(!((CalAddress_t)nodeManager->freeNodeList & 0xf));\
00463   } \
00464   else{ \
00465     CalBddNode_t *_freeNodeList, *_nextNode, *_node; \
00466     _freeNodeList = \
00467         (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); \
00468     for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0; \
00469         _node != _freeNodeList; _nextNode = _node--){ \
00470       _node->nextBddNode = _nextNode; \
00471     } \
00472     nodeManager->freeNodeList = _freeNodeList + 1; \
00473     node = _node; \
00474     if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
00475       (nodeManager)->maxNumPages *= 2;                                      \
00476       (nodeManager)->pageList =                                            \
00477           Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
00478                          (nodeManager)->maxNumPages);                       \
00479     }                                                                       \
00480     (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
00481   } \
00482   ((CalBddNode_t *)(node))->nextBddNode = next; \
00483   ((CalBddNode_t *)(node))->thenBddId = CalBddGetBddId(thenBdd); \
00484   ((CalBddNode_t *)(node))->elseBddId = CalBddGetBddId(elseBdd); \
00485   ((CalBddNode_t *)(node))->thenBddNode = CalBddGetBddNode(thenBdd); \
00486   ((CalBddNode_t *)(node))->elseBddNode = CalBddGetBddNode(elseBdd); \
00487 }
00488 
00489 #define CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode)\
00490 { \
00491   if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){ \
00492     dupNode = nodeManager->freeNodeList; \
00493     nodeManager->freeNodeList = ((CalBddNode_t *)(dupNode))->nextBddNode; \
00494   } \
00495   else{ \
00496     CalBddNode_t *_freeNodeList, *_nextNode, *_node; \
00497     _freeNodeList = \
00498         (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); \
00499     for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0; \
00500         _node != _freeNodeList; _nextNode = _node--){ \
00501       _node->nextBddNode = _nextNode; \
00502     } \
00503     nodeManager->freeNodeList = _freeNodeList + 1; \
00504     dupNode = _node; \
00505     if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
00506       (nodeManager)->maxNumPages *= 2;                                      \
00507       (nodeManager)->pageList =                                            \
00508           Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
00509                          (nodeManager)->maxNumPages);                       \
00510     }                                                                       \
00511     (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
00512   } \
00513   ((CalBddNode_t *)(dupNode))->nextBddNode = (node)->nextBddNode; \
00514   ((CalBddNode_t *)(dupNode))->thenBddId = (node)->thenBddId;\
00515   ((CalBddNode_t *)(dupNode))->elseBddId = (node)->elseBddId;\
00516   ((CalBddNode_t *)(dupNode))->thenBddNode = (node)->thenBddNode;\
00517   ((CalBddNode_t *)(dupNode))->elseBddNode = (node)->elseBddNode; \
00518 }
00519 
00520 /* Record manager size range stuff */
00521 
00522 #define CAL_BDD_NEW_REC(bddManager, type) ((type *)Cal_MemNewRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT]))
00523 #define CAL_BDD_FREE_REC(bddManager, rec, type) Cal_MemFreeRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT], (rec))
00524 
00525 /*
00526 ** We would like to do repacking if :
00527 ** i) The id has more than minimum number of pages.
00528 ** ii) The ratio between the actual number of entries and the capacity is
00529 **     less than a threshold.
00530 */
00531 #define CalBddIdNeedsRepacking(bddManager, id)                              \
00532 ((bddManager->nodeManagerArray[id]->numPages > CAL_NUM_PAGES_THRESHOLD) && (bddManager->uniqueTable[id]->numEntries < bddManager->tableRepackThreshold *  \
00533   bddManager->nodeManagerArray[id]->numPages * NUM_NODES_PER_PAGE))
00534 
00535 
00536 /*
00537  * Macros for managing Cal_Bdd_t and CalBddNode_t.
00538  * INTERNAL FUNCTIONS SHOULD NOT TOUCH THE INTERNAL FIELDS
00539  * FUNCTIONS IN calTerminal.c ARE EXCEPTION TO THIS GENERAL RULE
00540  *
00541  * {CalBdd} X {Get, Put} X {ThenBddId, ElseBddId, ThenBddNode, ElseBddNode,
00542  *     ThenBdd, ElseBdd, BddId, BddNode, NextBddNode}
00543  * {CalBdd} X {Get, Put, Icr, Dcr, Add} X {RefCount}
00544  * {CalBdd,CalBddNode} X {Get} X {BddIndex}
00545  * {CalBdd} X {Is} X {RefCountZero, OutPos, BddOne, BddZero, BddNull, BddConst} 
00546  * {CalBddManager} X {Get} X {BddZero, BddOne, BddNull}
00547  * {CalBddNode} X {Get, Put} X {ThenBddId, ElseBddId, ThenBddNode, ElseBddNode,
00548  *     ThenBdd, ElseBdd, NextBddNode}
00549  * {CalBddNode} X {Get, Put, Icr, Dcr, Add} X {RefCount}
00550  * {CalBddNode} X {Is} X {RefCountZero, OutPos}
00551  * {CalBddEqual, CalBddNodeEqual}
00552  *
00553  * {CalRequest} X {Get, Put} X {ThenRequestId, ElseRequestId, ThenRequestNode,
00554  *     ElseRequestNode, ThenRequest, ElseRequest, RequestId, RequestNode,
00555  *     F, G, Next}
00556  * {CalRequest} X {Is} X {Null}
00557  * {CalRequestNode} X {Get, Put} X {ThenRequestId, ElseRequestId,
00558  *     ThenRequestNode, ElseRequestNode, ThenRequest, ElseRequest, F, G, Next}
00559  */
00560 
00561 #define CAL_BDD_POINTER(f) ((CalBddNode_t *)(((CalAddress_t)f) & \
00562     ~(CalAddress_t)0xf))
00563 #define CAL_TAG0(pointer) ((CalAddress_t)((CalAddress_t)(pointer) & 0x1))
00564 #define CalBddIsComplement(calBdd) ((int)CAL_TAG0((calBdd).bddNode))
00565 #define CalBddUpdatePhase(calBdd, complement) \
00566     ((calBdd).bddNode = \
00567     (CalBddNode_t *)((CalAddress_t)((calBdd).bddNode) ^ complement))
00568 
00569 #define CalBddZero(bddManager) ((bddManager)->bddZero)
00570 #define CalBddOne(bddManager) ((bddManager)->bddOne)
00571 #define CalBddNull(bddManager) ((bddManager)->bddNull)
00572 #define CalBddIsBddConst(calBdd) ((calBdd).bddId == 0)
00573 /* We are cheating here. Ideally we should compare both the id as well as the bdd node */
00574 #define CalBddIsEqual(calBdd1, calBdd2)\
00575     (((calBdd1).bddNode == (calBdd2).bddNode))
00576 #define CalBddIsComplementEqual(calBdd1, calBdd2) \
00577     (((calBdd1).bddNode == \
00578     (CalBddNode_t *)(((CalAddress_t)(calBdd2).bddNode) ^ 0x1)))
00579 #define CalBddSameOrNegation(calBdd1, calBdd2)  \
00580     (CAL_BDD_POINTER((calBdd1).bddNode) == CAL_BDD_POINTER((calBdd2).bddNode))
00581 
00582 /* CAUTION: MACRO ASSUMES THAT THE INDEX CORRESPONDING TO varId IS LESS THAN OR
00583  * EQUAL TO THE INDEX OF calBdd */
00584 #define CalBddGetCofactors(calBdd, varId, fx, fxbar) \
00585 { \
00586     if(varId == (calBdd).bddId){ \
00587       CalBddGetThenBdd(calBdd, fx); \
00588       CalBddGetElseBdd(calBdd, fxbar); \
00589     } \
00590     else{ \
00591       fx = calBdd; \
00592       fxbar = calBdd; \
00593     } \
00594 }
00595 
00596 #define CalBddGetThenBddId(calBdd) CAL_BDD_POINTER((calBdd).bddNode)->thenBddId
00597 #define CalBddGetElseBddId(calBdd) CAL_BDD_POINTER((calBdd).bddNode)->elseBddId
00598 #define CalBddGetThenBddIndex(bddManager, calBdd) \
00599     (bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->thenBddId])
00600 #define CalBddGetElseBddIndex(bddManager, calBdd) \
00601     (bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->elseBddId])
00602 
00603 #define CalBddGetThenBddNode(calBdd) \
00604     ((CalBddNode_t*) \
00605     (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode) \
00606     & ~0xe) ^ (CAL_TAG0((calBdd).bddNode))))
00607 
00608 #define CalBddGetElseBddNode(calBdd) \
00609     ((CalBddNode_t*) \
00610     (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode) \
00611     & ~0xe) ^ (CAL_TAG0((calBdd).bddNode))))
00612  
00613 #define CalBddGetThenBdd(calBdd, _thenBdd) \
00614 { \
00615   CalBddNode_t *_bddNode, *_bddNodeTagged; \
00616   _bddNodeTagged = (calBdd).bddNode; \
00617   _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
00618   (_thenBdd).bddId = _bddNode->thenBddId; \
00619   (_thenBdd).bddNode = (CalBddNode_t*) (((CalAddress_t) (_bddNode->thenBddNode) \
00620       & ~0xe)^(CAL_TAG0(_bddNodeTagged))); \
00621 }
00622 
00623 #define CalBddGetElseBdd(calBdd, _elseBdd) \
00624 { \
00625   CalBddNode_t *_bddNode, *_bddNodeTagged; \
00626   _bddNodeTagged = (calBdd).bddNode; \
00627   _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
00628   (_elseBdd).bddId = _bddNode->elseBddId; \
00629   (_elseBdd).bddNode = (CalBddNode_t*) (((CalAddress_t) (_bddNode->elseBddNode) \
00630         & ~0xe)^(CAL_TAG0(_bddNodeTagged)));\
00631 }
00632 
00633 
00634 #define CalBddGetBddId(calBdd) ((calBdd).bddId)
00635 #define CalBddGetBddIndex(bddManager, calBdd) \
00636     (bddManager->idToIndex[(calBdd).bddId])
00637 #define CalBddGetBddNode(calBdd) ((calBdd).bddNode)
00638 #define CalBddGetBddNodeNot(calBdd) \
00639     ((CalBddNode_t*)(((CalAddress_t)((calBdd).bddNode))^0x1))
00640 
00641 #define CalBddGetNextBddNode(calBdd) \
00642     ((CalBddNode_t *)(((CalAddress_t) \
00643     (CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & ~0xf))
00644 
00645 #define CalBddPutThenBddId(calBdd, _thenBddId) \
00646     (CAL_BDD_POINTER((calBdd).bddNode)->thenBddId = _thenBddId)
00647 #define CalBddPutElseBddId(calBdd, _elseBddId) \
00648     (CAL_BDD_POINTER((calBdd).bddNode)->elseBddId = _elseBddId)
00649 
00650 #define CalBddPutThenBddNode(calBdd, _thenBddNode) \
00651 { \
00652   CalBddNode_t *_bddNode; \
00653   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00654   _bddNode->thenBddNode = (CalBddNode_t*) \
00655       (((CalAddress_t)(_bddNode->thenBddNode) & 0xe)| \
00656       (((CalAddress_t) _thenBddNode) & ~0xe)); \
00657 }
00658 
00659 #define CalBddPutElseBddNode(calBdd, _elseBddNode) \
00660 { \
00661   CalBddNode_t *_bddNode; \
00662   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00663   _bddNode->elseBddNode = (CalBddNode_t*) \
00664       (((CalAddress_t)(_bddNode->elseBddNode) & 0xe)| \
00665       (((CalAddress_t) _elseBddNode) & ~0xe));  \
00666 }
00667  
00668 #define CalBddPutThenBdd(calBdd, thenBdd) \
00669 { \
00670   CalBddNode_t *_bddNode; \
00671   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00672   _bddNode->thenBddId = (thenBdd).bddId; \
00673   _bddNode->thenBddNode = (CalBddNode_t*) \
00674       (((CalAddress_t)(_bddNode->thenBddNode) & 0xe)| \
00675       (((CalAddress_t)(thenBdd).bddNode) & ~0xe)); \
00676 }
00677 
00678 #define CalBddPutElseBdd(calBdd, elseBdd) \
00679 { \
00680   CalBddNode_t *_bddNode; \
00681   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00682   _bddNode->elseBddId = (elseBdd).bddId; \
00683   _bddNode->elseBddNode = (CalBddNode_t*) \
00684       (((CalAddress_t)(_bddNode->elseBddNode) & 0xe)| \
00685       (((CalAddress_t)(elseBdd).bddNode) & ~0xe)); \
00686 }
00687 
00688 #define CalBddPutBddId(calBdd, _bddId) ((calBdd).bddId = _bddId)
00689 #define CalBddPutBddNode(calBdd, _bddNode) ((calBdd).bddNode = _bddNode)
00690 #define CalBddPutNextBddNode(calBdd, _nextBddNode) \
00691 { \
00692   CalBddNode_t *_bddNode; \
00693   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00694   _bddNode->nextBddNode = (CalBddNode_t*) \
00695       (((CalAddress_t)(_bddNode->nextBddNode) & 0xf)|  \
00696       (((CalAddress_t) _nextBddNode) & ~0xf));   \
00697 }
00698 
00699 #define CalBddGetRefCount(calBdd, refCount) \
00700 { \
00701   CalBddNode_t *_bddNode; \
00702   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00703   refCount = ((CalAddress_t)(_bddNode->thenBddNode) & 0x2); \
00704   refCount <<= 3; \
00705   refCount |= ((CalAddress_t)(_bddNode->elseBddNode) & 0xe); \
00706   refCount <<= 3; \
00707   refCount |= ((CalAddress_t)(_bddNode->nextBddNode) & 0xf); \
00708 }
00709                                         
00710 #define CalBddPutRefCount(calBdd, count) \
00711 { \
00712   Cal_BddRefCount_t _nextTag, _thenTag, _elseTag; \
00713   CalBddNode_t *_bddNode; \
00714   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00715   _nextTag = (count & 0xf); \
00716   _thenTag = ((count >> 6) & 0x2); \
00717   _elseTag = ((count >> 3) & 0xe); \
00718   _bddNode->nextBddNode = (CalBddNode_t*) \
00719       ((((CalAddress_t)(_bddNode->nextBddNode)) & ~0xf) | _nextTag); \
00720   _bddNode->thenBddNode = (CalBddNode_t*) \
00721       ((((CalAddress_t)(_bddNode->thenBddNode)) & ~0x2) | _thenTag); \
00722   _bddNode->elseBddNode = (CalBddNode_t*) \
00723       ((((CalAddress_t)(_bddNode->elseBddNode)) & ~0xe) | _elseTag); \
00724 }
00725 
00726 #define CalBddIcrRefCount(calBdd) \
00727 { CalBddNode_t *_bddNode; \
00728   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00729   if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf){ \
00730     _bddNode->nextBddNode = \
00731         (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) + 1); \
00732   } \
00733   else{ \
00734     if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe){ \
00735       _bddNode->nextBddNode = \
00736           (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
00737       _bddNode->elseBddNode = \
00738           (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) + 0x2); \
00739     } \
00740     else{ \
00741       if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0){ \
00742         _bddNode->nextBddNode = \
00743             (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
00744         _bddNode->elseBddNode = \
00745             (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) & ~0xe); \
00746         _bddNode->thenBddNode = \
00747             (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) | 0x2); \
00748       } \
00749     } \
00750   } \
00751 }
00752 
00753 #define CalBddDcrRefCount(calBdd) \
00754 { CalBddNode_t *_bddNode; \
00755   _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
00756   if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) == 0x0){ \
00757     if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) == 0x0){ \
00758       if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0x0){ \
00759         CalBddWarningMessage("Trying to decrement reference count below zero"); \
00760       } \
00761       else{ \
00762         _bddNode->thenBddNode = \
00763             (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) & ~0x2); \
00764         _bddNode->elseBddNode = \
00765             (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) | 0xe); \
00766         _bddNode->nextBddNode = \
00767             (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
00768       } \
00769     } \
00770     else{ \
00771       _bddNode->elseBddNode = \
00772           (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) - 0x2); \
00773       _bddNode->nextBddNode = \
00774           (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
00775     } \
00776   } \
00777   else if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf \
00778       ||  ((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe  \
00779       ||  ((CalAddress_t)(_bddNode->thenBddNode) & 0x2) != 0x2){ \
00780     _bddNode->nextBddNode = \
00781         (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) - 1); \
00782   } \
00783 }
00784 
00785 #define CalBddAddRefCount(calBdd, num) \
00786 { \
00787   Cal_BddRefCount_t _count; \
00788   CalBddGetRefCount(calBdd, _count); \
00789   if(_count < CAL_MAX_REF_COUNT){ \
00790     _count += num; \
00791     if(_count > CAL_MAX_REF_COUNT){ \
00792       _count = CAL_MAX_REF_COUNT; \
00793     } \
00794     CalBddPutRefCount(calBdd, _count); \
00795   } \
00796 }
00797 
00798 #define CalBddIsRefCountZero(calBdd) \
00799     (((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode)) & 0x2) \
00800     || (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode)) & 0xe)\
00801     || (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & 0xf))\
00802     ? 0 : 1)
00803 
00804 #define CalBddIsRefCountMax(calBdd) \
00805     ((((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode)) & 0x2) == 0x2) \
00806     && ((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode)) & 0xe) == 0xe)\
00807     && ((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & 0xf) == 0xf))\
00808     ? 1 : 0)
00809 
00810 #define CalBddFree(calBdd) CalBddDcrRefCount(calBdd)
00811 
00812 #define CalBddIsOutPos(calBdd)  (!(((CalAddress_t)(calBdd).bddNode) & 0x1))
00813 
00814 #define CalBddIsBddOne(manager, calBdd) CalBddIsEqual(calBdd, (manager)->bddOne)
00815 #define CalBddIsBddZero(manager, calBdd) CalBddIsEqual(calBdd, (manager)->bddZero)
00816 #define CalBddIsBddNull(manager, calBdd) CalBddIsEqual(calBdd,(manager)->bddNull)
00817 #define CalBddManagerGetBddOne(manager) ((manager)->bddOne)
00818 #define CalBddManagerGetBddZero(manager) ((manager)->bddZero)
00819 #define CalBddManagerGetBddNull(manager) (manager)->bddNull
00820 
00821 
00822 
00823 #define CalBddGetMinId2(bddManager, calBdd1, calBdd2, topId) \
00824 { \
00825   Cal_BddId_t _id1, _id2; \
00826   Cal_BddIndex_t _index1, _index2; \
00827   _id1 = CalBddGetBddId((calBdd1)); \
00828   _id2 = CalBddGetBddId((calBdd2)); \
00829   _index1 = (bddManager)->idToIndex[_id1]; \
00830   _index2 = (bddManager)->idToIndex[_id2]; \
00831   if (_index1 < _index2) topId = _id1; \
00832   else topId = _id2; \
00833 }
00834 
00835 #define CalBddGetMinId3(bddManager, calBdd1, calBdd2, calBdd3, topId) \
00836 { \
00837   Cal_BddId_t _id1, _id2, _id3; \
00838   Cal_BddIndex_t _index1, _index2, _index3; \
00839   _id1 = CalBddGetBddId((calBdd1)); \
00840   _id2 = CalBddGetBddId((calBdd2)); \
00841   _id3 = CalBddGetBddId((calBdd3)); \
00842   _index1 = (bddManager)->idToIndex[_id1]; \
00843   _index2 = (bddManager)->idToIndex[_id2]; \
00844   _index3 = (bddManager)->idToIndex[_id3]; \
00845   if(_index1 <= _index2){ \
00846     if(_index1 <= _index3){ \
00847       topId = _id1; \
00848     } \
00849     else{ \
00850       topId = _id3; \
00851     } \
00852   } \
00853   else{ \
00854     if(_index2 <= _index3){ \
00855       topId = _id2; \
00856     } \
00857     else{ \
00858       topId = _id3; \
00859     } \
00860   } \
00861 }
00862 
00863 #define CalBddGetMinIndex2(bddManager, calBdd1, calBdd2, topIndex) \
00864 { \
00865   Cal_BddIndex_t _index1, _index2; \
00866   _index1 = bddManager->idToIndex[CalBddGetBddId(calBdd1)]; \
00867   _index2 = bddManager->idToIndex[CalBddGetBddId(calBdd2)]; \
00868   if (_index1 < _index2) topIndex = _index1; \
00869   else topIndex = _index2; \
00870 }
00871 
00872 #define CalBddGetMinIndex3(bddManager, calBdd1, calBdd2, calBdd3, topIndex) \
00873 { \
00874   Cal_BddId_t _id1, _id2, _id3; \
00875   Cal_BddIndex_t _index1, _index2, _index3; \
00876   _id1 = CalBddGetBddId((calBdd1)); \
00877   _id2 = CalBddGetBddId((calBdd2)); \
00878   _id3 = CalBddGetBddId((calBdd3)); \
00879   _index1 = (bddManager)->idToIndex[_id1]; \
00880   _index2 = (bddManager)->idToIndex[_id2]; \
00881   _index3 = (bddManager)->idToIndex[_id3]; \
00882   if(_index1 <= _index2){ \
00883     if(_index1 <= _index3){ \
00884       topIndex = _index1; \
00885     } \
00886     else{ \
00887       topIndex = _index3; \
00888     } \
00889   } \
00890   else{ \
00891     if(_index2 <= _index3){ \
00892       topIndex = _index2; \
00893     } \
00894     else{ \
00895       topIndex = _index3; \
00896     } \
00897   } \
00898 }
00899 
00900 #define CalBddGetMinIdAndMinIndex(bddManager, calBdd1, calBdd2, topId, topIndex)\
00901 { \
00902   Cal_BddId_t _id1, _id2; \
00903   Cal_BddIndex_t _index1, _index2; \
00904   _id1 = CalBddGetBddId((calBdd1)); \
00905   _id2 = CalBddGetBddId((calBdd2)); \
00906   _index1 = (bddManager)->idToIndex[_id1]; \
00907   _index2 = (bddManager)->idToIndex[_id2]; \
00908   if (_index1 < _index2){ \
00909     topId = _id1; \
00910     topIndex = _index1; \
00911   } \
00912   else { \
00913     topId = _id2; \
00914     topIndex = _index2; \
00915   } \
00916 }
00917 
00918 #define CalBddNot(calBdd1, calBdd2) \
00919 { \
00920   (calBdd2).bddId = (calBdd1).bddId; \
00921   (calBdd2).bddNode = (CalBddNode_t *)((CalAddress_t)(calBdd1).bddNode ^ 0x1); \
00922 }
00923 
00924 #define CAL_BDD_OUT_OF_ORDER(f, g) \
00925     ((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g))
00926 
00927 #define CAL_BDD_SWAP(f, g) \
00928 { \
00929   Cal_Bdd_t _tmp; \
00930   _tmp = f; \
00931   f = g; \
00932   g = _tmp; \
00933 }
00934 
00935 
00936 /* BddNode related Macros */
00937 #define CalBddNodeGetThenBddId(_bddNode) ((_bddNode)->thenBddId)
00938 #define CalBddNodeGetElseBddId(_bddNode) ((_bddNode)->elseBddId)
00939 #define CalBddNodeGetThenBddIndex(bddManager, _bddNode) \
00940     bddManager->idToIndex[((_bddNode)->thenBddId)]
00941 #define CalBddNodeGetElseBddIndex(bddManager, _bddNode) \
00942     bddManager->idToIndex[((_bddNode)->elseBddId)]
00943 #define CalBddNodeGetThenBddNode(_bddNode) \
00944     ((CalBddNode_t *)((CalAddress_t)((_bddNode)->thenBddNode) & ~0xe))
00945 #define CalBddNodeGetElseBddNode(_bddNode) \
00946     ((CalBddNode_t *)((CalAddress_t)((_bddNode)->elseBddNode) & ~0xe))
00947  
00948 #define CalBddNodeGetThenBdd(_bddNode, _thenBdd) \
00949 { \
00950   (_thenBdd).bddId = (_bddNode)->thenBddId; \
00951   (_thenBdd).bddNode =  \
00952       (CalBddNode_t*) (((CalAddress_t) ((_bddNode)->thenBddNode) & ~0xe)); \
00953 }
00954 
00955 #define CalBddNodeGetElseBdd(_bddNode, _elseBdd) \
00956 { \
00957   (_elseBdd).bddId = (_bddNode)->elseBddId; \
00958   (_elseBdd).bddNode = \
00959       (CalBddNode_t*) (((CalAddress_t) ((_bddNode)->elseBddNode) & ~0xe)); \
00960 }
00961 
00962 #define CalBddNodeGetNextBddNode(_bddNode) \
00963     ((CalBddNode_t *)(((CalAddress_t) ((_bddNode)->nextBddNode)) & ~0xf))
00964 
00965 #define CalBddNodePutThenBddId(_bddNode, _thenBddId) \
00966     ((_bddNode)->thenBddId = _thenBddId)
00967 
00968 #define CalBddNodePutElseBddId(_bddNode, _elseBddId) \
00969     ((_bddNode)->elseBddId = _elseBddId)
00970 
00971 #define CalBddNodePutThenBddNode(_bddNode, _thenBddNode) \
00972 { \
00973   (_bddNode)->thenBddNode = (CalBddNode_t*) \
00974       (((CalAddress_t)((_bddNode)->thenBddNode) & 0xe)| \
00975        (((CalAddress_t) _thenBddNode) & ~0xe)); \
00976 }
00977 
00978 #define CalBddNodePutElseBddNode(_bddNode, _elseBddNode) \
00979 { \
00980   (_bddNode)->elseBddNode = (CalBddNode_t*) \
00981       (((CalAddress_t)((_bddNode)->elseBddNode) & 0xe)| \
00982       (((CalAddress_t) _elseBddNode) & ~0xe));  \
00983 }
00984  
00985 #define CalBddNodePutThenBdd(_bddNode, _thenBdd) \
00986 { \
00987   (_bddNode)->thenBddId = (_thenBdd).bddId; \
00988   (_bddNode)->thenBddNode = (CalBddNode_t*) \
00989       (((CalAddress_t)((_bddNode)->thenBddNode) & 0xe)| \
00990        (((CalAddress_t)(_thenBdd).bddNode) & ~0xe)); \
00991 }
00992 
00993 #define CalBddNodePutElseBdd(_bddNode, _elseBdd) \
00994 { \
00995   (_bddNode)->elseBddId = (_elseBdd).bddId; \
00996   (_bddNode)->elseBddNode = (CalBddNode_t*) \
00997       (((CalAddress_t)((_bddNode)->elseBddNode) & 0xe)| \
00998        (((CalAddress_t) (_elseBdd).bddNode) & ~0xe)); \
00999 }
01000 
01001 #define CalBddNodePutNextBddNode(_bddNode, _nextBddNode) \
01002 { \
01003   (_bddNode)->nextBddNode = (CalBddNode_t*) \
01004       (((CalAddress_t)((_bddNode)->nextBddNode) & 0xf)|  \
01005        (((CalAddress_t) _nextBddNode) & ~0xf));  \
01006 }
01007 
01008 
01009 #define CalBddNodeGetRefCount(_bddNode, refCount) \
01010 { \
01011   refCount = ((CalAddress_t)(_bddNode->thenBddNode) & 0x2); \
01012   refCount <<= 3; \
01013   refCount |= ((CalAddress_t)(_bddNode->elseBddNode) & 0xe); \
01014   refCount <<= 3; \
01015   refCount |= ((CalAddress_t)(_bddNode->nextBddNode) & 0xf); \
01016 }
01017                                         
01018 #define CalBddNodePutRefCount(_bddNode, count) \
01019 { \
01020   Cal_BddRefCount_t _nextTag, _thenTag, _elseTag; \
01021   _nextTag = (count & 0xf); \
01022   _thenTag = ((count >> 6) & 0x2); \
01023   _elseTag = ((count >> 3) & 0xe); \
01024   _bddNode->nextBddNode = (CalBddNode_t*) \
01025       ((((CalAddress_t)(_bddNode->nextBddNode)) & ~0xf) | _nextTag); \
01026   _bddNode->thenBddNode = (CalBddNode_t*) \
01027       ((((CalAddress_t)(_bddNode->thenBddNode)) & ~0x2) | _thenTag); \
01028   _bddNode->elseBddNode = (CalBddNode_t*) \
01029       ((((CalAddress_t)(_bddNode->elseBddNode)) & ~0xe) | _elseTag); \
01030 }
01031 
01032 #define CalBddNodeDcrRefCount(_bddNode) \
01033 { \
01034   if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) == 0x0){ \
01035     if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) == 0x0){ \
01036       if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0x0){ \
01037         CalBddWarningMessage("Trying to decrement reference count below zero"); \
01038       } \
01039       else{ \
01040         _bddNode->thenBddNode = \
01041             (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) & ~0x2); \
01042         _bddNode->elseBddNode = \
01043             (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) | 0xe); \
01044         _bddNode->nextBddNode = \
01045             (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
01046       } \
01047     } \
01048     else{ \
01049       _bddNode->elseBddNode = \
01050           (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) - 0x2); \
01051       _bddNode->nextBddNode = \
01052           (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
01053     } \
01054   } \
01055   else if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf \
01056       ||  ((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe  \
01057       ||  ((CalAddress_t)(_bddNode->thenBddNode) & 0x2) != 0x2){ \
01058     _bddNode->nextBddNode = \
01059         (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) - 1); \
01060   } \
01061 }
01062 
01063 #define CalBddNodeIcrRefCount(_bddNode) \
01064 { \
01065   if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf){ \
01066     _bddNode->nextBddNode = \
01067         (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) + 1); \
01068   } \
01069   else{ \
01070     if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe){ \
01071       _bddNode->nextBddNode = \
01072           (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
01073       _bddNode->elseBddNode = \
01074           (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) + 0x2); \
01075     } \
01076     else{ \
01077       if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0){ \
01078         _bddNode->nextBddNode = \
01079             (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
01080         _bddNode->elseBddNode = \
01081             (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) & ~0xe); \
01082         _bddNode->thenBddNode = \
01083             (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) | 0x2); \
01084       } \
01085     } \
01086   } \
01087 }
01088 
01089 #define CalBddNodeAddRefCount(__bddNode, num)                           \
01090 { \
01091   Cal_BddRefCount_t _count; \
01092   CalBddNodeGetRefCount(__bddNode, _count); \
01093   _count += num; \
01094   if(_count > CAL_MAX_REF_COUNT){ \
01095     _count = CAL_MAX_REF_COUNT; \
01096   } \
01097   CalBddNodePutRefCount(__bddNode, _count); \
01098 }
01099 
01100 #define CalBddNodeIsRefCountZero(_bddNode) \
01101     (((((CalAddress_t) ((_bddNode)->thenBddNode)) & 0x2) || \
01102     (((CalAddress_t) ((_bddNode)->elseBddNode)) & 0xe) || \
01103     (((CalAddress_t) ((_bddNode)->nextBddNode)) & 0xf)) \
01104     ? 0 : 1)
01105 
01106 #define CalBddNodeIsRefCountMax(_bddNode) \
01107     ((((((CalAddress_t) ((_bddNode)->thenBddNode)) & 0x2) == 0x2)&& \
01108     ((((CalAddress_t) ((_bddNode)->elseBddNode)) & 0xe) == 0xe)&& \
01109     ((((CalAddress_t) ((_bddNode)->nextBddNode)) & 0xf) == 0xf)) \
01110     ? 1 : 0)
01111 
01112 #define CalBddNodeIsOutPos(bddNode)  (!(((CalAddress_t)bddNode) & 0x1))
01113 #define CalBddNodeRegular(bddNode) ((CalBddNode_t *)(((unsigned long)(bddNode)) & ~01))
01114 #define CalBddRegular(calBdd1, calBdd2)                 \
01115 {                                                       \
01116   calBdd2.bddId = calBdd1.bddId;                        \
01117   calBdd2.bddNode = CalBddNodeRegular(calBdd1.bddNode); \
01118 }
01119 
01120 #define CalBddNodeEqual(calBddNode1, calBddNode2)\
01121   ((CalAddress_t)calBddNode1 == (CalAddress_t)calBddNode2)
01122 
01123 #define CalBddNodeNot(bddNode) ((CalBddNode_t*)(((CalAddress_t)(bddNode))^0x1))
01124 
01125 /* Mark / Unmark */
01126 #define CalBddIsMarked(calBdd) \
01127     CalBddNodeIsMarked(CAL_BDD_POINTER((calBdd).bddNode))
01128 
01129 #define CalBddMark(calBdd) \
01130     CalBddNodeMark(CAL_BDD_POINTER((calBdd).bddNode))
01131 
01132 #define CalBddUnmark(calBdd) \
01133     CalBddNodeUnmark(CAL_BDD_POINTER((calBdd).bddNode))
01134 
01135 #define CalBddGetMark(calBdd) \
01136     CalBddNodeGetMark(CAL_BDD_POINTER((calBdd).bddNode))
01137 
01138 #define CalBddPutMark(calBdd, mark) \
01139     CalBddNodePutMark(CAL_BDD_POINTER((calBdd).bddNode), (mark))
01140 
01141 #define CalBddNodeIsMarked(bddNode) \
01142   ((((CalAddress_t)((bddNode)->thenBddNode)) & 0x4) >> 2)
01143 
01144 #define CalBddNodeMark(bddNode) \
01145   ((bddNode)->thenBddNode = \
01146      (CalBddNode_t *)(((CalAddress_t)(bddNode)->thenBddNode) | 0x4))
01147 
01148 #define CalBddNodeUnmark(bddNode) \
01149   ((bddNode)->thenBddNode = \
01150      (CalBddNode_t *)(((CalAddress_t)(bddNode)->thenBddNode) & ~0x4))
01151 
01152 #define CalBddNodeGetMark(bddNode) \
01153   ((((CalAddress_t)((bddNode)->thenBddNode)) & 0xc) >> 2)
01154 
01155 #define CalBddNodePutMark(bddNode, mark) \
01156   ((bddNode)->thenBddNode = (CalBddNode_t *) \
01157       ((((CalAddress_t)(bddNode)->thenBddNode) & ~0xc) | ((mark) << 2)))
01158 
01159 
01160 /* THIS SHOULD BE CHANGED TO MACROS WITH ARGUMENTS */
01161 #define CalRequestGetThenRequestId  CalBddGetThenBddId
01162 #define CalRequestGetElseRequestId CalBddGetElseBddId
01163 #define CalRequestGetThenRequestNode   CalBddGetThenBddNode
01164 #define CalRequestGetElseRequestNode  CalBddGetElseBddNode
01165 #define CalRequestGetThenRequest  CalBddGetThenBdd
01166 #define CalRequestGetElseRequest  CalBddGetElseBdd
01167 #define CalRequestGetRequestId  CalBddGetBddId
01168 #define CalRequestGetRequestNode CalBddGetBddNode
01169 #define CalRequestGetF CalBddGetThenBdd
01170 #define CalRequestGetG CalBddGetElseBdd
01171 #define CalRequestGetNextNode CalBddGetNextBddNode
01172 
01173 #define CalRequestPutThenRequestId  CalBddPutThenBddId
01174 #define CalRequestPutElseRequestId CalBddPutElseBddId
01175 #define CalRequestPutThenRequestNode   CalBddPutThenBddNode
01176 #define CalRequestPutElseRequestNode  CalBddPutElseBddNode
01177 #define CalRequestPutThenRequest  CalBddPutThenBdd
01178 #define CalRequestPutElseRequest  CalBddPutElseBdd
01179 #define CalRequestPutRequestId  CalBddPutBddId
01180 #define CalRequestPutRequestNode CalBddPutBddNode
01181 #define CalRequestPutF CalBddPutThenBdd
01182 #define CalRequestPutG CalBddPutElseBdd
01183 #define CalRequestPutNextNode CalBddPutNextBddNode
01184 
01185 /* Macros related to the CalRequestNode */
01186 
01187 #define CalRequestNodeGetThenRequestId  CalBddNodeGetThenBddId
01188 #define CalRequestNodeGetElseRequestId CalBddNodeGetElseBddId
01189 #define CalRequestNodeGetThenRequestNode   CalBddNodeGetThenBddNode
01190 #define CalRequestNodeGetElseRequestNode  CalBddNodeGetElseBddNode
01191 #define CalRequestNodeGetThenRequest  CalBddNodeGetThenBdd
01192 #define CalRequestNodeGetElseRequest  CalBddNodeGetElseBdd
01193 #define CalRequestNodeGetF CalBddNodeGetThenBdd
01194 #define CalRequestNodeGetG CalBddNodeGetElseBdd
01195 #define CalRequestNodeGetNextRequestNode CalBddNodeGetNextBddNode
01196 
01197 #define CalRequestNodePutThenRequestId  CalBddNodePutThenBddId
01198 #define CalRequestNodePutElseRequestId CalBddNodePutElseBddId
01199 #define CalRequestNodePutThenRequestNode   CalBddNodePutThenBddNode
01200 #define CalRequestNodePutElseRequestNode  CalBddNodePutElseBddNode
01201 #define CalRequestNodePutThenRequest  CalBddNodePutThenBdd
01202 #define CalRequestNodePutElseRequest  CalBddNodePutElseBdd
01203 #define CalRequestNodePutF CalBddNodePutThenBdd
01204 #define CalRequestNodePutG CalBddNodePutElseBdd
01205 #define CalRequestNodePutNextRequestNode CalBddNodePutNextBddNode
01206 #define CalRequestIsNull(calRequest) \
01207     ((CalRequestGetRequestId(calRequest) == 0) \
01208     && (CalRequestGetRequestNode(calRequest) == 0))
01209                                       
01210 #define CalRequestIsMarked CalBddIsMarked
01211 #define CalRequestMark CalBddMark
01212 #define CalRequestUnmark CalBddUnmark
01213 #define CalRequestGetMark CalBddGetMark
01214 #define CalRequestPutMark CalBddPutMark
01215 #define CalRequestNodeIsMarked CalBddNodeIsMarked
01216 #define CalRequestNodeMark CalBddNodeMark
01217 #define CalRequestNodeUnmark CalBddNodeUnmark
01218 #define CalRequestNodeGetMark CalBddNodeGetMark
01219 #define CalRequestNodePutMark CalBddNodePutMark
01220 
01221 #define CalRequestNodeGetCofactors(bddManager,requestNode,fx,fxbar,gx,gxbar) \
01222 { \
01223   Cal_Bdd_t __f, __g; \
01224   Cal_BddIndex_t __index1, __index2; \
01225   CalRequestNodeGetF(requestNode, __f); \
01226   CalRequestNodeGetG(requestNode, __g); \
01227   __index1 = (bddManager)->idToIndex[CalBddGetBddId(__f)]; \
01228   __index2 = (bddManager)->idToIndex[CalBddGetBddId(__g)]; \
01229   if(__index1 == __index2){ \
01230     CalBddGetThenBdd(__f, fx); \
01231     CalBddGetElseBdd(__f, fxbar); \
01232     CalBddGetThenBdd(__g, gx); \
01233     CalBddGetElseBdd(__g, gxbar); \
01234   } \
01235   else if(__index1 < __index2){ \
01236     CalBddGetThenBdd(__f, fx); \
01237     CalBddGetElseBdd(__f, fxbar); \
01238     gx = gxbar = __g; \
01239   } \
01240   else{ \
01241     fx = fxbar = __f; \
01242     CalBddGetThenBdd(__g, gx); \
01243     CalBddGetElseBdd(__g, gxbar); \
01244   } \
01245 }
01246 
01247 #define CalBddPairGetCofactors(bddManager,f,g,fx,fxbar,gx,gxbar) \
01248 { \
01249   Cal_BddIndex_t __index1, __index2; \
01250   __index1 = (bddManager)->idToIndex[CalBddGetBddId(f)]; \
01251   __index2 = (bddManager)->idToIndex[CalBddGetBddId(g)]; \
01252   if(__index1 == __index2){ \
01253     CalBddGetThenBdd(f, fx); \
01254     CalBddGetElseBdd(f, fxbar); \
01255     CalBddGetThenBdd(g, gx); \
01256     CalBddGetElseBdd(g, gxbar); \
01257   } \
01258   else if(__index1 < __index2){ \
01259     CalBddGetThenBdd(f, fx); \
01260     CalBddGetElseBdd(f, fxbar); \
01261     gx = gxbar = g; \
01262   } \
01263   else{ \
01264     fx = fxbar = f; \
01265     CalBddGetThenBdd(g, gx); \
01266     CalBddGetElseBdd(g, gxbar); \
01267   } \
01268 }
01269 
01270 #define CalBddIsForwarded(bdd) \
01271   (CAL_BDD_POINTER(CalBddGetElseBddNode(bdd)) == FORWARD_FLAG)
01272 
01273 #define CalBddNodeIsForwarded(bddNode) \
01274   (((CalAddress_t)(CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode)))) == FORWARD_FLAG)
01275 
01276 #define CalBddForward(bdd) \
01277 { \
01278   CalBddNode_t *_bddNode, *_bddNodeTagged; \
01279   _bddNodeTagged = CalBddGetBddNode(bdd); \
01280   _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
01281   (bdd).bddId = _bddNode->thenBddId; \
01282   (bdd).bddNode = (CalBddNode_t*) \
01283                   (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
01284                    ^(CAL_TAG0(_bddNodeTagged))); \
01285 }
01286 
01287 #define CalBddNodeForward(_bddNodeTagged) \
01288 { \
01289   CalBddNode_t *_bddNode; \
01290   _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
01291   _bddNodeTagged = (CalBddNode_t*) \
01292                   (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
01293                    ^(CAL_TAG0(_bddNodeTagged))); \
01294 }
01295 
01296 #define CalBddNodeIsForwardedTo(_bddNodeTagged) \
01297 { \
01298   CalBddNode_t *__bddNode;\
01299   __bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
01300   if(CalBddNodeGetElseBddNode(__bddNode) == FORWARD_FLAG){ \
01301     _bddNodeTagged = (CalBddNode_t*) \
01302                      (((CalAddress_t)(__bddNode->thenBddNode) & ~0xe)        \
01303                       ^(CAL_TAG0(_bddNodeTagged))); \
01304   } \
01305 }
01306 
01307 #define CalRequestIsForwardedTo(request) \
01308 { \
01309   CalBddNode_t *__bddNode, *__bddNodeTagged; \
01310   __bddNodeTagged = (request).bddNode; \
01311   __bddNode = CAL_BDD_POINTER(__bddNodeTagged); \
01312   if(CalRequestNodeGetElseRequestNode(__bddNode) == FORWARD_FLAG){ \
01313     (request).bddId = __bddNode->thenBddId; \
01314     (request).bddNode = (CalBddNode_t*) \
01315                         (((CalAddress_t)(__bddNode->thenBddNode) & ~0xe)        \
01316                          ^(CAL_TAG0(__bddNodeTagged))); \
01317   } \
01318 }
01319 
01320 #define CalBddIsForwardedTo CalRequestIsForwardedTo
01321 
01322 #define CalBddNormalize(fBdd, gBdd) \
01323 { \
01324   Cal_Bdd_t _tmpBdd; \
01325   if((unsigned long)CAL_BDD_POINTER(CalBddGetBddNode(gBdd)) < \
01326       (unsigned long)CAL_BDD_POINTER(CalBddGetBddNode(fBdd))){ \
01327     _tmpBdd = fBdd; \
01328     fBdd = gBdd; \
01329     gBdd = _tmpBdd; \
01330   } \
01331 }
01332 
01333 /* Depth aliased as RefCount */
01334 #define CalBddGetDepth CalBddGetRefCount
01335 #define CalBddPutDepth CalBddPutRefCount
01336 #define CalRequestNodeGetDepth CalBddNodeGetRefCount
01337 #define CalRequestNodeGetRefCount CalBddNodeGetRefCount
01338 #define CalRequestNodeAddRefCount CalBddNodeAddRefCount
01339 #define CalRequestAddRefCount CalBddAddRefCount
01340 #define CalRequestNodePutDepth CalBddNodePutRefCount
01341 
01342 #define CalITERequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar, hx, hxbar) \
01343 { \
01344   Cal_Bdd_t __f, __g, __h; \
01345   Cal_BddIndex_t __index1, __index2, __index3; \
01346   CalBddNode_t *__ptrIndirect; \
01347   CalRequestNodeGetThenRequest(requestNode, __f); \
01348   __ptrIndirect = CalRequestNodeGetElseRequestNode(requestNode); \
01349   CalRequestNodeGetThenRequest(__ptrIndirect, __g); \
01350   CalRequestNodeGetElseRequest(__ptrIndirect, __h); \
01351   __index1 = (bddManager)->idToIndex[CalBddGetBddId(__f)]; \
01352   __index2 = (bddManager)->idToIndex[CalBddGetBddId(__g)]; \
01353   __index3 = (bddManager)->idToIndex[CalBddGetBddId(__h)]; \
01354   if(__index1 == __index2){ \
01355     if(__index3 == __index1){ \
01356       CalBddGetThenBdd(__f, fx); \
01357       CalBddGetElseBdd(__f, fxbar); \
01358       CalBddGetThenBdd(__g, gx); \
01359       CalBddGetElseBdd(__g, gxbar); \
01360       CalBddGetThenBdd(__h, hx); \
01361       CalBddGetElseBdd(__h, hxbar); \
01362     } \
01363     else if(__index3 < __index1){ \
01364       fx = fxbar = __f; \
01365       gx = gxbar = __g; \
01366       CalBddGetThenBdd(__h, hx); \
01367       CalBddGetElseBdd(__h, hxbar); \
01368     } \
01369     else{ \
01370       CalBddGetThenBdd(__f, fx); \
01371       CalBddGetElseBdd(__f, fxbar); \
01372       CalBddGetThenBdd(__g, gx); \
01373       CalBddGetElseBdd(__g, gxbar); \
01374       hx = hxbar = __h; \
01375     } \
01376   } \
01377   else if(__index1 < __index2){ \
01378     if(__index3 == __index1){ \
01379       CalBddGetThenBdd(__f, fx); \
01380       CalBddGetElseBdd(__f, fxbar); \
01381       gx = gxbar = __g; \
01382       CalBddGetThenBdd(__h, hx); \
01383       CalBddGetElseBdd(__h, hxbar); \
01384     } \
01385     else if(__index3 < __index1){ \
01386       fx = fxbar = __f; \
01387       gx = gxbar = __g; \
01388       CalBddGetThenBdd(__h, hx); \
01389       CalBddGetElseBdd(__h, hxbar); \
01390     } \
01391     else{ \
01392       CalBddGetThenBdd(__f, fx); \
01393       CalBddGetElseBdd(__f, fxbar); \
01394       gx = gxbar = __g; \
01395       hx = hxbar = __h; \
01396     } \
01397   } \
01398   else{ \
01399     if(__index3 == __index2){ \
01400       fx = fxbar = __f; \
01401       CalBddGetThenBdd(__g, gx); \
01402       CalBddGetElseBdd(__g, gxbar); \
01403       CalBddGetThenBdd(__h, hx); \
01404       CalBddGetElseBdd(__h, hxbar); \
01405     } \
01406     else if(__index3 < __index2){ \
01407       fx = fxbar = __f; \
01408       gx = gxbar = __g; \
01409       CalBddGetThenBdd(__h, hx); \
01410       CalBddGetElseBdd(__h, hxbar); \
01411     } \
01412     else{ \
01413       fx = fxbar = __f; \
01414       CalBddGetThenBdd(__g, gx); \
01415       CalBddGetElseBdd(__g, gxbar); \
01416       hx = hxbar = __h; \
01417     } \
01418   } \
01419 }
01420 
01421 
01422 #define CalCacheTableOneInsert(bddManager, f, result, opCode, cacheLevel) CalCacheTableTwoInsert(bddManager, f, (bddManager)->bddOne, result, opCode, cacheLevel)
01423 
01424 #define CalCacheTableOneLookup(bddManager, f, opCode, resultPtr) CalCacheTableTwoLookup(bddManager, f, (bddManager)->bddOne, opCode, resultPtr)
01425 
01426 #ifdef USE_POWER_OF_2
01427 #define CalDoHash2(thenBddNode, elseBddNode, table) \
01428    (((((CalAddress_t)thenBddNode) + ((CalAddress_t)elseBddNode)) / NODE_SIZE) & ((table)->numBins - 1))
01429 #else
01430 #define CalDoHash2(thenBddNode, elseBddNode, table) \
01431                               (((((CalAddress_t)thenBddNode) + \
01432                                  ((CalAddress_t)elseBddNode)) / NODE_SIZE)% \
01433                                (table)->numBins)
01434 #endif
01435 
01436 #if HAVE_STDARG_H
01437 EXTERN int CalBddPreProcessing(Cal_BddManager_t *bddManager, int count, ...);
01438 #else
01439 EXTERN int CalBddPreProcessing();
01440 #endif
01441 
01444 /*---------------------------------------------------------------------------*/
01445 /* Function prototypes                                                       */
01446 /*---------------------------------------------------------------------------*/
01447 
01448 EXTERN Cal_Bdd_t CalBddIf(Cal_BddManager bddManager, Cal_Bdd_t F);
01449 EXTERN int CalBddIsCubeStep(Cal_BddManager bddManager, Cal_Bdd_t f);
01450 EXTERN int CalBddTypeAux(Cal_BddManager_t * bddManager, Cal_Bdd_t f);
01451 EXTERN Cal_Bdd_t CalBddIdentity(Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd);
01452 EXTERN void CalHashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t calOpProc);
01453 EXTERN void CalHashTableReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t * uniqueTableForId);
01454 EXTERN void CalAssociationListFree(Cal_BddManager_t * bddManager);
01455 EXTERN void CalVarAssociationRepackUpdate(Cal_BddManager_t * bddManager, Cal_BddId_t id);
01456 EXTERN void CalCheckAssociationValidity(Cal_BddManager_t * bddManager);
01457 EXTERN void CalReorderAssociationFix(Cal_BddManager_t *bddManager);
01458 EXTERN void CalRequestNodeListCompose(Cal_BddManager_t * bddManager, CalRequestNode_t * requestNodeList, Cal_BddIndex_t composeIndex);
01459 EXTERN void CalHashTableComposeApply(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, Cal_BddIndex_t gIndex, CalHashTable_t **reqQueForCompose, CalHashTable_t **reqQueForITE);
01460 EXTERN void CalComposeRequestCreate(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t h, Cal_BddIndex_t composeIndex, CalHashTable_t **reqQueForCompose, CalHashTable_t **reqQueForITE, Cal_Bdd_t *resultPtr);
01461 EXTERN void CalRequestNodeListArrayITE(Cal_BddManager_t *bddManager, CalRequestNode_t **requestNodeListArray);
01462 EXTERN Cal_Bdd_t CalBddOpITEBF(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h);
01463 EXTERN void CalHashTableITEApply(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **reqQueAtPipeDepth);
01464 EXTERN Cal_Bdd_t CalBddITE(Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t H);
01465 EXTERN Cal_Bdd_t CalBddManagerCreateNewVar(Cal_BddManager_t * bddManager, Cal_BddIndex_t index);
01466 EXTERN void CalRequestNodeListArrayOp(Cal_BddManager_t * bddManager, CalRequestNode_t ** requestNodeListArray, CalOpProc_t calOpProc);
01467 EXTERN Cal_Bdd_t CalBddOpBF(Cal_BddManager_t * bddManager, CalOpProc_t calOpProc, Cal_Bdd_t F, Cal_Bdd_t G);
01468 EXTERN int main(int argc, char **argv);
01469 EXTERN Cal_Bdd_t CalBddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *assoc);
01470 EXTERN int CalOpBddVarSubstitute(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * resultBddPtr);
01471 EXTERN long CalBddFindBlock(Cal_Block block, long index);
01472 EXTERN void CalBddBlockDelta(Cal_Block b, long delta);
01473 EXTERN Cal_Block CalBddShiftBlock(Cal_BddManager_t *bddManager, Cal_Block b, long index);
01474 EXTERN unsigned long CalBlockMemoryConsumption(Cal_Block block);
01475 EXTERN void CalFreeBlockRecursively(Cal_Block block);
01476 EXTERN CalCacheTable_t * CalCacheTableTwoInit(Cal_BddManager_t *bddManager);
01477 EXTERN int CalCacheTableTwoQuit(CalCacheTable_t *cacheTable);
01478 EXTERN void CalCacheTableTwoInsert(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t result, unsigned long opCode, int cacheLevel);
01479 EXTERN int CalCacheTableTwoLookup(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned long opCode, Cal_Bdd_t *resultBddPtr);
01480 EXTERN void CalCacheTableTwoFlush(CalCacheTable_t *cacheTable);
01481 EXTERN int CalCacheTableTwoFlushAll(CalCacheTable_t *cacheTable);
01482 EXTERN void CalCacheTableTwoGCFlush(CalCacheTable_t *cacheTable);
01483 EXTERN void CalCacheTableTwoRepackUpdate(CalCacheTable_t *cacheTable);
01484 EXTERN void CalCheckCacheTableValidity(Cal_BddManager bddManager);
01485 EXTERN void CalCacheTableTwoFixResultPointers(Cal_BddManager_t *bddManager);
01486 EXTERN void CalCacheTablePrint(Cal_BddManager_t *bddManager);
01487 EXTERN void CalBddManagerGetCacheTableData(Cal_BddManager_t *bddManager, unsigned long *cacheSize, unsigned long *cacheEntries, unsigned long *cacheInsertions, unsigned long *cacheLookups, unsigned long *cacheHits, unsigned long *cacheCollisions);
01488 EXTERN void CalCacheTableRehash(Cal_BddManager_t *bddManager);
01489 EXTERN void CalCacheTableTwoFlushAssociationId(Cal_BddManager_t *bddManager, int associationId);
01490 EXTERN unsigned long CalCacheTableMemoryConsumption(CalCacheTable_t *cacheTable);
01491 EXTERN void CalBddManagerGCCheck(Cal_BddManager_t * bddManager);
01492 EXTERN int CalHashTableGC(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable);
01493 EXTERN void CalRepackNodesAfterGC(Cal_BddManager_t *bddManager);
01494 EXTERN CalHashTable_t * CalHashTableInit(Cal_BddManager_t *bddManager, Cal_BddId_t bddId);
01495 EXTERN int CalHashTableQuit(Cal_BddManager_t *bddManager, CalHashTable_t * hashTable);
01496 EXTERN void CalHashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t * bddNode);
01497 EXTERN int CalHashTableFindOrAdd(CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
01498 EXTERN int CalHashTableAddDirectAux(CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
01499 EXTERN void CalHashTableCleanUp(CalHashTable_t * hashTable);
01500 EXTERN int CalHashTableLookup(CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
01501 EXTERN void CalHashTableDelete(CalHashTable_t * hashTable, CalBddNode_t * bddNode);
01502 EXTERN int CalUniqueTableForIdLookup(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
01503 EXTERN int CalUniqueTableForIdFindOrAdd(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
01504 EXTERN void CalHashTableRehash(CalHashTable_t *hashTable, int grow);
01505 EXTERN void CalUniqueTableForIdRehashNode(CalHashTable_t *hashTable, CalBddNode_t *bddNode, CalBddNode_t *thenBddNode, CalBddNode_t *elseBddNode);
01506 EXTERN unsigned long CalBddUniqueTableNumLockedNodes(Cal_BddManager_t *bddManager, CalHashTable_t *uniqueTableForId);
01507 EXTERN void CalPackNodes(Cal_BddManager_t *bddManager);
01508 EXTERN void CalBddPackNodesForSingleId(Cal_BddManager_t *bddManager, Cal_BddId_t id);
01509 EXTERN void CalBddPackNodesAfterReorderForSingleId(Cal_BddManager_t *bddManager, int fixForwardedNodesFlag, int bestIndex, int bottomIndex);
01510 EXTERN void CalBddPackNodesForMultipleIds(Cal_BddManager_t *bddManager, Cal_BddId_t beginId, int numLevels);
01511 EXTERN CalHashTable_t * CalHashTableOneInit(Cal_BddManager_t * bddManager, int itemSize);
01512 EXTERN void CalHashTableOneQuit(CalHashTable_t * hashTable);
01513 EXTERN void CalHashTableOneInsert(CalHashTable_t * hashTable, Cal_Bdd_t keyBdd, char * valuePtr);
01514 EXTERN int CalHashTableOneLookup(CalHashTable_t * hashTable, Cal_Bdd_t keyBdd, char ** valuePtrPtr);
01515 EXTERN int CalHashTableThreeFindOrAdd(CalHashTable_t * hashTable, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, Cal_Bdd_t * bddPtr);
01516 EXTERN void CalSetInteract(Cal_BddManager_t *bddManager, int x, int y);
01517 EXTERN int CalTestInteract(Cal_BddManager_t *bddManager, int x, int y);
01518 EXTERN int CalInitInteract(Cal_BddManager_t *bddManager);
01519 EXTERN CalPageManager_t * CalPageManagerInit(int numPagesPerSegment);
01520 EXTERN int CalPageManagerQuit(CalPageManager_t * pageManager);
01521 EXTERN void CalPageManagerPrint(CalPageManager_t * pageManager);
01522 EXTERN CalNodeManager_t * CalNodeManagerInit(CalPageManager_t * pageManager);
01523 EXTERN int CalNodeManagerQuit(CalNodeManager_t * nodeManager);
01524 EXTERN void CalNodeManagerPrint(CalNodeManager_t * nodeManager);
01525 EXTERN CalAddress_t * CalPageManagerAllocPage(CalPageManager_t * pageManager);
01526 EXTERN void CalPageManagerFreePage(CalPageManager_t * pageManager, CalAddress_t * page);
01527 EXTERN int CalIncreasingOrderCompare(const void *a, const void *b);
01528 EXTERN int CalDecreasingOrderCompare(const void *a, const void *b);
01529 EXTERN void CalBddReorderFixProvisionalNodes(Cal_BddManager_t *bddManager);
01530 EXTERN void CalCheckPipelineValidity(Cal_BddManager_t *bddManager);
01531 EXTERN char * CalBddVarName(Cal_BddManager_t *bddManager, Cal_Bdd_t v, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env);
01532 EXTERN void CalBddNumberSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalHashTable_t *hashTable, long *next);
01533 EXTERN void CalBddMarkSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f);
01534 EXTERN int CalOpExists(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * resultBddPtr);
01535 EXTERN int CalOpRelProd(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t * resultBddPtr);
01536 EXTERN int CalOpCofactor(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t c, Cal_Bdd_t * resultBddPtr);
01537 EXTERN void CalBddReorderAuxBF(Cal_BddManager_t * bddManager);
01538 EXTERN void CalBddReorderFixCofactors(Cal_BddManager bddManager, Cal_BddId_t id);
01539 EXTERN void CalFixupAssoc(Cal_BddManager_t *bddManager, long id1, long id2, CalAssociation_t *assoc);
01540 EXTERN void CalBddReorderReclaimForwardedNodes(Cal_BddManager bddManager, int startIndex, int endIndex);
01541 EXTERN void CalBddReorderBlockSift(Cal_BddManager_t *bddManager, double maxSizeFactor);
01542 EXTERN void CalBddReorderBlockWindow(Cal_BddManager bddManager, Cal_Block block, char *levels);
01543 EXTERN void CalBddReorderAuxDF(Cal_BddManager_t *bddManager);
01544 EXTERN void CalAlignCollisionChains(Cal_BddManager_t *bddManager);
01545 EXTERN void CalBddReorderFixUserBddPtrs(Cal_BddManager bddManager);
01546 EXTERN int CalCheckAllValidity(Cal_BddManager bddManager);
01547 EXTERN int CalCheckValidityOfNodesForId(Cal_BddManager bddManager, int id);
01548 EXTERN int CalCheckValidityOfNodesForWindow(Cal_BddManager bddManager, Cal_BddIndex_t index, int numLevels);
01549 EXTERN int CalCheckValidityOfANode(Cal_BddManager_t *bddManager, CalBddNode_t *bddNode, int id);
01550 EXTERN void CalCheckRefCountValidity(Cal_BddManager_t *bddManager);
01551 EXTERN int CalCheckAssoc(Cal_BddManager_t *bddManager);
01552 EXTERN void CalBddReorderVarSift(Cal_BddManager bddManager, double maxSizeFactor);
01553 EXTERN void CalBddReorderVarWindow(Cal_BddManager bddManager, char *levels);
01554 EXTERN int CalOpAnd(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
01555 EXTERN int CalOpNand(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
01556 EXTERN int CalOpOr(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
01557 EXTERN int CalOpXor(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
01558 EXTERN Cal_Bdd_t CalOpITE(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, CalHashTable_t **reqQueForITE);
01559 EXTERN int main(int argc, char ** argv);
01560 EXTERN void CalUniqueTablePrint(Cal_BddManager_t *bddManager);
01561 EXTERN void CalBddFunctionPrint(Cal_BddManager_t * bddManager, Cal_Bdd_t calBdd, char * name);
01562 EXTERN int CalBddPreProcessing(Cal_BddManager_t *bddManager, int count, ...);
01563 EXTERN int CalBddPostProcessing(Cal_BddManager_t *bddManager);
01564 EXTERN int CalBddArrayPreProcessing(Cal_BddManager_t *bddManager, Cal_Bdd *userBddArray);
01565 EXTERN Cal_Bdd_t CalBddGetInternalBdd(Cal_BddManager bddManager, Cal_Bdd userBdd);
01566 EXTERN Cal_Bdd CalBddGetExternalBdd(Cal_BddManager_t *bddManager, Cal_Bdd_t internalBdd);
01567 EXTERN void CalBddFatalMessage(char *string);
01568 EXTERN void CalBddWarningMessage(char *string);
01569 EXTERN void CalBddNodePrint(CalBddNode_t *bddNode);
01570 EXTERN void CalBddPrint(Cal_Bdd_t calBdd);
01571 EXTERN void CalHashTablePrint(CalHashTable_t *hashTable);
01572 EXTERN void CalHashTableOnePrint(CalHashTable_t *hashTable, int flag);
01573 EXTERN void CalUtilSRandom(long seed);
01574 EXTERN long CalUtilRandom(void);
01575 
01578 #endif /* _INT */