src/calBdd/calInt.h File Reference

#include "cal.h"

Include dependency graph for calInt.h:

This graph shows which files directly or indirectly include this file:

Data Structures
struct	Cal_BddStruct
struct	CalNodeManagerStruct
struct	CalPageManagerStruct
struct	CalBddNodeStruct
struct	CalHashTableStruct
struct	CalAssociationStruct
struct	Cal_BlockStruct
struct	Cal_BddManagerStruct
Defines
#define	CAL_MIN_GC_LIMIT 10000
#define	CAL_REPACK_AFTER_GC_THRESHOLD 0.75
#define	CAL_TABLE_REPACK_THRESHOLD 0.9
#define	CAL_BDD_REORDER_THRESHOLD 10000
#define	CAL_NUM_PAGES_THRESHOLD 3
#define	CAL_NUM_FORWARDED_NODES_LIMIT 50000
#define	CAL_GC_CHECK 100
#define	NODE_SIZE sizeof(CalBddNode_t)
#define	PAGE_SIZE 4096
#define	LG_PAGE_SIZE 12
#define	NUM_NODES_PER_PAGE (PAGE_SIZE/NODE_SIZE)
#define	MAX_NUM_SEGMENTS 32
#define	NUM_PAGES_PER_SEGMENT 64
#define	MIN_NUM_PAGES_PER_SEGMENT 4
#define	MAX_NUM_PAGES 10
#define	MIN_REC_SIZE CAL_ALLOC_ALIGNMENT
#define	MAX_REC_SIZE (sizeof(CalHashTable_t))
#define	NUM_REC_MGRS (((MAX_REC_SIZE-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT)+1)
#define	TRUE 1
#define	FALSE 0
#define	CAL_BDD_OK 0
#define	CAL_BDD_OVERFLOWED 1
#define	CAL_BDD_NULL_ID ((unsigned short) ((1 << 8*sizeof(unsigned short)) - 1))
#define	CAL_BDD_CONST_ID 0
#define	CAL_MAX_VAR_ID ((unsigned short) (CAL_BDD_NULL_ID - 1))
#define	CAL_BDD_NULL_INDEX (unsigned short) ((1 << 8*sizeof(unsigned short)) - 1)
#define	CAL_BDD_CONST_INDEX CAL_BDD_NULL_INDEX
#define	CAL_MAX_VAR_INDEX (CAL_BDD_NULL_INDEX - 1)
#define	CAL_MAX_REF_COUNT (unsigned short)((1 << 8*sizeof(char)) - 1)
#define	CAL_INFINITY (1 << 20)
#define	MAX_INSERT_DEPTH 256
#define	PIPELINE_EXECUTION_DEPTH 1
#define	DEFAULT_DEPTH 4
#define	DEFAULT_MAX_DEPTH 6
#define	FORWARD_FLAG 0
#define	HASH_TABLE_DEFAULT_MAX_DENSITY 5
#define	HASH_TABLE_DEFAULT_SIZE_INDEX 8
#define	HASH_TABLE_DEFAULT_NUM_BINS TABLE_SIZE(HASH_TABLE_DEFAULT_SIZE_INDEX)
#define	HASH_TABLE_DEFAULT_MAX_CAPACITY HASH_TABLE_DEFAULT_NUM_BINS*HASH_TABLE_DEFAULT_MAX_DENSITY
#define	USE_POWER_OF_2
#define	TABLE_SIZE(sizeIndex) (1<<sizeIndex)
#define	CAL_OP_INVALID 0x0000
#define	CAL_OP_OR 0x1000
#define	CAL_OP_AND 0x2000
#define	CAL_OP_NAND 0x3000
#define	CAL_OP_QUANT 0x4000
#define	CAL_OP_REL_PROD 0x5000
#define	CAL_OP_COMPOSE 0x6000
#define	CAL_OP_SUBST 0x7000
#define	CAL_OP_VAR_SUBSTITUTE 0x8000
#define	CAL_LARGE_BDD (1<<19)
#define	CalNodeManagerAllocNode(nodeManager, node)
#define	CalNodeManagerFreeNode(nodeManager, node)
#define	CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd, next, node)
#define	CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode)
#define	CAL_BDD_NEW_REC(bddManager, type) ((type *)Cal_MemNewRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT]))
#define	CAL_BDD_FREE_REC(bddManager, rec, type) Cal_MemFreeRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT], (rec))
#define	CalBddIdNeedsRepacking(bddManager, id)
#define	CAL_BDD_POINTER(f)
#define	CAL_TAG0(pointer) ((CalAddress_t)((CalAddress_t)(pointer) & 0x1))
#define	CalBddIsComplement(calBdd) ((int)CAL_TAG0((calBdd).bddNode))
#define	CalBddUpdatePhase(calBdd, complement)
#define	CalBddZero(bddManager) ((bddManager)->bddZero)
#define	CalBddOne(bddManager) ((bddManager)->bddOne)
#define	CalBddNull(bddManager) ((bddManager)->bddNull)
#define	CalBddIsBddConst(calBdd) ((calBdd).bddId == 0)
#define	CalBddIsEqual(calBdd1, calBdd2) (((calBdd1).bddNode == (calBdd2).bddNode))
#define	CalBddIsComplementEqual(calBdd1, calBdd2)
#define	CalBddSameOrNegation(calBdd1, calBdd2) (CAL_BDD_POINTER((calBdd1).bddNode) == CAL_BDD_POINTER((calBdd2).bddNode))
#define	CalBddGetCofactors(calBdd, varId, fx, fxbar)
#define	CalBddGetThenBddId(calBdd) CAL_BDD_POINTER((calBdd).bddNode)->thenBddId
#define	CalBddGetElseBddId(calBdd) CAL_BDD_POINTER((calBdd).bddNode)->elseBddId
#define	CalBddGetThenBddIndex(bddManager, calBdd) (bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->thenBddId])
#define	CalBddGetElseBddIndex(bddManager, calBdd) (bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->elseBddId])
#define	CalBddGetThenBddNode(calBdd)
#define	CalBddGetElseBddNode(calBdd)
#define	CalBddGetThenBdd(calBdd, _thenBdd)
#define	CalBddGetElseBdd(calBdd, _elseBdd)
#define	CalBddGetBddId(calBdd) ((calBdd).bddId)
#define	CalBddGetBddIndex(bddManager, calBdd) (bddManager->idToIndex[(calBdd).bddId])
#define	CalBddGetBddNode(calBdd) ((calBdd).bddNode)
#define	CalBddGetBddNodeNot(calBdd) ((CalBddNode_t*)(((CalAddress_t)((calBdd).bddNode))^0x1))
#define	CalBddGetNextBddNode(calBdd)
#define	CalBddPutThenBddId(calBdd, _thenBddId) (CAL_BDD_POINTER((calBdd).bddNode)->thenBddId = _thenBddId)
#define	CalBddPutElseBddId(calBdd, _elseBddId) (CAL_BDD_POINTER((calBdd).bddNode)->elseBddId = _elseBddId)
#define	CalBddPutThenBddNode(calBdd, _thenBddNode)
#define	CalBddPutElseBddNode(calBdd, _elseBddNode)
#define	CalBddPutThenBdd(calBdd, thenBdd)
#define	CalBddPutElseBdd(calBdd, elseBdd)
#define	CalBddPutBddId(calBdd, _bddId) ((calBdd).bddId = _bddId)
#define	CalBddPutBddNode(calBdd, _bddNode) ((calBdd).bddNode = _bddNode)
#define	CalBddPutNextBddNode(calBdd, _nextBddNode)
#define	CalBddGetRefCount(calBdd, refCount)
#define	CalBddPutRefCount(calBdd, count)
#define	CalBddIcrRefCount(calBdd)
#define	CalBddDcrRefCount(calBdd)
#define	CalBddAddRefCount(calBdd, num)
#define	CalBddIsRefCountZero(calBdd)
#define	CalBddIsRefCountMax(calBdd)
#define	CalBddFree(calBdd) CalBddDcrRefCount(calBdd)
#define	CalBddIsOutPos(calBdd) (!(((CalAddress_t)(calBdd).bddNode) & 0x1))
#define	CalBddIsBddOne(manager, calBdd) CalBddIsEqual(calBdd, (manager)->bddOne)
#define	CalBddIsBddZero(manager, calBdd) CalBddIsEqual(calBdd, (manager)->bddZero)
#define	CalBddIsBddNull(manager, calBdd) CalBddIsEqual(calBdd,(manager)->bddNull)
#define	CalBddManagerGetBddOne(manager) ((manager)->bddOne)
#define	CalBddManagerGetBddZero(manager) ((manager)->bddZero)
#define	CalBddManagerGetBddNull(manager) (manager)->bddNull
#define	CalBddGetMinId2(bddManager, calBdd1, calBdd2, topId)
#define	CalBddGetMinId3(bddManager, calBdd1, calBdd2, calBdd3, topId)
#define	CalBddGetMinIndex2(bddManager, calBdd1, calBdd2, topIndex)
#define	CalBddGetMinIndex3(bddManager, calBdd1, calBdd2, calBdd3, topIndex)
#define	CalBddGetMinIdAndMinIndex(bddManager, calBdd1, calBdd2, topId, topIndex)
#define	CalBddNot(calBdd1, calBdd2)
#define	CAL_BDD_OUT_OF_ORDER(f, g) ((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g))
#define	CAL_BDD_SWAP(f, g)
#define	CalBddNodeGetThenBddId(_bddNode) ((_bddNode)->thenBddId)
#define	CalBddNodeGetElseBddId(_bddNode) ((_bddNode)->elseBddId)
#define	CalBddNodeGetThenBddIndex(bddManager, _bddNode) bddManager->idToIndex[((_bddNode)->thenBddId)]
#define	CalBddNodeGetElseBddIndex(bddManager, _bddNode) bddManager->idToIndex[((_bddNode)->elseBddId)]
#define	CalBddNodeGetThenBddNode(_bddNode) ((CalBddNode_t *)((CalAddress_t)((_bddNode)->thenBddNode) & ~0xe))
#define	CalBddNodeGetElseBddNode(_bddNode) ((CalBddNode_t *)((CalAddress_t)((_bddNode)->elseBddNode) & ~0xe))
#define	CalBddNodeGetThenBdd(_bddNode, _thenBdd)
#define	CalBddNodeGetElseBdd(_bddNode, _elseBdd)
#define	CalBddNodeGetNextBddNode(_bddNode) ((CalBddNode_t *)(((CalAddress_t) ((_bddNode)->nextBddNode)) & ~0xf))
#define	CalBddNodePutThenBddId(_bddNode, _thenBddId) ((_bddNode)->thenBddId = _thenBddId)
#define	CalBddNodePutElseBddId(_bddNode, _elseBddId) ((_bddNode)->elseBddId = _elseBddId)
#define	CalBddNodePutThenBddNode(_bddNode, _thenBddNode)
#define	CalBddNodePutElseBddNode(_bddNode, _elseBddNode)
#define	CalBddNodePutThenBdd(_bddNode, _thenBdd)
#define	CalBddNodePutElseBdd(_bddNode, _elseBdd)
#define	CalBddNodePutNextBddNode(_bddNode, _nextBddNode)
#define	CalBddNodeGetRefCount(_bddNode, refCount)
#define	CalBddNodePutRefCount(_bddNode, count)
#define	CalBddNodeDcrRefCount(_bddNode)
#define	CalBddNodeIcrRefCount(_bddNode)
#define	CalBddNodeAddRefCount(__bddNode, num)
#define	CalBddNodeIsRefCountZero(_bddNode)
#define	CalBddNodeIsRefCountMax(_bddNode)
#define	CalBddNodeIsOutPos(bddNode) (!(((CalAddress_t)bddNode) & 0x1))
#define	CalBddNodeRegular(bddNode) ((CalBddNode_t *)(((unsigned long)(bddNode)) & ~01))
#define	CalBddRegular(calBdd1, calBdd2)
#define	CalBddNodeEqual(calBddNode1, calBddNode2) ((CalAddress_t)calBddNode1 == (CalAddress_t)calBddNode2)
#define	CalBddNodeNot(bddNode) ((CalBddNode_t*)(((CalAddress_t)(bddNode))^0x1))
#define	CalBddIsMarked(calBdd) CalBddNodeIsMarked(CAL_BDD_POINTER((calBdd).bddNode))
#define	CalBddMark(calBdd) CalBddNodeMark(CAL_BDD_POINTER((calBdd).bddNode))
#define	CalBddUnmark(calBdd) CalBddNodeUnmark(CAL_BDD_POINTER((calBdd).bddNode))
#define	CalBddGetMark(calBdd) CalBddNodeGetMark(CAL_BDD_POINTER((calBdd).bddNode))
#define	CalBddPutMark(calBdd, mark) CalBddNodePutMark(CAL_BDD_POINTER((calBdd).bddNode), (mark))
#define	CalBddNodeIsMarked(bddNode) ((((CalAddress_t)((bddNode)->thenBddNode)) & 0x4) >> 2)
#define	CalBddNodeMark(bddNode)
#define	CalBddNodeUnmark(bddNode)
#define	CalBddNodeGetMark(bddNode) ((((CalAddress_t)((bddNode)->thenBddNode)) & 0xc) >> 2)
#define	CalBddNodePutMark(bddNode, mark)
#define	CalRequestGetThenRequestId CalBddGetThenBddId
#define	CalRequestGetElseRequestId CalBddGetElseBddId
#define	CalRequestGetThenRequestNode CalBddGetThenBddNode
#define	CalRequestGetElseRequestNode CalBddGetElseBddNode
#define	CalRequestGetThenRequest CalBddGetThenBdd
#define	CalRequestGetElseRequest CalBddGetElseBdd
#define	CalRequestGetRequestId CalBddGetBddId
#define	CalRequestGetRequestNode CalBddGetBddNode
#define	CalRequestGetF CalBddGetThenBdd
#define	CalRequestGetG CalBddGetElseBdd
#define	CalRequestGetNextNode CalBddGetNextBddNode
#define	CalRequestPutThenRequestId CalBddPutThenBddId
#define	CalRequestPutElseRequestId CalBddPutElseBddId
#define	CalRequestPutThenRequestNode CalBddPutThenBddNode
#define	CalRequestPutElseRequestNode CalBddPutElseBddNode
#define	CalRequestPutThenRequest CalBddPutThenBdd
#define	CalRequestPutElseRequest CalBddPutElseBdd
#define	CalRequestPutRequestId CalBddPutBddId
#define	CalRequestPutRequestNode CalBddPutBddNode
#define	CalRequestPutF CalBddPutThenBdd
#define	CalRequestPutG CalBddPutElseBdd
#define	CalRequestPutNextNode CalBddPutNextBddNode
#define	CalRequestNodeGetThenRequestId CalBddNodeGetThenBddId
#define	CalRequestNodeGetElseRequestId CalBddNodeGetElseBddId
#define	CalRequestNodeGetThenRequestNode CalBddNodeGetThenBddNode
#define	CalRequestNodeGetElseRequestNode CalBddNodeGetElseBddNode
#define	CalRequestNodeGetThenRequest CalBddNodeGetThenBdd
#define	CalRequestNodeGetElseRequest CalBddNodeGetElseBdd
#define	CalRequestNodeGetF CalBddNodeGetThenBdd
#define	CalRequestNodeGetG CalBddNodeGetElseBdd
#define	CalRequestNodeGetNextRequestNode CalBddNodeGetNextBddNode
#define	CalRequestNodePutThenRequestId CalBddNodePutThenBddId
#define	CalRequestNodePutElseRequestId CalBddNodePutElseBddId
#define	CalRequestNodePutThenRequestNode CalBddNodePutThenBddNode
#define	CalRequestNodePutElseRequestNode CalBddNodePutElseBddNode
#define	CalRequestNodePutThenRequest CalBddNodePutThenBdd
#define	CalRequestNodePutElseRequest CalBddNodePutElseBdd
#define	CalRequestNodePutF CalBddNodePutThenBdd
#define	CalRequestNodePutG CalBddNodePutElseBdd
#define	CalRequestNodePutNextRequestNode CalBddNodePutNextBddNode
#define	CalRequestIsNull(calRequest)
#define	CalRequestIsMarked CalBddIsMarked
#define	CalRequestMark CalBddMark
#define	CalRequestUnmark CalBddUnmark
#define	CalRequestGetMark CalBddGetMark
#define	CalRequestPutMark CalBddPutMark
#define	CalRequestNodeIsMarked CalBddNodeIsMarked
#define	CalRequestNodeMark CalBddNodeMark
#define	CalRequestNodeUnmark CalBddNodeUnmark
#define	CalRequestNodeGetMark CalBddNodeGetMark
#define	CalRequestNodePutMark CalBddNodePutMark
#define	CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar)
#define	CalBddPairGetCofactors(bddManager, f, g, fx, fxbar, gx, gxbar)
#define	CalBddIsForwarded(bdd) (CAL_BDD_POINTER(CalBddGetElseBddNode(bdd)) == FORWARD_FLAG)
#define	CalBddNodeIsForwarded(bddNode) (((CalAddress_t)(CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode)))) == FORWARD_FLAG)
#define	CalBddForward(bdd)
#define	CalBddNodeForward(_bddNodeTagged)
#define	CalBddNodeIsForwardedTo(_bddNodeTagged)
#define	CalRequestIsForwardedTo(request)
#define	CalBddIsForwardedTo CalRequestIsForwardedTo
#define	CalBddNormalize(fBdd, gBdd)
#define	CalBddGetDepth CalBddGetRefCount
#define	CalBddPutDepth CalBddPutRefCount
#define	CalRequestNodeGetDepth CalBddNodeGetRefCount
#define	CalRequestNodeGetRefCount CalBddNodeGetRefCount
#define	CalRequestNodeAddRefCount CalBddNodeAddRefCount
#define	CalRequestAddRefCount CalBddAddRefCount
#define	CalRequestNodePutDepth CalBddNodePutRefCount
#define	CalITERequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar, hx, hxbar)
#define	CalCacheTableOneInsert(bddManager, f, result, opCode, cacheLevel) CalCacheTableTwoInsert(bddManager, f, (bddManager)->bddOne, result, opCode, cacheLevel)
#define	CalCacheTableOneLookup(bddManager, f, opCode, resultPtr) CalCacheTableTwoLookup(bddManager, f, (bddManager)->bddOne, opCode, resultPtr)
#define	CalDoHash2(thenBddNode, elseBddNode, table) (((((CalAddress_t)thenBddNode) + ((CalAddress_t)elseBddNode)) / NODE_SIZE) & ((table)->numBins - 1))
Typedefs
typedef struct Cal_BddStruct	Cal_Bdd_t
typedef struct CalBddNodeStruct	CalBddNode_t
typedef unsigned short	Cal_BddRefCount_t
typedef struct CalPageManagerStruct	CalPageManager_t
typedef struct CalNodeManagerStruct	CalNodeManager_t
typedef struct CalListStruct	CalList_t
typedef struct CalHashTableStruct	CalHashTable_t
typedef struct CalHashTableStruct *	CalReqQueForId_t
typedef struct CalHashTableStruct	CalReqQueForIdAtDepth_t
typedef struct CalAssociationStruct	CalAssociation_t
typedef struct CalBddNodeStruct	CalRequestNode_t
typedef struct Cal_BddStruct	CalRequest_t
typedef struct CalCacheTableStruct	CalCacheTable_t
typedef int(*	CalBddNodeToIndexFn_t )(CalBddNode_t *, Cal_BddId_t)
typedef unsigned long	CalAddress_t
typedef struct Cal_BlockStruct	Cal_Block_t
typedef int(*	CalOpProc_t )(Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t, Cal_Bdd_t *)
typedef int(*	CalOpProc1_t )(Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t *)
typedef enum CalPipeStateEnum	CalPipeState_t
Enumerations
enum	CalPipeStateEnum { READY, CREATE, UPDATE }
Functions
EXTERN int	CalBddPreProcessing ()
EXTERN Cal_Bdd_t	CalBddIf (Cal_BddManager bddManager, Cal_Bdd_t F)
EXTERN int	CalBddIsCubeStep (Cal_BddManager bddManager, Cal_Bdd_t f)
EXTERN int	CalBddTypeAux (Cal_BddManager_t *bddManager, Cal_Bdd_t f)
EXTERN Cal_Bdd_t	CalBddIdentity (Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd)
EXTERN void	CalHashTableApply (Cal_BddManager_t bddManager, CalHashTable_t hashTable, CalHashTable_t **reqQueAtPipeDepth, CalOpProc_t calOpProc)
EXTERN void	CalHashTableReduce (Cal_BddManager_t bddManager, CalHashTable_t hashTable, CalHashTable_t *uniqueTableForId)
EXTERN void	CalAssociationListFree (Cal_BddManager_t *bddManager)
EXTERN void	CalVarAssociationRepackUpdate (Cal_BddManager_t *bddManager, Cal_BddId_t id)
EXTERN void	CalCheckAssociationValidity (Cal_BddManager_t *bddManager)
EXTERN void	CalReorderAssociationFix (Cal_BddManager_t *bddManager)
EXTERN void	CalRequestNodeListCompose (Cal_BddManager_t bddManager, CalRequestNode_t requestNodeList, Cal_BddIndex_t composeIndex)
EXTERN void	CalHashTableComposeApply (Cal_BddManager_t bddManager, CalHashTable_t hashTable, Cal_BddIndex_t gIndex, CalHashTable_t reqQueForCompose, CalHashTable_t reqQueForITE)
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)
EXTERN void	CalRequestNodeListArrayITE (Cal_BddManager_t bddManager, CalRequestNode_t *requestNodeListArray)
EXTERN Cal_Bdd_t	CalBddOpITEBF (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h)
EXTERN void	CalHashTableITEApply (Cal_BddManager_t bddManager, CalHashTable_t hashTable, CalHashTable_t **reqQueAtPipeDepth)
EXTERN Cal_Bdd_t	CalBddITE (Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t H)
EXTERN Cal_Bdd_t	CalBddManagerCreateNewVar (Cal_BddManager_t *bddManager, Cal_BddIndex_t index)
EXTERN void	CalRequestNodeListArrayOp (Cal_BddManager_t bddManager, CalRequestNode_t *requestNodeListArray, CalOpProc_t calOpProc)
EXTERN Cal_Bdd_t	CalBddOpBF (Cal_BddManager_t *bddManager, CalOpProc_t calOpProc, Cal_Bdd_t F, Cal_Bdd_t G)
EXTERN int	main (int argc, char **argv)
EXTERN Cal_Bdd_t	CalBddVarSubstitute (Cal_BddManager bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *assoc)
EXTERN int	CalOpBddVarSubstitute (Cal_BddManager_t bddManager, Cal_Bdd_t f, Cal_Bdd_t resultBddPtr)
EXTERN long	CalBddFindBlock (Cal_Block block, long index)
EXTERN void	CalBddBlockDelta (Cal_Block b, long delta)
EXTERN Cal_Block	CalBddShiftBlock (Cal_BddManager_t *bddManager, Cal_Block b, long index)
EXTERN unsigned long	CalBlockMemoryConsumption (Cal_Block block)
EXTERN void	CalFreeBlockRecursively (Cal_Block block)
EXTERN CalCacheTable_t *	CalCacheTableTwoInit (Cal_BddManager_t *bddManager)
EXTERN int	CalCacheTableTwoQuit (CalCacheTable_t *cacheTable)
EXTERN void	CalCacheTableTwoInsert (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t result, unsigned long opCode, int cacheLevel)
EXTERN int	CalCacheTableTwoLookup (Cal_BddManager_t bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned long opCode, Cal_Bdd_t resultBddPtr)
EXTERN void	CalCacheTableTwoFlush (CalCacheTable_t *cacheTable)
EXTERN int	CalCacheTableTwoFlushAll (CalCacheTable_t *cacheTable)
EXTERN void	CalCacheTableTwoGCFlush (CalCacheTable_t *cacheTable)
EXTERN void	CalCacheTableTwoRepackUpdate (CalCacheTable_t *cacheTable)
EXTERN void	CalCheckCacheTableValidity (Cal_BddManager bddManager)
EXTERN void	CalCacheTableTwoFixResultPointers (Cal_BddManager_t *bddManager)
EXTERN void	CalCacheTablePrint (Cal_BddManager_t *bddManager)
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)
EXTERN void	CalCacheTableRehash (Cal_BddManager_t *bddManager)
EXTERN void	CalCacheTableTwoFlushAssociationId (Cal_BddManager_t *bddManager, int associationId)
EXTERN unsigned long	CalCacheTableMemoryConsumption (CalCacheTable_t *cacheTable)
EXTERN void	CalBddManagerGCCheck (Cal_BddManager_t *bddManager)
EXTERN int	CalHashTableGC (Cal_BddManager_t bddManager, CalHashTable_t hashTable)
EXTERN void	CalRepackNodesAfterGC (Cal_BddManager_t *bddManager)
EXTERN CalHashTable_t *	CalHashTableInit (Cal_BddManager_t *bddManager, Cal_BddId_t bddId)
EXTERN int	CalHashTableQuit (Cal_BddManager_t bddManager, CalHashTable_t hashTable)
EXTERN void	CalHashTableAddDirect (CalHashTable_t hashTable, CalBddNode_t bddNode)
EXTERN int	CalHashTableFindOrAdd (CalHashTable_t hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t bddPtr)
EXTERN int	CalHashTableAddDirectAux (CalHashTable_t hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t bddPtr)
EXTERN void	CalHashTableCleanUp (CalHashTable_t *hashTable)
EXTERN int	CalHashTableLookup (CalHashTable_t hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t bddPtr)
EXTERN void	CalHashTableDelete (CalHashTable_t hashTable, CalBddNode_t bddNode)
EXTERN int	CalUniqueTableForIdLookup (Cal_BddManager_t bddManager, CalHashTable_t hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t *bddPtr)
EXTERN int	CalUniqueTableForIdFindOrAdd (Cal_BddManager_t bddManager, CalHashTable_t hashTable, Cal_Bdd_t thenBdd, Cal_Bdd_t elseBdd, Cal_Bdd_t *bddPtr)
EXTERN void	CalHashTableRehash (CalHashTable_t *hashTable, int grow)
EXTERN void	CalUniqueTableForIdRehashNode (CalHashTable_t hashTable, CalBddNode_t bddNode, CalBddNode_t thenBddNode, CalBddNode_t elseBddNode)
EXTERN unsigned long	CalBddUniqueTableNumLockedNodes (Cal_BddManager_t bddManager, CalHashTable_t uniqueTableForId)
EXTERN void	CalPackNodes (Cal_BddManager_t *bddManager)
EXTERN void	CalBddPackNodesForSingleId (Cal_BddManager_t *bddManager, Cal_BddId_t id)
EXTERN void	CalBddPackNodesAfterReorderForSingleId (Cal_BddManager_t *bddManager, int fixForwardedNodesFlag, int bestIndex, int bottomIndex)
EXTERN void	CalBddPackNodesForMultipleIds (Cal_BddManager_t *bddManager, Cal_BddId_t beginId, int numLevels)
EXTERN CalHashTable_t *	CalHashTableOneInit (Cal_BddManager_t *bddManager, int itemSize)
EXTERN void	CalHashTableOneQuit (CalHashTable_t *hashTable)
EXTERN void	CalHashTableOneInsert (CalHashTable_t hashTable, Cal_Bdd_t keyBdd, char valuePtr)
EXTERN int	CalHashTableOneLookup (CalHashTable_t hashTable, Cal_Bdd_t keyBdd, char *valuePtrPtr)
EXTERN int	CalHashTableThreeFindOrAdd (CalHashTable_t hashTable, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, Cal_Bdd_t bddPtr)
EXTERN void	CalSetInteract (Cal_BddManager_t *bddManager, int x, int y)
EXTERN int	CalTestInteract (Cal_BddManager_t *bddManager, int x, int y)
EXTERN int	CalInitInteract (Cal_BddManager_t *bddManager)
EXTERN CalPageManager_t *	CalPageManagerInit (int numPagesPerSegment)
EXTERN int	CalPageManagerQuit (CalPageManager_t *pageManager)
EXTERN void	CalPageManagerPrint (CalPageManager_t *pageManager)
EXTERN CalNodeManager_t *	CalNodeManagerInit (CalPageManager_t *pageManager)
EXTERN int	CalNodeManagerQuit (CalNodeManager_t *nodeManager)
EXTERN void	CalNodeManagerPrint (CalNodeManager_t *nodeManager)
EXTERN CalAddress_t *	CalPageManagerAllocPage (CalPageManager_t *pageManager)
EXTERN void	CalPageManagerFreePage (CalPageManager_t pageManager, CalAddress_t page)
EXTERN int	CalIncreasingOrderCompare (const void a, const void b)
EXTERN int	CalDecreasingOrderCompare (const void a, const void b)
EXTERN void	CalBddReorderFixProvisionalNodes (Cal_BddManager_t *bddManager)
EXTERN void	CalCheckPipelineValidity (Cal_BddManager_t *bddManager)
EXTERN char *	CalBddVarName (Cal_BddManager_t *bddManager, Cal_Bdd_t v, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env)
EXTERN void	CalBddNumberSharedNodes (Cal_BddManager_t bddManager, Cal_Bdd_t f, CalHashTable_t hashTable, long *next)
EXTERN void	CalBddMarkSharedNodes (Cal_BddManager_t *bddManager, Cal_Bdd_t f)
EXTERN int	CalOpExists (Cal_BddManager_t bddManager, Cal_Bdd_t f, Cal_Bdd_t resultBddPtr)
EXTERN int	CalOpRelProd (Cal_BddManager_t bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t resultBddPtr)
EXTERN int	CalOpCofactor (Cal_BddManager_t bddManager, Cal_Bdd_t f, Cal_Bdd_t c, Cal_Bdd_t resultBddPtr)
EXTERN void	CalBddReorderAuxBF (Cal_BddManager_t *bddManager)
EXTERN void	CalBddReorderFixCofactors (Cal_BddManager bddManager, Cal_BddId_t id)
EXTERN void	CalFixupAssoc (Cal_BddManager_t bddManager, long id1, long id2, CalAssociation_t assoc)
EXTERN void	CalBddReorderReclaimForwardedNodes (Cal_BddManager bddManager, int startIndex, int endIndex)
EXTERN void	CalBddReorderBlockSift (Cal_BddManager_t *bddManager, double maxSizeFactor)
EXTERN void	CalBddReorderBlockWindow (Cal_BddManager bddManager, Cal_Block block, char *levels)
EXTERN void	CalBddReorderAuxDF (Cal_BddManager_t *bddManager)
EXTERN void	CalAlignCollisionChains (Cal_BddManager_t *bddManager)
EXTERN void	CalBddReorderFixUserBddPtrs (Cal_BddManager bddManager)
EXTERN int	CalCheckAllValidity (Cal_BddManager bddManager)
EXTERN int	CalCheckValidityOfNodesForId (Cal_BddManager bddManager, int id)
EXTERN int	CalCheckValidityOfNodesForWindow (Cal_BddManager bddManager, Cal_BddIndex_t index, int numLevels)
EXTERN int	CalCheckValidityOfANode (Cal_BddManager_t bddManager, CalBddNode_t bddNode, int id)
EXTERN void	CalCheckRefCountValidity (Cal_BddManager_t *bddManager)
EXTERN int	CalCheckAssoc (Cal_BddManager_t *bddManager)
EXTERN void	CalBddReorderVarSift (Cal_BddManager bddManager, double maxSizeFactor)
EXTERN void	CalBddReorderVarWindow (Cal_BddManager bddManager, char *levels)
EXTERN int	CalOpAnd (Cal_BddManager_t bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t resultBddPtr)
EXTERN int	CalOpNand (Cal_BddManager_t bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t resultBddPtr)
EXTERN int	CalOpOr (Cal_BddManager_t bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t resultBddPtr)
EXTERN int	CalOpXor (Cal_BddManager_t bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t resultBddPtr)
EXTERN Cal_Bdd_t	CalOpITE (Cal_BddManager_t bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, CalHashTable_t *reqQueForITE)
EXTERN void	CalUniqueTablePrint (Cal_BddManager_t *bddManager)
EXTERN void	CalBddFunctionPrint (Cal_BddManager_t bddManager, Cal_Bdd_t calBdd, char name)
EXTERN int	CalBddPreProcessing (Cal_BddManager_t *bddManager, int count,...)
EXTERN int	CalBddPostProcessing (Cal_BddManager_t *bddManager)
EXTERN int	CalBddArrayPreProcessing (Cal_BddManager_t bddManager, Cal_Bdd userBddArray)
EXTERN Cal_Bdd_t	CalBddGetInternalBdd (Cal_BddManager bddManager, Cal_Bdd userBdd)
EXTERN Cal_Bdd	CalBddGetExternalBdd (Cal_BddManager_t *bddManager, Cal_Bdd_t internalBdd)
EXTERN void	CalBddFatalMessage (char *string)
EXTERN void	CalBddWarningMessage (char *string)
EXTERN void	CalBddNodePrint (CalBddNode_t *bddNode)
EXTERN void	CalBddPrint (Cal_Bdd_t calBdd)
EXTERN void	CalHashTablePrint (CalHashTable_t *hashTable)
EXTERN void	CalHashTableOnePrint (CalHashTable_t *hashTable, int flag)
EXTERN void	CalUtilSRandom (long seed)
EXTERN long	CalUtilRandom (void)
Variables
unsigned long	calPrimes []

