src/calBdd/calBddITE.c

Go to the documentation of this file.

#include "calInt.h"

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

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

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


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

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
Cal_Bdd
Cal_BddITE(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd,
           Cal_Bdd hUserBdd)
{
  Cal_Bdd_t result;
  Cal_Bdd userResult;
  Cal_Bdd_t F, G, H;
  if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd)){
    F = CalBddGetInternalBdd(bddManager, fUserBdd);
    G = CalBddGetInternalBdd(bddManager, gUserBdd);
    H = CalBddGetInternalBdd(bddManager, hUserBdd);
    result = CalBddOpITEBF(bddManager, F, G, H);
  }
  else {
    return (Cal_Bdd) 0;
  }
  userResult =  CalBddGetExternalBdd(bddManager, result);
  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
    Cal_BddFree(bddManager, userResult);
    Cal_BddManagerGC(bddManager);
    return (Cal_Bdd) 0;
  }
  return userResult;
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


void
CalRequestNodeListArrayITE(Cal_BddManager_t *bddManager,
                          CalRequestNode_t **requestNodeListArray)
{
  CalRequestNode_t *requestNode, *ptrIndirect;
  CalRequest_t F, G, H, result;
  int pipeDepth, bddId, bddIndex;
  CalHashTable_t **reqQueAtPipeDepth, *hashTable, *uniqueTableForId;
  CalHashTable_t ***reqQue = bddManager->reqQue;
  
  /* ReqQueInsertUsingReqListArray */
  for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
    reqQueAtPipeDepth = reqQue[pipeDepth];
    for(requestNode = requestNodeListArray[pipeDepth];
        requestNode != Cal_Nil(CalRequestNode_t);
        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
      CalRequestNodeGetThenRequest(requestNode, F);
      CalRequestIsForwardedTo(F);
      ptrIndirect = CalRequestNodeGetElseRequestNode(requestNode);
      CalRequestNodeGetThenRequest(ptrIndirect, G);
      CalRequestIsForwardedTo(G);
      CalRequestNodeGetElseRequest(ptrIndirect, H);
      CalRequestIsForwardedTo(H);
      CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], ptrIndirect);
      result = CalOpITE(bddManager, F, G, H, reqQueAtPipeDepth);
      CalRequestNodePutThenRequest(requestNode, result);
      CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
    }
  }

  /* ReqQueApply */
  for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
    bddId = bddManager->indexToId[bddIndex];
    for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
      reqQueAtPipeDepth = reqQue[pipeDepth];
      hashTable = reqQueAtPipeDepth[bddId];
      if(hashTable->numEntries){
        CalHashTableITEApply(bddManager, hashTable, reqQueAtPipeDepth);
      }
    }
  }

  /* ReqQueReduce */
  for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
    bddId = bddManager->indexToId[bddIndex];
    uniqueTableForId = bddManager->uniqueTable[bddId];
    for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
      hashTable = reqQue[pipeDepth][bddId];
      if(hashTable->numEntries){
        CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
      }
    }
  }

  /* ReqListArrayReqForward */
  for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
    for(requestNode = requestNodeListArray[pipeDepth];
        requestNode != Cal_Nil(CalRequestNode_t);
        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
      CalRequestNodeGetThenRequest(requestNode, result);
      CalRequestIsForwardedTo(result);
      CalRequestNodePutThenRequest(requestNode, result);
    }
  }

  /* ReqQueCleanUp */
  for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
    reqQueAtPipeDepth = reqQue[pipeDepth];
    for(bddId = 1; bddId <= bddManager->numVars; bddId++){
      CalHashTableCleanUp(reqQueAtPipeDepth[bddId]);
    }
  }
}

Cal_Bdd_t
CalBddOpITEBF(
  Cal_BddManager_t *bddManager,
  Cal_Bdd_t  f,
  Cal_Bdd_t  g,
  Cal_Bdd_t  h)
{
  Cal_Bdd_t result;
  Cal_BddId_t bddId;
  /*Cal_BddIndex_t minIndex;*/
  int minIndex;
  int bddIndex;
  CalHashTable_t *hashTable;
  CalHashTable_t *uniqueTableForId;
  CalHashTable_t **reqQueForITE = bddManager->reqQue[0];
  
  result = CalOpITE(bddManager, f, g, h, reqQueForITE);
  
  CalBddGetMinIndex3(bddManager, f, g, h, minIndex);
  /* ReqQueApply */
  for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
    bddId = bddManager->indexToId[bddIndex];
    hashTable = reqQueForITE[bddId];
    if(hashTable->numEntries){
      CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
    }
  }

  /* ReqQueReduce */
  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
    bddId = bddManager->indexToId[bddIndex];
    uniqueTableForId = bddManager->uniqueTable[bddId];
    hashTable = reqQueForITE[bddId];
    if(hashTable->numEntries){
      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
    }
  }

  CalRequestIsForwardedTo(result);

  /* Clean up */
  for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
    bddId = bddManager->indexToId[bddIndex];
    CalHashTableCleanUp(reqQueForITE[bddId]);
  }

  return result;
}

void
CalHashTableITEApply(
  Cal_BddManager_t *bddManager,
  CalHashTable_t *hashTable,
  CalHashTable_t **reqQueAtPipeDepth)
{
  int i, numBins = hashTable->numBins;
  CalBddNode_t **bins = hashTable->bins;
  CalRequestNode_t *requestNode;
  Cal_Bdd_t fx, gx, fxbar, gxbar, hx, hxbar, result;
  CalNodeManager_t *nodeManager = hashTable->nodeManager;
  
  for(i = 0; i < numBins; i++){
    for(requestNode = bins[i];
        requestNode != Cal_Nil(CalRequestNode_t);
        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
      /* Process the requestNode */
      CalITERequestNodeGetCofactors(bddManager, requestNode,
          fx, fxbar, gx, gxbar, hx, hxbar);
      result = CalOpITE(bddManager, fx, gx, hx, reqQueAtPipeDepth);
      CalBddIcrRefCount(result);
      CalRequestNodePutThenRequest(requestNode, result);
      result = CalOpITE(bddManager, fxbar, gxbar, hxbar, reqQueAtPipeDepth);
      CalBddIcrRefCount(result);
      CalNodeManagerFreeNode(nodeManager,
          CalRequestNodeGetElseRequestNode(requestNode));
      CalRequestNodePutElseRequest(requestNode, result);
    }
  }
}

Cal_Bdd_t
CalBddITE(Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G,
          Cal_Bdd_t H)
{
  Cal_Bdd_t result;
  result = CalBddOpITEBF(bddManager, F, G, H);
  CalBddIcrRefCount(result);
  return result;
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

---