src/calBdd/calBddSupport.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 Cal_Bdd_t * CalBddSupportStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * support);
static void CalBddUnmarkNodes(Cal_BddManager_t * bddManager, Cal_Bdd_t f);
static int CalBddDependsOnStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_BddIndex_t varIndex, int mark);

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

void
Cal_BddSupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
               Cal_Bdd *support)
{
  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
    Cal_Bdd_t *internalSupport = Cal_MemAlloc(Cal_Bdd_t, bddManager->numVars+1);
    Cal_Bdd_t *end;
    int i = 0;
    end = CalBddSupportStep(bddManager, f, internalSupport);
    *end = CalBddNull(bddManager);
    CalBddUnmarkNodes(bddManager, f);
    while (CalBddIsBddNull(bddManager, internalSupport[i]) == 0){
      *support = CalBddGetExternalBdd(bddManager, internalSupport[i]);
      support++;
      i++;
    }
    Cal_MemFree(internalSupport);
  }
  *support = (Cal_Bdd) 0;
}

int
Cal_BddDependsOn(Cal_BddManager bddManager, Cal_Bdd  fUserBdd,
                 Cal_Bdd varUserBdd)
{
  Cal_BddIndex_t bddIndex;
  Cal_Bdd_t f, var;
  
  if(CalBddPreProcessing(bddManager, 2, fUserBdd, varUserBdd)){
    f = CalBddGetInternalBdd(bddManager, fUserBdd);
    var = CalBddGetInternalBdd(bddManager, varUserBdd);
    if(CalBddIsBddConst(var)){
      return 1;
    }
    bddIndex = CalBddGetBddIndex(bddManager, var);
    CalBddDependsOnStep(bddManager, f, bddIndex, 1);
    return CalBddDependsOnStep(bddManager, f, bddIndex, 0);
  }
  return (0);
}


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

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

static Cal_Bdd_t *
CalBddSupportStep(
  Cal_BddManager_t * bddManager,
  Cal_Bdd_t  f,
  Cal_Bdd_t * support)
{
  Cal_Bdd_t tempBdd;

  if(CalBddIsMarked(f) || CalBddIsBddConst(f)){
    return support;
  }
  tempBdd = bddManager->varBdds[CalBddGetBddId(f)];
  if(!CalBddIsMarked(tempBdd)){
    CalBddMark(tempBdd);
    *support = tempBdd;
    ++support;
  }
  CalBddMark(f);
  CalBddGetThenBdd(f, tempBdd);
  support = CalBddSupportStep(bddManager, tempBdd, support);
  CalBddGetElseBdd(f, tempBdd);
  return CalBddSupportStep(bddManager, tempBdd, support);
}


static void
CalBddUnmarkNodes(
  Cal_BddManager_t * bddManager,
  Cal_Bdd_t  f)
{
  Cal_Bdd_t tempBdd;

  if(!CalBddIsMarked(f) || CalBddIsBddConst(f)){
    return;
  }
  CalBddUnmark(f);
  tempBdd = bddManager->varBdds[CalBddGetBddId(f)];
  CalBddUnmark(tempBdd);
  CalBddGetThenBdd(f, tempBdd);
  CalBddUnmarkNodes(bddManager, tempBdd);
  CalBddGetElseBdd(f, tempBdd);
  CalBddUnmarkNodes(bddManager, tempBdd);
}


static int
CalBddDependsOnStep(
  Cal_BddManager_t * bddManager,
  Cal_Bdd_t  f,
  Cal_BddIndex_t  varIndex,
  int  mark)
{
  Cal_BddIndex_t fIndex;
  Cal_Bdd_t tempBdd;

  fIndex=CalBddGetBddIndex(bddManager, f);
  if(fIndex > varIndex){
    return 0;
  }
  if(fIndex == varIndex){
    return 1;
  }
  if((mark && CalBddIsMarked(f)) || (!mark && !CalBddIsMarked(f))){
    return (0);
  }
  if(mark){
    CalBddMark(f);
  }
  else{
    CalBddUnmark(f);
  }
  CalBddGetThenBdd(f, tempBdd);
  if(CalBddDependsOnStep(bddManager, tempBdd, varIndex, mark)){
    return 1;
  }
  CalBddGetElseBdd(f, tempBdd);
  return CalBddDependsOnStep(bddManager, tempBdd, varIndex, mark);
}

---