source: vis_dev/glu-2.3/src/calBdd/calInt.h @ 40

Last change on this file since 40 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 63.7 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [calInt.h]
4
5  PackageName [cal]
6
7  Synopsis    [The internal data structures, macros and function declarations]
8
9  Description []
10
11  SeeAlso     [cal.h]
12
13  Author      [Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu
14               Jagesh Sanghavi  (sanghavi@ic.eecs.berkeley.edu)]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: calInt.h,v 1.11 2002/09/14 20:19:58 fabio Exp $]
36
37******************************************************************************/
38
39#ifndef _CALINT
40#define _CALINT
41
42#include "cal.h"
43
44/* Make sure variable argument lists work */
45#if HAVE_STDARG_H
46#  include <stdarg.h>
47#else
48#  if HAVE_VARARGS_H
49#    include <varargs.h>
50#  else
51#    error "Need to have HAVE_STDARG_H or HAVE_VARARGS_H defined for variable arguments"
52#  endif
53#endif
54
55
56
57/*---------------------------------------------------------------------------*/
58/* Constant declarations                                                     */
59/*---------------------------------------------------------------------------*/
60/* Begin Performance Related Constants */
61
62/* Garbage collection and reordering related constants */
63/* The following constants could significantly affect the
64   performance of the package */ 
65
66
67#define CAL_MIN_GC_LIMIT 10000 /* minimum number of nodes in the unique table
68                                  before performing garbage collection. It can
69                                  be overridden by user define node limit */
70
71
72
73
74#define CAL_REPACK_AFTER_GC_THRESHOLD 0.75 /* If the number of nodes fall below
75                                           this factor after garbage
76                                           collection, repacking should be
77                                           done */ 
78/* A note about repacking after garbage collection: Since repacking
79** moves the node pointers, it is important that "user" does not have
80** access to internal node pointers during such times. If for some
81** purposes the node handle is needed and also there is a possibility of
82** garbage collection being invoked, this field (repackAfterGCThreshold) of
83** the bdd manager should be set to 0.
84*/
85
86#define CAL_TABLE_REPACK_THRESHOLD 0.9 /* If the page utility of a unique
87                                            table (for some id) goes below this, repacking
88                                            would be done */ 
89
90#define CAL_BDD_REORDER_THRESHOLD 10000 /* Don't perform reordering below these
91                                           many nodes */
92
93#define CAL_NUM_PAGES_THRESHOLD 3
94
95#define CAL_NUM_FORWARDED_NODES_LIMIT 50000 /* maximum number of forwarded nodes
96                                               allowed during BF reordering */
97
98#define CAL_GC_CHECK 100       /* garbage collection check performed after
99                                  addition of every GC_CHECK number of nodes to
100                                  the unique table */
101
102/* End Performance Related Constants */
103
104/* Memory Management related constants */
105#define NODE_SIZE sizeof(CalBddNode_t)          /* sizeof(CalBddNode_t) */
106
107#ifndef PAGE_SIZE
108#  define PAGE_SIZE 4096        /* size of a virtual memory page */
109#endif
110#ifndef LG_PAGE_SIZE
111#  define LG_PAGE_SIZE 12       /* log2 of the page size */
112#endif
113
114#define NUM_NODES_PER_PAGE (PAGE_SIZE/NODE_SIZE)
115
116#define MAX_NUM_SEGMENTS 32
117#define NUM_PAGES_PER_SEGMENT 64 /* We start with grabbing 64 pages at a time */
118#define MIN_NUM_PAGES_PER_SEGMENT 4
119#define MAX_NUM_PAGES 10
120
121#define MIN_REC_SIZE CAL_ALLOC_ALIGNMENT
122#define MAX_REC_SIZE (sizeof(CalHashTable_t)) /* size of hash table */
123#define NUM_REC_MGRS (((MAX_REC_SIZE-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT)+1)
124
125
126
127
128/* true / false */
129#ifndef TRUE
130#define TRUE 1
131#endif
132#ifndef FALSE
133#define FALSE 0
134#endif
135
136
137
138
139/* Error Codes */
140#define CAL_BDD_OK 0
141#define CAL_BDD_OVERFLOWED 1
142
143/* bdd variable id and index related constants */
144#define CAL_BDD_NULL_ID ((unsigned short) ((1 << 8*sizeof(unsigned short)) - 1))
145#define CAL_BDD_CONST_ID 0
146#define CAL_MAX_VAR_ID ((unsigned short) (CAL_BDD_NULL_ID - 1))
147#define CAL_BDD_NULL_INDEX (unsigned short) ((1 << 8*sizeof(unsigned short)) - 1)
148#define CAL_BDD_CONST_INDEX CAL_BDD_NULL_INDEX
149#define CAL_MAX_VAR_INDEX (CAL_BDD_NULL_INDEX - 1)
150#define CAL_MAX_REF_COUNT (unsigned short)((1 << 8*sizeof(char)) - 1)
151#define CAL_INFINITY (1 << 20)
152
153/* Pipeline related constants */
154#define MAX_INSERT_DEPTH 256
155#define PIPELINE_EXECUTION_DEPTH 1
156#define DEFAULT_DEPTH 4
157#define DEFAULT_MAX_DEPTH 6
158
159
160#define FORWARD_FLAG 0     /* Flag used to identify redundant nodes */
161
162
163/* Hash table management related constants. */
164#define HASH_TABLE_DEFAULT_MAX_DENSITY 5
165#define HASH_TABLE_DEFAULT_SIZE_INDEX 8
166#define HASH_TABLE_DEFAULT_NUM_BINS TABLE_SIZE(HASH_TABLE_DEFAULT_SIZE_INDEX)
167#define HASH_TABLE_DEFAULT_MAX_CAPACITY HASH_TABLE_DEFAULT_NUM_BINS*HASH_TABLE_DEFAULT_MAX_DENSITY
168extern unsigned long calPrimes[];
169
170#define USE_POWER_OF_2
171#ifdef  USE_POWER_OF_2
172#define TABLE_SIZE(sizeIndex) (1<<sizeIndex)
173#else
174#define TABLE_SIZE(sizeIndex) (calPrimes[sizeIndex])
175#endif
176
177
178/* Codes to be used in cache table */
179#define  CAL_OP_INVALID 0x0000
180#define  CAL_OP_OR 0x1000
181#define  CAL_OP_AND 0x2000
182#define  CAL_OP_NAND 0x3000
183#define  CAL_OP_QUANT 0x4000
184#define  CAL_OP_REL_PROD 0x5000
185#define  CAL_OP_COMPOSE 0x6000
186#define  CAL_OP_SUBST 0x7000
187#define  CAL_OP_VAR_SUBSTITUTE 0x8000
188
189#define  CAL_LARGE_BDD (1<<19) /* For smaller BDDs, we would
190                                  use depth-first exist and forall routines */
191
192
193/*---------------------------------------------------------------------------*/
194/* Type declarations                                                         */
195/*---------------------------------------------------------------------------*/
196typedef struct Cal_BddStruct Cal_Bdd_t;
197typedef struct CalBddNodeStruct CalBddNode_t;
198typedef unsigned short Cal_BddRefCount_t;
199typedef struct CalPageManagerStruct CalPageManager_t;
200typedef struct CalNodeManagerStruct CalNodeManager_t;
201typedef struct CalListStruct CalList_t;
202typedef struct CalHashTableStruct CalHashTable_t;
203typedef struct CalHashTableStruct *CalReqQueForId_t;
204typedef struct CalHashTableStruct CalReqQueForIdAtDepth_t;
205typedef struct CalAssociationStruct CalAssociation_t;
206typedef struct CalBddNodeStruct CalRequestNode_t;
207typedef struct Cal_BddStruct CalRequest_t;
208typedef struct CalCacheTableStruct CalCacheTable_t;
209typedef int (*CalBddNodeToIndexFn_t)(CalBddNode_t*, Cal_BddId_t);
210typedef unsigned long CalAddress_t;
211typedef struct Cal_BlockStruct Cal_Block_t;
212
213struct Cal_BddStruct {
214  Cal_BddId_t bddId;      /* variable id */
215  CalBddNode_t *bddNode;  /* pointer to the bdd node */
216};
217
218typedef int (*CalOpProc_t) (Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t, Cal_Bdd_t *); 
219typedef int (*CalOpProc1_t) (Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t *); 
220
221
222/*---------------------------------------------------------------------------*/
223/* Stucture declarations                                                     */
224/*---------------------------------------------------------------------------*/
225
226enum CalPipeStateEnum { READY, CREATE, UPDATE };
227typedef enum CalPipeStateEnum CalPipeState_t;
228
229struct CalNodeManagerStruct{
230  CalPageManager_t *pageManager;
231  CalBddNode_t *freeNodeList;
232  int numPages;
233  int maxNumPages;
234  CalAddress_t **pageList;
235};
236
237struct CalPageManagerStruct {
238  CalAddress_t *freePageList;
239  CalAddress_t **pageSegmentArray; /* Array of pointers to segments */
240  int *numPagesArray; /* Number of pages in each segment */
241  int numSegments;
242  int totalNumPages; /* Total number of pages = sum of elements of numPagesArray */
243  int numPagesPerSegment;
244  int maxNumSegments;
245};
246
247struct CalBddNodeStruct {
248  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 */
249
250  CalBddNode_t *thenBddNode;
251  CalBddNode_t *elseBddNode;
252  Cal_BddId_t thenBddId;
253  Cal_BddId_t elseBddId;
254};
255
256struct CalHashTableStruct {
257  int sizeIndex;
258  long numBins;
259  long maxCapacity;
260  CalBddNode_t **bins;
261  Cal_BddId_t bddId;
262  CalNodeManager_t *nodeManager;
263  CalBddNode_t *requestNodeList;
264 /* The following two fields are added to improve the performance of hash table clean up.*/
265  CalBddNode_t startNode;
266  CalBddNode_t *endNode;
267  long numEntries;
268};
269
270struct CalAssociationStruct {
271  Cal_Bdd_t *varAssociation;
272  int lastBddIndex;
273  int id;
274  int refCount;
275  CalAssociation_t *next;
276};
277
278struct Cal_BlockStruct
279{
280  long numChildren;
281  Cal_Block_t **children;
282  int reorderable;
283  long firstIndex;
284  long lastIndex;
285};
286
287/* Cal_BddManager_t - manages the BDD nodes */
288struct Cal_BddManagerStruct {
289
290  int numVars; /*
291                * Number of BDD variables present in the manager. This does
292                * not include the constant. The maximum number of variables
293                * manager can have is CAL_MAX_VAR_ID (as opposed to
294                CAL_MAX_VAR_ID+1, id "0" being used for constant).
295                * CAL_MAX_VAR_ID = (((1 << 16) - 1) -1 )
296                */
297  int maxNumVars; /* Maximum number of variables which can be created without
298                     reallocating memory */
299
300  Cal_Bdd_t *varBdds; /* Array of Cal_Bdd_t's. Cal_Bdd_t[i] is the BDD
301                         corresponding to variable with id "i". */
302 
303  /* memory management */
304  CalPageManager_t *pageManager1;  /* manages memory pages */
305  CalPageManager_t *pageManager2;  /* manages memory pages */
306  CalNodeManager_t **nodeManagerArray; /*
307                                        * nodeManagerArray[i] is the node
308                                        * manager for the variable with id = i.
309                                        */     
310  /* special nodes */
311  Cal_Bdd_t bddOne; /* Constant: Id = 0; Index = CAL_MAX_INDEX */
312  Cal_Bdd_t bddZero;
313  Cal_Bdd_t bddNull;
314  CalBddNode_t *userOneBdd;
315  CalBddNode_t *userZeroBdd;
316
317  Cal_BddId_t *indexToId; /*
318                           * Table mapping index to id. If there are n
319                           * variables, then this table has n entries from
320                           * 0 to n-1 (indexToId[0] through indexToId[n-1]).
321                           */
322  Cal_BddIndex_t *idToIndex; /*
323                              * Table mapping id to index:
324                              * idToIndex[0] = CAL_MAX_INDEX
325                              * If there are n variables in the manager, then
326                              * corresponding to these variables this table
327                              * has entries from 1 to n (idToIndex[1] through
328                              * idToIndex[n]).
329                              */
330 
331  CalHashTable_t **uniqueTable; /* uniqueTable[i] is the unique table for the
332                                 * variable id " i". Unique table for an id is
333                                 * a hash table of the nodes with that
334                                 * variable id.
335                                 */
336  CalCacheTable_t *cacheTable; /* Computed table */
337
338  /* Special functions */
339  void (*TransformFn) (Cal_BddManager_t*, CalAddress_t, CalAddress_t,
340       CalAddress_t*, CalAddress_t*, Cal_Pointer_t);
341  Cal_Pointer_t transformEnv;
342
343  /* logic operation management */
344  CalHashTable_t ***reqQue;     /* reqQue[depth][id] is the hash table of
345                                 * requests corresponding to variable id "id"
346                                 * and the request depth "depth".
347                                 */
348                               
349  /* Pipeline related information */
350  int depth;
351  int maxDepth;
352  CalPipeState_t pipelineState;
353  CalOpProc_t pipelineFn;
354  int pipelineDepth;
355  int currentPipelineDepth;
356  CalRequestNode_t **requestNodeArray;/* Used for pipelined operations. */
357  CalRequestNode_t *userProvisionalNodeList;   /* List of user BDD nodes
358                                                  pointing to provisional
359                                                  BDDs */
360  CalRequestNode_t **requestNodeListArray;
361 
362
363  /* garbage collection related information */
364  unsigned long numNodes;
365  unsigned long numPeakNodes;
366  unsigned long numNodesFreed;
367  int gcCheck;
368  unsigned long uniqueTableGCLimit;
369  int  numGC;
370  int gcMode;
371  unsigned long nodeLimit;
372  int overflow;
373  float repackAfterGCThreshold;
374 
375
376  /* Association related stuff */
377  CalAssociation_t *currentAssociation;
378  CalAssociation_t *associationList;
379  CalAssociation_t *tempAssociation;
380  unsigned short tempOpCode; /* To store the id of temporary associations. */
381 
382  /* Variable reordering related stuff */
383  long *interact; /* Interaction matrix */
384  int dynamicReorderingEnableFlag;
385  int reorderMethod;
386  int reorderTechnique;
387  long numForwardedNodes;
388  int numReorderings;
389  long maxNumVarsSiftedPerReordering;
390  long numSwaps;
391  long numTrivialSwaps;
392  long maxNumSwapsPerReordering;
393  double maxSiftingGrowth;
394  long reorderingThreshold;
395  long maxForwardedNodes;
396  float tableRepackThreshold;
397  Cal_Block superBlock; /* Variable blocks */
398
399
400  void *hooks;
401  int debugFlag;
402
403 
404};
405
406
407/*---------------------------------------------------------------------------*/
408/* Variable declarations                                                     */
409/*---------------------------------------------------------------------------*/
410#ifdef COMPUTE_MEMORY_OVERHEAD
411long calNumEntriesAfterReduce, calNumEntriesAfterApply;
412double calAfterReduceToAfterApplyNodesRatio, calAfterReduceToUniqueTableNodesRatio;
413#endif
414
415/*---------------------------------------------------------------------------*/
416/* Macro declarations                                                        */
417/*---------------------------------------------------------------------------*/ 
418
419
420#define CalNodeManagerAllocNode(nodeManager, node)                          \
421{                                                                           \
422  if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){                 \
423    node = nodeManager->freeNodeList;                                       \
424    nodeManager->freeNodeList = ((CalBddNode_t *)(node))->nextBddNode;      \
425    Cal_Assert(!((CalAddress_t)nodeManager->freeNodeList & 0xf));\
426  }                                                                         \
427  else{                                                                     \
428    CalBddNode_t *_freeNodeList, *_nextNode, *_node;                        \
429    _freeNodeList =                                                         \
430        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager);  \
431    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0;       \
432        _node != _freeNodeList; _nextNode = _node--){                       \
433      _node->nextBddNode = _nextNode;                                       \
434    }                                                                       \
435    nodeManager->freeNodeList = _freeNodeList + 1;                          \
436    node = _node;                                                           \
437    if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
438      (nodeManager)->maxNumPages *= 2;                                      \
439      (nodeManager)->pageList =                                            \
440          Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
441                         (nodeManager)->maxNumPages);                       \
442    }                                                                       \
443    (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
444  }                                                                         \
445  ((CalBddNode_t *)(node))->nextBddNode = 0;                                \
446  ((CalBddNode_t *)(node))->thenBddId = 0;                                  \
447  ((CalBddNode_t *)(node))->elseBddId = 0;                                  \
448  ((CalBddNode_t *)(node))->thenBddNode = 0;                                \
449  ((CalBddNode_t *)(node))->elseBddNode = 0;                                \
450}
451
452#define CalNodeManagerFreeNode(nodeManager, node) \
453{ \
454  (node)->nextBddNode = (nodeManager)->freeNodeList; \
455  (nodeManager)->freeNodeList = node; \
456}
457#define CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd, next, node) \
458{ \
459  if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){ \
460    node = nodeManager->freeNodeList; \
461    nodeManager->freeNodeList = ((CalBddNode_t *)(node))->nextBddNode; \
462    Cal_Assert(!((CalAddress_t)nodeManager->freeNodeList & 0xf));\
463  } \
464  else{ \
465    CalBddNode_t *_freeNodeList, *_nextNode, *_node; \
466    _freeNodeList = \
467        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); \
468    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0; \
469        _node != _freeNodeList; _nextNode = _node--){ \
470      _node->nextBddNode = _nextNode; \
471    } \
472    nodeManager->freeNodeList = _freeNodeList + 1; \
473    node = _node; \
474    if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
475      (nodeManager)->maxNumPages *= 2;                                      \
476      (nodeManager)->pageList =                                            \
477          Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
478                         (nodeManager)->maxNumPages);                       \
479    }                                                                       \
480    (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
481  } \
482  ((CalBddNode_t *)(node))->nextBddNode = next; \
483  ((CalBddNode_t *)(node))->thenBddId = CalBddGetBddId(thenBdd); \
484  ((CalBddNode_t *)(node))->elseBddId = CalBddGetBddId(elseBdd); \
485  ((CalBddNode_t *)(node))->thenBddNode = CalBddGetBddNode(thenBdd); \
486  ((CalBddNode_t *)(node))->elseBddNode = CalBddGetBddNode(elseBdd); \
487}
488
489#define CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode)\
490{ \
491  if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){ \
492    dupNode = nodeManager->freeNodeList; \
493    nodeManager->freeNodeList = ((CalBddNode_t *)(dupNode))->nextBddNode; \
494  } \
495  else{ \
496    CalBddNode_t *_freeNodeList, *_nextNode, *_node; \
497    _freeNodeList = \
498        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); \
499    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0; \
500        _node != _freeNodeList; _nextNode = _node--){ \
501      _node->nextBddNode = _nextNode; \
502    } \
503    nodeManager->freeNodeList = _freeNodeList + 1; \
504    dupNode = _node; \
505    if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
506      (nodeManager)->maxNumPages *= 2;                                      \
507      (nodeManager)->pageList =                                            \
508          Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
509                         (nodeManager)->maxNumPages);                       \
510    }                                                                       \
511    (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
512  } \
513  ((CalBddNode_t *)(dupNode))->nextBddNode = (node)->nextBddNode; \
514  ((CalBddNode_t *)(dupNode))->thenBddId = (node)->thenBddId;\
515  ((CalBddNode_t *)(dupNode))->elseBddId = (node)->elseBddId;\
516  ((CalBddNode_t *)(dupNode))->thenBddNode = (node)->thenBddNode;\
517  ((CalBddNode_t *)(dupNode))->elseBddNode = (node)->elseBddNode; \
518}
519
520/* Record manager size range stuff */
521
522#define CAL_BDD_NEW_REC(bddManager, type) ((type *)Cal_MemNewRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT]))
523#define CAL_BDD_FREE_REC(bddManager, rec, type) Cal_MemFreeRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT], (rec))
524
525/*
526** We would like to do repacking if :
527** i) The id has more than minimum number of pages.
528** ii) The ratio between the actual number of entries and the capacity is
529**     less than a threshold.
530*/
531#define CalBddIdNeedsRepacking(bddManager, id)                              \
532((bddManager->nodeManagerArray[id]->numPages > CAL_NUM_PAGES_THRESHOLD) && (bddManager->uniqueTable[id]->numEntries < bddManager->tableRepackThreshold *  \
533  bddManager->nodeManagerArray[id]->numPages * NUM_NODES_PER_PAGE))
534
535
536/*
537 * Macros for managing Cal_Bdd_t and CalBddNode_t.
538 * INTERNAL FUNCTIONS SHOULD NOT TOUCH THE INTERNAL FIELDS
539 * FUNCTIONS IN calTerminal.c ARE EXCEPTION TO THIS GENERAL RULE
540 *
541 * {CalBdd} X {Get, Put} X {ThenBddId, ElseBddId, ThenBddNode, ElseBddNode,
542 *     ThenBdd, ElseBdd, BddId, BddNode, NextBddNode}
543 * {CalBdd} X {Get, Put, Icr, Dcr, Add} X {RefCount}
544 * {CalBdd,CalBddNode} X {Get} X {BddIndex}
545 * {CalBdd} X {Is} X {RefCountZero, OutPos, BddOne, BddZero, BddNull, BddConst}
546 * {CalBddManager} X {Get} X {BddZero, BddOne, BddNull}
547 * {CalBddNode} X {Get, Put} X {ThenBddId, ElseBddId, ThenBddNode, ElseBddNode,
548 *     ThenBdd, ElseBdd, NextBddNode}
549 * {CalBddNode} X {Get, Put, Icr, Dcr, Add} X {RefCount}
550 * {CalBddNode} X {Is} X {RefCountZero, OutPos}
551 * {CalBddEqual, CalBddNodeEqual}
552 *
553 * {CalRequest} X {Get, Put} X {ThenRequestId, ElseRequestId, ThenRequestNode,
554 *     ElseRequestNode, ThenRequest, ElseRequest, RequestId, RequestNode,
555 *     F, G, Next}
556 * {CalRequest} X {Is} X {Null}
557 * {CalRequestNode} X {Get, Put} X {ThenRequestId, ElseRequestId,
558 *     ThenRequestNode, ElseRequestNode, ThenRequest, ElseRequest, F, G, Next}
559 */
560
561#define CAL_BDD_POINTER(f) ((CalBddNode_t *)(((CalAddress_t)f) & \
562    ~(CalAddress_t)0xf))
563#define CAL_TAG0(pointer) ((CalAddress_t)((CalAddress_t)(pointer) & 0x1))
564#define CalBddIsComplement(calBdd) ((int)CAL_TAG0((calBdd).bddNode))
565#define CalBddUpdatePhase(calBdd, complement) \
566    ((calBdd).bddNode = \
567    (CalBddNode_t *)((CalAddress_t)((calBdd).bddNode) ^ complement))
568
569#define CalBddZero(bddManager) ((bddManager)->bddZero)
570#define CalBddOne(bddManager) ((bddManager)->bddOne)
571#define CalBddNull(bddManager) ((bddManager)->bddNull)
572#define CalBddIsBddConst(calBdd) ((calBdd).bddId == 0)
573/* We are cheating here. Ideally we should compare both the id as well as the bdd node */
574#define CalBddIsEqual(calBdd1, calBdd2)\
575    (((calBdd1).bddNode == (calBdd2).bddNode))
576#define CalBddIsComplementEqual(calBdd1, calBdd2) \
577    (((calBdd1).bddNode == \
578    (CalBddNode_t *)(((CalAddress_t)(calBdd2).bddNode) ^ 0x1)))
579#define CalBddSameOrNegation(calBdd1, calBdd2)  \
580    (CAL_BDD_POINTER((calBdd1).bddNode) == CAL_BDD_POINTER((calBdd2).bddNode))
581
582/* CAUTION: MACRO ASSUMES THAT THE INDEX CORRESPONDING TO varId IS LESS THAN OR
583 * EQUAL TO THE INDEX OF calBdd */
584#define CalBddGetCofactors(calBdd, varId, fx, fxbar) \
585{ \
586    if(varId == (calBdd).bddId){ \
587      CalBddGetThenBdd(calBdd, fx); \
588      CalBddGetElseBdd(calBdd, fxbar); \
589    } \
590    else{ \
591      fx = calBdd; \
592      fxbar = calBdd; \
593    } \
594}
595
596#define CalBddGetThenBddId(calBdd) CAL_BDD_POINTER((calBdd).bddNode)->thenBddId
597#define CalBddGetElseBddId(calBdd) CAL_BDD_POINTER((calBdd).bddNode)->elseBddId
598#define CalBddGetThenBddIndex(bddManager, calBdd) \
599    (bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->thenBddId])
600#define CalBddGetElseBddIndex(bddManager, calBdd) \
601    (bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->elseBddId])
602
603#define CalBddGetThenBddNode(calBdd) \
604    ((CalBddNode_t*) \
605    (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode) \
606    & ~0xe) ^ (CAL_TAG0((calBdd).bddNode))))
607
608#define CalBddGetElseBddNode(calBdd) \
609    ((CalBddNode_t*) \
610    (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode) \
611    & ~0xe) ^ (CAL_TAG0((calBdd).bddNode))))
612 
613#define CalBddGetThenBdd(calBdd, _thenBdd) \
614{ \
615  CalBddNode_t *_bddNode, *_bddNodeTagged; \
616  _bddNodeTagged = (calBdd).bddNode; \
617  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
618  (_thenBdd).bddId = _bddNode->thenBddId; \
619  (_thenBdd).bddNode = (CalBddNode_t*) (((CalAddress_t) (_bddNode->thenBddNode) \
620      & ~0xe)^(CAL_TAG0(_bddNodeTagged))); \
621}
622
623#define CalBddGetElseBdd(calBdd, _elseBdd) \
624{ \
625  CalBddNode_t *_bddNode, *_bddNodeTagged; \
626  _bddNodeTagged = (calBdd).bddNode; \
627  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
628  (_elseBdd).bddId = _bddNode->elseBddId; \
629  (_elseBdd).bddNode = (CalBddNode_t*) (((CalAddress_t) (_bddNode->elseBddNode) \
630        & ~0xe)^(CAL_TAG0(_bddNodeTagged)));\
631}
632
633
634#define CalBddGetBddId(calBdd) ((calBdd).bddId)
635#define CalBddGetBddIndex(bddManager, calBdd) \
636    (bddManager->idToIndex[(calBdd).bddId])
637#define CalBddGetBddNode(calBdd) ((calBdd).bddNode)
638#define CalBddGetBddNodeNot(calBdd) \
639    ((CalBddNode_t*)(((CalAddress_t)((calBdd).bddNode))^0x1))
640
641#define CalBddGetNextBddNode(calBdd) \
642    ((CalBddNode_t *)(((CalAddress_t) \
643    (CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & ~0xf))
644
645#define CalBddPutThenBddId(calBdd, _thenBddId) \
646    (CAL_BDD_POINTER((calBdd).bddNode)->thenBddId = _thenBddId)
647#define CalBddPutElseBddId(calBdd, _elseBddId) \
648    (CAL_BDD_POINTER((calBdd).bddNode)->elseBddId = _elseBddId)
649
650#define CalBddPutThenBddNode(calBdd, _thenBddNode) \
651{ \
652  CalBddNode_t *_bddNode; \
653  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
654  _bddNode->thenBddNode = (CalBddNode_t*) \
655      (((CalAddress_t)(_bddNode->thenBddNode) & 0xe)| \
656      (((CalAddress_t) _thenBddNode) & ~0xe)); \
657}
658
659#define CalBddPutElseBddNode(calBdd, _elseBddNode) \
660{ \
661  CalBddNode_t *_bddNode; \
662  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
663  _bddNode->elseBddNode = (CalBddNode_t*) \
664      (((CalAddress_t)(_bddNode->elseBddNode) & 0xe)| \
665      (((CalAddress_t) _elseBddNode) & ~0xe));  \
666}
667 
668#define CalBddPutThenBdd(calBdd, thenBdd) \
669{ \
670  CalBddNode_t *_bddNode; \
671  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
672  _bddNode->thenBddId = (thenBdd).bddId; \
673  _bddNode->thenBddNode = (CalBddNode_t*) \
674      (((CalAddress_t)(_bddNode->thenBddNode) & 0xe)| \
675      (((CalAddress_t)(thenBdd).bddNode) & ~0xe)); \
676}
677
678#define CalBddPutElseBdd(calBdd, elseBdd) \
679{ \
680  CalBddNode_t *_bddNode; \
681  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
682  _bddNode->elseBddId = (elseBdd).bddId; \
683  _bddNode->elseBddNode = (CalBddNode_t*) \
684      (((CalAddress_t)(_bddNode->elseBddNode) & 0xe)| \
685      (((CalAddress_t)(elseBdd).bddNode) & ~0xe)); \
686}
687
688#define CalBddPutBddId(calBdd, _bddId) ((calBdd).bddId = _bddId)
689#define CalBddPutBddNode(calBdd, _bddNode) ((calBdd).bddNode = _bddNode)
690#define CalBddPutNextBddNode(calBdd, _nextBddNode) \
691{ \
692  CalBddNode_t *_bddNode; \
693  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
694  _bddNode->nextBddNode = (CalBddNode_t*) \
695      (((CalAddress_t)(_bddNode->nextBddNode) & 0xf)|  \
696      (((CalAddress_t) _nextBddNode) & ~0xf));   \
697}
698
699#define CalBddGetRefCount(calBdd, refCount) \
700{ \
701  CalBddNode_t *_bddNode; \
702  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
703  refCount = ((CalAddress_t)(_bddNode->thenBddNode) & 0x2); \
704  refCount <<= 3; \
705  refCount |= ((CalAddress_t)(_bddNode->elseBddNode) & 0xe); \
706  refCount <<= 3; \
707  refCount |= ((CalAddress_t)(_bddNode->nextBddNode) & 0xf); \
708}
709                                       
710#define CalBddPutRefCount(calBdd, count) \
711{ \
712  Cal_BddRefCount_t _nextTag, _thenTag, _elseTag; \
713  CalBddNode_t *_bddNode; \
714  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
715  _nextTag = (count & 0xf); \
716  _thenTag = ((count >> 6) & 0x2); \
717  _elseTag = ((count >> 3) & 0xe); \
718  _bddNode->nextBddNode = (CalBddNode_t*) \
719      ((((CalAddress_t)(_bddNode->nextBddNode)) & ~0xf) | _nextTag); \
720  _bddNode->thenBddNode = (CalBddNode_t*) \
721      ((((CalAddress_t)(_bddNode->thenBddNode)) & ~0x2) | _thenTag); \
722  _bddNode->elseBddNode = (CalBddNode_t*) \
723      ((((CalAddress_t)(_bddNode->elseBddNode)) & ~0xe) | _elseTag); \
724}
725
726#define CalBddIcrRefCount(calBdd) \
727{ CalBddNode_t *_bddNode; \
728  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
729  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf){ \
730    _bddNode->nextBddNode = \
731        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) + 1); \
732  } \
733  else{ \
734    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe){ \
735      _bddNode->nextBddNode = \
736          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
737      _bddNode->elseBddNode = \
738          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) + 0x2); \
739    } \
740    else{ \
741      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0){ \
742        _bddNode->nextBddNode = \
743            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
744        _bddNode->elseBddNode = \
745            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) & ~0xe); \
746        _bddNode->thenBddNode = \
747            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) | 0x2); \
748      } \
749    } \
750  } \
751}
752
753#define CalBddDcrRefCount(calBdd) \
754{ CalBddNode_t *_bddNode; \
755  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
756  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) == 0x0){ \
757    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) == 0x0){ \
758      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0x0){ \
759        CalBddWarningMessage("Trying to decrement reference count below zero"); \
760      } \
761      else{ \
762        _bddNode->thenBddNode = \
763            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) & ~0x2); \
764        _bddNode->elseBddNode = \
765            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) | 0xe); \
766        _bddNode->nextBddNode = \
767            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
768      } \
769    } \
770    else{ \
771      _bddNode->elseBddNode = \
772          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) - 0x2); \
773      _bddNode->nextBddNode = \
774          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
775    } \
776  } \
777  else if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf \
778      ||  ((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe  \
779      ||  ((CalAddress_t)(_bddNode->thenBddNode) & 0x2) != 0x2){ \
780    _bddNode->nextBddNode = \
781        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) - 1); \
782  } \
783}
784
785#define CalBddAddRefCount(calBdd, num) \
786{ \
787  Cal_BddRefCount_t _count; \
788  CalBddGetRefCount(calBdd, _count); \
789  if(_count < CAL_MAX_REF_COUNT){ \
790    _count += num; \
791    if(_count > CAL_MAX_REF_COUNT){ \
792      _count = CAL_MAX_REF_COUNT; \
793    } \
794    CalBddPutRefCount(calBdd, _count); \
795  } \
796}
797
798#define CalBddIsRefCountZero(calBdd) \
799    (((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode)) & 0x2) \
800    || (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode)) & 0xe)\
801    || (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & 0xf))\
802    ? 0 : 1)
803
804#define CalBddIsRefCountMax(calBdd) \
805    ((((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode)) & 0x2) == 0x2) \
806    && ((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode)) & 0xe) == 0xe)\
807    && ((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & 0xf) == 0xf))\
808    ? 1 : 0)
809
810#define CalBddFree(calBdd) CalBddDcrRefCount(calBdd)
811
812#define CalBddIsOutPos(calBdd)  (!(((CalAddress_t)(calBdd).bddNode) & 0x1))
813
814#define CalBddIsBddOne(manager, calBdd) CalBddIsEqual(calBdd, (manager)->bddOne)
815#define CalBddIsBddZero(manager, calBdd) CalBddIsEqual(calBdd, (manager)->bddZero)
816#define CalBddIsBddNull(manager, calBdd) CalBddIsEqual(calBdd,(manager)->bddNull)
817#define CalBddManagerGetBddOne(manager) ((manager)->bddOne)
818#define CalBddManagerGetBddZero(manager) ((manager)->bddZero)
819#define CalBddManagerGetBddNull(manager) (manager)->bddNull
820
821
822
823#define CalBddGetMinId2(bddManager, calBdd1, calBdd2, topId) \
824{ \
825  Cal_BddId_t _id1, _id2; \
826  Cal_BddIndex_t _index1, _index2; \
827  _id1 = CalBddGetBddId((calBdd1)); \
828  _id2 = CalBddGetBddId((calBdd2)); \
829  _index1 = (bddManager)->idToIndex[_id1]; \
830  _index2 = (bddManager)->idToIndex[_id2]; \
831  if (_index1 < _index2) topId = _id1; \
832  else topId = _id2; \
833}
834
835#define CalBddGetMinId3(bddManager, calBdd1, calBdd2, calBdd3, topId) \
836{ \
837  Cal_BddId_t _id1, _id2, _id3; \
838  Cal_BddIndex_t _index1, _index2, _index3; \
839  _id1 = CalBddGetBddId((calBdd1)); \
840  _id2 = CalBddGetBddId((calBdd2)); \
841  _id3 = CalBddGetBddId((calBdd3)); \
842  _index1 = (bddManager)->idToIndex[_id1]; \
843  _index2 = (bddManager)->idToIndex[_id2]; \
844  _index3 = (bddManager)->idToIndex[_id3]; \
845  if(_index1 <= _index2){ \
846    if(_index1 <= _index3){ \
847      topId = _id1; \
848    } \
849    else{ \
850      topId = _id3; \
851    } \
852  } \
853  else{ \
854    if(_index2 <= _index3){ \
855      topId = _id2; \
856    } \
857    else{ \
858      topId = _id3; \
859    } \
860  } \
861}
862
863#define CalBddGetMinIndex2(bddManager, calBdd1, calBdd2, topIndex) \
864{ \
865  Cal_BddIndex_t _index1, _index2; \
866  _index1 = bddManager->idToIndex[CalBddGetBddId(calBdd1)]; \
867  _index2 = bddManager->idToIndex[CalBddGetBddId(calBdd2)]; \
868  if (_index1 < _index2) topIndex = _index1; \
869  else topIndex = _index2; \
870}
871
872#define CalBddGetMinIndex3(bddManager, calBdd1, calBdd2, calBdd3, topIndex) \
873{ \
874  Cal_BddId_t _id1, _id2, _id3; \
875  Cal_BddIndex_t _index1, _index2, _index3; \
876  _id1 = CalBddGetBddId((calBdd1)); \
877  _id2 = CalBddGetBddId((calBdd2)); \
878  _id3 = CalBddGetBddId((calBdd3)); \
879  _index1 = (bddManager)->idToIndex[_id1]; \
880  _index2 = (bddManager)->idToIndex[_id2]; \
881  _index3 = (bddManager)->idToIndex[_id3]; \
882  if(_index1 <= _index2){ \
883    if(_index1 <= _index3){ \
884      topIndex = _index1; \
885    } \
886    else{ \
887      topIndex = _index3; \
888    } \
889  } \
890  else{ \
891    if(_index2 <= _index3){ \
892      topIndex = _index2; \
893    } \
894    else{ \
895      topIndex = _index3; \
896    } \
897  } \
898}
899
900#define CalBddGetMinIdAndMinIndex(bddManager, calBdd1, calBdd2, topId, topIndex)\
901{ \
902  Cal_BddId_t _id1, _id2; \
903  Cal_BddIndex_t _index1, _index2; \
904  _id1 = CalBddGetBddId((calBdd1)); \
905  _id2 = CalBddGetBddId((calBdd2)); \
906  _index1 = (bddManager)->idToIndex[_id1]; \
907  _index2 = (bddManager)->idToIndex[_id2]; \
908  if (_index1 < _index2){ \
909    topId = _id1; \
910    topIndex = _index1; \
911  } \
912  else { \
913    topId = _id2; \
914    topIndex = _index2; \
915  } \
916}
917
918#define CalBddNot(calBdd1, calBdd2) \
919{ \
920  (calBdd2).bddId = (calBdd1).bddId; \
921  (calBdd2).bddNode = (CalBddNode_t *)((CalAddress_t)(calBdd1).bddNode ^ 0x1); \
922}
923
924#define CAL_BDD_OUT_OF_ORDER(f, g) \
925    ((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g))
926
927#define CAL_BDD_SWAP(f, g) \
928{ \
929  Cal_Bdd_t _tmp; \
930  _tmp = f; \
931  f = g; \
932  g = _tmp; \
933}
934
935
936/* BddNode related Macros */
937#define CalBddNodeGetThenBddId(_bddNode) ((_bddNode)->thenBddId)
938#define CalBddNodeGetElseBddId(_bddNode) ((_bddNode)->elseBddId)
939#define CalBddNodeGetThenBddIndex(bddManager, _bddNode) \
940    bddManager->idToIndex[((_bddNode)->thenBddId)]
941#define CalBddNodeGetElseBddIndex(bddManager, _bddNode) \
942    bddManager->idToIndex[((_bddNode)->elseBddId)]
943#define CalBddNodeGetThenBddNode(_bddNode) \
944    ((CalBddNode_t *)((CalAddress_t)((_bddNode)->thenBddNode) & ~0xe))
945#define CalBddNodeGetElseBddNode(_bddNode) \
946    ((CalBddNode_t *)((CalAddress_t)((_bddNode)->elseBddNode) & ~0xe))
947 
948#define CalBddNodeGetThenBdd(_bddNode, _thenBdd) \
949{ \
950  (_thenBdd).bddId = (_bddNode)->thenBddId; \
951  (_thenBdd).bddNode =  \
952      (CalBddNode_t*) (((CalAddress_t) ((_bddNode)->thenBddNode) & ~0xe)); \
953}
954
955#define CalBddNodeGetElseBdd(_bddNode, _elseBdd) \
956{ \
957  (_elseBdd).bddId = (_bddNode)->elseBddId; \
958  (_elseBdd).bddNode = \
959      (CalBddNode_t*) (((CalAddress_t) ((_bddNode)->elseBddNode) & ~0xe)); \
960}
961
962#define CalBddNodeGetNextBddNode(_bddNode) \
963    ((CalBddNode_t *)(((CalAddress_t) ((_bddNode)->nextBddNode)) & ~0xf))
964
965#define CalBddNodePutThenBddId(_bddNode, _thenBddId) \
966    ((_bddNode)->thenBddId = _thenBddId)
967
968#define CalBddNodePutElseBddId(_bddNode, _elseBddId) \
969    ((_bddNode)->elseBddId = _elseBddId)
970
971#define CalBddNodePutThenBddNode(_bddNode, _thenBddNode) \
972{ \
973  (_bddNode)->thenBddNode = (CalBddNode_t*) \
974      (((CalAddress_t)((_bddNode)->thenBddNode) & 0xe)| \
975       (((CalAddress_t) _thenBddNode) & ~0xe)); \
976}
977
978#define CalBddNodePutElseBddNode(_bddNode, _elseBddNode) \
979{ \
980  (_bddNode)->elseBddNode = (CalBddNode_t*) \
981      (((CalAddress_t)((_bddNode)->elseBddNode) & 0xe)| \
982      (((CalAddress_t) _elseBddNode) & ~0xe));  \
983}
984 
985#define CalBddNodePutThenBdd(_bddNode, _thenBdd) \
986{ \
987  (_bddNode)->thenBddId = (_thenBdd).bddId; \
988  (_bddNode)->thenBddNode = (CalBddNode_t*) \
989      (((CalAddress_t)((_bddNode)->thenBddNode) & 0xe)| \
990       (((CalAddress_t)(_thenBdd).bddNode) & ~0xe)); \
991}
992
993#define CalBddNodePutElseBdd(_bddNode, _elseBdd) \
994{ \
995  (_bddNode)->elseBddId = (_elseBdd).bddId; \
996  (_bddNode)->elseBddNode = (CalBddNode_t*) \
997      (((CalAddress_t)((_bddNode)->elseBddNode) & 0xe)| \
998       (((CalAddress_t) (_elseBdd).bddNode) & ~0xe)); \
999}
1000
1001#define CalBddNodePutNextBddNode(_bddNode, _nextBddNode) \
1002{ \
1003  (_bddNode)->nextBddNode = (CalBddNode_t*) \
1004      (((CalAddress_t)((_bddNode)->nextBddNode) & 0xf)|  \
1005       (((CalAddress_t) _nextBddNode) & ~0xf));  \
1006}
1007
1008
1009#define CalBddNodeGetRefCount(_bddNode, refCount) \
1010{ \
1011  refCount = ((CalAddress_t)(_bddNode->thenBddNode) & 0x2); \
1012  refCount <<= 3; \
1013  refCount |= ((CalAddress_t)(_bddNode->elseBddNode) & 0xe); \
1014  refCount <<= 3; \
1015  refCount |= ((CalAddress_t)(_bddNode->nextBddNode) & 0xf); \
1016}
1017                                       
1018#define CalBddNodePutRefCount(_bddNode, count) \
1019{ \
1020  Cal_BddRefCount_t _nextTag, _thenTag, _elseTag; \
1021  _nextTag = (count & 0xf); \
1022  _thenTag = ((count >> 6) & 0x2); \
1023  _elseTag = ((count >> 3) & 0xe); \
1024  _bddNode->nextBddNode = (CalBddNode_t*) \
1025      ((((CalAddress_t)(_bddNode->nextBddNode)) & ~0xf) | _nextTag); \
1026  _bddNode->thenBddNode = (CalBddNode_t*) \
1027      ((((CalAddress_t)(_bddNode->thenBddNode)) & ~0x2) | _thenTag); \
1028  _bddNode->elseBddNode = (CalBddNode_t*) \
1029      ((((CalAddress_t)(_bddNode->elseBddNode)) & ~0xe) | _elseTag); \
1030}
1031
1032#define CalBddNodeDcrRefCount(_bddNode) \
1033{ \
1034  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) == 0x0){ \
1035    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) == 0x0){ \
1036      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0x0){ \
1037        CalBddWarningMessage("Trying to decrement reference count below zero"); \
1038      } \
1039      else{ \
1040        _bddNode->thenBddNode = \
1041            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) & ~0x2); \
1042        _bddNode->elseBddNode = \
1043            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) | 0xe); \
1044        _bddNode->nextBddNode = \
1045            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
1046      } \
1047    } \
1048    else{ \
1049      _bddNode->elseBddNode = \
1050          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) - 0x2); \
1051      _bddNode->nextBddNode = \
1052          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
1053    } \
1054  } \
1055  else if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf \
1056      ||  ((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe  \
1057      ||  ((CalAddress_t)(_bddNode->thenBddNode) & 0x2) != 0x2){ \
1058    _bddNode->nextBddNode = \
1059        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) - 1); \
1060  } \
1061}
1062
1063#define CalBddNodeIcrRefCount(_bddNode) \
1064{ \
1065  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf){ \
1066    _bddNode->nextBddNode = \
1067        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) + 1); \
1068  } \
1069  else{ \
1070    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe){ \
1071      _bddNode->nextBddNode = \
1072          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
1073      _bddNode->elseBddNode = \
1074          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) + 0x2); \
1075    } \
1076    else{ \
1077      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0){ \
1078        _bddNode->nextBddNode = \
1079            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
1080        _bddNode->elseBddNode = \
1081            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) & ~0xe); \
1082        _bddNode->thenBddNode = \
1083            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) | 0x2); \
1084      } \
1085    } \
1086  } \
1087}
1088
1089#define CalBddNodeAddRefCount(__bddNode, num)                           \
1090{ \
1091  Cal_BddRefCount_t _count; \
1092  CalBddNodeGetRefCount(__bddNode, _count); \
1093  _count += num; \
1094  if(_count > CAL_MAX_REF_COUNT){ \
1095    _count = CAL_MAX_REF_COUNT; \
1096  } \
1097  CalBddNodePutRefCount(__bddNode, _count); \
1098}
1099
1100#define CalBddNodeIsRefCountZero(_bddNode) \
1101    (((((CalAddress_t) ((_bddNode)->thenBddNode)) & 0x2) || \
1102    (((CalAddress_t) ((_bddNode)->elseBddNode)) & 0xe) || \
1103    (((CalAddress_t) ((_bddNode)->nextBddNode)) & 0xf)) \
1104    ? 0 : 1)
1105
1106#define CalBddNodeIsRefCountMax(_bddNode) \
1107    ((((((CalAddress_t) ((_bddNode)->thenBddNode)) & 0x2) == 0x2)&& \
1108    ((((CalAddress_t) ((_bddNode)->elseBddNode)) & 0xe) == 0xe)&& \
1109    ((((CalAddress_t) ((_bddNode)->nextBddNode)) & 0xf) == 0xf)) \
1110    ? 1 : 0)
1111
1112#define CalBddNodeIsOutPos(bddNode)  (!(((CalAddress_t)bddNode) & 0x1))
1113#define CalBddNodeRegular(bddNode) ((CalBddNode_t *)(((unsigned long)(bddNode)) & ~01))
1114#define CalBddRegular(calBdd1, calBdd2)                 \
1115{                                                       \
1116  calBdd2.bddId = calBdd1.bddId;                        \
1117  calBdd2.bddNode = CalBddNodeRegular(calBdd1.bddNode); \
1118}
1119
1120#define CalBddNodeEqual(calBddNode1, calBddNode2)\
1121  ((CalAddress_t)calBddNode1 == (CalAddress_t)calBddNode2)
1122
1123#define CalBddNodeNot(bddNode) ((CalBddNode_t*)(((CalAddress_t)(bddNode))^0x1))
1124
1125/* Mark / Unmark */
1126#define CalBddIsMarked(calBdd) \
1127    CalBddNodeIsMarked(CAL_BDD_POINTER((calBdd).bddNode))
1128
1129#define CalBddMark(calBdd) \
1130    CalBddNodeMark(CAL_BDD_POINTER((calBdd).bddNode))
1131
1132#define CalBddUnmark(calBdd) \
1133    CalBddNodeUnmark(CAL_BDD_POINTER((calBdd).bddNode))
1134
1135#define CalBddGetMark(calBdd) \
1136    CalBddNodeGetMark(CAL_BDD_POINTER((calBdd).bddNode))
1137
1138#define CalBddPutMark(calBdd, mark) \
1139    CalBddNodePutMark(CAL_BDD_POINTER((calBdd).bddNode), (mark))
1140
1141#define CalBddNodeIsMarked(bddNode) \
1142  ((((CalAddress_t)((bddNode)->thenBddNode)) & 0x4) >> 2)
1143
1144#define CalBddNodeMark(bddNode) \
1145  ((bddNode)->thenBddNode = \
1146     (CalBddNode_t *)(((CalAddress_t)(bddNode)->thenBddNode) | 0x4))
1147
1148#define CalBddNodeUnmark(bddNode) \
1149  ((bddNode)->thenBddNode = \
1150     (CalBddNode_t *)(((CalAddress_t)(bddNode)->thenBddNode) & ~0x4))
1151
1152#define CalBddNodeGetMark(bddNode) \
1153  ((((CalAddress_t)((bddNode)->thenBddNode)) & 0xc) >> 2)
1154
1155#define CalBddNodePutMark(bddNode, mark) \
1156  ((bddNode)->thenBddNode = (CalBddNode_t *) \
1157      ((((CalAddress_t)(bddNode)->thenBddNode) & ~0xc) | ((mark) << 2)))
1158
1159
1160/* THIS SHOULD BE CHANGED TO MACROS WITH ARGUMENTS */
1161#define CalRequestGetThenRequestId  CalBddGetThenBddId
1162#define CalRequestGetElseRequestId CalBddGetElseBddId
1163#define CalRequestGetThenRequestNode   CalBddGetThenBddNode
1164#define CalRequestGetElseRequestNode  CalBddGetElseBddNode
1165#define CalRequestGetThenRequest  CalBddGetThenBdd
1166#define CalRequestGetElseRequest  CalBddGetElseBdd
1167#define CalRequestGetRequestId  CalBddGetBddId
1168#define CalRequestGetRequestNode CalBddGetBddNode
1169#define CalRequestGetF CalBddGetThenBdd
1170#define CalRequestGetG CalBddGetElseBdd
1171#define CalRequestGetNextNode CalBddGetNextBddNode
1172
1173#define CalRequestPutThenRequestId  CalBddPutThenBddId
1174#define CalRequestPutElseRequestId CalBddPutElseBddId
1175#define CalRequestPutThenRequestNode   CalBddPutThenBddNode
1176#define CalRequestPutElseRequestNode  CalBddPutElseBddNode
1177#define CalRequestPutThenRequest  CalBddPutThenBdd
1178#define CalRequestPutElseRequest  CalBddPutElseBdd
1179#define CalRequestPutRequestId  CalBddPutBddId
1180#define CalRequestPutRequestNode CalBddPutBddNode
1181#define CalRequestPutF CalBddPutThenBdd
1182#define CalRequestPutG CalBddPutElseBdd
1183#define CalRequestPutNextNode CalBddPutNextBddNode
1184
1185/* Macros related to the CalRequestNode */
1186
1187#define CalRequestNodeGetThenRequestId  CalBddNodeGetThenBddId
1188#define CalRequestNodeGetElseRequestId CalBddNodeGetElseBddId
1189#define CalRequestNodeGetThenRequestNode   CalBddNodeGetThenBddNode
1190#define CalRequestNodeGetElseRequestNode  CalBddNodeGetElseBddNode
1191#define CalRequestNodeGetThenRequest  CalBddNodeGetThenBdd
1192#define CalRequestNodeGetElseRequest  CalBddNodeGetElseBdd
1193#define CalRequestNodeGetF CalBddNodeGetThenBdd
1194#define CalRequestNodeGetG CalBddNodeGetElseBdd
1195#define CalRequestNodeGetNextRequestNode CalBddNodeGetNextBddNode
1196
1197#define CalRequestNodePutThenRequestId  CalBddNodePutThenBddId
1198#define CalRequestNodePutElseRequestId CalBddNodePutElseBddId
1199#define CalRequestNodePutThenRequestNode   CalBddNodePutThenBddNode
1200#define CalRequestNodePutElseRequestNode  CalBddNodePutElseBddNode
1201#define CalRequestNodePutThenRequest  CalBddNodePutThenBdd
1202#define CalRequestNodePutElseRequest  CalBddNodePutElseBdd
1203#define CalRequestNodePutF CalBddNodePutThenBdd
1204#define CalRequestNodePutG CalBddNodePutElseBdd
1205#define CalRequestNodePutNextRequestNode CalBddNodePutNextBddNode
1206#define CalRequestIsNull(calRequest) \
1207    ((CalRequestGetRequestId(calRequest) == 0) \
1208    && (CalRequestGetRequestNode(calRequest) == 0))
1209                                     
1210#define CalRequestIsMarked CalBddIsMarked
1211#define CalRequestMark CalBddMark
1212#define CalRequestUnmark CalBddUnmark
1213#define CalRequestGetMark CalBddGetMark
1214#define CalRequestPutMark CalBddPutMark
1215#define CalRequestNodeIsMarked CalBddNodeIsMarked
1216#define CalRequestNodeMark CalBddNodeMark
1217#define CalRequestNodeUnmark CalBddNodeUnmark
1218#define CalRequestNodeGetMark CalBddNodeGetMark
1219#define CalRequestNodePutMark CalBddNodePutMark
1220
1221#define CalRequestNodeGetCofactors(bddManager,requestNode,fx,fxbar,gx,gxbar) \
1222{ \
1223  Cal_Bdd_t __f, __g; \
1224  Cal_BddIndex_t __index1, __index2; \
1225  CalRequestNodeGetF(requestNode, __f); \
1226  CalRequestNodeGetG(requestNode, __g); \
1227  __index1 = (bddManager)->idToIndex[CalBddGetBddId(__f)]; \
1228  __index2 = (bddManager)->idToIndex[CalBddGetBddId(__g)]; \
1229  if(__index1 == __index2){ \
1230    CalBddGetThenBdd(__f, fx); \
1231    CalBddGetElseBdd(__f, fxbar); \
1232    CalBddGetThenBdd(__g, gx); \
1233    CalBddGetElseBdd(__g, gxbar); \
1234  } \
1235  else if(__index1 < __index2){ \
1236    CalBddGetThenBdd(__f, fx); \
1237    CalBddGetElseBdd(__f, fxbar); \
1238    gx = gxbar = __g; \
1239  } \
1240  else{ \
1241    fx = fxbar = __f; \
1242    CalBddGetThenBdd(__g, gx); \
1243    CalBddGetElseBdd(__g, gxbar); \
1244  } \
1245}
1246
1247#define CalBddPairGetCofactors(bddManager,f,g,fx,fxbar,gx,gxbar) \
1248{ \
1249  Cal_BddIndex_t __index1, __index2; \
1250  __index1 = (bddManager)->idToIndex[CalBddGetBddId(f)]; \
1251  __index2 = (bddManager)->idToIndex[CalBddGetBddId(g)]; \
1252  if(__index1 == __index2){ \
1253    CalBddGetThenBdd(f, fx); \
1254    CalBddGetElseBdd(f, fxbar); \
1255    CalBddGetThenBdd(g, gx); \
1256    CalBddGetElseBdd(g, gxbar); \
1257  } \
1258  else if(__index1 < __index2){ \
1259    CalBddGetThenBdd(f, fx); \
1260    CalBddGetElseBdd(f, fxbar); \
1261    gx = gxbar = g; \
1262  } \
1263  else{ \
1264    fx = fxbar = f; \
1265    CalBddGetThenBdd(g, gx); \
1266    CalBddGetElseBdd(g, gxbar); \
1267  } \
1268}
1269
1270#define CalBddIsForwarded(bdd) \
1271  (CAL_BDD_POINTER(CalBddGetElseBddNode(bdd)) == FORWARD_FLAG)
1272
1273#define CalBddNodeIsForwarded(bddNode) \
1274  (((CalAddress_t)(CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode)))) == FORWARD_FLAG)
1275
1276#define CalBddForward(bdd) \
1277{ \
1278  CalBddNode_t *_bddNode, *_bddNodeTagged; \
1279  _bddNodeTagged = CalBddGetBddNode(bdd); \
1280  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
1281  (bdd).bddId = _bddNode->thenBddId; \
1282  (bdd).bddNode = (CalBddNode_t*) \
1283                  (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
1284                   ^(CAL_TAG0(_bddNodeTagged))); \
1285}
1286
1287#define CalBddNodeForward(_bddNodeTagged) \
1288{ \
1289  CalBddNode_t *_bddNode; \
1290  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
1291  _bddNodeTagged = (CalBddNode_t*) \
1292                  (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
1293                   ^(CAL_TAG0(_bddNodeTagged))); \
1294}
1295
1296#define CalBddNodeIsForwardedTo(_bddNodeTagged) \
1297{ \
1298  CalBddNode_t *__bddNode;\
1299  __bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
1300  if(CalBddNodeGetElseBddNode(__bddNode) == FORWARD_FLAG){ \
1301    _bddNodeTagged = (CalBddNode_t*) \
1302                     (((CalAddress_t)(__bddNode->thenBddNode) & ~0xe)        \
1303                      ^(CAL_TAG0(_bddNodeTagged))); \
1304  } \
1305}
1306
1307#define CalRequestIsForwardedTo(request) \
1308{ \
1309  CalBddNode_t *__bddNode, *__bddNodeTagged; \
1310  __bddNodeTagged = (request).bddNode; \
1311  __bddNode = CAL_BDD_POINTER(__bddNodeTagged); \
1312  if(CalRequestNodeGetElseRequestNode(__bddNode) == FORWARD_FLAG){ \
1313    (request).bddId = __bddNode->thenBddId; \
1314    (request).bddNode = (CalBddNode_t*) \
1315                        (((CalAddress_t)(__bddNode->thenBddNode) & ~0xe)        \
1316                         ^(CAL_TAG0(__bddNodeTagged))); \
1317  } \
1318}
1319
1320#define CalBddIsForwardedTo CalRequestIsForwardedTo
1321
1322#define CalBddNormalize(fBdd, gBdd) \
1323{ \
1324  Cal_Bdd_t _tmpBdd; \
1325  if((unsigned long)CAL_BDD_POINTER(CalBddGetBddNode(gBdd)) < \
1326      (unsigned long)CAL_BDD_POINTER(CalBddGetBddNode(fBdd))){ \
1327    _tmpBdd = fBdd; \
1328    fBdd = gBdd; \
1329    gBdd = _tmpBdd; \
1330  } \
1331}
1332
1333/* Depth aliased as RefCount */
1334#define CalBddGetDepth CalBddGetRefCount
1335#define CalBddPutDepth CalBddPutRefCount
1336#define CalRequestNodeGetDepth CalBddNodeGetRefCount
1337#define CalRequestNodeGetRefCount CalBddNodeGetRefCount
1338#define CalRequestNodeAddRefCount CalBddNodeAddRefCount
1339#define CalRequestAddRefCount CalBddAddRefCount
1340#define CalRequestNodePutDepth CalBddNodePutRefCount
1341
1342#define CalITERequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar, hx, hxbar) \
1343{ \
1344  Cal_Bdd_t __f, __g, __h; \
1345  Cal_BddIndex_t __index1, __index2, __index3; \
1346  CalBddNode_t *__ptrIndirect; \
1347  CalRequestNodeGetThenRequest(requestNode, __f); \
1348  __ptrIndirect = CalRequestNodeGetElseRequestNode(requestNode); \
1349  CalRequestNodeGetThenRequest(__ptrIndirect, __g); \
1350  CalRequestNodeGetElseRequest(__ptrIndirect, __h); \
1351  __index1 = (bddManager)->idToIndex[CalBddGetBddId(__f)]; \
1352  __index2 = (bddManager)->idToIndex[CalBddGetBddId(__g)]; \
1353  __index3 = (bddManager)->idToIndex[CalBddGetBddId(__h)]; \
1354  if(__index1 == __index2){ \
1355    if(__index3 == __index1){ \
1356      CalBddGetThenBdd(__f, fx); \
1357      CalBddGetElseBdd(__f, fxbar); \
1358      CalBddGetThenBdd(__g, gx); \
1359      CalBddGetElseBdd(__g, gxbar); \
1360      CalBddGetThenBdd(__h, hx); \
1361      CalBddGetElseBdd(__h, hxbar); \
1362    } \
1363    else if(__index3 < __index1){ \
1364      fx = fxbar = __f; \
1365      gx = gxbar = __g; \
1366      CalBddGetThenBdd(__h, hx); \
1367      CalBddGetElseBdd(__h, hxbar); \
1368    } \
1369    else{ \
1370      CalBddGetThenBdd(__f, fx); \
1371      CalBddGetElseBdd(__f, fxbar); \
1372      CalBddGetThenBdd(__g, gx); \
1373      CalBddGetElseBdd(__g, gxbar); \
1374      hx = hxbar = __h; \
1375    } \
1376  } \
1377  else if(__index1 < __index2){ \
1378    if(__index3 == __index1){ \
1379      CalBddGetThenBdd(__f, fx); \
1380      CalBddGetElseBdd(__f, fxbar); \
1381      gx = gxbar = __g; \
1382      CalBddGetThenBdd(__h, hx); \
1383      CalBddGetElseBdd(__h, hxbar); \
1384    } \
1385    else if(__index3 < __index1){ \
1386      fx = fxbar = __f; \
1387      gx = gxbar = __g; \
1388      CalBddGetThenBdd(__h, hx); \
1389      CalBddGetElseBdd(__h, hxbar); \
1390    } \
1391    else{ \
1392      CalBddGetThenBdd(__f, fx); \
1393      CalBddGetElseBdd(__f, fxbar); \
1394      gx = gxbar = __g; \
1395      hx = hxbar = __h; \
1396    } \
1397  } \
1398  else{ \
1399    if(__index3 == __index2){ \
1400      fx = fxbar = __f; \
1401      CalBddGetThenBdd(__g, gx); \
1402      CalBddGetElseBdd(__g, gxbar); \
1403      CalBddGetThenBdd(__h, hx); \
1404      CalBddGetElseBdd(__h, hxbar); \
1405    } \
1406    else if(__index3 < __index2){ \
1407      fx = fxbar = __f; \
1408      gx = gxbar = __g; \
1409      CalBddGetThenBdd(__h, hx); \
1410      CalBddGetElseBdd(__h, hxbar); \
1411    } \
1412    else{ \
1413      fx = fxbar = __f; \
1414      CalBddGetThenBdd(__g, gx); \
1415      CalBddGetElseBdd(__g, gxbar); \
1416      hx = hxbar = __h; \
1417    } \
1418  } \
1419}
1420
1421
1422#define CalCacheTableOneInsert(bddManager, f, result, opCode, cacheLevel) CalCacheTableTwoInsert(bddManager, f, (bddManager)->bddOne, result, opCode, cacheLevel)
1423
1424#define CalCacheTableOneLookup(bddManager, f, opCode, resultPtr) CalCacheTableTwoLookup(bddManager, f, (bddManager)->bddOne, opCode, resultPtr)
1425
1426#ifdef USE_POWER_OF_2
1427#define CalDoHash2(thenBddNode, elseBddNode, table) \
1428   (((((CalAddress_t)thenBddNode) + ((CalAddress_t)elseBddNode)) / NODE_SIZE) & ((table)->numBins - 1))
1429#else
1430#define CalDoHash2(thenBddNode, elseBddNode, table) \
1431                              (((((CalAddress_t)thenBddNode) + \
1432                                 ((CalAddress_t)elseBddNode)) / NODE_SIZE)% \
1433                               (table)->numBins)
1434#endif
1435
1436#if HAVE_STDARG_H
1437EXTERN int CalBddPreProcessing(Cal_BddManager_t *bddManager, int count, ...);
1438#else
1439EXTERN int CalBddPreProcessing();
1440#endif
1441
1442/**AutomaticStart*************************************************************/
1443
1444/*---------------------------------------------------------------------------*/
1445/* Function prototypes                                                       */
1446/*---------------------------------------------------------------------------*/
1447
1448EXTERN Cal_Bdd_t CalBddIf(Cal_BddManager bddManager, Cal_Bdd_t F);
1449EXTERN int CalBddIsCubeStep(Cal_BddManager bddManager, Cal_Bdd_t f);
1450EXTERN int CalBddTypeAux(Cal_BddManager_t * bddManager, Cal_Bdd_t f);
1451EXTERN Cal_Bdd_t CalBddIdentity(Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd);
1452EXTERN void CalHashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t calOpProc);
1453EXTERN void CalHashTableReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t * uniqueTableForId);
1454EXTERN void CalAssociationListFree(Cal_BddManager_t * bddManager);
1455EXTERN void CalVarAssociationRepackUpdate(Cal_BddManager_t * bddManager, Cal_BddId_t id);
1456EXTERN void CalCheckAssociationValidity(Cal_BddManager_t * bddManager);
1457EXTERN void CalReorderAssociationFix(Cal_BddManager_t *bddManager);
1458EXTERN void CalRequestNodeListCompose(Cal_BddManager_t * bddManager, CalRequestNode_t * requestNodeList, Cal_BddIndex_t composeIndex);
1459EXTERN void CalHashTableComposeApply(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, Cal_BddIndex_t gIndex, CalHashTable_t **reqQueForCompose, CalHashTable_t **reqQueForITE);
1460EXTERN 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);
1461EXTERN void CalRequestNodeListArrayITE(Cal_BddManager_t *bddManager, CalRequestNode_t **requestNodeListArray);
1462EXTERN Cal_Bdd_t CalBddOpITEBF(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h);
1463EXTERN void CalHashTableITEApply(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **reqQueAtPipeDepth);
1464EXTERN Cal_Bdd_t CalBddITE(Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t H);
1465EXTERN Cal_Bdd_t CalBddManagerCreateNewVar(Cal_BddManager_t * bddManager, Cal_BddIndex_t index);
1466EXTERN void CalRequestNodeListArrayOp(Cal_BddManager_t * bddManager, CalRequestNode_t ** requestNodeListArray, CalOpProc_t calOpProc);
1467EXTERN Cal_Bdd_t CalBddOpBF(Cal_BddManager_t * bddManager, CalOpProc_t calOpProc, Cal_Bdd_t F, Cal_Bdd_t G);
1468EXTERN int main(int argc, char **argv);
1469EXTERN Cal_Bdd_t CalBddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *assoc);
1470EXTERN int CalOpBddVarSubstitute(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * resultBddPtr);
1471EXTERN long CalBddFindBlock(Cal_Block block, long index);
1472EXTERN void CalBddBlockDelta(Cal_Block b, long delta);
1473EXTERN Cal_Block CalBddShiftBlock(Cal_BddManager_t *bddManager, Cal_Block b, long index);
1474EXTERN unsigned long CalBlockMemoryConsumption(Cal_Block block);
1475EXTERN void CalFreeBlockRecursively(Cal_Block block);
1476EXTERN CalCacheTable_t * CalCacheTableTwoInit(Cal_BddManager_t *bddManager);
1477EXTERN int CalCacheTableTwoQuit(CalCacheTable_t *cacheTable);
1478EXTERN void CalCacheTableTwoInsert(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t result, unsigned long opCode, int cacheLevel);
1479EXTERN int CalCacheTableTwoLookup(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned long opCode, Cal_Bdd_t *resultBddPtr);
1480EXTERN void CalCacheTableTwoFlush(CalCacheTable_t *cacheTable);
1481EXTERN int CalCacheTableTwoFlushAll(CalCacheTable_t *cacheTable);
1482EXTERN void CalCacheTableTwoGCFlush(CalCacheTable_t *cacheTable);
1483EXTERN void CalCacheTableTwoRepackUpdate(CalCacheTable_t *cacheTable);
1484EXTERN void CalCheckCacheTableValidity(Cal_BddManager bddManager);
1485EXTERN void CalCacheTableTwoFixResultPointers(Cal_BddManager_t *bddManager);
1486EXTERN void CalCacheTablePrint(Cal_BddManager_t *bddManager);
1487EXTERN void CalBddManagerGetCacheTableData(Cal_BddManager_t *bddManager, unsigned long *cacheSize, unsigned long *cacheEntries, unsigned long *cacheInsertions, unsigned long *cacheLookups, unsigned long *cacheHits, unsigned long *cacheCollisions);
1488EXTERN void CalCacheTableRehash(Cal_BddManager_t *bddManager);
1489EXTERN void CalCacheTableTwoFlushAssociationId(Cal_BddManager_t *bddManager, int associationId);
1490EXTERN unsigned long CalCacheTableMemoryConsumption(CalCacheTable_t *cacheTable);
1491EXTERN void CalBddManagerGCCheck(Cal_BddManager_t * bddManager);
1492EXTERN int CalHashTableGC(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable);
1493EXTERN void CalRepackNodesAfterGC(Cal_BddManager_t *bddManager);
1494EXTERN CalHashTable_t * CalHashTableInit(Cal_BddManager_t *bddManager, Cal_BddId_t bddId);
1495EXTERN int CalHashTableQuit(Cal_BddManager_t *bddManager, CalHashTable_t * hashTable);
1496EXTERN void CalHashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t * bddNode);
1497EXTERN int CalHashTableFindOrAdd(CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
1498EXTERN int CalHashTableAddDirectAux(CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
1499EXTERN void CalHashTableCleanUp(CalHashTable_t * hashTable);
1500EXTERN int CalHashTableLookup(CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
1501EXTERN void CalHashTableDelete(CalHashTable_t * hashTable, CalBddNode_t * bddNode);
1502EXTERN int CalUniqueTableForIdLookup(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
1503EXTERN int CalUniqueTableForIdFindOrAdd(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t * bddPtr);
1504EXTERN void CalHashTableRehash(CalHashTable_t *hashTable, int grow);
1505EXTERN void CalUniqueTableForIdRehashNode(CalHashTable_t *hashTable, CalBddNode_t *bddNode, CalBddNode_t *thenBddNode, CalBddNode_t *elseBddNode);
1506EXTERN unsigned long CalBddUniqueTableNumLockedNodes(Cal_BddManager_t *bddManager, CalHashTable_t *uniqueTableForId);
1507EXTERN void CalPackNodes(Cal_BddManager_t *bddManager);
1508EXTERN void CalBddPackNodesForSingleId(Cal_BddManager_t *bddManager, Cal_BddId_t id);
1509EXTERN void CalBddPackNodesAfterReorderForSingleId(Cal_BddManager_t *bddManager, int fixForwardedNodesFlag, int bestIndex, int bottomIndex);
1510EXTERN void CalBddPackNodesForMultipleIds(Cal_BddManager_t *bddManager, Cal_BddId_t beginId, int numLevels);
1511EXTERN CalHashTable_t * CalHashTableOneInit(Cal_BddManager_t * bddManager, int itemSize);
1512EXTERN void CalHashTableOneQuit(CalHashTable_t * hashTable);
1513EXTERN void CalHashTableOneInsert(CalHashTable_t * hashTable, Cal_Bdd_t keyBdd, char * valuePtr);
1514EXTERN int CalHashTableOneLookup(CalHashTable_t * hashTable, Cal_Bdd_t keyBdd, char ** valuePtrPtr);
1515EXTERN int CalHashTableThreeFindOrAdd(CalHashTable_t * hashTable, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, Cal_Bdd_t * bddPtr);
1516EXTERN void CalSetInteract(Cal_BddManager_t *bddManager, int x, int y);
1517EXTERN int CalTestInteract(Cal_BddManager_t *bddManager, int x, int y);
1518EXTERN int CalInitInteract(Cal_BddManager_t *bddManager);
1519EXTERN CalPageManager_t * CalPageManagerInit(int numPagesPerSegment);
1520EXTERN int CalPageManagerQuit(CalPageManager_t * pageManager);
1521EXTERN void CalPageManagerPrint(CalPageManager_t * pageManager);
1522EXTERN CalNodeManager_t * CalNodeManagerInit(CalPageManager_t * pageManager);
1523EXTERN int CalNodeManagerQuit(CalNodeManager_t * nodeManager);
1524EXTERN void CalNodeManagerPrint(CalNodeManager_t * nodeManager);
1525EXTERN CalAddress_t * CalPageManagerAllocPage(CalPageManager_t * pageManager);
1526EXTERN void CalPageManagerFreePage(CalPageManager_t * pageManager, CalAddress_t * page);
1527EXTERN int CalIncreasingOrderCompare(const void *a, const void *b);
1528EXTERN int CalDecreasingOrderCompare(const void *a, const void *b);
1529EXTERN void CalBddReorderFixProvisionalNodes(Cal_BddManager_t *bddManager);
1530EXTERN void CalCheckPipelineValidity(Cal_BddManager_t *bddManager);
1531EXTERN char * CalBddVarName(Cal_BddManager_t *bddManager, Cal_Bdd_t v, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env);
1532EXTERN void CalBddNumberSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalHashTable_t *hashTable, long *next);
1533EXTERN void CalBddMarkSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f);
1534EXTERN int CalOpExists(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * resultBddPtr);
1535EXTERN int CalOpRelProd(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t * resultBddPtr);
1536EXTERN int CalOpCofactor(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t c, Cal_Bdd_t * resultBddPtr);
1537EXTERN void CalBddReorderAuxBF(Cal_BddManager_t * bddManager);
1538EXTERN void CalBddReorderFixCofactors(Cal_BddManager bddManager, Cal_BddId_t id);
1539EXTERN void CalFixupAssoc(Cal_BddManager_t *bddManager, long id1, long id2, CalAssociation_t *assoc);
1540EXTERN void CalBddReorderReclaimForwardedNodes(Cal_BddManager bddManager, int startIndex, int endIndex);
1541EXTERN void CalBddReorderBlockSift(Cal_BddManager_t *bddManager, double maxSizeFactor);
1542EXTERN void CalBddReorderBlockWindow(Cal_BddManager bddManager, Cal_Block block, char *levels);
1543EXTERN void CalBddReorderAuxDF(Cal_BddManager_t *bddManager);
1544EXTERN void CalAlignCollisionChains(Cal_BddManager_t *bddManager);
1545EXTERN void CalBddReorderFixUserBddPtrs(Cal_BddManager bddManager);
1546EXTERN int CalCheckAllValidity(Cal_BddManager bddManager);
1547EXTERN int CalCheckValidityOfNodesForId(Cal_BddManager bddManager, int id);
1548EXTERN int CalCheckValidityOfNodesForWindow(Cal_BddManager bddManager, Cal_BddIndex_t index, int numLevels);
1549EXTERN int CalCheckValidityOfANode(Cal_BddManager_t *bddManager, CalBddNode_t *bddNode, int id);
1550EXTERN void CalCheckRefCountValidity(Cal_BddManager_t *bddManager);
1551EXTERN int CalCheckAssoc(Cal_BddManager_t *bddManager);
1552EXTERN void CalBddReorderVarSift(Cal_BddManager bddManager, double maxSizeFactor);
1553EXTERN void CalBddReorderVarWindow(Cal_BddManager bddManager, char *levels);
1554EXTERN int CalOpAnd(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
1555EXTERN int CalOpNand(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
1556EXTERN int CalOpOr(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
1557EXTERN int CalOpXor(Cal_BddManager_t * bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t * resultBddPtr);
1558EXTERN Cal_Bdd_t CalOpITE(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, CalHashTable_t **reqQueForITE);
1559EXTERN int main(int argc, char ** argv);
1560EXTERN void CalUniqueTablePrint(Cal_BddManager_t *bddManager);
1561EXTERN void CalBddFunctionPrint(Cal_BddManager_t * bddManager, Cal_Bdd_t calBdd, char * name);
1562EXTERN int CalBddPreProcessing(Cal_BddManager_t *bddManager, int count, ...);
1563EXTERN int CalBddPostProcessing(Cal_BddManager_t *bddManager);
1564EXTERN int CalBddArrayPreProcessing(Cal_BddManager_t *bddManager, Cal_Bdd *userBddArray);
1565EXTERN Cal_Bdd_t CalBddGetInternalBdd(Cal_BddManager bddManager, Cal_Bdd userBdd);
1566EXTERN Cal_Bdd CalBddGetExternalBdd(Cal_BddManager_t *bddManager, Cal_Bdd_t internalBdd);
1567EXTERN void CalBddFatalMessage(char *string);
1568EXTERN void CalBddWarningMessage(char *string);
1569EXTERN void CalBddNodePrint(CalBddNode_t *bddNode);
1570EXTERN void CalBddPrint(Cal_Bdd_t calBdd);
1571EXTERN void CalHashTablePrint(CalHashTable_t *hashTable);
1572EXTERN void CalHashTableOnePrint(CalHashTable_t *hashTable, int flag);
1573EXTERN void CalUtilSRandom(long seed);
1574EXTERN long CalUtilRandom(void);
1575
1576/**AutomaticEnd***************************************************************/
1577
1578#endif /* _INT */
Note: See TracBrowser for help on using the repository browser.