Define Documentation

#define CAL_BDD_CONST_ID 0

Definition at line 145 of file calInt.h.

#define CAL_BDD_CONST_INDEX CAL_BDD_NULL_INDEX

Definition at line 148 of file calInt.h.

#define CAL_BDD_FREE_REC	(	bddManager,
		rec,
		type	)	Cal_MemFreeRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT], (rec))

Definition at line 523 of file calInt.h.

#define CAL_BDD_NEW_REC	(	bddManager,
		type		)	((type *)Cal_MemNewRec((bddManager)->recordMgrArray[(CAL_ROUNDUP(sizeof(type))-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT]))

Definition at line 522 of file calInt.h.

#define CAL_BDD_NULL_ID ((unsigned short) ((1 << 8*sizeof(unsigned short)) - 1))

Definition at line 144 of file calInt.h.

#define CAL_BDD_NULL_INDEX (unsigned short) ((1 << 8*sizeof(unsigned short)) - 1)

Definition at line 147 of file calInt.h.

#define CAL_BDD_OK 0

Definition at line 140 of file calInt.h.

#define CAL_BDD_OUT_OF_ORDER	(	f,
		g		)	((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g))

Definition at line 924 of file calInt.h.

#define CAL_BDD_OVERFLOWED 1

Definition at line 141 of file calInt.h.

#define CAL_BDD_POINTER ( f )

Value:

((CalBddNode_t *)(((CalAddress_t)f) & \
    ~(CalAddress_t)0xf))

Definition at line 561 of file calInt.h.

#define CAL_BDD_REORDER_THRESHOLD 10000

Definition at line 90 of file calInt.h.

#define CAL_BDD_SWAP	(	f,
		g		)

Value:

{ \
  Cal_Bdd_t _tmp; \
  _tmp = f; \
  f = g; \
  g = _tmp; \
}

Definition at line 927 of file calInt.h.

#define CAL_GC_CHECK 100

Definition at line 98 of file calInt.h.

#define CAL_INFINITY (1 << 20)

Definition at line 151 of file calInt.h.

#define CAL_LARGE_BDD (1<<19)

Definition at line 189 of file calInt.h.

#define CAL_MAX_REF_COUNT (unsigned short)((1 << 8*sizeof(char)) - 1)

Definition at line 150 of file calInt.h.

#define CAL_MAX_VAR_ID ((unsigned short) (CAL_BDD_NULL_ID - 1))

Definition at line 146 of file calInt.h.

#define CAL_MAX_VAR_INDEX (CAL_BDD_NULL_INDEX - 1)

Definition at line 149 of file calInt.h.

#define CAL_MIN_GC_LIMIT 10000

CHeaderFile*****************************************************************

FileName [calInt.h]

PackageName [cal]

Synopsis [The internal data structures, macros and function declarations]

Description []

SeeAlso [cal.h]

Author [Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu Jagesh Sanghavi (sanghavi@ic.eecs.berkeley.edu)]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calInt.h,v 1.11 2002/09/14 20:19:58 fabio Exp

]

Definition at line 67 of file calInt.h.

#define CAL_NUM_FORWARDED_NODES_LIMIT 50000

Definition at line 95 of file calInt.h.

#define CAL_NUM_PAGES_THRESHOLD 3

Definition at line 93 of file calInt.h.

#define CAL_OP_AND 0x2000

Definition at line 181 of file calInt.h.

#define CAL_OP_COMPOSE 0x6000

Definition at line 185 of file calInt.h.

#define CAL_OP_INVALID 0x0000

Definition at line 179 of file calInt.h.

#define CAL_OP_NAND 0x3000

Definition at line 182 of file calInt.h.

#define CAL_OP_OR 0x1000

Definition at line 180 of file calInt.h.

#define CAL_OP_QUANT 0x4000

Definition at line 183 of file calInt.h.

#define CAL_OP_REL_PROD 0x5000

Definition at line 184 of file calInt.h.

#define CAL_OP_SUBST 0x7000

Definition at line 186 of file calInt.h.

#define CAL_OP_VAR_SUBSTITUTE 0x8000

Definition at line 187 of file calInt.h.

#define CAL_REPACK_AFTER_GC_THRESHOLD 0.75

Definition at line 74 of file calInt.h.

#define CAL_TABLE_REPACK_THRESHOLD 0.9

Definition at line 86 of file calInt.h.

#define CAL_TAG0 ( pointer ) ((CalAddress_t)((CalAddress_t)(pointer) & 0x1))

Definition at line 563 of file calInt.h.

#define CalBddAddRefCount	(	calBdd,
		num		)

Value:

{ \
  Cal_BddRefCount_t _count; \
  CalBddGetRefCount(calBdd, _count); \
  if(_count < CAL_MAX_REF_COUNT){ \
    _count += num; \
    if(_count > CAL_MAX_REF_COUNT){ \
      _count = CAL_MAX_REF_COUNT; \
    } \
    CalBddPutRefCount(calBdd, _count); \
  } \
}

Definition at line 785 of file calInt.h.

#define CalBddDcrRefCount ( calBdd )

Value:

{ CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) == 0x0){ \
    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) == 0x0){ \
      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0x0){ \
        CalBddWarningMessage("Trying to decrement reference count below zero"); \
      } \
      else{ \
        _bddNode->thenBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) & ~0x2); \
        _bddNode->elseBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) | 0xe); \
        _bddNode->nextBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
      } \
    } \
    else{ \
      _bddNode->elseBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) - 0x2); \
      _bddNode->nextBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
    } \
  } \
  else if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf \
      ||  ((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe  \
      ||  ((CalAddress_t)(_bddNode->thenBddNode) & 0x2) != 0x2){ \
    _bddNode->nextBddNode = \
        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) - 1); \
  } \
}

Definition at line 753 of file calInt.h.

#define CalBddForward ( bdd )

Value:

{ \
  CalBddNode_t *_bddNode, *_bddNodeTagged; \
  _bddNodeTagged = CalBddGetBddNode(bdd); \
  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
  (bdd).bddId = _bddNode->thenBddId; \
  (bdd).bddNode = (CalBddNode_t*) \
                  (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
                   ^(CAL_TAG0(_bddNodeTagged))); \
}

Definition at line 1276 of file calInt.h.

#define CalBddFree ( calBdd ) CalBddDcrRefCount(calBdd)

Definition at line 810 of file calInt.h.

#define CalBddGetBddId ( calBdd ) ((calBdd).bddId)

Definition at line 634 of file calInt.h.

#define CalBddGetBddIndex	(	bddManager,
		calBdd		)	(bddManager->idToIndex[(calBdd).bddId])

Definition at line 635 of file calInt.h.

#define CalBddGetBddNode ( calBdd ) ((calBdd).bddNode)

Definition at line 637 of file calInt.h.

#define CalBddGetBddNodeNot ( calBdd ) ((CalBddNode_t*)(((CalAddress_t)((calBdd).bddNode))^0x1))

Definition at line 638 of file calInt.h.

#define CalBddGetCofactors	(	calBdd,
		varId,
		fx,
		fxbar	)

Value:

{ \
    if(varId == (calBdd).bddId){ \
      CalBddGetThenBdd(calBdd, fx); \
      CalBddGetElseBdd(calBdd, fxbar); \
    } \
    else{ \
      fx = calBdd; \
      fxbar = calBdd; \
    } \
}

Definition at line 584 of file calInt.h.

#define CalBddGetDepth CalBddGetRefCount

Definition at line 1334 of file calInt.h.

#define CalBddGetElseBdd	(	calBdd,
		_elseBdd		)

Value:

{ \
  CalBddNode_t *_bddNode, *_bddNodeTagged; \
  _bddNodeTagged = (calBdd).bddNode; \
  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
  (_elseBdd).bddId = _bddNode->elseBddId; \
  (_elseBdd).bddNode = (CalBddNode_t*) (((CalAddress_t) (_bddNode->elseBddNode) \
        & ~0xe)^(CAL_TAG0(_bddNodeTagged)));\
}

Definition at line 623 of file calInt.h.

#define CalBddGetElseBddId ( calBdd ) CAL_BDD_POINTER((calBdd).bddNode)->elseBddId

Definition at line 597 of file calInt.h.

#define CalBddGetElseBddIndex	(	bddManager,
		calBdd		)	(bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->elseBddId])

Definition at line 600 of file calInt.h.

#define CalBddGetElseBddNode ( calBdd )

Value:

((CalBddNode_t*) \
    (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode) \
    & ~0xe) ^ (CAL_TAG0((calBdd).bddNode))))

Definition at line 608 of file calInt.h.

#define CalBddGetMark ( calBdd ) CalBddNodeGetMark(CAL_BDD_POINTER((calBdd).bddNode))

Definition at line 1135 of file calInt.h.

#define CalBddGetMinId2	(	bddManager,
		calBdd1,
		calBdd2,
		topId	)

Value:

{ \
  Cal_BddId_t _id1, _id2; \
  Cal_BddIndex_t _index1, _index2; \
  _id1 = CalBddGetBddId((calBdd1)); \
  _id2 = CalBddGetBddId((calBdd2)); \
  _index1 = (bddManager)->idToIndex[_id1]; \
  _index2 = (bddManager)->idToIndex[_id2]; \
  if (_index1 < _index2) topId = _id1; \
  else topId = _id2; \
}

Definition at line 823 of file calInt.h.

#define CalBddGetMinId3	(	bddManager,
		calBdd1,
		calBdd2,
		calBdd3,
		topId	)

Value:

{ \
  Cal_BddId_t _id1, _id2, _id3; \
  Cal_BddIndex_t _index1, _index2, _index3; \
  _id1 = CalBddGetBddId((calBdd1)); \
  _id2 = CalBddGetBddId((calBdd2)); \
  _id3 = CalBddGetBddId((calBdd3)); \
  _index1 = (bddManager)->idToIndex[_id1]; \
  _index2 = (bddManager)->idToIndex[_id2]; \
  _index3 = (bddManager)->idToIndex[_id3]; \
  if(_index1 <= _index2){ \
    if(_index1 <= _index3){ \
      topId = _id1; \
    } \
    else{ \
      topId = _id3; \
    } \
  } \
  else{ \
    if(_index2 <= _index3){ \
      topId = _id2; \
    } \
    else{ \
      topId = _id3; \
    } \
  } \
}

Definition at line 835 of file calInt.h.

#define CalBddGetMinIdAndMinIndex	(	bddManager,
		calBdd1,
		calBdd2,
		topId,
		topIndex	)

Value:

{ \
  Cal_BddId_t _id1, _id2; \
  Cal_BddIndex_t _index1, _index2; \
  _id1 = CalBddGetBddId((calBdd1)); \
  _id2 = CalBddGetBddId((calBdd2)); \
  _index1 = (bddManager)->idToIndex[_id1]; \
  _index2 = (bddManager)->idToIndex[_id2]; \
  if (_index1 < _index2){ \
    topId = _id1; \
    topIndex = _index1; \
  } \
  else { \
    topId = _id2; \
    topIndex = _index2; \
  } \
}

Definition at line 900 of file calInt.h.

#define CalBddGetMinIndex2	(	bddManager,
		calBdd1,
		calBdd2,
		topIndex	)

Value:

{ \
  Cal_BddIndex_t _index1, _index2; \
  _index1 = bddManager->idToIndex[CalBddGetBddId(calBdd1)]; \
  _index2 = bddManager->idToIndex[CalBddGetBddId(calBdd2)]; \
  if (_index1 < _index2) topIndex = _index1; \
  else topIndex = _index2; \
}

Definition at line 863 of file calInt.h.

#define CalBddGetMinIndex3	(	bddManager,
		calBdd1,
		calBdd2,
		calBdd3,
		topIndex	)

Value:

{ \
  Cal_BddId_t _id1, _id2, _id3; \
  Cal_BddIndex_t _index1, _index2, _index3; \
  _id1 = CalBddGetBddId((calBdd1)); \
  _id2 = CalBddGetBddId((calBdd2)); \
  _id3 = CalBddGetBddId((calBdd3)); \
  _index1 = (bddManager)->idToIndex[_id1]; \
  _index2 = (bddManager)->idToIndex[_id2]; \
  _index3 = (bddManager)->idToIndex[_id3]; \
  if(_index1 <= _index2){ \
    if(_index1 <= _index3){ \
      topIndex = _index1; \
    } \
    else{ \
      topIndex = _index3; \
    } \
  } \
  else{ \
    if(_index2 <= _index3){ \
      topIndex = _index2; \
    } \
    else{ \
      topIndex = _index3; \
    } \
  } \
}

Definition at line 872 of file calInt.h.

#define CalBddGetNextBddNode ( calBdd )

Value:

((CalBddNode_t *)(((CalAddress_t) \
    (CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & ~0xf))

Definition at line 641 of file calInt.h.

#define CalBddGetRefCount	(	calBdd,
		refCount		)

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  refCount = ((CalAddress_t)(_bddNode->thenBddNode) & 0x2); \
  refCount <<= 3; \
  refCount |= ((CalAddress_t)(_bddNode->elseBddNode) & 0xe); \
  refCount <<= 3; \
  refCount |= ((CalAddress_t)(_bddNode->nextBddNode) & 0xf); \
}

Definition at line 699 of file calInt.h.

#define CalBddGetThenBdd	(	calBdd,
		_thenBdd		)

Value:

{ \
  CalBddNode_t *_bddNode, *_bddNodeTagged; \
  _bddNodeTagged = (calBdd).bddNode; \
  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
  (_thenBdd).bddId = _bddNode->thenBddId; \
  (_thenBdd).bddNode = (CalBddNode_t*) (((CalAddress_t) (_bddNode->thenBddNode) \
      & ~0xe)^(CAL_TAG0(_bddNodeTagged))); \
}

Definition at line 613 of file calInt.h.

#define CalBddGetThenBddId ( calBdd ) CAL_BDD_POINTER((calBdd).bddNode)->thenBddId

Definition at line 596 of file calInt.h.

#define CalBddGetThenBddIndex	(	bddManager,
		calBdd		)	(bddManager->idToIndex[CAL_BDD_POINTER((calBdd).bddNode)->thenBddId])

Definition at line 598 of file calInt.h.

#define CalBddGetThenBddNode ( calBdd )

Value:

((CalBddNode_t*) \
    (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode) \
    & ~0xe) ^ (CAL_TAG0((calBdd).bddNode))))

Definition at line 603 of file calInt.h.

#define CalBddIcrRefCount ( calBdd )

Value:

{ CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf){ \
    _bddNode->nextBddNode = \
        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) + 1); \
  } \
  else{ \
    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe){ \
      _bddNode->nextBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
      _bddNode->elseBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) + 0x2); \
    } \
    else{ \
      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0){ \
        _bddNode->nextBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
        _bddNode->elseBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) & ~0xe); \
        _bddNode->thenBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) | 0x2); \
      } \
    } \
  } \
}

Definition at line 726 of file calInt.h.

#define CalBddIdNeedsRepacking	(	bddManager,
		id		)

Value:

((bddManager->nodeManagerArray[id]->numPages > CAL_NUM_PAGES_THRESHOLD) && (bddManager->uniqueTable[id]->numEntries < bddManager->tableRepackThreshold *  \
  bddManager->nodeManagerArray[id]->numPages * NUM_NODES_PER_PAGE))

Definition at line 531 of file calInt.h.

#define CalBddIsBddConst ( calBdd ) ((calBdd).bddId == 0)

Definition at line 572 of file calInt.h.

#define CalBddIsBddNull	(	manager,
		calBdd		)	CalBddIsEqual(calBdd,(manager)->bddNull)

Definition at line 816 of file calInt.h.

#define CalBddIsBddOne	(	manager,
		calBdd		)	CalBddIsEqual(calBdd, (manager)->bddOne)

Definition at line 814 of file calInt.h.

#define CalBddIsBddZero	(	manager,
		calBdd		)	CalBddIsEqual(calBdd, (manager)->bddZero)

Definition at line 815 of file calInt.h.

#define CalBddIsComplement ( calBdd ) ((int)CAL_TAG0((calBdd).bddNode))

Definition at line 564 of file calInt.h.

#define CalBddIsComplementEqual	(	calBdd1,
		calBdd2		)

Value:

(((calBdd1).bddNode == \
    (CalBddNode_t *)(((CalAddress_t)(calBdd2).bddNode) ^ 0x1)))

Definition at line 576 of file calInt.h.

#define CalBddIsEqual	(	calBdd1,
		calBdd2		)	(((calBdd1).bddNode == (calBdd2).bddNode))

Definition at line 574 of file calInt.h.

#define CalBddIsForwarded ( bdd ) (CAL_BDD_POINTER(CalBddGetElseBddNode(bdd)) == FORWARD_FLAG)

Definition at line 1270 of file calInt.h.

#define CalBddIsForwardedTo CalRequestIsForwardedTo

Definition at line 1320 of file calInt.h.

#define CalBddIsMarked ( calBdd ) CalBddNodeIsMarked(CAL_BDD_POINTER((calBdd).bddNode))

Definition at line 1126 of file calInt.h.

#define CalBddIsOutPos ( calBdd ) (!(((CalAddress_t)(calBdd).bddNode) & 0x1))

Definition at line 812 of file calInt.h.

#define CalBddIsRefCountMax ( calBdd )

Value:

((((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode)) & 0x2) == 0x2) \
    && ((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode)) & 0xe) == 0xe)\
    && ((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & 0xf) == 0xf))\
    ? 1 : 0)

Definition at line 804 of file calInt.h.

#define CalBddIsRefCountZero ( calBdd )

Value:

(((((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->thenBddNode)) & 0x2) \
    || (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->elseBddNode)) & 0xe)\
    || (((CalAddress_t)(CAL_BDD_POINTER((calBdd).bddNode)->nextBddNode)) & 0xf))\
    ? 0 : 1)

Definition at line 798 of file calInt.h.

#define CalBddManagerGetBddNull ( manager ) (manager)->bddNull

Definition at line 819 of file calInt.h.

#define CalBddManagerGetBddOne ( manager ) ((manager)->bddOne)

Definition at line 817 of file calInt.h.

#define CalBddManagerGetBddZero ( manager ) ((manager)->bddZero)

Definition at line 818 of file calInt.h.

#define CalBddMark ( calBdd ) CalBddNodeMark(CAL_BDD_POINTER((calBdd).bddNode))

Definition at line 1129 of file calInt.h.

#define CalBddNodeAddRefCount	(	__bddNode,
		num		)

Value:

{ \
  Cal_BddRefCount_t _count; \
  CalBddNodeGetRefCount(__bddNode, _count); \
  _count += num; \
  if(_count > CAL_MAX_REF_COUNT){ \
    _count = CAL_MAX_REF_COUNT; \
  } \
  CalBddNodePutRefCount(__bddNode, _count); \
}

Definition at line 1089 of file calInt.h.

#define CalBddNodeDcrRefCount ( _bddNode )

Value:

{ \
  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) == 0x0){ \
    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) == 0x0){ \
      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0x0){ \
        CalBddWarningMessage("Trying to decrement reference count below zero"); \
      } \
      else{ \
        _bddNode->thenBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) & ~0x2); \
        _bddNode->elseBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) | 0xe); \
        _bddNode->nextBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
      } \
    } \
    else{ \
      _bddNode->elseBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) - 0x2); \
      _bddNode->nextBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) | 0xf); \
    } \
  } \
  else if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf \
      ||  ((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe  \
      ||  ((CalAddress_t)(_bddNode->thenBddNode) & 0x2) != 0x2){ \
    _bddNode->nextBddNode = \
        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) - 1); \
  } \
}

Definition at line 1032 of file calInt.h.

#define CalBddNodeEqual	(	calBddNode1,
		calBddNode2		)	((CalAddress_t)calBddNode1 == (CalAddress_t)calBddNode2)

Definition at line 1120 of file calInt.h.

#define CalBddNodeForward ( _bddNodeTagged )

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
  _bddNodeTagged = (CalBddNode_t*) \
                  (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
                   ^(CAL_TAG0(_bddNodeTagged))); \
}

Definition at line 1287 of file calInt.h.

#define CalBddNodeGetElseBdd	(	_bddNode,
		_elseBdd		)

Value:

{ \
  (_elseBdd).bddId = (_bddNode)->elseBddId; \
  (_elseBdd).bddNode = \
      (CalBddNode_t*) (((CalAddress_t) ((_bddNode)->elseBddNode) & ~0xe)); \
}

Definition at line 955 of file calInt.h.

#define CalBddNodeGetElseBddId ( _bddNode ) ((_bddNode)->elseBddId)

Definition at line 938 of file calInt.h.

#define CalBddNodeGetElseBddIndex	(	bddManager,
		_bddNode		)	bddManager->idToIndex[((_bddNode)->elseBddId)]

Definition at line 941 of file calInt.h.

#define CalBddNodeGetElseBddNode ( _bddNode ) ((CalBddNode_t *)((CalAddress_t)((_bddNode)->elseBddNode) & ~0xe))

Definition at line 945 of file calInt.h.

#define CalBddNodeGetMark ( bddNode ) ((((CalAddress_t)((bddNode)->thenBddNode)) & 0xc) >> 2)

Definition at line 1152 of file calInt.h.

#define CalBddNodeGetNextBddNode ( _bddNode ) ((CalBddNode_t *)(((CalAddress_t) ((_bddNode)->nextBddNode)) & ~0xf))

Definition at line 962 of file calInt.h.

#define CalBddNodeGetRefCount	(	_bddNode,
		refCount		)

Value:

{ \
  refCount = ((CalAddress_t)(_bddNode->thenBddNode) & 0x2); \
  refCount <<= 3; \
  refCount |= ((CalAddress_t)(_bddNode->elseBddNode) & 0xe); \
  refCount <<= 3; \
  refCount |= ((CalAddress_t)(_bddNode->nextBddNode) & 0xf); \
}

Definition at line 1009 of file calInt.h.

#define CalBddNodeGetThenBdd	(	_bddNode,
		_thenBdd		)

Value:

{ \
  (_thenBdd).bddId = (_bddNode)->thenBddId; \
  (_thenBdd).bddNode =  \
      (CalBddNode_t*) (((CalAddress_t) ((_bddNode)->thenBddNode) & ~0xe)); \
}

Definition at line 948 of file calInt.h.

#define CalBddNodeGetThenBddId ( _bddNode ) ((_bddNode)->thenBddId)

Definition at line 937 of file calInt.h.

#define CalBddNodeGetThenBddIndex	(	bddManager,
		_bddNode		)	bddManager->idToIndex[((_bddNode)->thenBddId)]

Definition at line 939 of file calInt.h.

#define CalBddNodeGetThenBddNode ( _bddNode ) ((CalBddNode_t *)((CalAddress_t)((_bddNode)->thenBddNode) & ~0xe))

Definition at line 943 of file calInt.h.

#define CalBddNodeIcrRefCount ( _bddNode )

Value:

{ \
  if(((CalAddress_t)(_bddNode->nextBddNode) & 0xf) != 0xf){ \
    _bddNode->nextBddNode = \
        (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) + 1); \
  } \
  else{ \
    if(((CalAddress_t)(_bddNode->elseBddNode) & 0xe) != 0xe){ \
      _bddNode->nextBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
      _bddNode->elseBddNode = \
          (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) + 0x2); \
    } \
    else{ \
      if(((CalAddress_t)(_bddNode->thenBddNode) & 0x2) == 0){ \
        _bddNode->nextBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->nextBddNode) & ~0xf); \
        _bddNode->elseBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->elseBddNode) & ~0xe); \
        _bddNode->thenBddNode = \
            (CalBddNode_t *)((CalAddress_t)(_bddNode->thenBddNode) | 0x2); \
      } \
    } \
  } \
}

Definition at line 1063 of file calInt.h.

#define CalBddNodeIsForwarded ( bddNode ) (((CalAddress_t)(CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode)))) == FORWARD_FLAG)

Definition at line 1273 of file calInt.h.

#define CalBddNodeIsForwardedTo ( _bddNodeTagged )

Value:

{ \
  CalBddNode_t *__bddNode;\
  __bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
  if(CalBddNodeGetElseBddNode(__bddNode) == FORWARD_FLAG){ \
    _bddNodeTagged = (CalBddNode_t*) \
                     (((CalAddress_t)(__bddNode->thenBddNode) & ~0xe)        \
                      ^(CAL_TAG0(_bddNodeTagged))); \
  } \
}

Definition at line 1296 of file calInt.h.

#define CalBddNodeIsMarked ( bddNode ) ((((CalAddress_t)((bddNode)->thenBddNode)) & 0x4) >> 2)

Definition at line 1141 of file calInt.h.

#define CalBddNodeIsOutPos ( bddNode ) (!(((CalAddress_t)bddNode) & 0x1))

Definition at line 1112 of file calInt.h.

#define CalBddNodeIsRefCountMax ( _bddNode )

Value:

((((((CalAddress_t) ((_bddNode)->thenBddNode)) & 0x2) == 0x2)&& \
    ((((CalAddress_t) ((_bddNode)->elseBddNode)) & 0xe) == 0xe)&& \
    ((((CalAddress_t) ((_bddNode)->nextBddNode)) & 0xf) == 0xf)) \
    ? 1 : 0)

Definition at line 1106 of file calInt.h.

#define CalBddNodeIsRefCountZero ( _bddNode )

Value:

(((((CalAddress_t) ((_bddNode)->thenBddNode)) & 0x2) || \
    (((CalAddress_t) ((_bddNode)->elseBddNode)) & 0xe) || \
    (((CalAddress_t) ((_bddNode)->nextBddNode)) & 0xf)) \
    ? 0 : 1)

Definition at line 1100 of file calInt.h.

#define CalBddNodeMark ( bddNode )

Value:

((bddNode)->thenBddNode = \
     (CalBddNode_t *)(((CalAddress_t)(bddNode)->thenBddNode) | 0x4))

Definition at line 1144 of file calInt.h.

#define CalBddNodeNot ( bddNode ) ((CalBddNode_t*)(((CalAddress_t)(bddNode))^0x1))

Definition at line 1123 of file calInt.h.

#define CalBddNodePutElseBdd	(	_bddNode,
		_elseBdd		)

Value:

{ \
  (_bddNode)->elseBddId = (_elseBdd).bddId; \
  (_bddNode)->elseBddNode = (CalBddNode_t*) \
      (((CalAddress_t)((_bddNode)->elseBddNode) & 0xe)| \
       (((CalAddress_t) (_elseBdd).bddNode) & ~0xe)); \
}

Definition at line 993 of file calInt.h.

#define CalBddNodePutElseBddId	(	_bddNode,
		_elseBddId		)	((_bddNode)->elseBddId = _elseBddId)

Definition at line 968 of file calInt.h.

#define CalBddNodePutElseBddNode	(	_bddNode,
		_elseBddNode		)

Value:

{ \
  (_bddNode)->elseBddNode = (CalBddNode_t*) \
      (((CalAddress_t)((_bddNode)->elseBddNode) & 0xe)| \
      (((CalAddress_t) _elseBddNode) & ~0xe));  \
}

Definition at line 978 of file calInt.h.

#define CalBddNodePutMark	(	bddNode,
		mark		)

Value:

((bddNode)->thenBddNode = (CalBddNode_t *) \
      ((((CalAddress_t)(bddNode)->thenBddNode) & ~0xc) | ((mark) << 2)))

Definition at line 1155 of file calInt.h.

#define CalBddNodePutNextBddNode	(	_bddNode,
		_nextBddNode		)

Value:

{ \
  (_bddNode)->nextBddNode = (CalBddNode_t*) \
      (((CalAddress_t)((_bddNode)->nextBddNode) & 0xf)|  \
       (((CalAddress_t) _nextBddNode) & ~0xf));  \
}

Definition at line 1001 of file calInt.h.

#define CalBddNodePutRefCount	(	_bddNode,
		count		)

Value:

{ \
  Cal_BddRefCount_t _nextTag, _thenTag, _elseTag; \
  _nextTag = (count & 0xf); \
  _thenTag = ((count >> 6) & 0x2); \
  _elseTag = ((count >> 3) & 0xe); \
  _bddNode->nextBddNode = (CalBddNode_t*) \
      ((((CalAddress_t)(_bddNode->nextBddNode)) & ~0xf) | _nextTag); \
  _bddNode->thenBddNode = (CalBddNode_t*) \
      ((((CalAddress_t)(_bddNode->thenBddNode)) & ~0x2) | _thenTag); \
  _bddNode->elseBddNode = (CalBddNode_t*) \
      ((((CalAddress_t)(_bddNode->elseBddNode)) & ~0xe) | _elseTag); \
}

Definition at line 1018 of file calInt.h.

#define CalBddNodePutThenBdd	(	_bddNode,
		_thenBdd		)

Value:

{ \
  (_bddNode)->thenBddId = (_thenBdd).bddId; \
  (_bddNode)->thenBddNode = (CalBddNode_t*) \
      (((CalAddress_t)((_bddNode)->thenBddNode) & 0xe)| \
       (((CalAddress_t)(_thenBdd).bddNode) & ~0xe)); \
}

Definition at line 985 of file calInt.h.

#define CalBddNodePutThenBddId	(	_bddNode,
		_thenBddId		)	((_bddNode)->thenBddId = _thenBddId)

Definition at line 965 of file calInt.h.

#define CalBddNodePutThenBddNode	(	_bddNode,
		_thenBddNode		)

Value:

{ \
  (_bddNode)->thenBddNode = (CalBddNode_t*) \
      (((CalAddress_t)((_bddNode)->thenBddNode) & 0xe)| \
       (((CalAddress_t) _thenBddNode) & ~0xe)); \
}

Definition at line 971 of file calInt.h.

#define CalBddNodeRegular ( bddNode ) ((CalBddNode_t *)(((unsigned long)(bddNode)) & ~01))

Definition at line 1113 of file calInt.h.

#define CalBddNodeUnmark ( bddNode )

Value:

((bddNode)->thenBddNode = \
     (CalBddNode_t *)(((CalAddress_t)(bddNode)->thenBddNode) & ~0x4))

Definition at line 1148 of file calInt.h.

#define CalBddNormalize	(	fBdd,
		gBdd		)

Value:

{ \
  Cal_Bdd_t _tmpBdd; \
  if((unsigned long)CAL_BDD_POINTER(CalBddGetBddNode(gBdd)) < \
      (unsigned long)CAL_BDD_POINTER(CalBddGetBddNode(fBdd))){ \
    _tmpBdd = fBdd; \
    fBdd = gBdd; \
    gBdd = _tmpBdd; \
  } \
}

Definition at line 1322 of file calInt.h.

#define CalBddNot	(	calBdd1,
		calBdd2		)

Value:

{ \
  (calBdd2).bddId = (calBdd1).bddId; \
  (calBdd2).bddNode = (CalBddNode_t *)((CalAddress_t)(calBdd1).bddNode ^ 0x1); \
}

Definition at line 918 of file calInt.h.

#define CalBddNull ( bddManager ) ((bddManager)->bddNull)

Definition at line 571 of file calInt.h.

#define CalBddOne ( bddManager ) ((bddManager)->bddOne)

Definition at line 570 of file calInt.h.

#define CalBddPairGetCofactors	(	bddManager,
		f,
		g,
		fx,
		fxbar,
		gx,
		gxbar	)

Value:

