src/calBdd/calBlk.c

Go to the documentation of this file.

#include "calInt.h"

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

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

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

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


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

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

static void AddBlock(Cal_Block b1, Cal_Block b2);

/* BDD variable block routines */
/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
Cal_Block
Cal_BddNewVarBlock(Cal_BddManager bddManager, Cal_Bdd variable, long length)
{
  Cal_Block b;
  Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, variable);
  
  if (CalBddTypeAux(bddManager, calBdd) != CAL_BDD_TYPE_POSVAR) {
    CalBddWarningMessage("Cal_BddNewVarBlock: second argument is not a positive variable\n"); 
    if (CalBddIsBddConst(calBdd)){
      return (Cal_Block) 0;
        }
  }

  /*b = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/
  b = Cal_MemAlloc(Cal_Block_t, 1);
  b->reorderable = 0;
  b->firstIndex = bddManager->idToIndex[calBdd.bddId];
  if (length <= 0) {
    CalBddWarningMessage("Cal_BddNewVarBlock: invalid final argument");
    length = 1;
  }
  b->lastIndex = b->firstIndex + length - 1;
  if (b->lastIndex >= bddManager->numVars) {
    CalBddWarningMessage("Cal_BddNewVarBlock: range covers non-existent variables"); 
    b->lastIndex = bddManager->numVars - 1;
  }
  AddBlock(bddManager->superBlock, b);
  return (b);
}
void
Cal_BddVarBlockReorderable(Cal_BddManager bddManager, Cal_Block block,
                           int reorderable)
{
  block->reorderable = reorderable;
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/
long
CalBddFindBlock(Cal_Block block, long index)
{
  long i, j, k;

  i = 0;
  j = block->numChildren-1;
  while (i <= j) {
    k = (i+j)/2;
    if (block->children[k]->firstIndex <= index &&
        block->children[k]->lastIndex >= index){
      return (k);
    }
    if (block->children[k]->firstIndex > index){
      j = k-1;
    }
    else {
      i = k+1;
    }
  }
  return i;
}

void
CalBddBlockDelta(Cal_Block b, long delta)
{
  long i;
  b->firstIndex += delta;
  b->lastIndex += delta;
  for (i=0; i < b->numChildren; ++i)
    CalBddBlockDelta(b->children[i], delta);
}


Cal_Block
CalBddShiftBlock(Cal_BddManager_t *bddManager, Cal_Block b, long index)
{
  long i, j;
  Cal_Block p;

  if (b->firstIndex >= index) {
    CalBddBlockDelta(b, 1l);
    return (b);
  }
  if (b->lastIndex < index) return (b);
  b->lastIndex++;
  i = CalBddFindBlock(b, index);
  if (i == b->numChildren || b->children[i]->firstIndex == index) {
    b->children = (Cal_Block *)
        Cal_MemRealloc(Cal_Block, b->children, b->numChildren+1);
    for (j = b->numChildren-1; j >= i; --j){
      b->children[j+1] = CalBddShiftBlock(bddManager, b->children[j], index);
    }
    b->numChildren++;
    /*p = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/
    p = Cal_MemAlloc(Cal_Block_t, 1);
    p->reorderable = 0;
    p->firstIndex = index;
    p->lastIndex = index;
    p->numChildren = 0;
    p->children = 0;
    b->children[i] = p;
  }
  else{
    while (i < b->numChildren) {
      CalBddShiftBlock(bddManager, b->children[i], index);
      ++i;
    }
  }
  return (b);
}
unsigned long
CalBlockMemoryConsumption(Cal_Block block)
{
  unsigned long totalBytes = 0;
  int i;
  
  totalBytes += sizeof(Cal_Block);
  for (i=0; i<block->numChildren; i++){
    totalBytes += CalBlockMemoryConsumption(block->children[i]);
  }
  return totalBytes;
}
void
CalFreeBlockRecursively(Cal_Block block)
{
  int i;
  
  for (i=0; i<block->numChildren; i++){
    CalFreeBlockRecursively(block->children[i]);
  }
  Cal_MemFree(block->children);
  Cal_MemFree(block);
}

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

static void
AddBlock(Cal_Block b1, Cal_Block b2)
{
  long i, j, k;
  Cal_Block start, end;

  if (b1->numChildren){
    i = CalBddFindBlock(b1, b2->firstIndex);
    start = b1->children[i];
    j = CalBddFindBlock(b1, b2->lastIndex);
    end = b1->children[j];
    if (i == j) {
      AddBlock(start, b2);
    }
    else {
      if (start->firstIndex != b2->firstIndex ||
          end->lastIndex != b2->lastIndex){
        CalBddFatalMessage("AddBlock: illegal block overlap");
      }
      b2->numChildren = j-i+1;
          b2->children = Cal_MemAlloc(Cal_Block, b2->numChildren); 
          for (k=0; k < b2->numChildren; ++k){
            b2->children[k] = b1->children[i+k];
      }
          b1->children[i] = b2;
          ++i;
          for (k=j+1; k < b1->numChildren; ++k, ++i){
            b1->children[i] = b1->children[k];
      }
          b1->numChildren -= (b2->numChildren-1);
          b1->children = (Cal_Block *)
          Cal_MemRealloc(Cal_Block, b1->children, b1->numChildren);
        }
  }
  else {
      /* b1 and b2 are blocks representing just single variables. */
      b1->numChildren = 1;
      b1->children = Cal_MemAlloc(Cal_Block, b1->numChildren); 
      b1->children[0] = b2;
      b2->numChildren = 0;
      b2->children = 0;
  }
}

---