src/calBdd/calInteract.c

Go to the documentation of this file.

#include "calInt.h"

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

#if SIZEOF_LONG == 8
#define BPL 64
#define LOGBPL 6
#else
#define BPL 32
#define LOGBPL 5
#endif

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


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


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


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


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

static void ddSuppInteract(Cal_BddManager_t *bddManager, Cal_Bdd_t f, int *support);
static void ddClearLocal(Cal_Bdd_t f);
static void ddUpdateInteract(Cal_BddManager_t *bddManager, int *support);

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


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


void
CalSetInteract(Cal_BddManager_t *bddManager, int x, int y)
{
    int posn, word, bit;

    Cal_Assert(x < y);
    Cal_Assert(y < bddManager->numVars);
    Cal_Assert(x >= 0);

    posn = ((((bddManager->numVars << 1) - x - 3) * x) >> 1) + y - 1;
    word = posn >> LOGBPL;
    bit = posn & (BPL-1);
    bddManager->interact[word] |= 1 << bit;

} /* end of CalSetInteract */


int
CalTestInteract(Cal_BddManager_t *bddManager, int x, int y)
{
    int posn, word, bit, result;

    x -= 1; 
    y -= 1;
    
    if (x > y) {
        int tmp = x;
        x = y;
        y = tmp;
    }
    Cal_Assert(x < y);
    Cal_Assert(y < bddManager->numVars);
    Cal_Assert(x >= 0);

    posn = ((((bddManager->numVars << 1) - x - 3) * x) >> 1) + y - 1;
    word = posn >> LOGBPL;
    bit = posn & (BPL-1);
    result = (bddManager->interact[word] >> bit) & 1;
    return(result);

} /* end of CalTestInteract */


int
CalInitInteract(Cal_BddManager_t *bddManager)
{
  int i,k;
  int words;
  long *interact;
  int *support;
  long numBins;
  CalBddNode_t **bins, *bddNode, *nextBddNode;
  
  int n = bddManager->numVars;
  
  words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
  bddManager->interact = interact = Cal_MemAlloc(long, words);
  if (interact == NULL) return(0);
  for (i = 0; i < words; i++) {
      interact[i] = 0;
  }
  
  support = Cal_MemAlloc(int, n);
  if (support == Cal_Nil(int)) {
    Cal_MemFree(interact);
    return(0);
  }
  bins = bddManager->uniqueTable[0]->bins;
  numBins = bddManager->uniqueTable[0]->numBins;
  for (i=0; i<numBins; i++){
    for (bddNode = bins[i]; bddNode; bddNode = nextBddNode) {
      Cal_Bdd_t internalBdd;
      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
      CalBddNodeGetThenBdd(bddNode, internalBdd);
      for (k = 0; k < n; k++) {
        support[k] = 0;
      }
      ddSuppInteract(bddManager, internalBdd, support);
      ddClearLocal(internalBdd);
      ddUpdateInteract(bddManager, support);
    }
  }
  /* If there are some results pending in the pipeline, we need to
     take those into account as well */

  if (bddManager->pipelineState == CREATE){
    CalRequestNode_t **requestNodeListArray =
        bddManager->requestNodeListArray; 
    Cal_Bdd_t resultBdd;
    for (i=0;
         i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
         i++){
      for (bddNode = *requestNodeListArray; bddNode;
           bddNode = nextBddNode){ 
        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
        Cal_Assert(CalBddNodeIsForwarded(bddNode));
        CalBddNodeGetThenBdd(bddNode, resultBdd);
        Cal_Assert(CalBddIsForwarded(resultBdd) == 0);
        for (k = 0; k < n; k++) {
          support[k] = 0;
        }
        ddSuppInteract(bddManager, resultBdd, support);
        ddClearLocal(resultBdd);
        ddUpdateInteract(bddManager, support);
      }
      requestNodeListArray++;
    }
  }
  
  
  Cal_MemFree(support);
  return(1);
  
} /* end of CalInitInteract */


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


static void
ddSuppInteract(Cal_BddManager_t *bddManager, Cal_Bdd_t f, int *support)
{
  Cal_Bdd_t thenBdd, elseBdd;

  if (CalBddIsBddConst(f) || CalBddIsMarked(f)){
    return;
  }
  support[f.bddId-1] = 1;
  CalBddGetThenBdd(f, thenBdd);
  CalBddGetElseBdd(f, elseBdd);
  ddSuppInteract(bddManager, thenBdd, support);
  ddSuppInteract(bddManager, elseBdd, support);
  CalBddMark(f);
  return;
} /* end of ddSuppInteract */


static void
ddClearLocal(Cal_Bdd_t f)
{
  Cal_Bdd_t thenBdd;
  Cal_Bdd_t elseBdd;
  CalBddGetElseBdd(f, elseBdd);  
  if (CalBddIsBddConst(f) || !CalBddIsMarked(f)){
    return;
  }
  /* clear visited flag */
  CalBddUnmark(f);
  CalBddGetThenBdd(f, thenBdd);
  CalBddGetElseBdd(f, elseBdd);
  ddClearLocal(thenBdd);
  ddClearLocal(elseBdd);
  return;
} /* end of ddClearLocal */


static void
ddUpdateInteract(Cal_BddManager_t *bddManager, int *support)
{
  int i,j;
  int n = bddManager->numVars;
  
  for (i = 0; i < n-1; i++) {
        if (support[i] == 1) {
      for (j = i+1; j < n; j++) {
                if (support[j] == 1) {
          CalSetInteract(bddManager, i, j);
                }
      }
        }
  }
} /* end of ddUpdateInteract */

---