{ \
  Cal_BddIndex_t __index1, __index2; \
  __index1 = (bddManager)->idToIndex[CalBddGetBddId(f)]; \
  __index2 = (bddManager)->idToIndex[CalBddGetBddId(g)]; \
  if(__index1 == __index2){ \
    CalBddGetThenBdd(f, fx); \
    CalBddGetElseBdd(f, fxbar); \
    CalBddGetThenBdd(g, gx); \
    CalBddGetElseBdd(g, gxbar); \
  } \
  else if(__index1 < __index2){ \
    CalBddGetThenBdd(f, fx); \
    CalBddGetElseBdd(f, fxbar); \
    gx = gxbar = g; \
  } \
  else{ \
    fx = fxbar = f; \
    CalBddGetThenBdd(g, gx); \
    CalBddGetElseBdd(g, gxbar); \
  } \
}

Definition at line 1247 of file calInt.h.

#define CalBddPutBddId	(	calBdd,
		_bddId		)	((calBdd).bddId = _bddId)

Definition at line 688 of file calInt.h.

#define CalBddPutBddNode	(	calBdd,
		_bddNode		)	((calBdd).bddNode = _bddNode)

Definition at line 689 of file calInt.h.

#define CalBddPutDepth CalBddPutRefCount

Definition at line 1335 of file calInt.h.

#define CalBddPutElseBdd	(	calBdd,
		elseBdd		)

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  _bddNode->elseBddId = (elseBdd).bddId; \
  _bddNode->elseBddNode = (CalBddNode_t*) \
      (((CalAddress_t)(_bddNode->elseBddNode) & 0xe)| \
      (((CalAddress_t)(elseBdd).bddNode) & ~0xe)); \
}

Definition at line 678 of file calInt.h.

#define CalBddPutElseBddId	(	calBdd,
		_elseBddId		)	(CAL_BDD_POINTER((calBdd).bddNode)->elseBddId = _elseBddId)

Definition at line 647 of file calInt.h.

#define CalBddPutElseBddNode	(	calBdd,
		_elseBddNode		)

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  _bddNode->elseBddNode = (CalBddNode_t*) \
      (((CalAddress_t)(_bddNode->elseBddNode) & 0xe)| \
      (((CalAddress_t) _elseBddNode) & ~0xe));  \
}

Definition at line 659 of file calInt.h.

#define CalBddPutMark	(	calBdd,
		mark		)	CalBddNodePutMark(CAL_BDD_POINTER((calBdd).bddNode), (mark))

Definition at line 1138 of file calInt.h.

#define CalBddPutNextBddNode	(	calBdd,
		_nextBddNode		)

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  _bddNode->nextBddNode = (CalBddNode_t*) \
      (((CalAddress_t)(_bddNode->nextBddNode) & 0xf)|  \
      (((CalAddress_t) _nextBddNode) & ~0xf));   \
}

Definition at line 690 of file calInt.h.

#define CalBddPutRefCount	(	calBdd,
		count		)

Value:

{ \
  Cal_BddRefCount_t _nextTag, _thenTag, _elseTag; \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  _nextTag = (count & 0xf); \
  _thenTag = ((count >> 6) & 0x2); \
  _elseTag = ((count >> 3) & 0xe); \
  _bddNode->nextBddNode = (CalBddNode_t*) \
      ((((CalAddress_t)(_bddNode->nextBddNode)) & ~0xf) | _nextTag); \
  _bddNode->thenBddNode = (CalBddNode_t*) \
      ((((CalAddress_t)(_bddNode->thenBddNode)) & ~0x2) | _thenTag); \
  _bddNode->elseBddNode = (CalBddNode_t*) \
      ((((CalAddress_t)(_bddNode->elseBddNode)) & ~0xe) | _elseTag); \
}

Definition at line 710 of file calInt.h.

#define CalBddPutThenBdd	(	calBdd,
		thenBdd		)

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  _bddNode->thenBddId = (thenBdd).bddId; \
  _bddNode->thenBddNode = (CalBddNode_t*) \
      (((CalAddress_t)(_bddNode->thenBddNode) & 0xe)| \
      (((CalAddress_t)(thenBdd).bddNode) & ~0xe)); \
}

Definition at line 668 of file calInt.h.

#define CalBddPutThenBddId	(	calBdd,
		_thenBddId		)	(CAL_BDD_POINTER((calBdd).bddNode)->thenBddId = _thenBddId)

Definition at line 645 of file calInt.h.

#define CalBddPutThenBddNode	(	calBdd,
		_thenBddNode		)

Value:

{ \
  CalBddNode_t *_bddNode; \
  _bddNode = CAL_BDD_POINTER((calBdd).bddNode); \
  _bddNode->thenBddNode = (CalBddNode_t*) \
      (((CalAddress_t)(_bddNode->thenBddNode) & 0xe)| \
      (((CalAddress_t) _thenBddNode) & ~0xe)); \
}

Definition at line 650 of file calInt.h.

#define CalBddRegular	(	calBdd1,
		calBdd2		)

Value:

{                                                       \
  calBdd2.bddId = calBdd1.bddId;                        \
  calBdd2.bddNode = CalBddNodeRegular(calBdd1.bddNode); \
}

Definition at line 1114 of file calInt.h.

#define CalBddSameOrNegation	(	calBdd1,
		calBdd2		)	(CAL_BDD_POINTER((calBdd1).bddNode) == CAL_BDD_POINTER((calBdd2).bddNode))

Definition at line 579 of file calInt.h.

#define CalBddUnmark ( calBdd ) CalBddNodeUnmark(CAL_BDD_POINTER((calBdd).bddNode))

Definition at line 1132 of file calInt.h.

#define CalBddUpdatePhase	(	calBdd,
		complement		)

Value:

((calBdd).bddNode = \
    (CalBddNode_t *)((CalAddress_t)((calBdd).bddNode) ^ complement))

Definition at line 565 of file calInt.h.

#define CalBddZero ( bddManager ) ((bddManager)->bddZero)

Definition at line 569 of file calInt.h.

#define CalCacheTableOneInsert	(	bddManager,
		f,
		result,
		opCode,
		cacheLevel	)	CalCacheTableTwoInsert(bddManager, f, (bddManager)->bddOne, result, opCode, cacheLevel)

Definition at line 1422 of file calInt.h.

#define CalCacheTableOneLookup	(	bddManager,
		f,
		opCode,
		resultPtr	)	CalCacheTableTwoLookup(bddManager, f, (bddManager)->bddOne, opCode, resultPtr)

Definition at line 1424 of file calInt.h.

#define CalDoHash2	(	thenBddNode,
		elseBddNode,
		table	)	(((((CalAddress_t)thenBddNode) + ((CalAddress_t)elseBddNode)) / NODE_SIZE) & ((table)->numBins - 1))

Definition at line 1427 of file calInt.h.

#define CalITERequestNodeGetCofactors	(	bddManager,
		requestNode,
		fx,
		fxbar,
		gx,
		gxbar,
		hx,
		hxbar	)

Definition at line 1342 of file calInt.h.

#define CalNodeManagerAllocNode	(	nodeManager,
		node		)

Value:

{                                                                           \
  if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){                 \
    node = nodeManager->freeNodeList;                                       \
    nodeManager->freeNodeList = ((CalBddNode_t *)(node))->nextBddNode;      \
    Cal_Assert(!((CalAddress_t)nodeManager->freeNodeList & 0xf));\
  }                                                                         \
  else{                                                                     \
    CalBddNode_t *_freeNodeList, *_nextNode, *_node;                        \
    _freeNodeList =                                                         \
        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager);  \
    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0;       \
        _node != _freeNodeList; _nextNode = _node--){                       \
      _node->nextBddNode = _nextNode;                                       \
    }                                                                       \
    nodeManager->freeNodeList = _freeNodeList + 1;                          \
    node = _node;                                                           \
    if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
      (nodeManager)->maxNumPages *= 2;                                      \
      (nodeManager)->pageList =                                            \
          Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
                         (nodeManager)->maxNumPages);                       \
    }                                                                       \
    (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
  }                                                                         \
  ((CalBddNode_t *)(node))->nextBddNode = 0;                                \
  ((CalBddNode_t *)(node))->thenBddId = 0;                                  \
  ((CalBddNode_t *)(node))->elseBddId = 0;                                  \
  ((CalBddNode_t *)(node))->thenBddNode = 0;                                \
  ((CalBddNode_t *)(node))->elseBddNode = 0;                                \
}

Definition at line 420 of file calInt.h.

#define CalNodeManagerCreateAndDupBddNode	(	nodeManager,
		node,
		dupNode	)

Value:

{ \
  if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){ \
    dupNode = nodeManager->freeNodeList; \
    nodeManager->freeNodeList = ((CalBddNode_t *)(dupNode))->nextBddNode; \
  } \
  else{ \
    CalBddNode_t *_freeNodeList, *_nextNode, *_node; \
    _freeNodeList = \
        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); \
    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0; \
        _node != _freeNodeList; _nextNode = _node--){ \
      _node->nextBddNode = _nextNode; \
    } \
    nodeManager->freeNodeList = _freeNodeList + 1; \
    dupNode = _node; \
    if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
      (nodeManager)->maxNumPages *= 2;                                      \
      (nodeManager)->pageList =                                            \
          Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
                         (nodeManager)->maxNumPages);                       \
    }                                                                       \
    (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
  } \
  ((CalBddNode_t *)(dupNode))->nextBddNode = (node)->nextBddNode; \
  ((CalBddNode_t *)(dupNode))->thenBddId = (node)->thenBddId;\
  ((CalBddNode_t *)(dupNode))->elseBddId = (node)->elseBddId;\
  ((CalBddNode_t *)(dupNode))->thenBddNode = (node)->thenBddNode;\
  ((CalBddNode_t *)(dupNode))->elseBddNode = (node)->elseBddNode; \
}

Definition at line 489 of file calInt.h.

#define CalNodeManagerFreeNode	(	nodeManager,
		node		)

Value:

{ \
  (node)->nextBddNode = (nodeManager)->freeNodeList; \
  (nodeManager)->freeNodeList = node; \
}

Definition at line 452 of file calInt.h.

#define CalNodeManagerInitBddNode	(	nodeManager,
		thenBdd,
		elseBdd,
		next,
		node	)

Value:

{ \
  if((nodeManager)->freeNodeList != Cal_Nil(CalBddNode_t)){ \
    node = nodeManager->freeNodeList; \
    nodeManager->freeNodeList = ((CalBddNode_t *)(node))->nextBddNode; \
    Cal_Assert(!((CalAddress_t)nodeManager->freeNodeList & 0xf));\
  } \
  else{ \
    CalBddNode_t *_freeNodeList, *_nextNode, *_node; \
    _freeNodeList = \
        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); \
    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0; \
        _node != _freeNodeList; _nextNode = _node--){ \
      _node->nextBddNode = _nextNode; \
    } \
    nodeManager->freeNodeList = _freeNodeList + 1; \
    node = _node; \
    if ((nodeManager)->numPages == (nodeManager)->maxNumPages){             \
      (nodeManager)->maxNumPages *= 2;                                      \
      (nodeManager)->pageList =                                            \
          Cal_MemRealloc(CalAddress_t *, (nodeManager)->pageList,          \
                         (nodeManager)->maxNumPages);                       \
    }                                                                       \
    (nodeManager)->pageList[(nodeManager)->numPages++] = (CalAddress_t *)_freeNodeList;    \
  } \
  ((CalBddNode_t *)(node))->nextBddNode = next; \
  ((CalBddNode_t *)(node))->thenBddId = CalBddGetBddId(thenBdd); \
  ((CalBddNode_t *)(node))->elseBddId = CalBddGetBddId(elseBdd); \
  ((CalBddNode_t *)(node))->thenBddNode = CalBddGetBddNode(thenBdd); \
  ((CalBddNode_t *)(node))->elseBddNode = CalBddGetBddNode(elseBdd); \
}

Definition at line 457 of file calInt.h.

#define CalRequestAddRefCount CalBddAddRefCount

Definition at line 1339 of file calInt.h.

#define CalRequestGetElseRequest CalBddGetElseBdd

Definition at line 1166 of file calInt.h.

#define CalRequestGetElseRequestId CalBddGetElseBddId

Definition at line 1162 of file calInt.h.

#define CalRequestGetElseRequestNode CalBddGetElseBddNode

Definition at line 1164 of file calInt.h.

#define CalRequestGetF CalBddGetThenBdd

Definition at line 1169 of file calInt.h.

#define CalRequestGetG CalBddGetElseBdd

Definition at line 1170 of file calInt.h.

#define CalRequestGetMark CalBddGetMark

Definition at line 1213 of file calInt.h.

#define CalRequestGetNextNode CalBddGetNextBddNode

Definition at line 1171 of file calInt.h.

#define CalRequestGetRequestId CalBddGetBddId

Definition at line 1167 of file calInt.h.

#define CalRequestGetRequestNode CalBddGetBddNode

Definition at line 1168 of file calInt.h.

#define CalRequestGetThenRequest CalBddGetThenBdd

Definition at line 1165 of file calInt.h.

#define CalRequestGetThenRequestId CalBddGetThenBddId

Definition at line 1161 of file calInt.h.

#define CalRequestGetThenRequestNode CalBddGetThenBddNode

Definition at line 1163 of file calInt.h.

#define CalRequestIsForwardedTo ( request )

Value:

{ \
  CalBddNode_t *__bddNode, *__bddNodeTagged; \
  __bddNodeTagged = (request).bddNode; \
  __bddNode = CAL_BDD_POINTER(__bddNodeTagged); \
  if(CalRequestNodeGetElseRequestNode(__bddNode) == FORWARD_FLAG){ \
    (request).bddId = __bddNode->thenBddId; \
    (request).bddNode = (CalBddNode_t*) \
                        (((CalAddress_t)(__bddNode->thenBddNode) & ~0xe)        \
                         ^(CAL_TAG0(__bddNodeTagged))); \
  } \
}

Definition at line 1307 of file calInt.h.

#define CalRequestIsMarked CalBddIsMarked

Definition at line 1210 of file calInt.h.

#define CalRequestIsNull ( calRequest )

Value:

((CalRequestGetRequestId(calRequest) == 0) \
    && (CalRequestGetRequestNode(calRequest) == 0))

Definition at line 1206 of file calInt.h.

#define CalRequestMark CalBddMark

Definition at line 1211 of file calInt.h.

#define CalRequestNodeAddRefCount CalBddNodeAddRefCount

Definition at line 1338 of file calInt.h.

#define CalRequestNodeGetCofactors	(	bddManager,
		requestNode,
		fx,
		fxbar,
		gx,
		gxbar	)

Value:

{ \
  Cal_Bdd_t __f, __g; \
  Cal_BddIndex_t __index1, __index2; \
  CalRequestNodeGetF(requestNode, __f); \
  CalRequestNodeGetG(requestNode, __g); \
  __index1 = (bddManager)->idToIndex[CalBddGetBddId(__f)]; \
  __index2 = (bddManager)->idToIndex[CalBddGetBddId(__g)]; \
  if(__index1 == __index2){ \
    CalBddGetThenBdd(__f, fx); \
    CalBddGetElseBdd(__f, fxbar); \
    CalBddGetThenBdd(__g, gx); \
    CalBddGetElseBdd(__g, gxbar); \
  } \
  else if(__index1 < __index2){ \
    CalBddGetThenBdd(__f, fx); \
    CalBddGetElseBdd(__f, fxbar); \
    gx = gxbar = __g; \
  } \
  else{ \
    fx = fxbar = __f; \
    CalBddGetThenBdd(__g, gx); \
    CalBddGetElseBdd(__g, gxbar); \
  } \
}

Definition at line 1221 of file calInt.h.

#define CalRequestNodeGetDepth CalBddNodeGetRefCount

Definition at line 1336 of file calInt.h.

#define CalRequestNodeGetElseRequest CalBddNodeGetElseBdd

Definition at line 1192 of file calInt.h.

#define CalRequestNodeGetElseRequestId CalBddNodeGetElseBddId

Definition at line 1188 of file calInt.h.

#define CalRequestNodeGetElseRequestNode CalBddNodeGetElseBddNode

Definition at line 1190 of file calInt.h.

#define CalRequestNodeGetF CalBddNodeGetThenBdd

Definition at line 1193 of file calInt.h.

#define CalRequestNodeGetG CalBddNodeGetElseBdd

Definition at line 1194 of file calInt.h.

#define CalRequestNodeGetMark CalBddNodeGetMark

Definition at line 1218 of file calInt.h.

#define CalRequestNodeGetNextRequestNode CalBddNodeGetNextBddNode

Definition at line 1195 of file calInt.h.

#define CalRequestNodeGetRefCount CalBddNodeGetRefCount

Definition at line 1337 of file calInt.h.

#define CalRequestNodeGetThenRequest CalBddNodeGetThenBdd

Definition at line 1191 of file calInt.h.

#define CalRequestNodeGetThenRequestId CalBddNodeGetThenBddId

Definition at line 1187 of file calInt.h.

#define CalRequestNodeGetThenRequestNode CalBddNodeGetThenBddNode

Definition at line 1189 of file calInt.h.

#define CalRequestNodeIsMarked CalBddNodeIsMarked

Definition at line 1215 of file calInt.h.

#define CalRequestNodeMark CalBddNodeMark

Definition at line 1216 of file calInt.h.

#define CalRequestNodePutDepth CalBddNodePutRefCount

Definition at line 1340 of file calInt.h.

#define CalRequestNodePutElseRequest CalBddNodePutElseBdd

Definition at line 1202 of file calInt.h.

#define CalRequestNodePutElseRequestId CalBddNodePutElseBddId

Definition at line 1198 of file calInt.h.

#define CalRequestNodePutElseRequestNode CalBddNodePutElseBddNode

Definition at line 1200 of file calInt.h.

#define CalRequestNodePutF CalBddNodePutThenBdd

Definition at line 1203 of file calInt.h.

#define CalRequestNodePutG CalBddNodePutElseBdd

Definition at line 1204 of file calInt.h.

#define CalRequestNodePutMark CalBddNodePutMark

Definition at line 1219 of file calInt.h.

#define CalRequestNodePutNextRequestNode CalBddNodePutNextBddNode

Definition at line 1205 of file calInt.h.

#define CalRequestNodePutThenRequest CalBddNodePutThenBdd

Definition at line 1201 of file calInt.h.

#define CalRequestNodePutThenRequestId CalBddNodePutThenBddId

Definition at line 1197 of file calInt.h.

#define CalRequestNodePutThenRequestNode CalBddNodePutThenBddNode

Definition at line 1199 of file calInt.h.

#define CalRequestNodeUnmark CalBddNodeUnmark

Definition at line 1217 of file calInt.h.

#define CalRequestPutElseRequest CalBddPutElseBdd

Definition at line 1178 of file calInt.h.

#define CalRequestPutElseRequestId CalBddPutElseBddId

Definition at line 1174 of file calInt.h.

#define CalRequestPutElseRequestNode CalBddPutElseBddNode

Definition at line 1176 of file calInt.h.

#define CalRequestPutF CalBddPutThenBdd

Definition at line 1181 of file calInt.h.

#define CalRequestPutG CalBddPutElseBdd

Definition at line 1182 of file calInt.h.

#define CalRequestPutMark CalBddPutMark

Definition at line 1214 of file calInt.h.

#define CalRequestPutNextNode CalBddPutNextBddNode

Definition at line 1183 of file calInt.h.

#define CalRequestPutRequestId CalBddPutBddId

Definition at line 1179 of file calInt.h.

#define CalRequestPutRequestNode CalBddPutBddNode

Definition at line 1180 of file calInt.h.

#define CalRequestPutThenRequest CalBddPutThenBdd

Definition at line 1177 of file calInt.h.

#define CalRequestPutThenRequestId CalBddPutThenBddId

Definition at line 1173 of file calInt.h.

#define CalRequestPutThenRequestNode CalBddPutThenBddNode

Definition at line 1175 of file calInt.h.

#define CalRequestUnmark CalBddUnmark

Definition at line 1212 of file calInt.h.

#define DEFAULT_DEPTH 4

Definition at line 156 of file calInt.h.

#define DEFAULT_MAX_DEPTH 6

Definition at line 157 of file calInt.h.

#define FALSE 0

Definition at line 133 of file calInt.h.

#define FORWARD_FLAG 0

Definition at line 160 of file calInt.h.

#define HASH_TABLE_DEFAULT_MAX_CAPACITY HASH_TABLE_DEFAULT_NUM_BINS*HASH_TABLE_DEFAULT_MAX_DENSITY

Definition at line 167 of file calInt.h.

#define HASH_TABLE_DEFAULT_MAX_DENSITY 5

Definition at line 164 of file calInt.h.

#define HASH_TABLE_DEFAULT_NUM_BINS TABLE_SIZE(HASH_TABLE_DEFAULT_SIZE_INDEX)

Definition at line 166 of file calInt.h.

#define HASH_TABLE_DEFAULT_SIZE_INDEX 8

Definition at line 165 of file calInt.h.

#define LG_PAGE_SIZE 12

Definition at line 111 of file calInt.h.

#define MAX_INSERT_DEPTH 256

Definition at line 154 of file calInt.h.

#define MAX_NUM_PAGES 10

Definition at line 119 of file calInt.h.

#define MAX_NUM_SEGMENTS 32

Definition at line 116 of file calInt.h.

#define MAX_REC_SIZE (sizeof(CalHashTable_t))

Definition at line 122 of file calInt.h.

#define MIN_NUM_PAGES_PER_SEGMENT 4

Definition at line 118 of file calInt.h.

#define MIN_REC_SIZE CAL_ALLOC_ALIGNMENT

Definition at line 121 of file calInt.h.

#define NODE_SIZE sizeof(CalBddNode_t)

Definition at line 105 of file calInt.h.

#define NUM_NODES_PER_PAGE (PAGE_SIZE/NODE_SIZE)

Definition at line 114 of file calInt.h.

#define NUM_PAGES_PER_SEGMENT 64

Definition at line 117 of file calInt.h.

#define NUM_REC_MGRS (((MAX_REC_SIZE-MIN_REC_SIZE)/CAL_ALLOC_ALIGNMENT)+1)

Definition at line 123 of file calInt.h.

#define PAGE_SIZE 4096

Definition at line 108 of file calInt.h.

#define PIPELINE_EXECUTION_DEPTH 1

Definition at line 155 of file calInt.h.

#define TABLE_SIZE ( sizeIndex ) (1<<sizeIndex)

Definition at line 172 of file calInt.h.

#define TRUE 1

Definition at line 130 of file calInt.h.

#define USE_POWER_OF_2

Definition at line 170 of file calInt.h.

Typedef Documentation

typedef struct Cal_BddStruct Cal_Bdd_t

Definition at line 196 of file calInt.h.

typedef unsigned short Cal_BddRefCount_t

Definition at line 198 of file calInt.h.

typedef struct Cal_BlockStruct Cal_Block_t

Definition at line 211 of file calInt.h.

typedef unsigned long CalAddress_t

Definition at line 210 of file calInt.h.

typedef struct CalAssociationStruct CalAssociation_t

Definition at line 205 of file calInt.h.

typedef struct CalBddNodeStruct CalBddNode_t

Definition at line 197 of file calInt.h.

typedef int(* CalBddNodeToIndexFn_t)(CalBddNode_t *, Cal_BddId_t)

Definition at line 209 of file calInt.h.

typedef struct CalCacheTableStruct CalCacheTable_t

Definition at line 208 of file calInt.h.

typedef struct CalHashTableStruct CalHashTable_t

Definition at line 202 of file calInt.h.

typedef struct CalListStruct CalList_t

Definition at line 201 of file calInt.h.

typedef struct CalNodeManagerStruct CalNodeManager_t

Definition at line 200 of file calInt.h.

typedef int(* CalOpProc1_t)(Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t *)

Definition at line 219 of file calInt.h.

typedef int(* CalOpProc_t)(Cal_BddManager, Cal_Bdd_t, Cal_Bdd_t, Cal_Bdd_t *)

Definition at line 218 of file calInt.h.

typedef struct CalPageManagerStruct CalPageManager_t

Definition at line 199 of file calInt.h.

typedef enum CalPipeStateEnum CalPipeState_t

Definition at line 227 of file calInt.h.

typedef struct CalHashTableStruct* CalReqQueForId_t

Definition at line 203 of file calInt.h.

typedef struct CalHashTableStruct CalReqQueForIdAtDepth_t

Definition at line 204 of file calInt.h.

typedef struct Cal_BddStruct CalRequest_t

Definition at line 207 of file calInt.h.

typedef struct CalBddNodeStruct CalRequestNode_t

Definition at line 206 of file calInt.h.

Enumeration Type Documentation

enum CalPipeStateEnum

Enumerator:

READY
CREATE
UPDATE

Definition at line 226 of file calInt.h.

00226 { READY, CREATE, UPDATE };

Function Documentation

EXTERN void CalAlignCollisionChains ( Cal_BddManager_t * bddManager )

EXTERN void CalAssociationListFree ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [Frees the variable associations]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 431 of file calAssociation.c.

00432 {
00433   CalAssociation_t *assoc, *nextAssoc;
00434   
00435   for(assoc = bddManager->associationList;
00436       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00437     nextAssoc = assoc->next;
00438     Cal_MemFree(assoc->varAssociation);
00439     /*CAL_BDD_FREE_REC(bddManager, assoc, CalAssociation_t);*/
00440     Cal_MemFree(assoc);
00441   }
00442 }

EXTERN int CalBddArrayPreProcessing	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd *	userBddArray
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 330 of file calUtil.c.

00331 {
00332   int i = 0;
00333   Cal_Bdd userBdd;
00334   while ((userBdd = userBddArray[i++])){
00335     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00336       return 0;
00337     }
00338   }
00339   return 1;
00340 }

EXTERN void CalBddBlockDelta	(	Cal_Block	b,
		long	delta
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 185 of file calBlk.c.

00186 {
00187   long i;
00188   b->firstIndex += delta;
00189   b->lastIndex += delta;
00190   for (i=0; i < b->numChildren; ++i)
00191     CalBddBlockDelta(b->children[i], delta);
00192 }

EXTERN void CalBddFatalMessage ( char * string )

Function********************************************************************

Name [CalBddFatalMessage]

Synopsis [Prints fatal message and exits.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 425 of file calUtil.c.

00426 {
00427   (void) fprintf(stderr,"Fatal: %s\n", string);
00428   exit(-1);
00429 }

EXTERN long CalBddFindBlock	(	Cal_Block	block,
		long	index
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 151 of file calBlk.c.

00152 {
00153   long i, j, k;
00154 
00155   i = 0;
00156   j = block->numChildren-1;
00157   while (i <= j) {
00158     k = (i+j)/2;
00159     if (block->children[k]->firstIndex <= index &&
00160         block->children[k]->lastIndex >= index){
00161       return (k);
00162     }
00163     if (block->children[k]->firstIndex > index){
00164       j = k-1;
00165     }
00166     else {
00167       i = k+1;
00168     }
00169   }
00170   return i;
00171 }

EXTERN void CalBddFunctionPrint	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	calBdd,
		char *	name
	)

Function********************************************************************

Synopsis [Prints the function implemented by the argument BDD]

Description [Prints the function implemented by the argument BDD]

SideEffects [None]

Definition at line 169 of file calUtil.c.

00172 {
00173   Cal_Bdd_t T,E;
00174   Cal_BddId_t id;
00175   char c;
00176   static int level;
00177 
00178   if(level == 0)printf("%s = ",name);
00179   level++;
00180   printf("( ");
00181   if(CalBddIsBddZero(bddManager, calBdd)){
00182     printf("0 ");
00183   }
00184   else if(CalBddIsBddOne(bddManager, calBdd)){
00185     printf("1 ");
00186   }
00187   else{
00188     id = CalBddGetBddId(calBdd);
00189     c = (char)((int)'a' + id - 1);
00190     printf("%c ", c);
00191     CalBddGetCofactors(calBdd, id, T, E);
00192     CalBddFunctionPrint(bddManager, T, " ");
00193     printf("+ %c' ", c);
00194     CalBddFunctionPrint(bddManager, E, " ");
00195   }
00196   level--;
00197   printf(") ");
00198   if(level == 0)printf("\n");
00199 }

EXTERN Cal_Bdd CalBddGetExternalBdd	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	internalBdd
	)

Function********************************************************************

Name [CalBddFatalMessage]

Synopsis [Prints fatal message and exits.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 386 of file calUtil.c.

00387 {
00388   CalHashTable_t *hashTableForUserBdd = bddManager->uniqueTable[0];
00389   Cal_Bdd_t resultBdd;
00390   int found;
00391   
00392   if(CalBddIsOutPos(internalBdd)){
00393     found = CalHashTableFindOrAdd(hashTableForUserBdd, internalBdd,
00394                           bddManager->bddOne, &resultBdd);
00395   }
00396   else {
00397     Cal_Bdd_t internalBddNot;
00398     CalBddNot(internalBdd, internalBddNot);
00399     found = CalHashTableFindOrAdd(hashTableForUserBdd, internalBddNot,
00400                           bddManager->bddOne, &resultBdd);
00401     CalBddNot(resultBdd, resultBdd);
00402   }
00403   if (found == 0){
00404     CalBddIcrRefCount(internalBdd);
00405   }
00406   CalBddIcrRefCount(resultBdd);
00407   return CalBddGetBddNode(resultBdd);
00408 }

EXTERN Cal_Bdd_t CalBddGetInternalBdd	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Function********************************************************************

Name [CalBddFatalMessage]

Synopsis [Prints fatal message and exits.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 357 of file calUtil.c.

00358 {
00359   Cal_Bdd_t resultBdd;
00360   if (CalBddNodeIsOutPos(userBdd)){
00361     CalBddNodeGetThenBdd(userBdd, resultBdd);
00362   }
00363   else {
00364     Cal_Bdd userBddNot = CalBddNodeNot(userBdd);
00365     Cal_Bdd_t internalBdd;
00366         CalBddNodeGetThenBdd(userBddNot,internalBdd);
00367     CalBddNot(internalBdd, resultBdd);
00368   }
00369   return resultBdd;
00370 }

EXTERN Cal_Bdd_t CalBddIdentity	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	calBdd
	)

Function********************************************************************

Synopsis [Returns the duplicate BDD of the argument BDD.]

Description [Returns the duplicate BDD of the argument BDD.]

SideEffects [The reference count of the BDD is increased by 1.]

SeeAlso [Cal_BddNot]

Definition at line 935 of file cal.c.

00936 {
00937   CalBddIcrRefCount(calBdd);
00938   return calBdd;
00939 }

EXTERN Cal_Bdd_t CalBddIf	(	Cal_BddManager	bddManager,
		Cal_Bdd_t	F
	)

AutomaticStart

Function********************************************************************

Synopsis [Returns the BDD corresponding to the top variable of the argument BDD.]

Description [Returns the BDD corresponding to the top variable of the argument BDD.]

SideEffects [None.]

Definition at line 852 of file cal.c.

00853 {
00854   if (CalBddIsBddConst(F)){
00855     CalBddWarningMessage("CalBddIf: argument is constant");
00856   }
00857   return bddManager->varBdds[CalBddGetBddId(F)];
00858 }

EXTERN int CalBddIsCubeStep	(	Cal_BddManager	bddManager,
		Cal_Bdd_t	f
	)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is a cube, 0 otherwise]

Description [Returns 1 if the argument BDD is a cube, 0 otherwise]

SideEffects [None]

Definition at line 870 of file cal.c.

00871 {
00872   Cal_Bdd_t f0, f1;
00873   if (CalBddIsBddConst(f)){
00874     if (CalBddIsBddZero(bddManager, f)){
00875       CalBddFatalMessage("Cal_BddIsCube called with 0");
00876     }
00877     else return 1;
00878   }
00879 
00880   CalBddGetThenBdd(f, f1);
00881   CalBddGetElseBdd(f, f0);
00882   /*
00883    * Exactly one branch of f must point to ZERO to be a cube.
00884    */
00885   if (CalBddIsBddZero(bddManager, f1)){
00886         return (CalBddIsCubeStep(bddManager, f0));
00887   } else if (CalBddIsBddZero(bddManager, f0)){
00888         return (CalBddIsCubeStep(bddManager, f1));
00889   } else { /* not a cube, because neither branch is zero */
00890         return 0;
00891   }
00892 }

EXTERN Cal_Bdd_t CalBddITE	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	F,
		Cal_Bdd_t	G,
		Cal_Bdd_t	H
	)

Function********************************************************************

