src/calBdd/calBddReorderTest.c

Go to the documentation of this file.

#include "calInt.h"

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

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

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


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static CalAddress_t asDoubleSpace[2];

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

#define CalBddReorderBddIsForwarded(bdd) \
  (CAL_BDD_POINTER(CalBddGetElseBddNode(bdd)) == FORWARD_FLAG)

#define CalBddReorderBddNodeIsForwarded(bddNode) \
  (CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode)) == FORWARD_FLAG)

#define CalBddReorderForward(bdd) \
{ \
  CalBddNode_t *_bddNode, *_bddNodeTagged; \
  _bddNodeTagged = CalBddGetBddNode(bdd); \
  _bddNode = CAL_BDD_POINTER(_bddNodeTagged); \
  (bdd).bddId = _bddNode->thenBddId; \
  (bdd).bddNode = (CalBddNode_t*) \
                  (((CalAddress_t)(_bddNode->thenBddNode) & ~0xe) \
                   ^(CAL_TAG0(_bddNodeTagged))); \
}

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

static double cpuTime();
static long elapsedTime();

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


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

int
main(int argc, char **argv)
{
  Cal_Bdd expected;
  Cal_Bdd a[100];
  Cal_Bdd temp1;
  Cal_Bdd temp2;
  Cal_Bdd b, c, d, e, f, g, result;
  Cal_BddManager_t *bddManager;
  CalBddNode_t *bddNode;
  int i;
  int numVars;
  int siftFlag = 0;
  
  if (argc == 1) {
    numVars = 5;
  } else if (argc >= 2) {
    numVars = atoi(argv[1]);
  }
  if (argc == 3) {
    siftFlag = 1;
  }

  bddManager = Cal_BddManagerInit();

  for (i = 0; i < 2 * numVars; i++) {
    a[i] = Cal_BddManagerCreateNewVarLast(bddManager);
  }

  result = Cal_BddZero(bddManager);
  for (i = 0; i < numVars; i++) {
    temp1 = Cal_BddAnd(bddManager, a[i], a[numVars + i]);
    temp2 = Cal_BddOr(bddManager, result, temp1);
    Cal_BddFree(bddManager, temp1);
    Cal_BddFree(bddManager, result);
    result = temp2;
  }
  Cal_BddManagerGC(bddManager);
  Cal_BddStats(bddManager, stdout);
  cpuTime();
  elapsedTime();
  printf("%%%%%%%%%%%% Reordering %%%%%%%%%%%%%%%%%%%\n");
  if (siftFlag){
    printf("Using Sift Technique\n");
    Cal_BddDynamicReordering(bddManager, CAL_REORDER_SIFT);
  }
  else{
    printf("Using Window Technique\n");
    Cal_BddDynamicReordering(bddManager, CAL_REORDER_WINDOW);
  }
  Cal_BddReorder(bddManager);
  printf("CPU time: %-8.2f\t Elapsed Time = %-10ld\n", cpuTime(), elapsedTime());
  printf("%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%\n");
  Cal_BddManagerGC(bddManager);
  Cal_BddStats(bddManager, stdout);
  /*Cal_BddFunctionPrint(bddManager, result, "Result");*/
  temp1 = Cal_BddZero(bddManager);
  for (i = 0; i < numVars; i++) {
    temp2 = Cal_BddAnd(bddManager, a[i], a[numVars + i]);
    expected = Cal_BddOr(bddManager, temp1, temp2);
    Cal_BddFree(bddManager, temp1);
    Cal_BddFree(bddManager, temp2);
    temp1 = expected;
  }

  if (!Cal_BddIsEqual(bddManager, result, expected)) {
    printf("ERROR: BDDs are not equal\n");
    Cal_BddFunctionPrint(bddManager, result, "Result");
    Cal_BddFunctionPrint(bddManager, expected, "Expected");
  }
  printf("\n%%%%%%BDDs are equal\n");
  Cal_BddFree(bddManager, result);
  Cal_BddFree(bddManager, expected);
  Cal_BddManagerGC(bddManager);
  Cal_BddStats(bddManager, stdout);
  Cal_BddManagerQuit(bddManager);
}


static double
cpuTime()
{
  static double timeNew, timeOld;
  struct rusage rusage;
  static flag = 0;

  getrusage(RUSAGE_SELF, &rusage);
  if (flag == 0){
    timeOld = timeNew = rusage.ru_utime.tv_sec+
        ((double)rusage.ru_utime.tv_usec)/1000000;
    flag = 1;
  }
  else {
    timeOld = timeNew;
    timeNew = rusage.ru_utime.tv_sec+
        ((float)rusage.ru_utime.tv_usec)/1000000;
  }
  return timeNew - timeOld;
}

static long
elapsedTime()
{
  static long time_new, time_old;
  struct timeval t;
  struct timezone tz;
  static flag = 0;
  
  gettimeofday(&t, &tz);
  if (flag == 0){
    time_old = time_new = t.tv_sec;
    flag = 1;
  }
  else {
    time_old = time_new;
    time_new =  t.tv_sec;
  }
  return time_new-time_old;
}

---