src/calBdd/calHashTableThree.c

Go to the documentation of this file.

#include "calInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/
#ifdef USE_POWER_OF_2
#define CalDoHash3(fBddNode, gBddNode, hBddNode,table) \
((((CalAddress_t)fBddNode + \
   (CalAddress_t)gBddNode + \
   (CalAddress_t) hBddNode) \
  / NODE_SIZE) & ((table)->numBins-1))
#else
#define CalDoHash3(fBddNode, gBddNode, hBddNode,table) \
  ((((CalAddress_t)fBddNode + \
  (CalAddress_t)gBddNode + \
  (CalAddress_t) hBddNode) \
  / NODE_SIZE)% table->numBins)
#endif

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void CalHashTableThreeRehash(CalHashTable_t *hashTable, int grow);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/
int
CalHashTableThreeFindOrAdd(CalHashTable_t * hashTable,
                           Cal_Bdd_t  f,
                           Cal_Bdd_t  g,
                           Cal_Bdd_t  h,
                           Cal_Bdd_t * bddPtr)
{
  CalBddNode_t *ptr, *ptrIndirect;
  Cal_Bdd_t tmpBdd;
  int hashValue;
  
  hashValue = CalDoHash3(CalBddGetBddNode(f), 
      CalBddGetBddNode(g), CalBddGetBddNode(h), hashTable);
  ptr = hashTable->bins[hashValue];
  while(ptr != Cal_Nil(CalBddNode_t)){
    CalBddNodeGetThenBdd(ptr, tmpBdd);
    if(CalBddIsEqual(f, tmpBdd)){
      ptrIndirect = CalBddNodeGetElseBddNode(ptr);
      CalBddNodeGetThenBdd(ptrIndirect, tmpBdd);
      if(CalBddIsEqual(g, tmpBdd)){
        CalBddNodeGetElseBdd(ptrIndirect, tmpBdd);
        if(CalBddIsEqual(h, tmpBdd)){
          CalBddPutBddId(*bddPtr, hashTable->bddId);
          CalBddPutBddNode(*bddPtr, ptr);
          return 1;
        }
      }
    }
    ptr = CalBddNodeGetNextBddNode(ptr);
  }
  hashTable->numEntries++;
  if(hashTable->numEntries > hashTable->maxCapacity){
    CalHashTableThreeRehash(hashTable,1);
    hashValue = CalDoHash3(CalBddGetBddNode(f),
        CalBddGetBddNode(g), CalBddGetBddNode(h), hashTable);
  }
  CalNodeManagerAllocNode(hashTable->nodeManager, ptr);
  CalNodeManagerAllocNode(hashTable->nodeManager, ptrIndirect);
  CalBddNodePutThenBdd(ptr, f);
  CalBddNodePutThenBdd(ptrIndirect, g);
  CalBddNodePutElseBdd(ptrIndirect, h);
  CalBddNodePutElseBddNode(ptr, ptrIndirect);
  CalBddNodePutNextBddNode(ptr, hashTable->bins[hashValue]);
  hashTable->bins[hashValue] = ptr;
  CalBddPutBddId(*bddPtr, hashTable->bddId);
  CalBddPutBddNode(*bddPtr, ptr);
  return 0;
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/
static void
CalHashTableThreeRehash(CalHashTable_t *hashTable, int grow)
{
  CalBddNode_t *ptr, *ptrIndirect, *next;
  CalBddNode_t **oldBins = hashTable->bins;
  int i, hashValue;
  int oldNumBins = hashTable->numBins;

  if(grow){
    hashTable->sizeIndex++;
  }
  else{
    if (hashTable->sizeIndex <= HASH_TABLE_DEFAULT_SIZE_INDEX){/* No need to rehash */
      return;
    }
    hashTable->sizeIndex--;
  }

  hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
  hashTable->numBins = hashTable->numBins;
  hashTable->maxCapacity = hashTable->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY;
  hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
  if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
    CalBddFatalMessage("out of memory");
  }
  for(i = 0; i < hashTable->numBins; i++){
    hashTable->bins[i] = Cal_Nil(CalBddNode_t);
  }

  for(i = 0; i < oldNumBins; i++){
    ptr = oldBins[i];
    while(ptr != Cal_Nil(CalBddNode_t)){
      next = CalBddNodeGetNextBddNode(ptr);
      ptrIndirect = CalBddNodeGetElseBddNode(ptr);
      hashValue = CalDoHash3(CalBddNodeGetThenBddNode(ptr),
          CalBddNodeGetThenBddNode(ptrIndirect),
          CalBddNodeGetElseBddNode(ptrIndirect), hashTable);
      CalBddNodePutNextBddNode(ptr, hashTable->bins[hashValue]);
      hashTable->bins[hashValue] = ptr;
      ptr = next;
    }
  }
  Cal_MemFree(oldBins);
}

---