Synopsis [Returns the BDD for logical If-Then-Else

Description [Returns the BDD for the logical operation IF f THEN g ELSE h

f g + f' h]

SideEffects [None]

SeeAlso [Cal_BddAnd, Cal_BddNand, Cal_BddOr, Cal_BddNor, Cal_BddXor, Cal_BddXnor]

Definition at line 322 of file calBddITE.c.

00324 {
00325   Cal_Bdd_t result;
00326   result = CalBddOpITEBF(bddManager, F, G, H);
00327   CalBddIcrRefCount(result);
00328   return result;
00329 }

EXTERN Cal_Bdd_t CalBddManagerCreateNewVar	(	Cal_BddManager_t *	bddManager,
		Cal_BddIndex_t	index
	)

Function********************************************************************

Synopsis [This function creates and returns a new variable with given index value.]

Description [Right now this function does not handle the case when the package is working in multiprocessor mode. We need to put in the necessary code later.]

SideEffects [If the number of variables in the manager exceeds that of value of numMaxVars, then we need to reallocate various fields of the manager. Also depending upon the value of "index", idToIndex and indexToId tables would change.]

Definition at line 567 of file calBddManager.c.

00568 {
00569   Cal_Bdd_t calBdd;
00570   Cal_BddId_t varId;
00571   int totalNumVars, maxNumVars, i;
00572   CalAssociation_t *association;
00573   
00574   if (bddManager->numVars == CAL_MAX_VAR_ID){
00575     CalBddFatalMessage("Cannot create any new variable, no more Id left."); 
00576   }
00577 
00578   /*
00579    * Get the total number of variables. If the index is more than the total
00580    * number of variables, then report error.
00581    */
00582   totalNumVars = bddManager->numVars;
00583   
00584   if (index > totalNumVars){
00585     CalBddFatalMessage("The variable index out of range");
00586   }
00587   
00588 
00589   /*
00590    * Create a new variable in the manager which contains this index.
00591    * This might lead to change in the id->index, and index->id
00592    * for other managers.
00593    */
00594 
00595   /*
00596    * If the number of variables is equal to the maximum number of variables
00597    * then reallocate memory.
00598    */
00599   if (bddManager->numVars == bddManager->maxNumVars){
00600     int oldMaxNumVars;
00601     CalAssociation_t *p;
00602     
00603     oldMaxNumVars = bddManager->maxNumVars;
00604     if ((maxNumVars = 2*oldMaxNumVars) > CAL_MAX_VAR_ID){
00605       maxNumVars = CAL_MAX_VAR_ID;
00606     }
00607     bddManager->maxNumVars = maxNumVars;
00608     bddManager->varBdds = Cal_MemRealloc(Cal_Bdd_t,
00609                                          bddManager->varBdds, maxNumVars+1); 
00610     
00611     bddManager->nodeManagerArray = Cal_MemRealloc(CalNodeManager_t *,
00612                                                   bddManager->nodeManagerArray, 
00613                                                   maxNumVars+1);
00614 
00615     bddManager->idToIndex = Cal_MemRealloc(Cal_BddIndex_t, bddManager->idToIndex,
00616                                         maxNumVars+1);
00617 
00618     bddManager->indexToId = Cal_MemRealloc(Cal_BddIndex_t, bddManager->indexToId,
00619                                         maxNumVars);
00620 
00621     bddManager->uniqueTable = Cal_MemRealloc(CalHashTable_t *,
00622                                           bddManager->uniqueTable, maxNumVars+1);
00623     
00624     for (i=0; i<bddManager->maxDepth; i++){
00625       bddManager->reqQue[i] = Cal_MemRealloc(CalHashTable_t *, bddManager->reqQue[i],
00626                                           maxNumVars+1);
00627     }
00628     bddManager->tempAssociation->varAssociation = 
00629         Cal_MemRealloc(Cal_Bdd_t, bddManager->tempAssociation->varAssociation,
00630         maxNumVars+1);
00631     /* CHECK LOOP INDICES */
00632     for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){
00633       bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
00634     }
00635     for(p = bddManager->associationList; p; p = p->next){
00636       p->varAssociation = 
00637           Cal_MemRealloc(Cal_Bdd_t, p->varAssociation, maxNumVars+1);
00638       /* CHECK LOOP INDICES */
00639       for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){
00640         p->varAssociation[i] = bddManager->bddNull;
00641       }
00642     }
00643   }
00644 
00645   /* If the variable has been created in the middle, shift the indices. */
00646   if (index != bddManager->numVars){
00647     for (i=0; i<bddManager->numVars; i++){
00648       if (bddManager->idToIndex[i+1] >= index){
00649         bddManager->idToIndex[i+1]++;
00650       }
00651     }
00652   }
00653 
00654   /* Fix indexToId table */
00655   for (i=bddManager->numVars; i>index; i--){
00656     bddManager->indexToId[i] = bddManager->indexToId[i-1];
00657   }
00658 
00659   for(association = bddManager->associationList; association;
00660                                               association =
00661                                                   association->next){
00662     if (association->lastBddIndex >= index){
00663       association->lastBddIndex++;
00664     }
00665   }
00666   if (bddManager->tempAssociation->lastBddIndex >= index){
00667     bddManager->tempAssociation->lastBddIndex++;
00668   }
00669   
00670   bddManager->numVars++;
00671   varId = bddManager->numVars;
00672 
00673   bddManager->idToIndex[varId] = index;
00674   bddManager->indexToId[index] = varId;
00675   
00676   bddManager->nodeManagerArray[varId] =
00677       CalNodeManagerInit(bddManager->pageManager2); 
00678   bddManager->uniqueTable[varId] =
00679       CalHashTableInit(bddManager, varId);
00680     
00681   /* insert node in the uniqueTableForId */
00682   CalHashTableAddDirectAux(bddManager->uniqueTable[varId],
00683                            bddManager->bddOne, bddManager->bddZero, &calBdd);
00684   CalBddPutRefCount(calBdd, CAL_MAX_REF_COUNT);
00685   bddManager->varBdds[varId] = calBdd;
00686 
00687   bddManager->numNodes++;
00688   
00689 #ifdef __OLD__
00690   /* initialize req_que_for_id */
00691   bddManager->reqQue[varId] = Cal_MemAlloc(CalHashTable_t*, bddManager->maxDepth);
00692   for (i=0; i<manager->maxDepth; i++){
00693     bddManager->reqQue[varId][i] = CalHashTableInit(bddManager, varId);
00694   }
00695 #endif
00696   
00697   /* initialize req_que_for_id */
00698   for (i=0; i<bddManager->maxDepth; i++){
00699     bddManager->reqQue[i][varId] =
00700         CalHashTableInit(bddManager, varId);
00701   }
00702   CalBddShiftBlock(bddManager, bddManager->superBlock, (long)index);
00703   return calBdd;
00704 }

EXTERN void CalBddManagerGCCheck ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 181 of file calGC.c.

00182 {
00183   if (bddManager->gcMode == 0) return;
00184   if (bddManager->gcCheck > 0) return;
00185   bddManager->gcCheck = CAL_GC_CHECK;
00186   if(bddManager->numNodes > bddManager->uniqueTableGCLimit){
00187     Cal_BddManagerGC(bddManager);
00188     Cal_BddManagerSetGCLimit(bddManager);
00189   }
00190 }

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
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 500 of file calCacheTableTwo.c.

00507 {
00508   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00509   *cacheSize += cacheTable->numBins;
00510   *cacheEntries += cacheTable->numEntries;
00511   *cacheInsertions += cacheTable->numInsertions;
00512   *cacheLookups += cacheTable->numLookups;
00513   *cacheHits += cacheTable->numHits;
00514   *cacheCollisions += cacheTable->numCollisions;
00515 }

EXTERN void CalBddMarkSharedNodes	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 209 of file calPrint.c.

00210 {
00211   int mark;
00212   Cal_Bdd_t thenBdd, elseBdd;
00213   
00214   if (CalBddIsOutPos(f) == 0){
00215     CalBddNot(f,f);
00216   }
00217   if (CalBddIsBddConst(f) || CalBddTypeAux(bddManager, f) ==
00218       CAL_BDD_TYPE_POSVAR)
00219     return; 
00220   if ((mark = CalBddGetMark(f))){
00221     if (mark == 1){
00222       CalBddPutMark(f, 2);
00223       return;
00224     }
00225   }
00226   CalBddPutMark(f, 1);
00227   CalBddGetThenBdd(f, thenBdd);
00228   CalBddGetElseBdd(f, elseBdd);
00229   CalBddMarkSharedNodes(bddManager, thenBdd);
00230   CalBddMarkSharedNodes(bddManager, elseBdd);
00231 }

EXTERN void CalBddNodePrint ( CalBddNode_t * bddNode )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 461 of file calUtil.c.

00462 {
00463   int refCount;
00464   CalBddNodeGetRefCount(bddNode, refCount);
00465   printf("Node (%lx) thenBdd(%2d %lx)  elseBdd(%2d %lx) ref_count (%d) next (%lx)\n",
00466          (CalAddress_t)bddNode,
00467          CalBddNodeGetThenBddId(bddNode),
00468          (CalAddress_t) CalBddNodeGetThenBddNode(bddNode), 
00469          CalBddNodeGetElseBddId(bddNode),
00470          (CalAddress_t) CalBddNodeGetElseBddNode(bddNode),
00471          refCount, (CalAddress_t)bddNode->nextBddNode);
00472 }

EXTERN void CalBddNumberSharedNodes	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		CalHashTable_t *	hashTable,
		long *	next
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 174 of file calPrint.c.

00176 {
00177   Cal_Bdd_t thenBdd, elseBdd;
00178   int mark;
00179   
00180   if (CalBddIsBddConst(f) || ((1 << CalBddTypeAux(bddManager, f)) &
00181                            ((1 << CAL_BDD_TYPE_POSVAR) |
00182                             (1 << CAL_BDD_TYPE_NEGVAR))))
00183     return;
00184   mark = CalBddGetMark(f);
00185   if (mark == 0) return;
00186   if (mark  == 2) {
00187     CalHashTableOneInsert(hashTable, f, (char *)next);
00188     ++*next;
00189   }
00190   CalBddPutMark(f, 0);
00191   CalBddGetThenBdd(f, thenBdd);
00192   CalBddGetElseBdd(f, elseBdd);
00193   CalBddNumberSharedNodes(bddManager, thenBdd, hashTable, next);
00194   CalBddNumberSharedNodes(bddManager, elseBdd, hashTable, next);
00195 }

EXTERN Cal_Bdd_t CalBddOpBF	(	Cal_BddManager_t *	bddManager,
		CalOpProc_t	calOpProc,
		Cal_Bdd_t	F,
		Cal_Bdd_t	G
	)

Function********************************************************************

Synopsis [Internal routine to compute a logical operation on a pair of BDDs]

Description [Internal routine to compute a logical operation on a pair of BDDs]

SideEffects [None]

Definition at line 705 of file calBddOp.c.

00710 {
00711   Cal_Bdd_t result;
00712   Cal_BddId_t minId, bddId;
00713   /*Cal_BddIndex_t minIndex; Commented out because of the problem on alpha*/ 
00714   int minIndex;
00715   int bddIndex;
00716   CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
00717   
00718   if (calOpProc(bddManager, F, G, &result)){
00719     return result;
00720   }
00721   CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
00722   hashTableArray = bddManager->reqQue[0];
00723   CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
00724   
00725   /* ReqQueApply */
00726   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00727     bddId = bddManager->indexToId[bddIndex];
00728     hashTable = hashTableArray[bddId];
00729     if(hashTable->numEntries){
00730       CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
00731     }
00732   }
00733 #ifdef COMPUTE_MEMORY_OVERHEAD
00734   {
00735     calNumEntriesAfterApply = 0;
00736     for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00737       bddId = bddManager->indexToId[bddIndex];
00738       hashTable = hashTableArray[bddId];
00739       calNumEntriesAfterApply += hashTable->numEntries;
00740     }
00741   }
00742 #endif
00743   /* ReqQueReduce */
00744   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00745     bddId = bddManager->indexToId[bddIndex];
00746     uniqueTableForId = bddManager->uniqueTable[bddId];
00747     hashTable = hashTableArray[bddId];
00748     if(hashTable->numEntries){
00749       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00750     }
00751   }
00752   CalRequestIsForwardedTo(result);
00753 
00754 #ifdef COMPUTE_MEMORY_OVERHEAD
00755   {
00756     CalRequestNode_t *requestNode;
00757     calNumEntriesAfterReduce = 0;
00758     for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00759       CalRequestNode_t *next;
00760       Cal_BddId_t bddId;
00761       
00762       bddId = bddManager->indexToId[bddIndex];
00763       hashTable = hashTableArray[bddId];
00764       for (requestNode = hashTable->requestNodeList; requestNode !=
00765                                                          Cal_Nil(CalRequestNode_t);
00766                                                      requestNode = next){
00767         next = CalRequestNodeGetNextRequestNode(requestNode);
00768         calNumEntriesAfterReduce++;
00769       }
00770     }
00771     calAfterReduceToAfterApplyNodesRatio =
00772         ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
00773     calAfterReduceToUniqueTableNodesRatio = 
00774         ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
00775   }
00776 #endif
00777 
00778   /* Clean up */
00779   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00780     bddId = bddManager->indexToId[bddIndex];
00781     CalHashTableCleanUp(hashTableArray[bddId]);
00782   }
00783   return result;
00784 }

EXTERN Cal_Bdd_t CalBddOpITEBF	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t	g,
		Cal_Bdd_t	h
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 218 of file calBddITE.c.

00223 {
00224   Cal_Bdd_t result;
00225   Cal_BddId_t bddId;
00226   /*Cal_BddIndex_t minIndex;*/
00227   int minIndex;
00228   int bddIndex;
00229   CalHashTable_t *hashTable;
00230   CalHashTable_t *uniqueTableForId;
00231   CalHashTable_t **reqQueForITE = bddManager->reqQue[0];
00232   
00233   result = CalOpITE(bddManager, f, g, h, reqQueForITE);
00234   
00235   CalBddGetMinIndex3(bddManager, f, g, h, minIndex);
00236   /* ReqQueApply */
00237   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00238     bddId = bddManager->indexToId[bddIndex];
00239     hashTable = reqQueForITE[bddId];
00240     if(hashTable->numEntries){
00241       CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
00242     }
00243   }
00244 
00245   /* ReqQueReduce */
00246   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00247     bddId = bddManager->indexToId[bddIndex];
00248     uniqueTableForId = bddManager->uniqueTable[bddId];
00249     hashTable = reqQueForITE[bddId];
00250     if(hashTable->numEntries){
00251       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00252     }
00253   }
00254 
00255   CalRequestIsForwardedTo(result);
00256 
00257   /* Clean up */
00258   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00259     bddId = bddManager->indexToId[bddIndex];
00260     CalHashTableCleanUp(reqQueForITE[bddId]);
00261   }
00262 
00263   return result;
00264 }

EXTERN void CalBddPackNodesAfterReorderForSingleId	(	Cal_BddManager_t *	bddManager,
		int	fixForwardedNodesFlag,
		int	bestIndex,
		int	bottomIndex
	)

Function********************************************************************

Synopsis [Packs the nodes if the variables which has just been sifted.]

Description [fixForwardedNodesFlag: Whether we need to fix the forwarded nodes of variables corresponding to bestIndex through bottomIndex. If this flag is set, then the forwarded nodes of these variables are traversed and updated after the nodes of the bestIndex have been copied. At the end the forwarded nodes are freed. If this flag is not set, it is assumed that the cleanup pass has already been performed.]

SideEffects [required]

SeeAlso [optional]

Definition at line 693 of file calHashTable.c.

00697 {
00698   /* We need to pack the nodes for this id and fix the cofactors of
00699      the upper indices.
00700      */
00701   CalBddNode_t *node, *nextBddNode, *dupNode, **oldBins;
00702   CalBddNode_t *thenBddNode, *elseBddNode, *bddNode;
00703   Cal_Bdd_t thenBdd;
00704   CalAddress_t *page;
00705   int id = bddManager->indexToId[bestIndex];
00706   CalNodeManager_t *nodeManager = bddManager->nodeManagerArray[id];
00707   CalAddress_t **oldPageList = nodeManager->pageList;
00708   int oldNumPages = nodeManager->numPages;
00709   CalHashTable_t *uniqueTableForId = bddManager->uniqueTable[id];
00710   int numPagesRequired, newSizeIndex, index, i;
00711   long oldNumBins, hashValue;
00712   
00713   
00714 #ifdef _CAL_VERBOSE
00715   fprintf(stdout,"Repacking id %3d\n", id);
00716 #endif
00717   
00718 
00719   nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
00720   nodeManager->numPages = 0;
00721   numPagesRequired = uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
00722   nodeManager->maxNumPages =
00723       2*(numPagesRequired ? numPagesRequired : 1);
00724 
00725   nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
00726                                        nodeManager->maxNumPages); 
00727   
00728   oldBins = uniqueTableForId->bins;
00729   oldNumBins = uniqueTableForId->numBins;
00730   /* Create the new set of bins */
00731   newSizeIndex =
00732       CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY);
00733 
00734   if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00735     newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00736   }
00737 
00738   uniqueTableForId->sizeIndex = newSizeIndex;
00739   uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00740   uniqueTableForId->maxCapacity =
00741       uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00742 
00743   uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00744                                         uniqueTableForId->numBins); 
00745   if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
00746     CalBddFatalMessage("out of memory");
00747   }
00748 
00749   memset((char *)uniqueTableForId->bins, 0, 
00750         uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
00751 
00752   for (i = 0; i < oldNumBins; i++){
00753     node = oldBins[i];
00754     while (node){
00755       nextBddNode = CalBddNodeGetNextBddNode(node);
00756       CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
00757       thenBddNode = CalBddNodeGetThenBddNode(dupNode);
00758       elseBddNode = CalBddNodeGetElseBddNode(dupNode);
00759       hashValue = CalDoHash2(thenBddNode, elseBddNode, uniqueTableForId);
00760       CalBddNodePutNextBddNode(dupNode, uniqueTableForId->bins[hashValue]);
00761       uniqueTableForId->bins[hashValue] = dupNode;
00762       CalBddNodePutThenBddNode(node, dupNode);
00763       CalBddNodePutThenBddId(node, id);
00764       CalBddNodePutElseBddNode(node, FORWARD_FLAG);
00765       node = nextBddNode;
00766       Cal_Assert(!(CalBddNodeIsRefCountZero(dupNode)));
00767     }
00768   }
00769   
00770   if (fixForwardedNodesFlag){
00771       CalBddNode_t *requestNodeList =
00772           bddManager->uniqueTable[id]->startNode.nextBddNode;  
00773       for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
00774         Cal_Assert(CalBddNodeIsForwarded(bddNode));
00775         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00776         CalBddNodeGetThenBdd(bddNode, thenBdd);
00777         if (CalBddGetBddId(thenBdd) == id){
00778           if (CalBddIsForwarded(thenBdd)) {
00779             CalBddForward(thenBdd);
00780             Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00781             CalBddNodePutThenBdd(bddNode, thenBdd);
00782           }
00783         }
00784         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00785       }
00786       for (index = bestIndex+1; index <= bottomIndex; index++){   
00787       int varId = bddManager->indexToId[index];
00788       requestNodeList =
00789           bddManager->uniqueTable[varId]->startNode.nextBddNode;   
00790       for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
00791         Cal_Assert(CalBddNodeIsForwarded(bddNode));
00792         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00793         CalBddNodeGetThenBdd(bddNode, thenBdd);
00794         if (CalBddIsForwarded(thenBdd)) {
00795           CalBddForward(thenBdd);
00796           Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00797           CalBddNodePutThenBdd(bddNode, thenBdd);
00798         }
00799         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00800       }
00801     }
00802   }
00803   
00804 /* Traverse the upper indices fixing the cofactors */
00805   for (index = bestIndex-1; index >= 0; index--){
00806     CalBddReorderFixCofactors(bddManager,
00807                            bddManager->indexToId[index]); 
00808   }
00809 
00810   if (bddManager->pipelineState == CREATE){
00811     /* There are some results computed in pipeline */
00812     CalBddReorderFixProvisionalNodes(bddManager);
00813   }
00814   
00815   /* Fix the user BDDs */
00816   CalBddReorderFixUserBddPtrs(bddManager);
00817 
00818   CalBddIsForwardedTo(bddManager->varBdds[id]);
00819 
00820   /* Fix the association */
00821   CalReorderAssociationFix(bddManager);
00822   
00823   /* Free the old bins */
00824   Cal_MemFree(oldBins);
00825 
00826   uniqueTableForId->endNode = &(uniqueTableForId->startNode);
00827   uniqueTableForId->startNode.nextBddNode = NULL;
00828   if (fixForwardedNodesFlag){
00829     CalBddReorderReclaimForwardedNodes(bddManager, bestIndex+1,
00830                                     bottomIndex);
00831   }
00832   /* Free the old pages */
00833   for (i = 0; i < oldNumPages; i++){
00834     page = oldPageList[i]; 
00835     CalPageManagerFreePage(nodeManager->pageManager, page);
00836   }
00837   Cal_MemFree(oldPageList);
00838   Cal_Assert(CalCheckAllValidity(bddManager));
00839 }

EXTERN void CalBddPackNodesForMultipleIds	(	Cal_BddManager_t *	bddManager,
		Cal_BddId_t	beginId,
		int	numLevels
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 853 of file calHashTable.c.

00856 00857 00858 00859 00860 00861 00862 00863 00864 00865 00866 00867 00868 00869 00870 00871 00872 00873 00874 00875 00876 00877 00878 00879 00880 00881 00882 00883 00884 00885 00886 00887 00888 00889 00890 00891 00892 00893 00894 00895 00896 00897 00898 00899 00900 00901 00902 00903 00904       } 00905 00906 00907 00908 00909 00910 00911 00912 00913 00914       } 00915 00916 00917 00918 00919 00920 00921 00922 00923 00924 00925 00926 00927           } 00928 00929 00930 00931           } 00932 00933 00934 00935 00936 00937 00938 00939 00940 00941 00942 00943         } 00944       } 00945 00946 00947 00948 00949 00950 00951 00952 00953 00954 00955 00956 00957 00958 00959 00960           } 00961 00962 00963 00964           } 00965 00966 00967 00968         } 00969 00970       } 00971 00972 00973 00974 00975 00976 00977 00978 00979 00980 00981 00982       } 00983 00984 00985     } 00986 00987 00988     } 00989   } 00990 00991 00992 00993 00994 00995 00996   } 00997 00998 00999 01000 01001 01002 01003   } 01004 01005 01006 01007 01008 01009 01010 01011 01012 01013 01014 01015 01016 01017 01018 01019     } 01020 01021   } 01022 01023 01024 }

class="fragment">00855 { /* We need to pack the nodes for this id and fix the cofactors of the upper indices. */ int index = bddManager->idToIndex[beginId]; int level, id; long i, j; CalBddNode_t *node, *nextBddNode, *dupNode, *thenBddNode; CalBddNode_t *elseBddNode, **oldBins; Cal_Bdd_t thenBdd, elseBdd; CalNodeManager_t *nodeManager; CalHashTable_t *uniqueTableForId; int someRepackingDone = 0; long oldNumBins, hashValue; int newSizeIndex; CalAddress_t *page, ***oldPageListArray, **oldPageList; int *oldNumPagesArray; int numPagesRequired; oldPageListArray = Cal_MemAlloc(CalAddress_t **, numLevels); oldNumPagesArray = Cal_MemAlloc(int, numLevels); for (level = numLevels-1; level >= 0; level--){ id = bddManager->indexToId[index+level]; oldNumPagesArray[level] = 0; oldPageListArray[level] = Cal_Nil(CalAddress_t *); if (CalBddIdNeedsRepacking(bddManager, id)){ nodeManager = bddManager->nodeManagerArray[id]; uniqueTableForId = bddManager->uniqueTable[id]; oldPageListArray[level] = nodeManager->pageList; oldNumPagesArray[level] = nodeManager->numPages; nodeManager->freeNodeList = Cal_Nil(CalBddNode_t); nodeManager->numPages = 0; numPagesRequired = uniqueTableForId->numEntries/NUM_NODES_PER_PAGE; nodeManager->maxNumPages = 2*(numPagesRequired ? numPagesRequired : 1); nodeManager->pageList = Cal_MemAlloc(CalAddress_t *, nodeManager->maxNumPages); oldBins = uniqueTableForId->bins; oldNumBins = uniqueTableForId->numBins; /* Create the new set of bins */ newSizeIndex = CeilLog2(uniqueTableForId->numEntries / HASH_TABLE_DEFAULT_MAX_DENSITY); if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){ newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX; uniqueTableForId->sizeIndex = newSizeIndex; uniqueTableForId->numBins = TABLE_SIZE(uniqueTableForId->sizeIndex); uniqueTableForId->maxCapacity = uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *, uniqueTableForId->numBins); if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){ CalBddFatalMessage("out of memory"); memset((char *)uniqueTableForId->bins, 0, uniqueTableForId->numBins*sizeof(CalBddNode_t *)); for (i = 0; i < oldNumBins; i++){ node = oldBins[i]; while (node){ nextBddNode = CalBddNodeGetNextBddNode(node); CalBddNodeGetThenBdd(node, thenBdd); CalBddNodeGetElseBdd(node, elseBdd); if (CalBddIsForwarded(thenBdd)){ CalBddForward(thenBdd); CalBddNodePutThenBdd(node, thenBdd); if (CalBddIsForwarded(elseBdd)){ CalBddForward(elseBdd); CalBddNodePutElseBdd(node, elseBdd); CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode); thenBddNode = CalBddNodeGetThenBddNode(dupNode); elseBddNode = CalBddNodeGetElseBddNode(dupNode); hashValue = CalDoHash2(thenBddNode, elseBddNode, uniqueTableForId); CalBddNodePutNextBddNode(dupNode, uniqueTableForId->bins[hashValue]); uniqueTableForId->bins[hashValue] = dupNode; CalBddNodePutThenBddNode(node, dupNode); CalBddNodePutThenBddId(node, id); CalBddNodePutElseBddNode(node, FORWARD_FLAG); node = nextBddNode; Cal_Assert(!(CalBddNodeIsRefCountZero(dupNode))); #ifdef __FOO__ /*fprintf(stdout,"Repacking id = %d, index = %d\n", id, index+level);*/ /* First put all the nodes in that list */ nodeList = Cal_Nil(CalBddNode_t); for (i = 0; i < uniqueTableForId->numBins; i++){ node = uniqueTableForId->bins[i]; while (node){ nextBddNode = CalBddNodeGetNextBddNode(node); /* The "then" and "else" pointers could be forwarded */ CalBddNodeGetThenBdd(node, thenBdd); CalBddNodeGetElseBdd(node, elseBdd); if (CalBddIsForwarded(thenBdd)){ CalBddForward(thenBdd); CalBddNodePutThenBdd(node, thenBdd); if (CalBddIsForwarded(elseBdd)){ CalBddForward(elseBdd); CalBddNodePutElseBdd(node, elseBdd); CalBddNodePutNextBddNode(node, nodeList); nodeList = node; node = nextBddNode; uniqueTableForId->bins[i] = Cal_Nil(CalBddNode_t); uniqueTableForId->numEntries = 0; for (node = nodeList; node; node = nextBddNode){ nextBddNode = CalBddNodeGetNextBddNode(node); CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode); /* Hash the dupNode */ CalHashTableAddDirect(uniqueTableForId, dupNode); /* Make the original node a forwarding node */ CalBddNodePutThenBddNode(node, dupNode); CalBddNodePutThenBddId(node, id); CalBddNodePutElseBddNode(node, FORWARD_FLAG); #endif someRepackingDone = 1; else if (someRepackingDone){ /* Still need to fix the cofactors */ CalBddReorderFixCofactors(bddManager, id); /* Traverse the upper indices fixing the cofactors */ for (i = index-1; i >= 0; i--){ CalBddReorderFixCofactors(bddManager, bddManager->indexToId[i]); /* Fix the user BDDs */ CalBddReorderFixUserBddPtrs(bddManager); if (bddManager->pipelineState == CREATE){ /* There are some results computed in pipeline */ CalBddReorderFixProvisionalNodes(bddManager); /* Fix Cache Tables */ (void)CalCacheTableTwoRepackUpdate(bddManager->cacheTable); for (level = numLevels - 1 ; level >= 0; level--){ id = bddManager->indexToId[index+level]; /* Update varBdd field of bdd manager */ CalBddIsForwardedTo(bddManager->varBdds[id]); /* Fix associations */ CalVarAssociationRepackUpdate(bddManager, id); /* Free the old pages */ nodeManager = bddManager->nodeManagerArray[id]; oldPageList = oldPageListArray[level]; for (j = 0; j < oldNumPagesArray[level]; j++){ page = oldPageList[j]; CalPageManagerFreePage(nodeManager->pageManager, page); if ((unsigned long)oldPageList) Cal_MemFree(oldPageList); Cal_MemFree(oldPageListArray); Cal_MemFree(oldNumPagesArray);

EXTERN void CalBddPackNodesForSingleId	(	Cal_BddManager_t *	bddManager,
		Cal_BddId_t	id
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 668 of file calHashTable.c.

00670 {
00671   /* Need to copy the one for "AfterReorder" and suitably modify. */
00672 }

EXTERN int CalBddPostProcessing ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 275 of file calUtil.c.

00276 {
00277   if (bddManager->gcCheck > 0) return CAL_BDD_OK;
00278   bddManager->gcCheck = CAL_GC_CHECK;
00279   if(bddManager->numNodes > bddManager->uniqueTableGCLimit){
00280     long origNodes = bddManager->numNodes;
00281     Cal_BddManagerGC(bddManager);
00282     if ((bddManager->numNodes > bddManager->reorderingThreshold) &&
00283         (3*bddManager->numNodes > 2* bddManager->uniqueTableGCLimit) &&
00284         (bddManager->dynamicReorderingEnableFlag) &&
00285         (bddManager->reorderTechnique != CAL_REORDER_NONE)){
00286       CalCacheTableTwoFlush(bddManager->cacheTable);
00287       if (bddManager->reorderMethod == CAL_REORDER_METHOD_BF){
00288         CalBddReorderAuxBF(bddManager);
00289       }
00290       else{
00291         CalBddReorderAuxDF(bddManager);
00292       }
00293     }
00294     else {
00295       /* Check if we should repack */
00296       Cal_Assert(CalCheckAllValidity(bddManager));
00297       if (bddManager->numNodes <
00298           bddManager->repackAfterGCThreshold*origNodes){
00299         CalRepackNodesAfterGC(bddManager);
00300       }
00301       Cal_Assert(CalCheckAllValidity(bddManager));
00302     }
00303     Cal_BddManagerSetGCLimit(bddManager);
00304     if (bddManager->nodeLimit && (bddManager->numNodes >
00305                                   bddManager->nodeLimit)){ 
00306       CalBddWarningMessage("Overflow: Node Limit Exceeded");
00307       bddManager->overflow = 1;
00308       return CAL_BDD_OVERFLOWED;
00309     }
00310     /*
00311      * Check to see if the cache table needs to be rehashed.
00312      */
00313     CalCacheTableRehash(bddManager);
00314   }
00315   return CAL_BDD_OK;
00316 }

EXTERN int CalBddPreProcessing	(	Cal_BddManager_t *	bddManager,
		int	count,
			...
	)

EXTERN int CalBddPreProcessing ( )

EXTERN void CalBddPrint ( Cal_Bdd_t calBdd )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 487 of file calUtil.c.

00488 {
00489   printf("Id(%2d) node(%lx) ",
00490       CalBddGetBddId(calBdd), (CalAddress_t) CalBddGetBddNode(calBdd));
00491   printf("thenBdd(%2d %lx)  elseBdd(%2d %lx)\n",
00492          CalBddGetThenBddId(calBdd),
00493          (CalAddress_t) CalBddGetThenBddNode(calBdd), 
00494          CalBddGetElseBddId(calBdd),
00495          (CalAddress_t) CalBddGetElseBddNode(calBdd));
00496 }

EXTERN void CalBddReorderAuxBF ( Cal_BddManager_t * bddManager )

AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 108 of file calReorderBF.c.

00109 {
00110   Cal_Assert(CalCheckAllValidity(bddManager));
00111   CalInitInteract(bddManager);
00112 #ifdef _CAL_QUANTIFY_
00113   quantify_start_recording_data();
00114 #endif
00115   if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
00116     char *levels = Cal_MemAlloc(char, bddManager->numVars);
00117     BddReorderVarWindow(bddManager, levels);
00118     Cal_MemFree(levels);
00119   }
00120   else {
00121     BddReorderVarSift(bddManager, bddManager->maxSiftingGrowth);
00122   }
00123 #ifdef _CAL_QUANTIFY_
00124   quantify_stop_recording_data();
00125 #endif
00126   Cal_Assert(CalCheckAllValidity(bddManager));
00127   Cal_MemFree(bddManager->interact);
00128   bddManager->numReorderings++;
00129 }

EXTERN void CalBddReorderAuxDF ( Cal_BddManager_t * bddManager )

AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 163 of file calReorderDF.c.

00164 {
00165   CalHashTableGC(bddManager, bddManager->uniqueTable[0]);
00166   /*Cal_BddManagerGC(bddManager);Cal_Assert(CalCheckAllValidity(bddManager));*/
00167   /* If we want to check the validity, we need to garbage collect */
00168   CalInitInteract(bddManager); /* Initialize the interaction matrix
00169                                   before changing the data structure */
00170   nodeManager = CalNodeManagerInit(bddManager->pageManager2);
00171   freeListId = 1;
00172 #ifdef _CAL_QUANTIFY_
00173   quantify_start_recording_data();
00174 #endif
00175   BddConvertDataStruct(bddManager);
00176   if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
00177     BddReorderStableWindow3(bddManager);
00178   }
00179   else {
00180     BddReorderSift(bddManager, bddManager->maxSiftingGrowth);
00181   }
00182   BddReallocateNodes(bddManager);
00183   BddConvertDataStructBack(bddManager);
00184 #ifdef _CAL_QUANTIFY_
00185   quantify_stop_recording_data();
00186 #endif
00187   nodeManager->numPages = 0; /* Since these pages have already been
00188                                 freed */
00189   CalNodeManagerQuit(nodeManager);
00190   Cal_Assert(CalCheckAllValidity(bddManager));
00191   Cal_MemFree(bddManager->interact);
00192   bddManager->numReorderings++;
00193 }

EXTERN void CalBddReorderBlockSift	(	Cal_BddManager_t *	bddManager,
		double	maxSizeFactor
	)

EXTERN void CalBddReorderBlockWindow	(	Cal_BddManager	bddManager,
		Cal_Block	block,
		char *	levels
	)

EXTERN void CalBddReorderFixCofactors	(	Cal_BddManager	bddManager,
		Cal_BddId_t	id
	)

Function********************************************************************

Synopsis [Fixes the cofactors of the nodes belonging to the given index.]

Description [This routine traverses the unique table and for each node, looks at the then and else cofactors. If needed fixes the cofactors.]

SideEffects [required]

SeeAlso [optional]

Definition at line 528 of file calReorderUtil.c.

00529 {
00530   CalHashTable_t *uniqueTableForId =
00531       bddManager->uniqueTable[id];
00532   CalBddNode_t *bddNode, *nextBddNode, **bins, *thenBddNode, *elseBddNode;
00533   Cal_Bdd_t f0, f1;
00534   long numBins;
00535   int i, rehashFlag;
00536   
00537   numBins = uniqueTableForId->numBins;
00538   bins = uniqueTableForId->bins;
00539 
00540   for(i = 0; i < numBins; i++) {
00541     for(bddNode = bins[i];
00542         bddNode != Cal_Nil(CalBddNode_t);
00543         bddNode = nextBddNode) {
00544       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00545       /*
00546        * Process one bddNode at a time
00547        */
00548       /*
00549       ** Because we have kept all the forwarding nodes in the list,
00550       ** this should not be a forwarding node.
00551       */
00552       Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00553       Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
00554       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00555       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00556       rehashFlag = 0;
00557       CalBddNodeGetThenBdd(bddNode, f1);
00558       CalBddNodeGetElseBdd(bddNode, f0);
00559       if (CalBddIsForwarded(f1)) {
00560         CalBddForward(f1);
00561         CalBddNodePutThenBdd(bddNode, f1);
00562         rehashFlag = 1;
00563       }
00564       Cal_Assert(CalBddIsForwarded(f1) == 0);
00565       if (CalBddIsForwarded(f0)) {
00566         CalBddForward(f0);
00567         CalBddNodePutElseBdd(bddNode, f0); 
00568         rehashFlag = 1;
00569       }
00570       Cal_Assert(CalBddIsForwarded(f0) == 0);
00571       /* Rehash if necessary */
00572       if (rehashFlag) {
00573         CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode, thenBddNode,
00574                                       elseBddNode);
00575       }
00576     }
00577   }
00578 }

EXTERN void CalBddReorderFixProvisionalNodes ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 404 of file calPipeline.c.

00405 {
00406   CalRequestNode_t **requestNodeListArray =
00407       bddManager->requestNodeListArray;
00408   CalRequestNode_t *node, *nextNode;
00409   int i;
00410   Cal_Bdd_t thenBdd, elseBdd;
00411   
00412   for (i=0;
00413        i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00414        i++){ 
00415     for (node = *requestNodeListArray; node; node = nextNode){
00416       nextNode = CalBddNodeGetNextBddNode(node);
00417       Cal_Assert(CalBddNodeIsForwarded(node));
00418       CalBddNodeGetThenBdd(node, thenBdd);
00419       if (CalBddIsForwarded(thenBdd)) {
00420         CalBddForward(thenBdd);
00421       }
00422       CalBddNodePutThenBdd(node, thenBdd);
00423       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00424     }
00425     requestNodeListArray++;
00426   }
00427   for (; i<bddManager->pipelineDepth; i++){
00428     for (node = *requestNodeListArray; node; node = nextNode){
00429       nextNode = CalBddNodeGetNextBddNode(node);
00430       Cal_Assert(CalBddNodeIsForwarded(node) == 0);
00431       CalBddNodeGetThenBdd(node, thenBdd);
00432       if (CalBddIsForwarded(thenBdd)) {
00433         CalBddForward(thenBdd);
00434       }
00435       CalBddNodePutThenBdd(node, thenBdd);
00436       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00437       CalBddNodeGetElseBdd(node, elseBdd);
00438       if (CalBddIsForwarded(elseBdd)) {
00439         CalBddForward(elseBdd);
00440       }
00441       CalBddNodePutElseBdd(node, elseBdd);
00442       Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00443     }
00444     requestNodeListArray++;
00445   }
00446 }

EXTERN void CalBddReorderFixUserBddPtrs ( Cal_BddManager bddManager )

CFile***********************************************************************

FileName [calReorderUtil.c]

PackageName [cal]

Synopsis [Some utility routines used by both breadth-first and depth-first reordering techniques.]

Description []

SeeAlso [optional]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calReorderUtil.c,v 1.3 2002/09/22 00:37:04 fabio Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 88 of file calReorderUtil.c.

00089 {
00090   CalHashTable_t *userBddUniqueTable = bddManager->uniqueTable[0];
00091   int i;
00092   int numBins;
00093   int rehashFlag;
00094   CalBddNode_t **bins;
00095   CalBddNode_t *bddNode;
00096   CalBddNode_t *nextBddNode;
00097   CalBddNode_t *thenBddNode;
00098   CalBddNode_t *elseBddNode;
00099   Cal_Bdd_t internalBdd;
00100 
00101   numBins = userBddUniqueTable->numBins;
00102   bins = userBddUniqueTable->bins;
00103 
00104   for(i = 0; i < numBins; i++) {
00105     for(bddNode = bins[i];
00106         bddNode != Cal_Nil(CalBddNode_t);
00107         bddNode = nextBddNode) {
00108       /*
00109        * Process one bddNode at a time
00110        */
00111       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00112       rehashFlag = 0;
00113 
00114       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00115       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00116       CalBddNodeGetThenBdd(bddNode, internalBdd);
00117       if (CalBddIsForwarded(internalBdd)) {
00118         CalBddForward(internalBdd);
00119         CalBddNodePutThenBdd(bddNode, internalBdd);
00120         rehashFlag = 1;
00121       }
00122       Cal_Assert(CalBddIsForwarded(internalBdd) == 0);
00123       /*Cal_Assert(!CalBddIsRefCountZero(internalBdd));*/
00124       /*
00125        * Rehash if necessary
00126        */
00127       if (rehashFlag) {
00128         CalUniqueTableForIdRehashNode(userBddUniqueTable, bddNode,
00129                                       thenBddNode, elseBddNode);
00130       }
00131     }
00132   }
00133 }

EXTERN void CalBddReorderReclaimForwardedNodes	(	Cal_BddManager	bddManager,
		int	startIndex,
		int	endIndex
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 592 of file calReorderUtil.c.

00594 {
00595   Cal_BddIndex_t index;
00596   Cal_BddId_t id;
00597   CalHashTable_t *uniqueTableForId;
00598   CalNodeManager_t *nodeManager;
00599   
00600   for(index = startIndex; index <= endIndex; index++){
00601     id = bddManager->indexToId[index];
00602     uniqueTableForId = bddManager->uniqueTable[id];
00603     nodeManager = uniqueTableForId->nodeManager;
00604     uniqueTableForId->endNode->nextBddNode = nodeManager->freeNodeList;
00605     nodeManager->freeNodeList = uniqueTableForId->startNode.nextBddNode;
00606     uniqueTableForId->endNode = &(uniqueTableForId->startNode);
00607     uniqueTableForId->startNode.nextBddNode = NULL;
00608   }
00609   bddManager->numForwardedNodes = 0;
00610 }

EXTERN void CalBddReorderVarSift	(	Cal_BddManager	bddManager,
		double	maxSizeFactor
	)

EXTERN void CalBddReorderVarWindow	(	Cal_BddManager	bddManager,
		char *	levels
	)

EXTERN Cal_Block CalBddShiftBlock	(	Cal_BddManager_t *	bddManager,
		Cal_Block	b,
		long	index
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 207 of file calBlk.c.

00208 {
00209   long i, j;
00210   Cal_Block p;
00211 
00212   if (b->firstIndex >= index) {
00213     CalBddBlockDelta(b, 1l);
00214     return (b);
00215   }
00216   if (b->lastIndex < index) return (b);
00217   b->lastIndex++;
00218   i = CalBddFindBlock(b, index);
00219   if (i == b->numChildren || b->children[i]->firstIndex == index) {
00220     b->children = (Cal_Block *)
00221         Cal_MemRealloc(Cal_Block, b->children, b->numChildren+1);
00222     for (j = b->numChildren-1; j >= i; --j){
00223       b->children[j+1] = CalBddShiftBlock(bddManager, b->children[j], index);
00224     }
00225     b->numChildren++;
00226     /*p = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/
00227     p = Cal_MemAlloc(Cal_Block_t, 1);
00228     p->reorderable = 0;
00229     p->firstIndex = index;
00230     p->lastIndex = index;
00231     p->numChildren = 0;
00232     p->children = 0;
00233     b->children[i] = p;
00234   }
00235   else{
00236     while (i < b->numChildren) {
00237       CalBddShiftBlock(bddManager, b->children[i], index);
00238       ++i;
00239     }
00240   }
00241   return (b);
00242 }

EXTERN int CalBddTypeAux	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f
	)

Function********************************************************************

Synopsis [Returns the BDD type by recursively traversing the argument BDD]

Description [Returns the BDD type by recursively traversing the argument BDD]

SideEffects [None]

Definition at line 904 of file cal.c.

00905 {
00906   Cal_Bdd_t thenBdd, elseBdd;
00907   
00908   if (CalBddIsBddConst(f)){
00909     if (CalBddIsBddZero(bddManager, f)) return (CAL_BDD_TYPE_ZERO);
00910     if (CalBddIsBddOne(bddManager, f)) return (CAL_BDD_TYPE_ONE);
00911   }
00912   CalBddGetThenBdd(f, thenBdd);
00913   CalBddGetElseBdd(f, elseBdd);
00914   if (CalBddIsBddOne(bddManager, thenBdd) &&
00915       CalBddIsBddZero(bddManager, elseBdd))
00916     return CAL_BDD_TYPE_POSVAR;
00917   if (CalBddIsBddZero(bddManager, thenBdd) &&
00918       CalBddIsBddOne(bddManager, elseBdd))
00919     return (CAL_BDD_TYPE_NEGVAR);
00920   return (CAL_BDD_TYPE_NONTERMINAL);
00921 }

EXTERN unsigned long CalBddUniqueTableNumLockedNodes	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	uniqueTableForId
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 617 of file calHashTable.c.

00619 {
00620   CalBddNode_t *bddNode;
00621   long i;
00622   unsigned long numLockedNodes = 0;
00623   
00624   for(i=0; i<uniqueTableForId->numBins; i++){
00625     bddNode = uniqueTableForId->bins[i];
00626     while (bddNode){
00627       numLockedNodes += CalBddNodeIsRefCountMax(bddNode);
00628       bddNode = CalBddNodeGetNextBddNode(bddNode);
00629     }
00630   }
00631   return numLockedNodes;
00632 }

EXTERN char* CalBddVarName	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	v,
		Cal_VarNamingFn_t	VarNamingFn,
		Cal_Pointer_t	env
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 144 of file calPrint.c.

00146 {
00147   char *name;
00148   if (VarNamingFn){
00149     Cal_Bdd userV = CalBddGetExternalBdd(bddManager, v);
00150     name = (*VarNamingFn)(bddManager, userV, env);
00151     Cal_BddFree(bddManager, userV);
00152   }
00153  else
00154    name=0;
00155   if (!name){
00156     sprintf(defaultVarName, "var.%d", CalBddGetBddIndex(bddManager, v));
00157     name = defaultVarName;
00158   }
00159   return (name);
00160 }

EXTERN Cal_Bdd_t CalBddVarSubstitute	(	Cal_BddManager	bddManager,
		Cal_Bdd_t	f,
		unsigned short	opCode,
		CalAssociation_t *	assoc
	)

Function********************************************************************

Synopsis [Substitute a set of variables by functions]

Description [Returns a BDD for f using the substitution defined by current variable association. Each variable is replaced by its associated BDDs. The substitution is effective simultaneously]

SideEffects [None]

SeeAlso [Cal_BddCompose]

Definition at line 143 of file calBddVarSubstitute.c.

00145 {
00146   CalRequest_t result;
00147   int bddId, bddIndex, lastIndex;
00148   CalHashTable_t *hashTable;
00149   CalHashTable_t *uniqueTableForId;
00150   CalHashTable_t **reqQueForSubstitute = bddManager->reqQue[0];
00151   CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
00152   Cal_BddId_t fId = CalBddGetBddId(f);
00153   /*Cal_BddIndex_t fIndex = bddManager->idToIndex[fId];*/
00154   int fIndex = bddManager->idToIndex[fId];
00155   
00156   if (CalOpBddVarSubstitute(bddManager, f, &result)){
00157     return result;
00158   }
00159 
00160   if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
00161     return result;
00162   }
00163   CalHashTableFindOrAdd(reqQueForSubstitute[fId], f, 
00164     bddManager->bddNull, &result);
00165 
00166   /* ReqQueApply */
00167   lastIndex = assoc->lastBddIndex;
00168   for(bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
00169     bddId = bddManager->indexToId[bddIndex];
00170     hashTable = reqQueForSubstitute[bddId];
00171     if(hashTable->numEntries){
00172       CalHashTableSubstituteApply(bddManager, hashTable, lastIndex, 
00173                                   reqQueForSubstitute, opCode);
00174     }
00175   }
00176 
00177   /* ReqQueReduce */
00178   for(bddIndex = bddManager->numVars - 1; bddIndex >= fIndex; bddIndex--){
00179     bddId = bddManager->indexToId[bddIndex];
00180     uniqueTableForId = bddManager->uniqueTable[bddId];
00181     hashTable = reqQueForSubstitute[bddId];
00182     if(hashTable->numEntries){
00183       CalHashTableSubstituteReduce(bddManager, hashTable,
00184                                    reqQueForITE, uniqueTableForId,
00185                                    opCode); 
00186     }
00187   }
00188 
00189   CalRequestIsForwardedTo(result);
00190 
00191   /* ReqQueCleanUp */
00192   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00193     CalHashTableCleanUp(reqQueForSubstitute[bddId]);
00194   }
00195   CalCacheTableTwoFixResultPointers(bddManager);
00196   CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
00197   return result;
00198 }

EXTERN void CalBddWarningMessage ( char * string )

Function********************************************************************

Name [CalBddWarningMessage]

Synopsis [Prints warning message.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 444 of file calUtil.c.

00445 {
00446   (void) fprintf(stderr,"Warning: %s\n", string);
00447 }

EXTERN unsigned long CalBlockMemoryConsumption ( Cal_Block block )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 255 of file calBlk.c.

00256 {
00257   unsigned long totalBytes = 0;
00258   int i;
00259   
00260   totalBytes += sizeof(Cal_Block);
00261   for (i=0; i<block->numChildren; i++){
00262     totalBytes += CalBlockMemoryConsumption(block->children[i]);
00263   }
00264   return totalBytes;
00265 }

EXTERN unsigned long CalCacheTableMemoryConsumption ( CalCacheTable_t * cacheTable )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 582 of file calCacheTableTwo.c.

00583 {
00584   return (unsigned long) (sizeof(cacheTable)+cacheTable->numBins*sizeof(CacheEntry_t));
00585 }

EXTERN void CalCacheTablePrint ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 483 of file calCacheTableTwo.c.

00484 {
00485   CacheTablePrint(bddManager->cacheTable);
00486 }

EXTERN void CalCacheTableRehash ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 529 of file calCacheTableTwo.c.

00530 {
00531   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00532   if((3*cacheTable->numBins < cacheTable->cacheRatio*cacheTable->numEntries) &&
00533      (32*cacheTable->numBins <
00534       8*(bddManager->numNodes))){
00535     CacheTableTwoRehash(cacheTable, 1);
00536   }
00537 }

EXTERN void CalCacheTableTwoFixResultPointers ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 452 of file calCacheTableTwo.c.

00453 {
00454   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00455   int i;
00456   CacheEntry_t *bin = cacheTable->bins;
00457   int numBins = cacheTable->numBins;
00458   
00459   for (i=0; i<numBins; bin++,i++){
00460     if ((CalAddress_t)bin->operand1 & 0x2){ /* If the result node is temporary
00461                                    node */
00462       CacheResultNodeIsForwardedTo(bin->resultBddNode, bin->resultBddId);
00463       bin->operand1 = (CalBddNode_t *)((CalAddress_t)bin->operand1 &
00464                                        ~0x2); /* It is no longer temporary */
00465     }
00466   }
00467 }

EXTERN void CalCacheTableTwoFlush ( CalCacheTable_t * cacheTable )

Function********************************************************************

Synopsis [Free a Cache table along with the associated storage.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 317 of file calCacheTableTwo.c.

00318 {
00319   memset((char *)cacheTable->bins, 0,
00320          cacheTable->numBins*sizeof(CacheEntry_t));
00321   cacheTable->numEntries = 0;
00322 }

EXTERN int CalCacheTableTwoFlushAll ( CalCacheTable_t * cacheTable )

Function********************************************************************

Synopsis [Free a Cache table along with the associated storage.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 336 of file calCacheTableTwo.c.

00337 {
00338   CalCacheTableTwoFlush(cacheTable);
00339   cacheTable->numInsertions = 0;
00340   cacheTable->numCollisions = 0;
00341   cacheTable->numLookups = 0;
00342   cacheTable->numHits = 0;
00343   return 0;
00344 }

EXTERN void CalCacheTableTwoFlushAssociationId	(	Cal_BddManager_t *	bddManager,
		int	associationId
	)

Function********************************************************************

Synopsis [Flushes the entries from the cache which correspond to the given associationId.]

Description []

SideEffects [Cache entries are affected.]

SeeAlso []

Definition at line 551 of file calCacheTableTwo.c.

00553 {
00554   CalCacheTable_t *cacheTable =   bddManager->cacheTable;
00555   int i;
00556   CacheEntry_t *bin;
00557   
00558   for (i=0; i < cacheTable->numBins; i++){
00559     bin = cacheTable->bins+i;
00560     if ((bin->opCode == (CAL_OP_QUANT+associationId)) ||
00561         (bin->opCode == (CAL_OP_REL_PROD+associationId)) ||
00562         (bin->opCode == (CAL_OP_VAR_SUBSTITUTE+associationId))){
00563       /* This entry needs to be freed */
00564       cacheTable->numEntries--;
00565       memset((char *)bin, 0, sizeof(CacheEntry_t));
00566     }
00567   }
00568 }

EXTERN void CalCacheTableTwoGCFlush ( CalCacheTable_t * cacheTable )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 357 of file calCacheTableTwo.c.

00358 {
00359   int i;
00360   CacheEntry_t *bin = cacheTable->bins;
00361   int numBins = cacheTable->numBins;
00362   if (cacheTable->numEntries == 0) return;
00363   for (i=0; i<numBins; bin++,i++){
00364     if (bin->opCode != CAL_OP_INVALID){
00365       if (CalBddNodeIsMarked((CAL_BDD_POINTER(bin->operand1))) ||
00366           CalBddNodeIsMarked((CAL_BDD_POINTER(bin->operand2))) ||
00367           CalBddNodeIsMarked((CAL_BDD_POINTER(bin->resultBddNode)))){
00368         /* This entry needs to be freed */
00369         cacheTable->numEntries--;
00370         memset((char *)bin, 0, sizeof(CacheEntry_t));
00371       }
00372     }
00373   }
00374 }

EXTERN CalCacheTable_t* CalCacheTableTwoInit ( Cal_BddManager_t * bddManager )

AutomaticEnd Function********************************************************************

Synopsis [Initialize a Cache table using default parameters.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 148 of file calCacheTableTwo.c.

00149 {
00150   CalCacheTable_t  *cacheTable;
00151   cacheTable = Cal_MemAlloc(CalCacheTable_t, 1);
00152   if (cacheTable == Cal_Nil(CalCacheTable_t)){
00153     CalBddFatalMessage("out of memory");
00154   }
00155   cacheTable->sizeIndex = CACHE_TABLE_DEFAULT_SIZE_INDEX;
00156   cacheTable->numBins = TABLE_SIZE(cacheTable->sizeIndex);
00157   cacheTable->cacheRatio = CACHE_TABLE_DEFAULT_CACHE_RATIO;
00158   cacheTable->bins = Cal_MemAlloc(CacheEntry_t, cacheTable->numBins);
00159   if(cacheTable->bins == Cal_Nil(CacheEntry_t)){
00160     CalBddFatalMessage("out of memory");
00161   }             
00162   memset((char *)cacheTable->bins, 0,
00163          cacheTable->numBins*sizeof(CacheEntry_t));
00164   cacheTable->numInsertions = 0;
00165   cacheTable->numEntries = 0;
00166   cacheTable->numHits = 0;
00167   cacheTable->numLookups = 0;
00168   cacheTable->numCollisions = 0;
00169   return cacheTable;
00170 }

EXTERN void CalCacheTableTwoInsert	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t	g,
		Cal_Bdd_t	result,
		unsigned long	opCode,
		int	cacheLevel
	)

Function********************************************************************

Synopsis [Directly insert a BDD node in the Cache table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 206 of file calCacheTableTwo.c.

00209 {
00210   int hashValue;
00211   CalCacheTable_t *cacheTable;
00212   CacheEntry_t *bin;
00213   CalBddNode_t *operand1Node, *operand2Node;
00214 
00215   cacheTable = bddManager->cacheTable;
00216   cacheTable->numInsertions++;
00217   hashValue = CacheTableTwoDoHash(cacheTable, CalBddGetBddNode(f),
00218                                   CalBddGetBddNode(g), opCode); 
00219 
00220   bin = cacheTable->bins + hashValue;
00221   if (bin->opCode != CAL_OP_INVALID){
00222     cacheTable->numCollisions++;
00223   }
00224   else{
00225     cacheTable->numEntries++;
00226   }
00227   
00228   bin->opCode = opCode;
00229   if ((CalAddress_t)CalBddGetBddNode(f) >
00230       (CalAddress_t)CalBddGetBddNode(g)){ 
00231     operand1Node = CalBddGetBddNode(g);
00232     operand2Node = CalBddGetBddNode(f);
00233   }
00234   else{
00235     operand1Node = CalBddGetBddNode(f);
00236     operand2Node = CalBddGetBddNode(g);
00237   }
00238   
00239   if (cacheLevel){
00240   /*
00241    * Mark this result as temporary node to be forwarded at the end of
00242    * operation. The reason we can use this tagging is because the
00243    * size of the structure is 16 bytes and we are requiring 8 or 16 byte
00244    * alignment (at least last 3 bits should be zero).
00245    */
00246     bin->operand1 = (CalBddNode_t *) (((CalAddress_t)operand1Node) | 0x2);
00247   }
00248   else {
00249     bin->operand1 = operand1Node;
00250   }
00251   bin->operand2 = operand2Node;
00252   bin->resultBddNode = CalBddGetBddNode(result);
00253   bin->resultBddId = CalBddGetBddId(result);
00254   return;
00255 }

EXTERN int CalCacheTableTwoLookup	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t	g,
		unsigned long	opCode,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 270 of file calCacheTableTwo.c.

00273 {
00274   int hashValue;
00275   CalCacheTable_t *cacheTable;
00276   CacheEntry_t *bin;
00277   CalBddNode_t *operand1Node, *operand2Node;
00278   
00279   cacheTable = bddManager->cacheTable;
00280   cacheTable->numLookups++;
00281   hashValue = CacheTableTwoDoHash(cacheTable, CalBddGetBddNode(f),
00282                                   CalBddGetBddNode(g), opCode); 
00283 
00284   bin = cacheTable->bins+hashValue;
00285   
00286   if ((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g)){
00287     operand1Node = CalBddGetBddNode(g);
00288     operand2Node = CalBddGetBddNode(f);
00289   }
00290   else{
00291     operand1Node = CalBddGetBddNode(f);
00292     operand2Node = CalBddGetBddNode(g);
00293   }
00294   if (CacheTableTwoCompareCacheEntry(bin, operand1Node, operand2Node,
00295                                      opCode)){
00296     CalBddPutBddId((*resultBddPtr), bin->resultBddId);
00297     CalBddPutBddNode((*resultBddPtr), bin->resultBddNode);
00298     cacheTable->numHits++;
00299     return 1;
00300   }
00301   *resultBddPtr = bddManager->bddNull;
00302   return 0;
00303 }

EXTERN int CalCacheTableTwoQuit ( CalCacheTable_t * cacheTable )

Function********************************************************************

Synopsis [Free a Cache table along with the associated storage.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 185 of file calCacheTableTwo.c.

00186 {
00187   if(cacheTable == Cal_Nil(CalCacheTable_t))return 1;
00188   Cal_MemFree(cacheTable->bins);
00189   Cal_MemFree(cacheTable);
00190   return 0;
00191 }

EXTERN void CalCacheTableTwoRepackUpdate ( CalCacheTable_t * cacheTable )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 388 of file calCacheTableTwo.c.

00389 {
00390   int i;
00391   CacheEntry_t *bin = cacheTable->bins;
00392   int numBins = cacheTable->numBins;
00393   
00394   for (i=0; i<numBins; bin++,i++){
00395     if (bin->opCode != CAL_OP_INVALID){
00396       if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand1))){
00397         CalBddNodeForward(bin->operand1);
00398       }
00399       if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand2))){
00400         CalBddNodeForward(bin->operand2);
00401       }
00402       if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->resultBddNode))){
00403         CalBddNodeForward(bin->resultBddNode);
00404       }
00405     }
00406   }
00407 }

EXTERN int CalCheckAllValidity ( Cal_BddManager bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 147 of file calReorderUtil.c.

00148 {
00149   int id;
00150   for(id = 0; id <= bddManager->numVars; id++){
00151     CalCheckValidityOfNodesForId(bddManager, id);
00152   }
00153   CalCheckAssociationValidity(bddManager);
00154   if (bddManager->pipelineState == CREATE){
00155     CalCheckPipelineValidity(bddManager);
00156   }
00157   CalCheckRefCountValidity(bddManager);
00158   CalCheckCacheTableValidity(bddManager);
00159   return 1;
00160 }

EXTERN int CalCheckAssoc ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 447 of file calReorderUtil.c.

00448 {
00449   CalAssociation_t *assoc, *nextAssoc;
00450   int i;
00451   int expectedLastBddIndex, bddIndex;
00452 
00453   for(assoc = bddManager->associationList;
00454       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00455     nextAssoc = assoc->next;
00456     expectedLastBddIndex = -1;
00457     for (i=1; i <= bddManager->numVars; i++){
00458       if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
00459         bddIndex = bddManager->idToIndex[i];
00460         if (expectedLastBddIndex < bddIndex){
00461           expectedLastBddIndex = bddIndex;
00462         }
00463       }
00464     }
00465     Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
00466   }
00467   /* fix temporary association */
00468   assoc = bddManager->tempAssociation;
00469   expectedLastBddIndex = -1;
00470   for (i=1; i <= bddManager->numVars; i++){
00471     if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
00472       bddIndex = bddManager->idToIndex[i];
00473       if (expectedLastBddIndex < bddIndex){
00474         expectedLastBddIndex = bddIndex;
00475       }
00476     }
00477   }
00478   Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
00479   return 1;
00480 }

EXTERN void CalCheckAssociationValidity ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [Checks the validity of association.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 492 of file calAssociation.c.

00493 {
00494   CalAssociation_t *assoc, *nextAssoc;
00495   int i;
00496   
00497   for(assoc = bddManager->associationList;
00498       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00499     nextAssoc = assoc->next;
00500     for (i=1; i <= bddManager->numVars; i++){
00501       Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
00502     }
00503   }
00504   /* temporary association */
00505   assoc = bddManager->tempAssociation;
00506   for (i=1; i <= bddManager->numVars; i++){
00507     Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
00508   }
00509 }

EXTERN void CalCheckCacheTableValidity ( Cal_BddManager bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 421 of file calCacheTableTwo.c.

00422 {
00423   CalCacheTable_t *cacheTable = bddManager->cacheTable;
00424   int i;
00425   CacheEntry_t *bin = cacheTable->bins;
00426   int numBins = cacheTable->numBins;
00427   
00428   for (i=0; i<numBins; bin++,i++){
00429     if (bin->opCode != CAL_OP_INVALID){
00430       Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand1))
00431                  == 0);
00432       Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand2))
00433                  == 0);
00434       Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->resultBddNode))
00435                  == 0);
00436     }
00437   }
00438 }

EXTERN void CalCheckPipelineValidity ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 460 of file calPipeline.c.

00461 {
00462   CalRequestNode_t **requestNodeListArray =
00463       bddManager->requestNodeListArray;
00464   CalRequestNode_t *node, *nextNode;
00465   int i;
00466   Cal_Bdd_t thenBdd, elseBdd;
00467   
00468   for (i=0;
00469        i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00470        i++){ 
00471     for (node = *requestNodeListArray; node; node = nextNode){
00472       nextNode = CalBddNodeGetNextBddNode(node);
00473       Cal_Assert(CalBddNodeIsForwarded(node));
00474       CalBddNodeGetThenBdd(node, thenBdd);
00475       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00476     }
00477     requestNodeListArray++;
00478   }
00479   for (; i<bddManager->pipelineDepth; i++){
00480     for (node = *requestNodeListArray; node; node = nextNode){
00481       nextNode = CalBddNodeGetNextBddNode(node);
00482       Cal_Assert(CalBddNodeIsForwarded(node) == 0); 
00483       CalBddNodeGetThenBdd(node, thenBdd);
00484       /*Cal_Assert(CalBddIsForwarded(thenBdd) == 0);*/
00485       /* This is possible since the actual BDD of thenBdd could have been
00486          computed and it is forwarded, however this node is not yet
00487          updated with the result */
00488       CalBddNodeGetElseBdd(node, elseBdd);
00489       /*Cal_Assert(CalBddIsForwarded(elseBdd) == 0);*/
00490     }
00491     requestNodeListArray++;
00492   }
00493 }

EXTERN void CalCheckRefCountValidity ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 315 of file calReorderUtil.c.

00316 {
00317   int i, numBins, index;
00318   CalHashTable_t *uniqueTableForId;
00319   CalBddNode_t *bddNode, *nextBddNode;
00320   Cal_Bdd_t thenBdd, elseBdd, internalBdd;
00321   CalAssociation_t *assoc, *nextAssoc;
00322   
00323   /* First traverse the user BDDs */
00324   uniqueTableForId = bddManager->uniqueTable[0];
00325   numBins = uniqueTableForId->numBins;
00326   for (i = 0; i < numBins; i++){
00327     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00328          bddNode = nextBddNode){
00329       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00330       CalBddNodeGetThenBdd(bddNode, internalBdd);
00331       CalBddDcrRefCount(internalBdd);
00332     }
00333   }
00334       /* Traverse the associations */
00335   
00336   for(assoc = bddManager->associationList;
00337       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00338     nextAssoc = assoc->next;
00339     for (i=1; i <= bddManager->numVars; i++){
00340         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00341             CalBddDcrRefCount(assoc->varAssociation[i]);
00342         }
00343     }
00344   }
00345   /* temporary association */
00346   assoc = bddManager->tempAssociation;
00347   for (i=1; i <= bddManager->numVars; i++){
00348       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00349           CalBddDcrRefCount(assoc->varAssociation[i]);
00350       }
00351   }
00352 
00353   
00354   /* Now traverse all the nodes in order */
00355   for (index = 0; index < bddManager->numVars; index++){
00356     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00357     numBins = uniqueTableForId->numBins;
00358     for (i = 0; i < numBins; i++){
00359       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00360            bddNode = nextBddNode){
00361         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00362         CalBddNodeGetThenBdd(bddNode, thenBdd);
00363         CalBddNodeGetElseBdd(bddNode, elseBdd);
00364         CalBddDcrRefCount(thenBdd);
00365         CalBddDcrRefCount(elseBdd);
00366       }
00367     }
00368   }
00369 
00370   /* All the reference count must be zero  or max */
00371   for (index = 0; index < bddManager->numVars; index++){
00372     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00373     numBins = uniqueTableForId->numBins;
00374     for (i = 0; i < numBins; i++){
00375       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00376            bddNode = nextBddNode){
00377         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00378         /* If the pipeline execution is going on, the following
00379            assertion will not hold */
00380         if (bddManager->pipelineState != CREATE){
00381           Cal_Assert(CalBddNodeIsRefCountZero(bddNode) ||
00382                      CalBddNodeIsRefCountMax(bddNode));
00383         }
00384       }
00385     }
00386   }
00387 
00388   /* Put back the ref count */
00389   /* traverse all the nodes in order */
00390   for (index = 0; index < bddManager->numVars; index++){
00391     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00392     numBins = uniqueTableForId->numBins;
00393     for (i = 0; i < numBins; i++){
00394       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00395            bddNode = nextBddNode){
00396         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00397         CalBddNodeGetThenBdd(bddNode, thenBdd);
00398         CalBddNodeGetElseBdd(bddNode, elseBdd);
00399         CalBddIcrRefCount(thenBdd);
00400         CalBddIcrRefCount(elseBdd);
00401       }
00402     }
00403   }
00404       /* Traverse the associations */
00405   for(assoc = bddManager->associationList;
00406       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00407     nextAssoc = assoc->next;
00408     for (i=1; i <= bddManager->numVars; i++){
00409         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00410             CalBddIcrRefCount(assoc->varAssociation[i]);
00411         }
00412     }
00413   }
00414   /* temporary association */
00415   assoc = bddManager->tempAssociation;
00416   for (i=1; i <= bddManager->numVars; i++){
00417       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00418           CalBddIcrRefCount(assoc->varAssociation[i]);
00419       }
00420   }
00421 
00422   /* Traverse the user BDDs */
00423   uniqueTableForId = bddManager->uniqueTable[0];
00424   numBins = uniqueTableForId->numBins;
00425   for (i = 0; i < numBins; i++){
00426     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00427          bddNode = nextBddNode){
00428       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00429       CalBddNodeGetThenBdd(bddNode, internalBdd);
00430       CalBddIcrRefCount(internalBdd);
00431     }
00432   }
00433 }

EXTERN int CalCheckValidityOfANode	(	Cal_BddManager_t *	bddManager,
		CalBddNode_t *	bddNode,
		int	id
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 263 of file calReorderUtil.c.

00265 {
00266   Cal_Bdd_t thenBdd, elseBdd, thenBdd_, elseBdd_, bdd;
00267   if (id != 0){
00268     /* id = 0 corresponds to the constants and the user BDDs */
00269     Cal_Assert(bddManager->idToIndex[id] <
00270                bddManager->idToIndex[bddNode->thenBddId]);   
00271     Cal_Assert(bddManager->idToIndex[id] < 
00272                bddManager->idToIndex[bddNode->elseBddId]);
00273   }
00274   Cal_Assert(!CalBddNodeIsForwarded(bddNode));
00275   Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
00276   CalBddNodeGetThenBdd(bddNode, thenBdd);
00277   CalBddNodeGetElseBdd(bddNode, elseBdd);
00278   Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00279   Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00280   Cal_Assert(!CalBddIsRefCountZero(thenBdd));
00281   Cal_Assert(!CalBddIsRefCountZero(elseBdd));
00282   /* Make sure that the then and else bdd nodes are part of the
00283      respective unique tables */
00284   if (bddNode->thenBddId != 0){
00285     CalBddGetThenBdd(thenBdd, thenBdd_);
00286     CalBddGetElseBdd(thenBdd, elseBdd_);
00287     Cal_Assert(
00288       CalUniqueTableForIdLookup(bddManager,
00289                                 bddManager->uniqueTable[bddNode->thenBddId],  
00290                                 thenBdd_, elseBdd_, &bdd));
00291   }
00292   if (bddNode->elseBddId != 0){
00293     CalBddGetThenBdd(elseBdd, thenBdd_);
00294     CalBddGetElseBdd(elseBdd, elseBdd_);
00295     Cal_Assert(
00296       CalUniqueTableForIdLookup(bddManager,
00297                                 bddManager->uniqueTable[bddNode->elseBddId],
00298                                 thenBdd_, elseBdd_, &bdd));
00299   }
00300   return 1;
00301 }

EXTERN int CalCheckValidityOfNodesForId	(	Cal_BddManager	bddManager,
		int	id
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 175 of file calReorderUtil.c.

00176 {
00177   int i, numBins;
00178   CalHashTable_t *uniqueTableForId;
00179   CalBddNode_t *bddNode, *nextBddNode;
00180   Cal_Bdd_t thenBdd, elseBdd;
00181   
00182   uniqueTableForId = bddManager->uniqueTable[id];
00183   Cal_Assert(uniqueTableForId->startNode.nextBddNode == NULL);
00184   numBins = uniqueTableForId->numBins;
00185   for (i = 0; i < numBins; i++){
00186     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00187          bddNode = nextBddNode){
00188       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00189       CalCheckValidityOfANode(bddManager, bddNode, id);
00190       CalBddNodeGetThenBdd(bddNode, thenBdd);
00191       CalBddNodeGetElseBdd(bddNode, elseBdd);
00192       Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
00193                             CalBddGetBddNode(elseBdd), 
00194                             uniqueTableForId) == i);
00195     }
00196   }
00197   return 1;
00198 }

EXTERN int CalCheckValidityOfNodesForWindow	(	Cal_BddManager	bddManager,
		Cal_BddIndex_t	index,
		int	numLevels
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 213 of file calReorderUtil.c.

00215 {
00216   int i, numBins, j;
00217   CalHashTable_t *uniqueTableForId;
00218   CalBddNode_t *bddNode, *nextBddNode;
00219   Cal_Bdd_t thenBdd, elseBdd;
00220 
00221   for (i = 0; i < numLevels; i++){
00222     uniqueTableForId =
00223         bddManager->uniqueTable[bddManager->indexToId[index+i]]; 
00224     numBins = uniqueTableForId->numBins;
00225     for (j = 0; j < numBins; j++){
00226       for (bddNode = uniqueTableForId->bins[j]; bddNode;
00227            bddNode = nextBddNode){
00228         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00229         Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00230         CalBddNodeGetThenBdd(bddNode, thenBdd);
00231         CalBddNodeGetElseBdd(bddNode, elseBdd);
00232         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00233         Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00234         Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
00235                               CalBddGetBddNode(elseBdd), 
00236                              uniqueTableForId) == j);
00237       }
00238     }
00239     for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
00240          bddNode = nextBddNode){ 
00241       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00242       CalBddNodeGetThenBdd(bddNode, thenBdd);
00243       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00244     }
00245   }
00246   return 1;
00247 }

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
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 304 of file calBddCompose.c.

00311 {
00312   Cal_BddIndex_t index;
00313   Cal_BddId_t bddId;
00314 
00315   index = CalBddGetBddIndex(bddManager, f);
00316   if(index > composeIndex){
00317     *resultPtr = f;
00318   }
00319   else if(index < composeIndex){
00320     CalBddGetMinId2(bddManager, f, h, bddId);
00321     CalHashTableFindOrAdd(reqQueForCompose[bddId], f, h, resultPtr);
00322   }
00323   else{
00324     Cal_Bdd_t calBdd1, calBdd2, calBdd3;
00325     calBdd1 = h;
00326     CalBddGetThenBdd(f, calBdd2);
00327     CalBddGetElseBdd(f, calBdd3);
00328     *resultPtr = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
00329   }
00330 }

EXTERN int CalDecreasingOrderCompare	(	const void *	a,
		const void *	b
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 241 of file calPerformanceTest.c.

00242 {
00243   return (*(int *)a-*(int *)b);
00244 }

EXTERN void CalFixupAssoc	(	Cal_BddManager_t *	bddManager,
		long	id1,
		long	id2,
		CalAssociation_t *	assoc
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 494 of file calReorderUtil.c.

00496 {
00497   if (assoc->lastBddIndex == -1) return;
00498   /* Variable with id1 is moving down a spot. */
00499   if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1]) == 0)
00500       && (assoc->lastBddIndex == bddManager->idToIndex[id1])){
00501     assoc->lastBddIndex++;
00502   }
00503   else if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1])) &&
00504            (CalBddIsBddNull(bddManager, assoc->varAssociation[id2]) ==
00505             0) && 
00506   (assoc->lastBddIndex == bddManager->idToIndex[id2])){
00507     assoc->lastBddIndex--;
00508   }
00509   Cal_Assert((assoc->lastBddIndex >= 0) && (assoc->lastBddIndex <=
00510                                            CAL_BDD_CONST_INDEX));
00511    
00512 }

EXTERN void CalFreeBlockRecursively ( Cal_Block block )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 278 of file calBlk.c.

00279 {
00280   int i;
00281   
00282   for (i=0; i<block->numChildren; i++){
00283     CalFreeBlockRecursively(block->children[i]);
00284   }
00285   Cal_MemFree(block->children);
00286   Cal_MemFree(block);
00287 }

EXTERN void CalHashTableAddDirect	(	CalHashTable_t *	hashTable,
		CalBddNode_t *	bddNode
	)

Function********************************************************************

Synopsis [Directly insert a BDD node in the hash table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 174 of file calHashTable.c.

00175 {
00176   int hashValue;
00177   CalBddNode_t *thenBddNode, *elseBddNode;
00178 
00179   hashTable->numEntries++;
00180   if(hashTable->numEntries >= hashTable->maxCapacity){
00181     CalHashTableRehash(hashTable, 1);
00182   }
00183   thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00184   elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00185   hashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
00186   CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
00187   hashTable->bins[hashValue] = bddNode;
00188 }

EXTERN int CalHashTableAddDirectAux	(	CalHashTable_t *	hashTable,
		Cal_Bdd_t	thenBdd,
		Cal_Bdd_t	elseBdd,
		Cal_Bdd_t *	bddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 253 of file calHashTable.c.

00256 {
00257   CalBddNode_t *ptr;
00258   int hashValue;
00259   
00260   hashTable->numEntries++;
00261   if(hashTable->numEntries >= hashTable->maxCapacity){
00262     CalHashTableRehash(hashTable, 1);
00263   }
00264   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd), CalBddGetBddNode(elseBdd),
00265                          hashTable); 
00266   CalNodeManagerInitBddNode(hashTable->nodeManager, thenBdd, elseBdd, 
00267       hashTable->bins[hashValue], ptr);
00268   hashTable->bins[hashValue] = ptr;
00269   CalBddPutBddId(*bddPtr, hashTable->bddId);
00270   CalBddPutBddNode(*bddPtr, ptr);
00271   return 0;
00272 }

EXTERN void CalHashTableApply	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable,
		CalHashTable_t **	reqQueAtPipeDepth,
		CalOpProc_t	calOpProc
	)

CFile***********************************************************************

FileName [calApplyReduce.c]

PackageName [cal]

Synopsis [Generic routines for processing temporary nodes during "apply" and "reduce" phases.]

Description []

SeeAlso [optional]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calApplyReduce.c,v 1.1.1.3 1998/05/04 00:58:49 hsv Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 91 of file calApplyReduce.c.

00094 {
00095   int i, numBins;
00096   CalBddNode_t **bins = 0;
00097   CalRequestNode_t *requestNode;
00098   Cal_Bdd_t fx, gx, fxbar, gxbar, result;
00099   Cal_BddId_t bddId;
00100 
00101   numBins = hashTable->numBins;
00102   bins = hashTable->bins;
00103   for(i = 0; i < numBins; i++){
00104     for(requestNode = bins[i];
00105         requestNode != Cal_Nil(CalRequestNode_t);
00106         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00107       /* Process the requestNode */
00108       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
00109       Cal_Assert(((CalAddress_t)(fx.bddNode)) & ~0xf);
00110       Cal_Assert(((CalAddress_t)(gx.bddNode)) & ~0xf);
00111       Cal_Assert(((CalAddress_t)(fxbar.bddNode)) & ~0xf);
00112       Cal_Assert(((CalAddress_t)(gxbar.bddNode)) & ~0xf);
00113       if((*calOpProc)(bddManager, fx, gx, &result) == 0){
00114         CalBddNormalize(fx, gx);
00115         CalBddGetMinId2(bddManager, fx, gx, bddId);
00116         CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fx, gx, &result);
00117       }
00118       CalBddIcrRefCount(result);
00119       CalRequestNodePutThenRequest(requestNode, result);
00120       if((*calOpProc)(bddManager, fxbar, gxbar, &result) == 0){
00121         CalBddNormalize(fxbar, gxbar);
00122         CalBddGetMinId2(bddManager, fxbar, gxbar, bddId);
00123         CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fxbar, gxbar, &result);
00124       }
00125       CalBddIcrRefCount(result);
00126       CalRequestNodePutElseRequest(requestNode, result);
00127     }
00128   }
00129 }

EXTERN void CalHashTableCleanUp ( CalHashTable_t * hashTable )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 286 of file calHashTable.c.

00287 {
00288   CalNodeManager_t *nodeManager;
00289 
00290   nodeManager = hashTable->nodeManager;
00291   hashTable->endNode->nextBddNode = nodeManager->freeNodeList;
00292   nodeManager->freeNodeList = hashTable->startNode.nextBddNode;
00293   hashTable->endNode = &(hashTable->startNode);
00294   hashTable->numEntries = 0;
00295   hashTable->startNode.nextBddNode = NULL;
00296   Cal_Assert(!(hashTable->requestNodeList));
00297   hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
00298   return;
00299 }

EXTERN void CalHashTableComposeApply	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable,
		Cal_BddIndex_t	gIndex,
		CalHashTable_t **	reqQueForCompose,
		CalHashTable_t **	reqQueForITE
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 219 of file calBddCompose.c.

00224 {
00225   int i, numBins = hashTable->numBins;
00226   CalBddNode_t **bins = hashTable->bins;
00227   CalRequestNode_t *requestNode;
00228   Cal_Bdd_t fx, fxbar;
00229   Cal_Bdd_t hx, hxbar;
00230   Cal_Bdd_t calBdd1, calBdd2, calBdd3;
00231   Cal_Bdd_t result;
00232   Cal_BddId_t bddId;
00233   Cal_BddIndex_t index;
00234   
00235   for(i = 0; i < numBins; i++){
00236     for(requestNode = bins[i];
00237         requestNode != Cal_Nil(CalRequestNode_t);
00238         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00239 
00240       /* Process the requestNode */
00241       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, hx, hxbar);
00242 
00243       /* Process left cofactor */
00244       index = CalBddGetBddIndex(bddManager, fx);
00245       if(index > gIndex){
00246         CalBddIcrRefCount(fx);
00247         CalRequestNodePutThenRequest(requestNode, fx);
00248       }
00249       else if(index < gIndex){
00250         CalBddGetMinId2(bddManager, fx, hx, bddId);
00251         CalHashTableFindOrAdd(reqQueForCompose[bddId], fx, hx, &result);
00252         CalBddIcrRefCount(result);
00253         CalRequestNodePutThenRequest(requestNode, result);
00254       }
00255       else{
00256         /* fxIndex == gIndex */
00257         /* RequestNodeThen = ITE(hx, fxThen, fxElse) */
00258         calBdd1 = hx;
00259         CalBddGetThenBdd(fx, calBdd2);
00260         CalBddGetElseBdd(fx, calBdd3);
00261         result = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
00262         CalBddIcrRefCount(result);
00263         CalRequestNodePutThenRequest(requestNode, result);
00264       }
00265 
00266       /* Process right cofactor */
00267       index = CalBddGetBddIndex(bddManager, fxbar);
00268       if(index > gIndex){
00269         CalBddIcrRefCount(fxbar);
00270         CalRequestNodePutElseRequest(requestNode, fxbar);
00271       }
00272       else if(index < gIndex){
00273         CalBddGetMinId2(bddManager, fxbar, hxbar, bddId);
00274         CalHashTableFindOrAdd(reqQueForCompose[bddId], fxbar, hxbar, &result);
00275         CalBddIcrRefCount(result);
00276         CalRequestNodePutElseRequest(requestNode, result);
00277       }
00278       else{
00279         /* fxbarIndex == gIndex */
00280         /* RequestNodeElse = ITE(hxbar, fxbarThen, fxbarElse) */
00281         calBdd1 = hxbar;
00282         CalBddGetThenBdd(fxbar, calBdd2);
00283         CalBddGetElseBdd(fxbar, calBdd3);
00284         result = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
00285         CalBddIcrRefCount(result);
00286         CalRequestNodePutElseRequest(requestNode, result);
00287       }
00288     }
00289   }
00290 }

EXTERN void CalHashTableDelete	(	CalHashTable_t *	hashTable,
		CalBddNode_t *	bddNode
	)

Function********************************************************************

Synopsis [Deletes a BDD node in the hash table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 354 of file calHashTable.c.

00355 {
00356   int hashValue;
00357   Cal_Bdd_t thenBdd, elseBdd;
00358   CalBddNode_t  *ptr, *last;
00359 
00360   CalBddNodeGetThenBdd(bddNode, thenBdd);
00361   CalBddNodeGetElseBdd(bddNode, elseBdd);
00362   hashValue =
00363       CalDoHash2(CalBddGetBddNode(thenBdd), CalBddGetBddNode(elseBdd), hashTable);
00364 
00365   last = Cal_Nil(CalBddNode_t);
00366   ptr = hashTable->bins[hashValue];
00367   while(ptr != Cal_Nil(CalBddNode_t)){
00368     if(ptr == bddNode){
00369       if(last == Cal_Nil(CalBddNode_t)){
00370         hashTable->bins[hashValue] = CalBddNodeGetNextBddNode(ptr);
00371       }
00372       else{
00373         CalBddNodePutNextBddNode(last, CalBddNodeGetNextBddNode(ptr));
00374       }
00375       hashTable->numEntries--;
00376       CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00377       return;
00378     }
00379     last = ptr;
00380     ptr = CalBddNodeGetNextBddNode(ptr);
00381   }
00382   CalBddWarningMessage("Trying to delete a non-existent node\n");
00383 }

EXTERN int CalHashTableFindOrAdd	(	CalHashTable_t *	hashTable,
		Cal_Bdd_t	thenBdd,
		Cal_Bdd_t	elseBdd,
		Cal_Bdd_t *	bddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 203 of file calHashTable.c.

00207 {
00208   CalBddNode_t *ptr;
00209   Cal_Bdd_t tmpBdd;
00210   int hashValue;
00211   
00212   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd), 
00213       CalBddGetBddNode(elseBdd), hashTable);
00214   ptr = hashTable->bins[hashValue];
00215   while(ptr != Cal_Nil(CalBddNode_t)){
00216     CalBddNodeGetThenBdd(ptr, tmpBdd);
00217     if(CalBddIsEqual(thenBdd, tmpBdd)){
00218       CalBddNodeGetElseBdd(ptr, tmpBdd);
00219       if(CalBddIsEqual(elseBdd, tmpBdd)){
00220         CalBddPutBddId(*bddPtr, hashTable->bddId);
00221         CalBddPutBddNode(*bddPtr, ptr);
00222         return 1;
00223       }
00224     }
00225     ptr = CalBddNodeGetNextBddNode(ptr);
00226   }
00227   hashTable->numEntries++;
00228   if(hashTable->numEntries > hashTable->maxCapacity){
00229     CalHashTableRehash(hashTable,1);
00230     hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
00231         CalBddGetBddNode(elseBdd), hashTable);
00232   }
00233   CalNodeManagerInitBddNode(hashTable->nodeManager, thenBdd, elseBdd, 
00234       hashTable->bins[hashValue], ptr);
00235   hashTable->bins[hashValue] = ptr;
00236   CalBddPutBddId(*bddPtr, hashTable->bddId);
00237   CalBddPutBddNode(*bddPtr, ptr);
00238   return 0;
00239 }

EXTERN int CalHashTableGC	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable
	)

Function********************************************************************

Synopsis [This function performs the garbage collection operation for a particular index.]

Description [The input is the hash table containing the nodes belonging to that level. Each bin of the hash table is traversed and the Bdd nodes with 0 reference count are put at the appropriate level in the processing que of the manager.]

SideEffects [The number of nodes in the hash table can possibly decrease.]

SeeAlso [optional]

Definition at line 208 of file calGC.c.

00209 {
00210   CalBddNode_t *last, *next, *ptr, *thenBddNode, *elseBddNode;
00211   int i;
00212   int oldNumEntries;
00213   
00214   oldNumEntries = hashTable->numEntries;
00215   for(i = 0; i < hashTable->numBins; i++){
00216     last = NULL;
00217     ptr = hashTable->bins[i];
00218     while(ptr != Cal_Nil(CalBddNode_t)){
00219       next = CalBddNodeGetNextBddNode(ptr);
00220       if(CalBddNodeIsRefCountZero(ptr)){
00221         if (last == NULL){
00222           hashTable->bins[i] = next;
00223         }
00224         else{
00225           CalBddNodePutNextBddNode(last,next);
00226         }
00227         thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(ptr));
00228         elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(ptr));
00229         CalBddNodeDcrRefCount(thenBddNode);
00230         CalBddNodeDcrRefCount(elseBddNode);
00231         CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00232         /* Mark the freed node for cache table clean up */
00233         /* We have to make sure that the clean up routine is called */
00234         /* right after this function (so that the marking remains */
00235         /* valid) */
00236         CalBddNodeMark(ptr);
00237         hashTable->numEntries--;
00238       }
00239       else {
00240         last = ptr;
00241       }
00242       ptr = next;
00243     }
00244   }
00245   return oldNumEntries - hashTable->numEntries;
00246 }

EXTERN CalHashTable_t* CalHashTableInit	(	Cal_BddManager_t *	bddManager,
		Cal_BddId_t	bddId
	)

AutomaticEnd Function********************************************************************

Synopsis [Initialize a hash table using default parameters.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 95 of file calHashTable.c.

00096 {
00097   CalHashTable_t *hashTable;
00098 
00099   hashTable = Cal_MemAlloc(CalHashTable_t, 1);
00100   /*hashTable = CAL_BDD_NEW_REC(bddManager, CalHashTable_t);*/
00101   if(hashTable == Cal_Nil(CalHashTable_t)){
00102     CalBddFatalMessage("out of memory");
00103   }
00104   hashTable->sizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00105   hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
00106   hashTable->maxCapacity = hashTable->numBins*HASH_TABLE_DEFAULT_MAX_DENSITY;
00107   hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
00108   if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
00109     CalBddFatalMessage("out of memory");
00110   }
00111   memset((char *)hashTable->bins, 0,
00112          hashTable->numBins*sizeof(CalBddNode_t *)); 
00113   hashTable->bddId = bddId;
00114   hashTable->nodeManager = bddManager->nodeManagerArray[bddId];
00115   hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
00116   memset((char *)(&(hashTable->startNode)), 0, sizeof(CalBddNode_t));
00117   hashTable->endNode = &(hashTable->startNode);
00118   hashTable->numEntries = 0;
00119   return hashTable;
00120 }

EXTERN void CalHashTableITEApply	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable,
		CalHashTable_t **	reqQueAtPipeDepth
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 278 of file calBddITE.c.

00282 {
00283   int i, numBins = hashTable->numBins;
00284   CalBddNode_t **bins = hashTable->bins;
00285   CalRequestNode_t *requestNode;
00286   Cal_Bdd_t fx, gx, fxbar, gxbar, hx, hxbar, result;
00287   CalNodeManager_t *nodeManager = hashTable->nodeManager;
00288   
00289   for(i = 0; i < numBins; i++){
00290     for(requestNode = bins[i];
00291         requestNode != Cal_Nil(CalRequestNode_t);
00292         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00293       /* Process the requestNode */
00294       CalITERequestNodeGetCofactors(bddManager, requestNode,
00295           fx, fxbar, gx, gxbar, hx, hxbar);
00296       result = CalOpITE(bddManager, fx, gx, hx, reqQueAtPipeDepth);
00297       CalBddIcrRefCount(result);
00298       CalRequestNodePutThenRequest(requestNode, result);
00299       result = CalOpITE(bddManager, fxbar, gxbar, hxbar, reqQueAtPipeDepth);
00300       CalBddIcrRefCount(result);
00301       CalNodeManagerFreeNode(nodeManager,
00302           CalRequestNodeGetElseRequestNode(requestNode));
00303       CalRequestNodePutElseRequest(requestNode, result);
00304     }
00305   }
00306 }

EXTERN int CalHashTableLookup	(	CalHashTable_t *	hashTable,
		Cal_Bdd_t	thenBdd,
		Cal_Bdd_t	elseBdd,
		Cal_Bdd_t *	bddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 314 of file calHashTable.c.

00319 {
00320   CalBddNode_t *ptr;
00321   Cal_Bdd_t tmpBdd;
00322   int hashValue;
00323   
00324   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
00325       CalBddGetBddNode(elseBdd), hashTable);
00326   ptr = hashTable->bins[hashValue];
00327   while(ptr != Cal_Nil(CalBddNode_t)){
00328     CalBddNodeGetThenBdd(ptr, tmpBdd);
00329     if(CalBddIsEqual(thenBdd, tmpBdd)){
00330       CalBddNodeGetElseBdd(ptr, tmpBdd);
00331       if(CalBddIsEqual(elseBdd, tmpBdd)){
00332         CalBddPutBddId(*bddPtr, hashTable->bddId);
00333         CalBddPutBddNode(*bddPtr, ptr);
00334         return 1;
00335       }
00336     }
00337     ptr = CalBddNodeGetNextBddNode(ptr);
00338   }
00339   return 0;
00340 }

EXTERN CalHashTable_t* CalHashTableOneInit	(	Cal_BddManager_t *	bddManager,
		int	itemSize
	)

AutomaticEnd Function********************************************************************

Synopsis [Initialize a hash table using default parameters.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 98 of file calHashTableOne.c.

00099 {
00100   int i;
00101   CalHashTable_t *hashTable;
00102 
00103   hashTable = Cal_MemAlloc(CalHashTable_t, 1);
00104   if(hashTable == Cal_Nil(CalHashTable_t)){
00105     CalBddFatalMessage("out of memory");
00106   }
00107   hashTable->sizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00108   hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
00109   hashTable->maxCapacity = hashTable->numBins*HASH_TABLE_DEFAULT_MAX_DENSITY;
00110   hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
00111   if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
00112     CalBddFatalMessage("out of memory");
00113   }
00114   for(i = 0; i < hashTable->numBins; i++){
00115     hashTable->bins[i] = Cal_Nil(CalBddNode_t);
00116   }
00117   hashTable->numEntries = 0;
00118   hashTable->bddId = (Cal_BddId_t)itemSize;
00119   if(itemSize > NODE_SIZE){
00120     CalBddFatalMessage("CalHashTableOneInit: itemSize exceeds NODE_SIZE");
00121   }
00122   hashTable->nodeManager = bddManager->nodeManagerArray[0];
00123   hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
00124   return hashTable;
00125 }

EXTERN void CalHashTableOneInsert	(	CalHashTable_t *	hashTable,
		Cal_Bdd_t	keyBdd,
		char *	valuePtr
	)

Function********************************************************************

Synopsis [Directly insert a BDD node in the hash table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 173 of file calHashTableOne.c.

00175 {
00176   int hashValue;
00177   CalBddNode_t *bddNode, *dataPtr;
00178 
00179   hashValue = HashTableOneDoHash(hashTable, keyBdd);
00180   hashTable->numEntries++;
00181   if(hashTable->numEntries >= hashTable->maxCapacity){
00182     HashTableOneRehash(hashTable, 1);
00183     hashValue = HashTableOneDoHash(hashTable, keyBdd);
00184   }
00185   CalNodeManagerAllocNode(hashTable->nodeManager, dataPtr);
00186   memcpy(dataPtr, valuePtr, (size_t)hashTable->bddId);
00187   CalNodeManagerAllocNode(hashTable->nodeManager, bddNode);
00188   CalBddNodePutThenBdd(bddNode, keyBdd);
00189   CalBddNodePutElseBddNode(bddNode, dataPtr);
00190   CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
00191   hashTable->bins[hashValue] = bddNode;
00192 }

EXTERN int CalHashTableOneLookup	(	CalHashTable_t *	hashTable,
		Cal_Bdd_t	keyBdd,
		char **	valuePtrPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 206 of file calHashTableOne.c.

00208 {
00209   CalBddNode_t *ptr;
00210   Cal_Bdd_t tmpBdd;
00211   int hashValue;
00212   
00213   hashValue = HashTableOneDoHash(hashTable, keyBdd);
00214   ptr = hashTable->bins[hashValue];
00215   while(ptr != Cal_Nil(CalBddNode_t)){
00216     CalBddNodeGetThenBdd(ptr, tmpBdd);
00217     if(CalBddIsEqual(keyBdd, tmpBdd)){
00218       if(valuePtrPtr){
00219         *valuePtrPtr = (char *)CalBddNodeGetElseBddNode(ptr);
00220       }
00221       return 1;
00222     }
00223     ptr = CalBddNodeGetNextBddNode(ptr);
00224   }
00225   if(valuePtrPtr){
00226     *valuePtrPtr = Cal_Nil(char);
00227   }
00228   return 0;
00229 }

EXTERN void CalHashTableOnePrint	(	CalHashTable_t *	hashTable,
		int	flag
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 575 of file calUtil.c.

00576 {
00577   int i;
00578   CalBddNode_t *ptr, *node;
00579   Cal_Bdd_t keyBdd;
00580 
00581   printf("*************************************************\n");
00582   for(i = 0; i < hashTable->numBins; i++){
00583     ptr = hashTable->bins[i];
00584     while(ptr != Cal_Nil(CalBddNode_t)){
00585       CalBddNodeGetThenBdd(ptr, keyBdd);
00586       node = CalBddNodeGetElseBddNode(ptr);
00587       if(flag == 1){
00588         printf("Key(%d %lx) Value(%f)\n", 
00589             CalBddGetBddId(keyBdd), (CalAddress_t)CalBddGetBddNode(keyBdd), *(double *)node); 
00590       }
00591       else{
00592         printf("Key(%d %lx) Value(%d)\n",
00593             CalBddGetBddId(keyBdd), (CalAddress_t)CalBddGetBddNode(keyBdd),  *(int *)node); 
00594       }
00595       ptr = CalBddNodeGetNextBddNode(ptr);
00596     }
00597   }
00598 }

EXTERN void CalHashTableOneQuit ( CalHashTable_t * hashTable )

Function********************************************************************

Synopsis [Free a hash table along with the associated storage.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 140 of file calHashTableOne.c.

00142 {
00143   CalBddNode_t *ptr, *next, *node;
00144   int i;
00145   if(hashTable == Cal_Nil(CalHashTable_t))return;
00146   for(i = 0; i < hashTable->numBins; i++){
00147     ptr = hashTable->bins[i];
00148     while(ptr != Cal_Nil(CalBddNode_t)){
00149       next = CalBddNodeGetNextBddNode(ptr);
00150       node = CalBddNodeGetElseBddNode(ptr);
00151       CalNodeManagerFreeNode(hashTable->nodeManager, node);
00152       CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00153       ptr = next;
00154     }
00155   }
00156   Cal_MemFree(hashTable->bins);
00157   Cal_MemFree(hashTable);
00158 }

EXTERN void CalHashTablePrint ( CalHashTable_t * hashTable )

Function********************************************************************

Synopsis [Prints a hash table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 530 of file calUtil.c.

00531 {
00532   int i;
00533   CalBddNode_t *ptr;
00534   Cal_Bdd_t calBdd, T, E;
00535   int refCount, firstFlag;
00536 
00537   printf("HashTable bddId(%d) entries(%ld) bins(%ld) capacity(%ld)\n",
00538          hashTable->bddId, hashTable->numEntries, hashTable->numBins,
00539          hashTable->maxCapacity);
00540   for(i = 0; i < hashTable->numBins; i++){
00541     ptr = hashTable->bins[i];
00542     firstFlag = 1;
00543     while(ptr != Cal_Nil(CalBddNode_t)){
00544       CalBddPutBddNode(calBdd, ptr);
00545       CalBddNodeGetThenBdd(ptr, T);
00546       CalBddNodeGetElseBdd(ptr, E);
00547       if (firstFlag){
00548         printf("\tbin = (%d) ", i);
00549         firstFlag = 0;
00550       }
00551       printf("\t\tbddNode(%lx) ", (CalAddress_t)ptr);
00552       printf("thenId(%d) ", CalBddGetBddId(T)); 
00553       printf("thenBddNode(%lx) ", (CalAddress_t) CalBddGetBddNode(T));
00554       printf("elseId(%d) ", CalBddGetBddId(E)); 
00555       printf("elseBddNode(%lx) ", (unsigned long)CalBddGetBddNode(E));
00556       CalBddGetRefCount(calBdd, refCount);
00557       printf("refCount(%d)\n", refCount);
00558       ptr = CalBddNodeGetNextBddNode(ptr);
00559     }
00560   }
00561 }

EXTERN int CalHashTableQuit	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable
	)

Function********************************************************************

Synopsis [Free a hash table along with the associated storage.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 135 of file calHashTable.c.

00136 {
00137   if(hashTable == Cal_Nil(CalHashTable_t))return 1;
00138   /*
00139   for(i = 0; i < hashTable->numBins; i++){
00140     ptr = hashTable->bins[i];
00141     while(ptr != Cal_Nil(CalBddNode_t)){
00142       next = CalBddNodeGetNextBddNode(ptr);
00143       CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00144       ptr = next;
00145     }
00146   }
00147   There is no need to free the nodes individually. They will be taken
00148   care of by the PageManagerQuit.
00149   We need to make sure that this function is called only during the global quitting.
00150   If it need be called at some intermediate point, we need to free the BDD nodes 
00151   appropriately.
00152   */
00153   
00154   Cal_MemFree(hashTable->bins);
00155   Cal_MemFree(hashTable);
00156   /*CAL_BDD_FREE_REC(bddManager, hashTable, CalHashTable_t);*/
00157   return 0;
00158 }

EXTERN void CalHashTableReduce	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable,
		CalHashTable_t *	uniqueTableForId
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 143 of file calApplyReduce.c.

00146 {
00147   int i, numBins = hashTable->numBins;
00148   CalBddNode_t **bins = hashTable->bins;
00149   Cal_BddId_t currentBddId = uniqueTableForId->bddId;
00150   CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
00151   CalRequestNode_t *requestNode, *next;
00152   CalBddNode_t *bddNode, *endNode;
00153   Cal_Bdd_t thenBdd, elseBdd, result;
00154   Cal_BddRefCount_t refCount;
00155 
00156   endNode = hashTable->endNode;
00157   for(i = 0; i < numBins; i++){
00158     for(requestNode = bins[i];
00159         requestNode != Cal_Nil(CalRequestNode_t);
00160         requestNode = next){
00161       next = CalRequestNodeGetNextRequestNode(requestNode);
00162       /* Process the requestNode */
00163       CalRequestNodeGetThenRequest(requestNode, thenBdd);
00164       CalRequestNodeGetElseRequest(requestNode, elseBdd);
00165       CalRequestIsForwardedTo(thenBdd);
00166       CalRequestIsForwardedTo(elseBdd);
00167       if(CalBddIsEqual(thenBdd, elseBdd)){
00168         CalRequestNodeGetRefCount(requestNode, refCount);
00169         CalRequestAddRefCount(thenBdd, refCount - 2);
00170         CalRequestNodePutThenRequest(requestNode, thenBdd);
00171         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00172         endNode->nextBddNode = requestNode;
00173         endNode = requestNode;
00174       }
00175       else
00176         if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00177           thenBdd, elseBdd, &result) == 1){
00178         CalBddDcrRefCount(thenBdd);
00179         CalBddDcrRefCount(elseBdd);
00180         CalRequestNodeGetRefCount(requestNode, refCount);
00181         CalBddAddRefCount(result, refCount);
00182         CalRequestNodePutThenRequest(requestNode, result);
00183         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00184         endNode->nextBddNode = requestNode;
00185         endNode = requestNode;
00186       }
00187       else if(CalBddIsOutPos(thenBdd)){
00188         CalRequestNodePutThenRequest(requestNode, thenBdd);
00189         CalRequestNodePutElseRequest(requestNode, elseBdd);
00190         CalHashTableAddDirect(uniqueTableForId, requestNode);
00191         bddManager->numNodes++;
00192         bddManager->gcCheck--;
00193       }
00194       else{
00195         CalNodeManagerAllocNode(nodeManager, bddNode);
00196         CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
00197         CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
00198         CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
00199         CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
00200         CalRequestNodeGetRefCount(requestNode, refCount);
00201         CalBddNodePutRefCount(bddNode, refCount);
00202         CalHashTableAddDirect(uniqueTableForId, bddNode);
00203         bddManager->numNodes++;
00204         bddManager->gcCheck--;
00205         CalRequestNodePutThenRequestId(requestNode, currentBddId);
00206         CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
00207         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00208         endNode->nextBddNode = requestNode;
00209         endNode = requestNode;
00210       }
00211     }
00212   }
00213   memset((char *)bins, 0, hashTable->numBins * sizeof(CalBddNode_t *));
00214   hashTable->endNode = endNode;
00215 }

EXTERN void CalHashTableRehash	(	CalHashTable_t *	hashTable,
		int	grow
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 498 of file calHashTable.c.

00499 {
00500   CalBddNode_t *ptr, *next;
00501   CalBddNode_t **oldBins = hashTable->bins;
00502   int i, hashValue;
00503   int oldNumBins = hashTable->numBins;
00504 
00505   if(grow){
00506     hashTable->sizeIndex++;
00507   }
00508   else{
00509     if (hashTable->sizeIndex <= HASH_TABLE_DEFAULT_SIZE_INDEX){/* No need to rehash */
00510       return;
00511     }
00512     hashTable->sizeIndex--;
00513   }
00514 
00515   hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
00516   hashTable->maxCapacity = hashTable->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY;
00517   hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
00518   if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
00519     CalBddFatalMessage("out of memory");
00520   }
00521   /*
00522   for(i = 0; i < hashTable->numBins; i++){
00523     hashTable->bins[i] = Cal_Nil(CalBddNode_t);
00524   }
00525   */
00526   memset((char *)hashTable->bins, 0,
00527          hashTable->numBins*sizeof(CalBddNode_t *));
00528 
00529   for(i = 0; i < oldNumBins; i++){
00530     ptr = oldBins[i];
00531     while(ptr != Cal_Nil(CalBddNode_t)){
00532       next = CalBddNodeGetNextBddNode(ptr);
00533       hashValue = CalDoHash2(CalBddNodeGetThenBddNode(ptr),
00534           CalBddNodeGetElseBddNode(ptr), hashTable);
00535       CalBddNodePutNextBddNode(ptr, hashTable->bins[hashValue]);
00536       hashTable->bins[hashValue] = ptr;
00537       ptr = next;
00538     }
00539   }
00540   Cal_MemFree(oldBins);
00541 }

EXTERN int CalHashTableThreeFindOrAdd	(	CalHashTable_t *	hashTable,
		Cal_Bdd_t	f,
		Cal_Bdd_t	g,
		Cal_Bdd_t	h,
		Cal_Bdd_t *	bddPtr
	)

AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 108 of file calHashTableThree.c.

00113 {
00114   CalBddNode_t *ptr, *ptrIndirect;
00115   Cal_Bdd_t tmpBdd;
00116   int hashValue;
00117   
00118   hashValue = CalDoHash3(CalBddGetBddNode(f), 
00119       CalBddGetBddNode(g), CalBddGetBddNode(h), hashTable);
00120   ptr = hashTable->bins[hashValue];
00121   while(ptr != Cal_Nil(CalBddNode_t)){
00122     CalBddNodeGetThenBdd(ptr, tmpBdd);
00123     if(CalBddIsEqual(f, tmpBdd)){
00124       ptrIndirect = CalBddNodeGetElseBddNode(ptr);
00125       CalBddNodeGetThenBdd(ptrIndirect, tmpBdd);
00126       if(CalBddIsEqual(g, tmpBdd)){
00127         CalBddNodeGetElseBdd(ptrIndirect, tmpBdd);
00128         if(CalBddIsEqual(h, tmpBdd)){
00129           CalBddPutBddId(*bddPtr, hashTable->bddId);
00130           CalBddPutBddNode(*bddPtr, ptr);
00131           return 1;
00132         }
00133       }
00134     }
00135     ptr = CalBddNodeGetNextBddNode(ptr);
00136   }
00137   hashTable->numEntries++;
00138   if(hashTable->numEntries > hashTable->maxCapacity){
00139     CalHashTableThreeRehash(hashTable,1);
00140     hashValue = CalDoHash3(CalBddGetBddNode(f),
00141         CalBddGetBddNode(g), CalBddGetBddNode(h), hashTable);
00142   }
00143   CalNodeManagerAllocNode(hashTable->nodeManager, ptr);
00144   CalNodeManagerAllocNode(hashTable->nodeManager, ptrIndirect);
00145   CalBddNodePutThenBdd(ptr, f);
00146   CalBddNodePutThenBdd(ptrIndirect, g);
00147   CalBddNodePutElseBdd(ptrIndirect, h);
00148   CalBddNodePutElseBddNode(ptr, ptrIndirect);
00149   CalBddNodePutNextBddNode(ptr, hashTable->bins[hashValue]);
00150   hashTable->bins[hashValue] = ptr;
00151   CalBddPutBddId(*bddPtr, hashTable->bddId);
00152   CalBddPutBddNode(*bddPtr, ptr);
00153   return 0;
00154 }

EXTERN int CalIncreasingOrderCompare	(	const void *	a,
		const void *	b
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 224 of file calPerformanceTest.c.

00225 {
00226   return (*(int *)b-*(int *)a);
00227 }

EXTERN int CalInitInteract ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [Initializes the interaction matrix.]

Description [Initializes the interaction matrix. The interaction matrix is implemented as a bit vector storing the upper triangle of the symmetric interaction matrix. The bit vector is kept in an array of long integers. The computation is based on a series of depth-first searches, one for each root of the DAG. A local flag (the mark bits) is used.]

SideEffects [None]

SeeAlso []

Definition at line 181 of file calInteract.c.

00182 {
00183   int i,k;
00184   int words;
00185   long *interact;
00186   int *support;
00187   long numBins;
00188   CalBddNode_t **bins, *bddNode, *nextBddNode;
00189   
00190   int n = bddManager->numVars;
00191   
00192   words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
00193   bddManager->interact = interact = Cal_MemAlloc(long, words);
00194   if (interact == NULL) return(0);
00195   for (i = 0; i < words; i++) {
00196       interact[i] = 0;
00197   }
00198   
00199   support = Cal_MemAlloc(int, n);
00200   if (support == Cal_Nil(int)) {
00201     Cal_MemFree(interact);
00202     return(0);
00203   }
00204   bins = bddManager->uniqueTable[0]->bins;
00205   numBins = bddManager->uniqueTable[0]->numBins;
00206   for (i=0; i<numBins; i++){
00207     for (bddNode = bins[i]; bddNode; bddNode = nextBddNode) {
00208       Cal_Bdd_t internalBdd;
00209       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00210       CalBddNodeGetThenBdd(bddNode, internalBdd);
00211       for (k = 0; k < n; k++) {
00212         support[k] = 0;
00213       }
00214       ddSuppInteract(bddManager, internalBdd, support);
00215       ddClearLocal(internalBdd);
00216       ddUpdateInteract(bddManager, support);
00217     }
00218   }
00219   /* If there are some results pending in the pipeline, we need to
00220      take those into account as well */
00221 
00222   if (bddManager->pipelineState == CREATE){
00223     CalRequestNode_t **requestNodeListArray =
00224         bddManager->requestNodeListArray; 
00225     Cal_Bdd_t resultBdd;
00226     for (i=0;
00227          i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00228          i++){
00229       for (bddNode = *requestNodeListArray; bddNode;
00230            bddNode = nextBddNode){ 
00231         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00232         Cal_Assert(CalBddNodeIsForwarded(bddNode));
00233         CalBddNodeGetThenBdd(bddNode, resultBdd);
00234         Cal_Assert(CalBddIsForwarded(resultBdd) == 0);
00235         for (k = 0; k < n; k++) {
00236           support[k] = 0;
00237         }
00238         ddSuppInteract(bddManager, resultBdd, support);
00239         ddClearLocal(resultBdd);
00240         ddUpdateInteract(bddManager, support);
00241       }
00242       requestNodeListArray++;
00243     }
00244   }
00245   
00246   
00247   Cal_MemFree(support);
00248   return(1);
00249   
00250 } /* end of CalInitInteract */

EXTERN CalNodeManager_t* CalNodeManagerInit ( CalPageManager_t * pageManager )

Function********************************************************************

Name [CalNodeManagerInit]

Synopsis [Initializes a node manager.]

Description [optional]

SideEffects []

SeeAlso [optional]

Definition at line 219 of file calMemoryManagement.c.

00220 {
00221   CalNodeManager_t *nodeManager;
00222   nodeManager = Cal_MemAlloc(CalNodeManager_t, 1);
00223   nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
00224   nodeManager->pageManager = pageManager;
00225   nodeManager->numPages = 0;
00226   nodeManager->maxNumPages = 10;
00227   nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
00228                                         nodeManager->maxNumPages);
00229   return nodeManager;
00230 }

EXTERN void CalNodeManagerPrint ( CalNodeManager_t * nodeManager )

Function********************************************************************

Name [CalNodeManagerPrint]

Synopsis [Prints address of each free node.]

Description [optional]

SideEffects []

SeeAlso [optional]

Definition at line 280 of file calMemoryManagement.c.

00282 {
00283   int i;
00284   CalBddNode_t *node;
00285   printf("****************** nodeManager ********************\n");
00286   printf("freeNodeList:\n");
00287   i = 0;
00288   node = nodeManager->freeNodeList;
00289   while(node){
00290     printf("%lx%c", (CalAddress_t)node, (i+1)%5?' ':'\n');
00291     i++;
00292     node = node->nextBddNode;
00293   }
00294   printf("\n");
00295 }

EXTERN int CalNodeManagerQuit ( CalNodeManager_t * nodeManager )

Function********************************************************************

Name [CalNodeManagerQuit]

Synopsis [Frees a node manager.]

Description [optional]

SideEffects [The associated nodes are lost.]

SeeAlso [optional]

Definition at line 247 of file calMemoryManagement.c.

00248 {
00249   if(nodeManager == Cal_Nil(CalNodeManager_t)){
00250     return 1;
00251   }
00252   else{
00253     int i;
00254     for (i = 0; i < nodeManager->numPages; i++){
00255       CalPageManagerFreePage(nodeManager->pageManager,
00256                              nodeManager->pageList[i]);
00257     }
00258     Cal_MemFree(nodeManager->pageList);
00259     Cal_MemFree(nodeManager);
00260     return 0;
00261   }
00262 }

EXTERN int CalOpAnd	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	F,
		Cal_Bdd_t	G,
		Cal_Bdd_t *	resultBddPtr
	)

CFile***********************************************************************

FileName [calTerminal.c]

PackageName [cal]

Synopsis [Contains the terminal function for various BDD operations.]

Description []

SeeAlso []

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calTerminal.c,v 1.1.1.2 1997/02/12 21:11:30 hsv Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 95 of file calTerminal.c.

00099 {
00100   if(CalBddIsBddConst(F)){
00101     if(CalBddIsBddOne(bddManager, F)){
00102       *resultBddPtr = G;
00103     }
00104     else{
00105       *resultBddPtr = F;
00106     }
00107     return 1;
00108   }
00109   else if(CalBddIsBddConst(G)){
00110     if(CalBddIsBddOne(bddManager, G)){
00111       *resultBddPtr = F;
00112     }
00113     else{
00114       *resultBddPtr = G;
00115     }
00116     return 1;
00117   }
00118   else{
00119     CalBddNode_t *bddNodeF, *bddNodeG;
00120     bddNodeF = CalBddGetBddNode(F);
00121     bddNodeG = CalBddGetBddNode(G);
00122     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00123       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00124         *resultBddPtr = CalBddZero(bddManager);
00125       }
00126       else{
00127         *resultBddPtr = F;
00128       }
00129       return 1;
00130     }
00131     else{
00132       return 0;
00133     }
00134   }
00135 }

EXTERN int CalOpBddVarSubstitute	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 212 of file calBddVarSubstitute.c.

00214 {
00215   if (bddManager->idToIndex[CalBddGetBddId(f)] >
00216       bddManager->currentAssociation->lastBddIndex){ 
00217     *resultBddPtr = f;
00218     return 1;
00219   }
00220   return 0;
00221 }

EXTERN int CalOpCofactor	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t	c,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 243 of file calReduce.c.

00248 {
00249   if (CalBddIsBddConst(c)){
00250     if (CalBddIsBddZero(bddManager, c)){
00251       *resultBddPtr = bddManager->bddNull;
00252     }
00253     else {
00254       *resultBddPtr = f;
00255     }
00256     return 1;
00257   }
00258   if (CalBddIsBddConst(f)){
00259     *resultBddPtr = f;
00260     return 1;
00261   }
00262   return 0;
00263 }

EXTERN int CalOpExists	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 260 of file calQuant.c.

00262 {
00263   if (((int)bddManager->idToIndex[CalBddGetBddId(f)]) >
00264       bddManager->currentAssociation->lastBddIndex){ 
00265     *resultBddPtr = f;
00266     return 1;
00267   }
00268   return 0;
00269 }

EXTERN Cal_Bdd_t CalOpITE	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t	g,
		Cal_Bdd_t	h,
		CalHashTable_t **	reqQueForITE
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 313 of file calTerminal.c.

00319 {
00320   CalBddNode_t *bddNode1, *bddNode2;
00321   int complementFlag = 0;
00322 
00323   /*
00324    * First phase: Make substitutions 
00325    * ITE(F,F,H) = ITE(F,1,H)
00326    * ITE(F,F',H) = ITE(F,0,H)
00327    * ITE(F,G,F) = ITE(F,G,0)
00328    * ITE(F,G,F') = ITE(F,G,1)
00329    */
00330   bddNode1 = CalBddGetBddNode(f);
00331   bddNode2 = CalBddGetBddNode(g);
00332   if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
00333     if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
00334       g = CalBddZero(bddManager);
00335     }
00336     else{
00337       g = CalBddOne(bddManager);
00338     }
00339   }
00340   bddNode2 = CalBddGetBddNode(h);
00341   if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
00342     if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
00343       h = CalBddOne(bddManager);
00344     }
00345     else{
00346       h = CalBddZero(bddManager);
00347     }
00348   }
00349 
00350   /*
00351    * Second phase: Fix the complement pointers.
00352    * There are 3 possible cases:
00353    * F +ve G -ve: ITE(F ,G',H ) = ITE(F ,G ,H')'
00354    * F -ve H +ve: ITE(F',G ,H ) = ITE(F ,H ,G)
00355    * F -ve H -ve: ITE(F',G ,H') = ITE(F ,H ,G')'
00356    */
00357   if(CalBddIsOutPos(f)){
00358     if(!CalBddIsOutPos(g)){
00359       CalBddNot(g, g);
00360       CalBddNot(h, h);
00361       complementFlag = 1;
00362     }
00363   }
00364   else{
00365     Cal_Bdd_t tmpBdd;
00366     CalBddNot(f, f);
00367     if(CalBddIsOutPos(h)){
00368       tmpBdd = g;
00369       g = h;
00370       h = tmpBdd;
00371     }
00372     else{
00373       tmpBdd = g;
00374       CalBddNot(h, g);
00375       CalBddNot(tmpBdd, h);
00376       complementFlag = 1;
00377     }
00378   }
00379 
00380   /*
00381    * Third phase: Check for the terminal cases; create new request if needed
00382    * ite(1,G,H) = G
00383    * ite(0,G,H) = H (impossible by construction in second phase)
00384    * ite(F,G,G) = G
00385    * ite(F,1,0) = F
00386    * ite(F,0,1) = F'(impossible by construction in second phase)
00387    */
00388   if(CalBddIsBddConst(f) || CalBddIsEqual(g, h)){
00389     CalBddUpdatePhase(g, complementFlag);
00390     return g;
00391   }
00392   else if(CalBddIsBddConst(g) && CalBddIsBddConst(h)){
00393     CalBddUpdatePhase(f, complementFlag);
00394     return f;
00395   }
00396   else{
00397     Cal_BddId_t bddId;
00398     Cal_Bdd_t result;
00399     CalBddGetMinId3(bddManager, f, g, h, bddId);
00400     CalHashTableThreeFindOrAdd(reqQueForITE[bddId], f, g, h, &result);
00401     CalBddUpdatePhase(result, complementFlag);
00402     return result;
00403   }
00404 }

EXTERN int CalOpNand	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	F,
		Cal_Bdd_t	G,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 149 of file calTerminal.c.

00153 {
00154   if(CalBddIsBddConst(F)){
00155     if(CalBddIsBddOne(bddManager, F)){
00156       CalBddNot(G, *resultBddPtr);
00157     }
00158     else{
00159       CalBddNot(F, *resultBddPtr);
00160     }
00161     return 1;
00162   }
00163   else if(CalBddIsBddConst(G)){
00164     if(CalBddIsBddOne(bddManager, G)){
00165       CalBddNot(F, *resultBddPtr);
00166     }
00167     else{
00168       CalBddNot(G, *resultBddPtr);
00169     }
00170     return 1;
00171   }
00172   else{
00173     CalBddNode_t *bddNodeF, *bddNodeG;
00174     bddNodeF = CalBddGetBddNode(F);
00175     bddNodeG = CalBddGetBddNode(G);
00176     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00177       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00178         *resultBddPtr = CalBddOne(bddManager);
00179       }
00180       else{
00181         CalBddNot(F, *resultBddPtr);
00182       }
00183       return 1;
00184     }
00185     else{
00186       return 0;
00187     }
00188   }
00189 }

EXTERN int CalOpOr	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	F,
		Cal_Bdd_t	G,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 203 of file calTerminal.c.

00208 {
00209   if(CalBddIsBddConst(F)){
00210     if(CalBddIsBddOne(bddManager, F)){
00211       *resultBddPtr = F;
00212     }
00213     else{
00214       *resultBddPtr = G;
00215     }
00216     return 1;
00217   }
00218   else if(CalBddIsBddConst(G)){
00219     if(CalBddIsBddOne(bddManager, G)){
00220       *resultBddPtr = G;
00221     }
00222     else{
00223       *resultBddPtr = F;
00224     }
00225     return 1;
00226   }
00227   else{
00228     CalBddNode_t *bddNodeF, *bddNodeG;
00229     bddNodeF = CalBddGetBddNode(F);
00230     bddNodeG = CalBddGetBddNode(G);
00231     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00232       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00233         *resultBddPtr = CalBddOne(bddManager);
00234       }
00235       else{
00236         *resultBddPtr = F;
00237       }
00238       return 1;
00239     }
00240     else{
00241       return 0;
00242     }
00243   }
00244 }

EXTERN int CalOpRelProd	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		Cal_Bdd_t	g,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 284 of file calQuant.c.

00286 {
00287   if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g) ||
00288       CalBddIsComplementEqual(f, g)){
00289     *resultBddPtr = bddManager->bddZero;
00290     return 1;
00291   }
00292   else if (CalBddIsBddOne(bddManager, f) && CalBddIsBddOne(bddManager, g)){
00293     *resultBddPtr = bddManager->bddOne;
00294     return 1;
00295   }
00296   return 0;
00297 }

EXTERN int CalOpXor	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	F,
		Cal_Bdd_t	G,
		Cal_Bdd_t *	resultBddPtr
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 258 of file calTerminal.c.

00263 {
00264   if(CalBddIsBddConst(F)){
00265     if(CalBddIsBddOne(bddManager, F)){
00266       CalBddNot(G, *resultBddPtr);
00267     }
00268     else{
00269       *resultBddPtr = G;
00270     }
00271     return 1;
00272   }
00273   else if(CalBddIsBddConst(G)){
00274     if(CalBddIsBddOne(bddManager, G)){
00275       CalBddNot(F, *resultBddPtr);
00276     }
00277     else{
00278       *resultBddPtr = F;
00279     }
00280     return 1;
00281   }
00282   else{
00283     CalBddNode_t *bddNodeF, *bddNodeG;
00284     bddNodeF = CalBddGetBddNode(F);
00285     bddNodeG = CalBddGetBddNode(G);
00286     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00287       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00288         *resultBddPtr = CalBddOne(bddManager);
00289       }
00290       else{
00291         *resultBddPtr = CalBddZero(bddManager);
00292       }
00293       return 1;
00294     }
00295     else{
00296       return 0;
00297     }
00298   }
00299 }

EXTERN void CalPackNodes ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 646 of file calHashTable.c.

00647 {
00648   int index, id;
00649   
00650   for (index = bddManager->numVars-1; index >= 0; index--){
00651     id = bddManager->indexToId[index];
00652     CalBddPackNodesForSingleId(bddManager, id);
00653   }
00654 }

EXTERN CalAddress_t* CalPageManagerAllocPage ( CalPageManager_t * pageManager )

Function********************************************************************

Name [PageMangerAllocPage]

Synopsis [Allocs a new page.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 312 of file calMemoryManagement.c.

00313 {
00314   CalAddress_t *page;
00315   char buffer[512];
00316   if(pageManager->freePageList == Cal_Nil(CalAddress_t)){
00317     if(PageManagerExpandStorage(pageManager) == FALSE){
00318       sprintf(buffer,
00319               "out of memory : Number of pages allocated = %d\n", 
00320               pageManager->totalNumPages);
00321       CalBddFatalMessage(buffer);
00322     }
00323   }
00324   page = pageManager->freePageList;
00325   pageManager->freePageList = (CalAddress_t *)*page;
00326   return page;
00327 }

EXTERN void CalPageManagerFreePage	(	CalPageManager_t *	pageManager,
		CalAddress_t *	page
	)

Function********************************************************************

Name [PageMangerFreePage]

Synopsis [Free a page.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 347 of file calMemoryManagement.c.

00348 {
00349   *page = (CalAddress_t)(pageManager->freePageList);
00350   pageManager->freePageList = page;
00351 }

EXTERN CalPageManager_t* CalPageManagerInit ( int numPagesPerSegment )

AutomaticEnd Function********************************************************************

Name [CalPageMangerInit]

Synopsis [Initializes a pageManager.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 114 of file calMemoryManagement.c.

00115 {
00116   CalPageManager_t *pageManager;
00117   pageManager = Cal_MemAlloc(CalPageManager_t, 1);
00118   pageManager->totalNumPages = 0;
00119   pageManager->numSegments = 0;
00120   pageManager->numPagesPerSegment = numPagesPerSegment;
00121   pageManager->maxNumSegments = MAX_NUM_SEGMENTS;
00122   pageManager->pageSegmentArray 
00123       = Cal_MemAlloc(CalAddress_t *, pageManager->maxNumSegments);
00124   pageManager->numPagesArray 
00125       = Cal_MemAlloc(int, pageManager->maxNumSegments);
00126   pageManager->freePageList = Cal_Nil(CalAddress_t);
00127   if(PageManagerExpandStorage(pageManager) == FALSE){
00128     Cal_MemFree(pageManager->pageSegmentArray);
00129     Cal_MemFree(pageManager);
00130     return Cal_Nil(CalPageManager_t);
00131   }
00132   return pageManager;
00133 }

EXTERN void CalPageManagerPrint ( CalPageManager_t * pageManager )

Function********************************************************************

Name [CalPageMangerPrint]

Synopsis [Prints address of each memory segment and address of each page.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 181 of file calMemoryManagement.c.

00183 {
00184   int i;
00185   CalAddress_t *page;
00186   printf("****************** pageManager ********************\n");
00187   printf("allocationList:\n");
00188   for(i = 0; i < pageManager->numSegments; i++){
00189     page = pageManager->pageSegmentArray[i];
00190     printf("%lx%c", (CalAddress_t)page, (i+1)%5?' ':'\n');
00191   }
00192   printf("\n");
00193   printf("freePageList:\n");
00194   i = 0;
00195   page = pageManager->freePageList;
00196   while(page){
00197     printf("%lx%c", (CalAddress_t)page, (i+1)%5?' ':'\n');
00198     i++;
00199     page = (CalAddress_t *)*page;
00200   }
00201   printf("\n");
00202 }

EXTERN int CalPageManagerQuit ( CalPageManager_t * pageManager )

Function********************************************************************

Name [CalPageMangerQuit]

Synopsis [Frees pageManager and associated pages.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 150 of file calMemoryManagement.c.

00152 {
00153   int i;
00154   if(pageManager == Cal_Nil(CalPageManager_t)){
00155     return 1;
00156   }
00157   for(i = 0; i < pageManager->numSegments; i++){
00158     free(pageManager->pageSegmentArray[i]);
00159   }
00160   Cal_MemFree(pageManager->pageSegmentArray);
00161   Cal_MemFree(pageManager->numPagesArray);
00162   Cal_MemFree(pageManager);
00163   return 0;
00164 }

EXTERN void CalReorderAssociationFix ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 523 of file calAssociation.c.

00524 {
00525   CalAssociation_t *assoc, *nextAssoc;
00526   int i;
00527   
00528   for(assoc = bddManager->associationList;
00529       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00530     nextAssoc = assoc->next;
00531     for (i=1; i <= bddManager->numVars; i++){
00532         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00533             CalBddIsForwardedTo(assoc->varAssociation[i]);
00534         }
00535     }
00536   }
00537   /* fix temporary association */
00538   assoc = bddManager->tempAssociation;
00539   for (i=1; i <= bddManager->numVars; i++){
00540       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00541           CalBddIsForwardedTo(assoc->varAssociation[i]);
00542       }
00543   }
00544 }

EXTERN void CalRepackNodesAfterGC ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 261 of file calGC.c.

00262 {
00263   int index, id, numPagesRequired, packingFlag, pageNum, nodeNum;
00264   int rehashFlag = 0;
00265   int newSizeIndex, hashValue;
00266   CalNodeManager_t *nodeManager;
00267   CalHashTable_t *uniqueTableForId;
00268   CalBddNode_t *bddNode, *thenBddNode, *elseBddNode, *freeNodeList;
00269   CalBddNode_t *newNode;
00270   Cal_Bdd_t thenBdd, elseBdd;
00271   
00272   packingFlag = 0;
00273   
00274   for (index = bddManager->numVars-1; index >= 0; index--){
00275     id = bddManager->indexToId[index];
00276     uniqueTableForId = bddManager->uniqueTable[id];
00277     nodeManager = uniqueTableForId->nodeManager;
00278     if (CalBddIdNeedsRepacking(bddManager, id) == 0){
00279       if (packingFlag == 0) continue; /* nothing needs to be done */
00280       /* We just need to update the cofactors and continue; */
00281       for (pageNum=0; pageNum < nodeManager->numPages; pageNum++){
00282         for(nodeNum = 0,
00283                 bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; 
00284             nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){
00285           if (CalBddNodeIsRefCountZero(bddNode) ||
00286               CalBddNodeIsForwarded(bddNode)) continue;
00287           thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00288           elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00289           CalBddNodeGetThenBdd(bddNode, thenBdd);
00290           CalBddNodeGetElseBdd(bddNode, elseBdd);
00291           if (CalBddIsForwarded(thenBdd)){
00292             CalBddForward(thenBdd);
00293             CalBddNodePutThenBdd(bddNode, thenBdd);
00294             rehashFlag = 1;
00295           }
00296           if (CalBddIsForwarded(elseBdd)){
00297             CalBddForward(elseBdd);
00298             CalBddNodePutElseBdd(bddNode, elseBdd);
00299             rehashFlag = 1;
00300           }
00301           Cal_Assert(!CalBddIsRefCountZero(thenBdd));
00302           Cal_Assert(!CalBddIsRefCountZero(elseBdd));
00303           Cal_Assert(bddManager->idToIndex[id] <
00304                      bddManager->idToIndex[bddNode->thenBddId]);   
00305           Cal_Assert(bddManager->idToIndex[id] < 
00306                      bddManager->idToIndex[bddNode->elseBddId]);
00307           if (rehashFlag){
00308             CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode,
00309                                           thenBddNode, elseBddNode);
00310           }
00311         }
00312       }
00313       continue; /* move to next higher index */
00314     }
00315     packingFlag = 1;
00316     if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) &&
00317         (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){
00318       /* Free the old bins */
00319       Cal_MemFree(uniqueTableForId->bins);
00320       /* Create the new set of bins */
00321       newSizeIndex =
00322           CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY); 
00323       if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00324         newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00325       }
00326       uniqueTableForId->sizeIndex = newSizeIndex;
00327       uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00328       uniqueTableForId->maxCapacity =
00329           uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00330       uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00331                                             uniqueTableForId->numBins); 
00332       if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
00333         CalBddFatalMessage("out of memory");
00334       }
00335     }
00336     /* Clear the unique table bins */
00337     memset((char *)uniqueTableForId->bins, 0,
00338            uniqueTableForId->numBins*sizeof(CalBddNode_t *));
00339     numPagesRequired =
00340         uniqueTableForId->numEntries/NUM_NODES_PER_PAGE+1;
00341     /* Traverse the first numPagesRequired pages of this nodeManager */
00342     /* Create the new free list */
00343     nodeManager->freeNodeList = freeNodeList = Cal_Nil(CalBddNode_t);
00344     for (pageNum = 0; pageNum < nodeManager->numPages; pageNum++){
00345       for(nodeNum = 0,
00346               bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; 
00347           nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){
00348         if(CalBddNodeIsRefCountZero(bddNode) ||
00349            CalBddNodeIsForwarded(bddNode)){
00350           if (pageNum < numPagesRequired){
00351             bddNode->nextBddNode = freeNodeList;
00352             freeNodeList = bddNode;
00353           }
00354           continue;
00355         }
00356         CalBddNodeGetThenBdd(bddNode, thenBdd);
00357         CalBddNodeGetElseBdd(bddNode, elseBdd);
00358         if (CalBddIsForwarded(thenBdd)){
00359           CalBddForward(thenBdd);
00360           CalBddNodePutThenBdd(bddNode, thenBdd);
00361         }
00362         if (CalBddIsForwarded(elseBdd)){
00363           CalBddForward(elseBdd);
00364           CalBddNodePutElseBdd(bddNode, elseBdd); 
00365         }
00366         if (pageNum < numPagesRequired){
00367           /* Simply insert the node in the unique table */
00368           hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode,
00369                                  uniqueTableForId); 
00370           CalBddNodePutNextBddNode(bddNode, uniqueTableForId->bins[hashValue]);
00371           uniqueTableForId->bins[hashValue] = bddNode;
00372         }
00373         else {
00374           /* Create a new node */
00375           newNode = freeNodeList;
00376           freeNodeList = newNode->nextBddNode;
00377           newNode->thenBddNode = bddNode->thenBddNode;
00378           newNode->elseBddNode = bddNode->elseBddNode;
00379           newNode->thenBddId = bddNode->thenBddId;
00380           newNode->elseBddId = bddNode->elseBddId;
00381           newNode->nextBddNode = bddNode->nextBddNode;
00382           bddNode->elseBddNode = FORWARD_FLAG;
00383           bddNode->thenBddId = id;
00384           bddNode->thenBddNode = newNode;
00385           hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode,
00386                                  uniqueTableForId); 
00387           CalBddNodePutNextBddNode(newNode, uniqueTableForId->bins[hashValue]);
00388           uniqueTableForId->bins[hashValue] = newNode;
00389         }
00390       }
00391       if (pageNum >= numPagesRequired){
00392         /* Free this page. I am assuming that there would not be any
00393            call to PageManagerAllocPage, until this function finishes */
00394         /* Also, CalPageManagerFreePage overwrites only the first field of
00395            the bdd node (the nextBddNode field), hence no relevant
00396            information is lost */
00397         CalPageManagerFreePage(nodeManager->pageManager,
00398                                nodeManager->pageList[pageNum]);
00399         nodeManager->pageList[pageNum] = 0;
00400       }
00401     }
00402 #ifdef _CAL_VERBOSE    
00403     printf("Recycled %4d pages for %3d id\n",
00404            nodeManager->numPages-numPagesRequired, id);
00405 #endif
00406     nodeManager->numPages = numPagesRequired;
00407     nodeManager->freeNodeList = freeNodeList;
00408   }
00409   /* Need to update the handles to the nodes being moved */
00410   if (bddManager->pipelineState == CREATE){
00411     /* There are some results computed in pipeline */
00412     CalBddReorderFixProvisionalNodes(bddManager);
00413   }
00414   
00415   CalCacheTableTwoRepackUpdate(bddManager->cacheTable);
00416 
00417   /* Fix the user BDDs */
00418   CalBddReorderFixUserBddPtrs(bddManager);
00419 
00420   /* Fix the association */
00421   CalReorderAssociationFix(bddManager);
00422 
00423   Cal_Assert(CalCheckAssoc(bddManager));
00424 }

EXTERN void CalRequestNodeListArrayITE	(	Cal_BddManager_t *	bddManager,
		CalRequestNode_t **	requestNodeListArray
	)

Function********************************************************************

Name [CalRequestNodeListArrayOp]

Synopsis [required]

Description [This routine is to be used for pipelined and superscalar ITE operations. Currently there is no user interface provided to this routine.]

SideEffects [required]

SeeAlso [optional]

Definition at line 133 of file calBddITE.c.

00135 {
00136   CalRequestNode_t *requestNode, *ptrIndirect;
00137   CalRequest_t F, G, H, result;
00138   int pipeDepth, bddId, bddIndex;
00139   CalHashTable_t **reqQueAtPipeDepth, *hashTable, *uniqueTableForId;
00140   CalHashTable_t ***reqQue = bddManager->reqQue;
00141   
00142   /* ReqQueInsertUsingReqListArray */
00143   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00144     reqQueAtPipeDepth = reqQue[pipeDepth];
00145     for(requestNode = requestNodeListArray[pipeDepth];
00146         requestNode != Cal_Nil(CalRequestNode_t);
00147         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00148       CalRequestNodeGetThenRequest(requestNode, F);
00149       CalRequestIsForwardedTo(F);
00150       ptrIndirect = CalRequestNodeGetElseRequestNode(requestNode);
00151       CalRequestNodeGetThenRequest(ptrIndirect, G);
00152       CalRequestIsForwardedTo(G);
00153       CalRequestNodeGetElseRequest(ptrIndirect, H);
00154       CalRequestIsForwardedTo(H);
00155       CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], ptrIndirect);
00156       result = CalOpITE(bddManager, F, G, H, reqQueAtPipeDepth);
00157       CalRequestNodePutThenRequest(requestNode, result);
00158       CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00159     }
00160   }
00161 
00162   /* ReqQueApply */
00163   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00164     bddId = bddManager->indexToId[bddIndex];
00165     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00166       reqQueAtPipeDepth = reqQue[pipeDepth];
00167       hashTable = reqQueAtPipeDepth[bddId];
00168       if(hashTable->numEntries){
00169         CalHashTableITEApply(bddManager, hashTable, reqQueAtPipeDepth);
00170       }
00171     }
00172   }
00173 
00174   /* ReqQueReduce */
00175   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00176     bddId = bddManager->indexToId[bddIndex];
00177     uniqueTableForId = bddManager->uniqueTable[bddId];
00178     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00179       hashTable = reqQue[pipeDepth][bddId];
00180       if(hashTable->numEntries){
00181         CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00182       }
00183     }
00184   }
00185 
00186   /* ReqListArrayReqForward */
00187   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00188     for(requestNode = requestNodeListArray[pipeDepth];
00189         requestNode != Cal_Nil(CalRequestNode_t);
00190         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00191       CalRequestNodeGetThenRequest(requestNode, result);
00192       CalRequestIsForwardedTo(result);
00193       CalRequestNodePutThenRequest(requestNode, result);
00194     }
00195   }
00196 
00197   /* ReqQueCleanUp */
00198   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00199     reqQueAtPipeDepth = reqQue[pipeDepth];
00200     for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00201       CalHashTableCleanUp(reqQueAtPipeDepth[bddId]);
00202     }
00203   }
00204 }

EXTERN void CalRequestNodeListArrayOp	(	Cal_BddManager_t *	bddManager,
		CalRequestNode_t **	requestNodeListArray,
		CalOpProc_t	calOpProc
	)

Function********************************************************************

Synopsis [Computes result BDDs for an array of lists, each entry of which is pair of pointers, each of which points to a operand BDD or an entry in another list with a smaller array index]

Description [Computes result BDDs for an array of lists, each entry of which is pair of pointers, each of which points to a operand BDD or an entry in another list with a smaller array index]

SideEffects [ThenBDD pointer of an entry is over written by the result BDD and ElseBDD pointer is marked using FORWARD_FLAG]

Definition at line 582 of file calBddOp.c.

00585 {
00586   CalRequestNode_t *requestNode;
00587   CalRequest_t F, G, result;
00588   int pipeDepth, bddId, bddIndex;
00589   CalHashTable_t **reqQueAtPipeDepth, *hashTable, *uniqueTableForId;
00590   CalHashTable_t ***reqQue = bddManager->reqQue;
00591   
00592   /* ReqQueInsertUsingReqListArray */
00593   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00594     reqQueAtPipeDepth = reqQue[pipeDepth];
00595     for(requestNode = requestNodeListArray[pipeDepth];
00596         requestNode != Cal_Nil(CalRequestNode_t);
00597         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00598       CalRequestNodeGetF(requestNode, F);
00599       CalRequestIsForwardedTo(F);
00600       CalRequestNodeGetG(requestNode, G);
00601       CalRequestIsForwardedTo(G);
00602       if((*calOpProc)(bddManager, F, G, &result) == 0){
00603         CalBddNormalize(F, G);
00604         CalBddGetMinId2(bddManager, F, G, bddId);
00605         CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], F, G, &result);
00606       }
00607       CalRequestNodePutThenRequest(requestNode, result);
00608       CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00609     }
00610   }
00611 
00612   /* ReqQueApply */
00613   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00614     bddId = bddManager->indexToId[bddIndex];
00615     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00616       reqQueAtPipeDepth = reqQue[pipeDepth];
00617       hashTable = reqQueAtPipeDepth[bddId];
00618       if(hashTable->numEntries){
00619         CalHashTableApply(bddManager, hashTable, reqQueAtPipeDepth, calOpProc);
00620       }
00621     }
00622   }
00623 
00624 #ifdef COMPUTE_MEMORY_OVERHEAD
00625   {
00626     calNumEntriesAfterApply = 0;
00627     for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00628       bddId = bddManager->indexToId[bddIndex];
00629       for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00630         reqQueAtPipeDepth = reqQue[pipeDepth];
00631         hashTable = reqQueAtPipeDepth[bddId];
00632         calNumEntriesAfterApply += hashTable->numEntries;
00633       }
00634     }
00635   }
00636 #endif
00637 
00638   /* ReqQueReduce */
00639   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00640     bddId = bddManager->indexToId[bddIndex];
00641     uniqueTableForId = bddManager->uniqueTable[bddId];
00642     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00643       hashTable = reqQue[pipeDepth][bddId];
00644       if(hashTable->numEntries){
00645         CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00646       }
00647     }
00648   }
00649 
00650 #ifdef COMPUTE_MEMORY_OVERHEAD
00651   {
00652     CalRequestNode_t *requestNode;
00653     calNumEntriesAfterReduce = 0;
00654     for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00655       CalRequestNode_t *next;
00656       Cal_BddId_t bddId;
00657       bddId = bddManager->indexToId[bddIndex];
00658       for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00659         hashTable = reqQue[pipeDepth][bddId];
00660         for (requestNode = hashTable->requestNodeList;
00661              requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
00662           next = CalRequestNodeGetNextRequestNode(requestNode);
00663           calNumEntriesAfterReduce++;
00664         }
00665       }
00666     }
00667     calAfterReduceToAfterApplyNodesRatio =
00668         ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
00669     calAfterReduceToUniqueTableNodesRatio = 
00670         ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
00671   }
00672 #endif
00673 
00674   /* ReqListArrayReqForward */
00675   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00676     for(requestNode = requestNodeListArray[pipeDepth];
00677         requestNode != Cal_Nil(CalRequestNode_t);
00678         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00679       CalRequestNodeGetThenRequest(requestNode, result);
00680       CalRequestIsForwardedTo(result);
00681       Cal_Assert(CalBddIsForwarded(result) == 0);
00682       CalRequestNodePutThenRequest(requestNode, result);
00683     }
00684   }
00685 
00686   /* ReqQueCleanUp */
00687   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00688     reqQueAtPipeDepth = reqQue[pipeDepth];
00689     for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00690       CalHashTableCleanUp(reqQueAtPipeDepth[bddId]);
00691     }
00692   }
00693 }

EXTERN void CalRequestNodeListCompose	(	Cal_BddManager_t *	bddManager,
		CalRequestNode_t *	requestNodeList,
		Cal_BddIndex_t	composeIndex
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

note [THERE IS A POSSIBILITY OF HAVING A PIPELINED VERSION NEED TO THINK IT THROUGH]

Definition at line 140 of file calBddCompose.c.

00143 {
00144   CalRequestNode_t *requestNode;
00145   CalRequest_t F, H, result;
00146   int bddId, bddIndex;
00147   CalHashTable_t *hashTable, *uniqueTableForId;
00148   CalHashTable_t **reqQueForCompose = bddManager->reqQue[0];
00149   CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
00150   
00151   /* ReqQueForComposeInsertUsingReqList */
00152   for(requestNode = requestNodeList;
00153       requestNode != Cal_Nil(CalRequestNode_t);
00154       requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00155     CalRequestNodeGetF(requestNode, F);
00156     CalRequestNodeGetG(requestNode, H);
00157     CalComposeRequestCreate(bddManager, F, H, composeIndex, 
00158         reqQueForCompose, reqQueForITE, &result);
00159     CalRequestNodePutThenRequest(requestNode, result);
00160     CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00161   }
00162 
00163   /* ReqQueApply */
00164   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00165     bddId = bddManager->indexToId[bddIndex];
00166     hashTable = reqQueForCompose[bddId];
00167     if(hashTable->numEntries){
00168       CalHashTableComposeApply(bddManager, hashTable, composeIndex, 
00169           reqQueForCompose, reqQueForITE);
00170     }
00171     hashTable = reqQueForITE[bddId];
00172     if(hashTable->numEntries){
00173       CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
00174     }
00175   }
00176 
00177   /* ReqQueReduce */
00178   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00179     bddId = bddManager->indexToId[bddIndex];
00180     uniqueTableForId = bddManager->uniqueTable[bddId];
00181     hashTable = reqQueForCompose[bddId];
00182     if(hashTable->numEntries){
00183       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00184     }
00185     hashTable = reqQueForITE[bddId];
00186     if(hashTable->numEntries){
00187       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00188     }
00189   }
00190 
00191   /* ReqListArrayReqForward */
00192   for(requestNode = requestNodeList; requestNode != Cal_Nil(CalRequestNode_t);
00193       requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00194     CalRequestNodeGetThenRequest(requestNode, result);
00195     CalRequestIsForwardedTo(result);
00196     CalRequestNodePutThenRequest(requestNode, result);
00197   }
00198 
00199   /* ReqQueCleanUp */
00200   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00201     CalHashTableCleanUp(reqQueForCompose[bddId]);
00202     CalHashTableCleanUp(reqQueForITE[bddId]);
00203   }
00204 }

EXTERN void CalSetInteract	(	Cal_BddManager_t *	bddManager,
		int	x,
		int	y
	)

AutomaticEnd Function********************************************************************

Synopsis [Set interaction matrix entries.]

Description [Given a pair of variables 0 <= x < y < table->size, sets the corresponding bit of the interaction matrix to 1.]

SideEffects [None]

SeeAlso []

Definition at line 109 of file calInteract.c.

00110 {
00111     int posn, word, bit;
00112 
00113     Cal_Assert(x < y);
00114     Cal_Assert(y < bddManager->numVars);
00115     Cal_Assert(x >= 0);
00116 
00117     posn = ((((bddManager->numVars << 1) - x - 3) * x) >> 1) + y - 1;
00118     word = posn >> LOGBPL;
00119     bit = posn & (BPL-1);
00120     bddManager->interact[word] |= 1 << bit;
00121 
00122 } /* end of CalSetInteract */

EXTERN int CalTestInteract	(	Cal_BddManager_t *	bddManager,
		int	x,
		int	y
	)

Function********************************************************************

Synopsis [Test interaction matrix entries.]

Description [Given a pair of variables 0 <= x < y < bddManager->numVars, tests whether the corresponding bit of the interaction matrix is 1. Returns the value of the bit.]

SideEffects [None]

SeeAlso []

Definition at line 139 of file calInteract.c.

00140 {
00141     int posn, word, bit, result;
00142 
00143     x -= 1; 
00144     y -= 1;
00145     
00146     if (x > y) {
00147         int tmp = x;
00148         x = y;
00149         y = tmp;
00150     }
00151     Cal_Assert(x < y);
00152     Cal_Assert(y < bddManager->numVars);
00153     Cal_Assert(x >= 0);
00154 
00155     posn = ((((bddManager->numVars << 1) - x - 3) * x) >> 1) + y - 1;
00156     word = posn >> LOGBPL;
00157     bit = posn & (BPL-1);
00158     result = (bddManager->interact[word] >> bit) & 1;
00159     return(result);
00160 
00161 } /* end of CalTestInteract */

EXTERN int CalUniqueTableForIdFindOrAdd	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable,
		Cal_Bdd_t	thenBdd,
		Cal_Bdd_t	elseBdd,
		Cal_Bdd_t *	bddPtr
	)

Function********************************************************************

Synopsis [find or add in the unique table for id.]

Description [optional]

SideEffects [If a new BDD node is created (found == false), then the numNodes field of the manager needs to be incremented.]

SeeAlso [optional]

Definition at line 459 of file calHashTable.c.

00465 {
00466   int found = 0; 
00467   if (CalBddIsEqual(thenBdd, elseBdd)){
00468     *bddPtr = thenBdd;
00469     found = 1;
00470   }
00471   else if(CalBddIsOutPos(thenBdd)){
00472     found = CalHashTableFindOrAdd(hashTable, thenBdd, elseBdd, bddPtr);
00473   }
00474   else{
00475     CalBddNot(thenBdd, thenBdd);
00476     CalBddNot(elseBdd, elseBdd);
00477     found = CalHashTableFindOrAdd(hashTable, thenBdd, elseBdd, bddPtr);
00478     CalBddNot(*bddPtr, *bddPtr);
00479   }
00480   if (!found) bddManager->numNodes++;
00481   return found;
00482 }

EXTERN int CalUniqueTableForIdLookup	(	Cal_BddManager_t *	bddManager,
		CalHashTable_t *	hashTable,
		Cal_Bdd_t	thenBdd,
		Cal_Bdd_t	elseBdd,
		Cal_Bdd_t *	bddPtr
	)

Function********************************************************************

Synopsis [Lookup unique table for id.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 398 of file calHashTable.c.

00404 {
00405   CalBddNode_t *ptr;
00406   Cal_Bdd_t tmpBdd;
00407   int hashValue;
00408   
00409   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
00410       CalBddGetBddNode(elseBdd), hashTable);
00411   ptr = hashTable->bins[hashValue];
00412   if(CalBddIsOutPos(thenBdd)){
00413     while(ptr != Cal_Nil(CalBddNode_t)){
00414       CalBddNodeGetThenBdd(ptr, tmpBdd);
00415       if(CalBddIsEqual(thenBdd, tmpBdd)){
00416         CalBddNodeGetElseBdd(ptr, tmpBdd);
00417         if(CalBddIsEqual(elseBdd, tmpBdd)){
00418           CalBddPutBddId(*bddPtr, hashTable->bddId);
00419           CalBddPutBddNode(*bddPtr, ptr);
00420           return 1;
00421         }
00422       }
00423       ptr = CalBddNodeGetNextBddNode(ptr);
00424     }
00425   }
00426   else{
00427     CalBddNot(thenBdd, thenBdd);
00428     CalBddNot(elseBdd, elseBdd);
00429     while(ptr != Cal_Nil(CalBddNode_t)){
00430       CalBddNodeGetThenBdd(ptr, tmpBdd);
00431       if(CalBddIsEqual(thenBdd, tmpBdd)){
00432         CalBddNodeGetElseBdd(ptr, tmpBdd);
00433         if(CalBddIsEqual(elseBdd, tmpBdd)){
00434           CalBddPutBddId(*bddPtr, hashTable->bddId);
00435           CalBddPutBddNode(*bddPtr, CalBddNodeNot(ptr));
00436           return 1;
00437         }
00438       }
00439       ptr = CalBddNodeGetNextBddNode(ptr);
00440     }
00441   }
00442   return 0;
00443 }

EXTERN void CalUniqueTableForIdRehashNode	(	CalHashTable_t *	hashTable,
		CalBddNode_t *	bddNode,
		CalBddNode_t *	thenBddNode,
		CalBddNode_t *	elseBddNode
	)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 555 of file calHashTable.c.

00559 {
00560   CalBddNode_t *nextBddNode;
00561   CalBddNode_t *ptr;
00562   int found;
00563   int hashValue;
00564   int oldHashValue;
00565   Cal_Bdd_t thenBdd;
00566 
00567   oldHashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
00568   hashValue = CalDoHash2(CalBddNodeGetThenBddNode(bddNode),
00569                          CalBddNodeGetElseBddNode(bddNode),
00570                          hashTable);
00571   CalBddNodeGetThenBdd(bddNode, thenBdd);
00572   if (CalBddIsComplement(thenBdd)) {
00573     CalBddFatalMessage("Complement edge on then pointer");
00574   }
00575   if (oldHashValue == hashValue) {
00576     return;
00577   }
00578 
00579   found = 0;
00580   ptr = hashTable->bins[oldHashValue];
00581   if ((ptr != Cal_Nil(CalBddNode_t)) && (ptr == bddNode)) {
00582     hashTable->bins[oldHashValue] = CalBddNodeGetNextBddNode(bddNode);
00583     found = 1;
00584   } else {
00585     while (ptr != Cal_Nil(CalBddNode_t)) {
00586       nextBddNode = CalBddNodeGetNextBddNode(ptr);
00587       if (nextBddNode == bddNode) {
00588         CalBddNodePutNextBddNode(ptr, CalBddNodeGetNextBddNode(bddNode));
00589         found = 1;
00590         break;
00591       }
00592       ptr = nextBddNode;
00593     }
00594   }
00595 
00596   if (!found) {
00597     CalBddFatalMessage("Node not found in the unique table");
00598   } else {
00599     CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
00600     hashTable->bins[hashValue] = bddNode;
00601   }
00602 }

EXTERN void CalUniqueTablePrint ( Cal_BddManager_t * bddManager )

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 151 of file calUtil.c.

00152 {
00153   int i;
00154   for(i = 0; i <= bddManager->numVars; i++){
00155     CalHashTablePrint(bddManager->uniqueTable[i]);
00156   }
00157 }

EXTERN long CalUtilRandom ( void )

Function********************************************************************

Synopsis [Portable random number generator.]

Description [Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The random generator can be explicitly initialized by calling CalUtilSRandom. If no explicit initialization is performed, then the seed 1 is assumed.]

SideEffects []

SeeAlso [CalUtilSRandom]

Definition at line 654 of file calUtil.c.

00655 {
00656     int i;      /* index in the shuffle table */
00657     long int w; /* work variable */
00658 
00659     /* utilRand == 0 if the geneartor has not been initialized yet. */
00660     if (utilRand == 0) CalUtilSRandom((long)1);
00661 
00662     /* Compute utilRand = (utilRand * CAL_LEQA1) % CAL_MODULUS1 avoiding
00663     ** overflows by Schrage's method.
00664     */
00665     w          = utilRand / CAL_LEQQ1;
00666     utilRand   = CAL_LEQA1 * (utilRand - w * CAL_LEQQ1) - w * CAL_LEQR1;
00667     utilRand  += (utilRand < 0) * CAL_MODULUS1;
00668 
00669     /* Compute utilRand2 = (utilRand2 * CAL_LEQA2) % CAL_MODULUS2 avoiding
00670     ** overflows by Schrage's method.
00671     */
00672     w          = utilRand2 / CAL_LEQQ2;
00673     utilRand2  = CAL_LEQA2 * (utilRand2 - w * CAL_LEQQ2) - w * CAL_LEQR2;
00674     utilRand2 += (utilRand2 < 0) * CAL_MODULUS2;
00675 
00676     /* utilRand is shuffled with the Bays-Durham algorithm.
00677     ** shuffleSelect and utilRand2 are combined to generate the output.
00678     */
00679 
00680     /* Pick one element from the shuffle table; "i" will be in the range
00681     ** from 0 to CAL_STAB_SIZE-1.
00682     */
00683     i = shuffleSelect / CAL_STAB_DIV;
00684     /* Mix the element of the shuffle table with the current iterate of
00685     ** the second sub-generator, and replace the chosen element of the
00686     ** shuffle table with the current iterate of the first sub-generator.
00687     */
00688     shuffleSelect   = shuffleTable[i] - utilRand2;
00689     shuffleTable[i] = utilRand;
00690     shuffleSelect  += (shuffleSelect < 1) * (CAL_MODULUS1 - 1);
00691     /* Since shuffleSelect != 0, and we want to be able to return 0,
00692     ** here we subtract 1 before returning.
00693     */
00694     return(shuffleSelect - 1);
00695 
00696 } /* end of CalUtilRandom */

EXTERN void CalUtilSRandom ( long seed )

Function********************************************************************

Synopsis [Initializer for the portable random number generator.]

Description [Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.]

SideEffects [None]

SeeAlso [CalUtilRandom]

Definition at line 617 of file calUtil.c.

00618 {
00619     int i;
00620 
00621     if (seed < 0)       utilRand = -seed;
00622     else if (seed == 0) utilRand = 1;
00623     else                utilRand = seed;
00624     utilRand2 = utilRand;
00625     /* Load the shuffle table (after 11 warm-ups). */
00626     for (i = 0; i < CAL_STAB_SIZE + 11; i++) {
00627         long int w;
00628         w = utilRand / CAL_LEQQ1;
00629         utilRand = CAL_LEQA1 * (utilRand - w * CAL_LEQQ1) - w * CAL_LEQR1;
00630         utilRand += (utilRand < 0) * CAL_MODULUS1;
00631         shuffleTable[i % CAL_STAB_SIZE] = utilRand;
00632     }
00633     shuffleSelect = shuffleTable[1 % CAL_STAB_SIZE];
00634 } /* end of CalUtilSRandom */

EXTERN void CalVarAssociationRepackUpdate	(	Cal_BddManager_t *	bddManager,
		Cal_BddId_t	id
	)

Function********************************************************************

Synopsis [Need to be called after repacking.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 456 of file calAssociation.c.

00458 {
00459   CalAssociation_t *assoc, *nextAssoc;
00460   int i;
00461   
00462   for(assoc = bddManager->associationList;
00463       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00464     nextAssoc = assoc->next;
00465     for (i=1; i <= bddManager->numVars; i++){
00466       if (CalBddGetBddId(assoc->varAssociation[i]) == id){
00467         CalBddForward(assoc->varAssociation[i]);
00468       }
00469     }
00470   }
00471   /* fix temporary association */
00472   assoc = bddManager->tempAssociation;
00473   for (i=1; i <= bddManager->numVars; i++){
00474     if (CalBddGetBddId(assoc->varAssociation[i]) == id){
00475       CalBddForward(assoc->varAssociation[i]);
00476     }
00477   }
00478 }

EXTERN int main	(	int	argc,
		char **	argv
	)

AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

AutomaticEnd Function********************************************************************

Synopsis [Main function for testcudd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 114 of file calBddReorderTest.c.

00115 {
00116   Cal_Bdd expected;
00117   Cal_Bdd a[100];
00118   Cal_Bdd temp1;
00119   Cal_Bdd temp2;
00120   Cal_Bdd b, c, d, e, f, g, result;
00121   Cal_BddManager_t *bddManager;
00122   CalBddNode_t *bddNode;
00123   int i;
00124   int numVars;
00125   int siftFlag = 0;
00126   
00127   if (argc == 1) {
00128     numVars = 5;
00129   } else if (argc >= 2) {
00130     numVars = atoi(argv[1]);
00131   }
00132   if (argc == 3) {
00133     siftFlag = 1;
00134   }
00135 
00136   bddManager = Cal_BddManagerInit();
00137 
00138   for (i = 0; i < 2 * numVars; i++) {
00139     a[i] = Cal_BddManagerCreateNewVarLast(bddManager);
00140   }
00141 
00142   result = Cal_BddZero(bddManager);
00143   for (i = 0; i < numVars; i++) {
00144     temp1 = Cal_BddAnd(bddManager, a[i], a[numVars + i]);
00145     temp2 = Cal_BddOr(bddManager, result, temp1);
00146     Cal_BddFree(bddManager, temp1);
00147     Cal_BddFree(bddManager, result);
00148     result = temp2;
00149   }
00150   Cal_BddManagerGC(bddManager);
00151   Cal_BddStats(bddManager, stdout);
00152   cpuTime();
00153   elapsedTime();
00154   printf("%%%%%%%%%%%% Reordering %%%%%%%%%%%%%%%%%%%\n");
00155   if (siftFlag){
00156     printf("Using Sift Technique\n");
00157     Cal_BddDynamicReordering(bddManager, CAL_REORDER_SIFT);
00158   }
00159   else{
00160     printf("Using Window Technique\n");
00161     Cal_BddDynamicReordering(bddManager, CAL_REORDER_WINDOW);
00162   }
00163   Cal_BddReorder(bddManager);
00164   printf("CPU time: %-8.2f\t Elapsed Time = %-10ld\n", cpuTime(), elapsedTime());
00165   printf("%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%\n");
00166   Cal_BddManagerGC(bddManager);
00167   Cal_BddStats(bddManager, stdout);
00168   /*Cal_BddFunctionPrint(bddManager, result, "Result");*/
00169   temp1 = Cal_BddZero(bddManager);
00170   for (i = 0; i < numVars; i++) {
00171     temp2 = Cal_BddAnd(bddManager, a[i], a[numVars + i]);
00172     expected = Cal_BddOr(bddManager, temp1, temp2);
00173     Cal_BddFree(bddManager, temp1);
00174     Cal_BddFree(bddManager, temp2);
00175     temp1 = expected;
00176   }
00177 
00178   if (!Cal_BddIsEqual(bddManager, result, expected)) {
00179     printf("ERROR: BDDs are not equal\n");
00180     Cal_BddFunctionPrint(bddManager, result, "Result");
00181     Cal_BddFunctionPrint(bddManager, expected, "Expected");
00182   }
00183   printf("\n%%%%%%BDDs are equal\n");
00184   Cal_BddFree(bddManager, result);
00185   Cal_BddFree(bddManager, expected);
00186   Cal_BddManagerGC(bddManager);
00187   Cal_BddStats(bddManager, stdout);
00188   Cal_BddManagerQuit(bddManager);
00189 }

Variable Documentation

unsigned long calPrimes[]

CFile***********************************************************************

FileName [calBddManager.c]

PackageName [cal]

Synopsis [Routines for maintaing the manager and creating variables etc.]

Description []

SeeAlso [optional]

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) ]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calBddManager.c,v 1.9 2002/09/21 20:39:24 fabio Exp

]

Definition at line 59 of file calBddManager.c.

src/calBdd/calInt.h File Reference

Data Structures

Defines

Typedefs

Enumerations

Functions

Variables

Define Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation

Variable Documentation