view release on metacpan or  search on metacpan

XS.xs  view on Meta::CPAN

int checkBuddy() {
  int i;

  if (!checkBDD (0))
    {
      fprintf (stderr, "bdd FALSE failed sanity check\n");
      dumpBDD_info (0);
      return 0;
    }

  if (!checkBDD (1))
    {
      fprintf (stderr, "bdd TRUE failed sanity check\n");
      dumpBDD_info (1);
      return 0;
    }

  for (i = bddvarnum; i < bddvarnum; i++)
    {
      if (!checkBDD (2 * i + 2))
	{
	  dumpBDD_info (2 * i + 2);
	  printf ("bdd variable #%d failed sanity check\n", i);
	  return 0;
	}

      if (!checkBDD (2 * i + 3))
	{
	  printf ("shadow of bdd variable #%d failed sanity check\n", i);
	  dumpBDD_info (2 * i + 3);
	  return 0;
	}
    }

    return 1;
}

int checkBDD(int bdd)
{
  if (!bddrunning)
    {
      bdd_error (BDD_RUNNING);
      return 0;
    }
  if (bdd < 0 || (bdd) >= bddnodesize)
    {
      bdd_error (BDD_ILLBDD);
      return 0;
    }
  if (bdd >= 2 && LOW (bdd) == -1)
    {
      bdd_error (BDD_ILLBDD);
      return 0;
    }

  if (bddnodes[bdd].refcou == 0)
    {
      fprintf (stderr, "ERROR: refcount is zero\n");
      return 0;
    }
  // refcount for TRUE and FALSE is saturated by default, ignore them!
  if (bdd > 2 && bddnodes[bdd].refcou == MAXREF)
    {
      fprintf (stderr, "ERROR: refcount is saturated\n");
      return 0;
    }

  return 1;
}

void printSet_rec(char *txt, int level, int bdd)
 {

  if (bdd == 0)
    {
      /*
       * do nothing
       */
      return;
    }
  else if (bdd == 1)
    {
      printf ("%s	1\n", txt);
      return;
    }
  else
    {
      BDD low = LOW (bdd);
      BDD high = HIGH (bdd);
      int l;
      char save;


      // printf("BDD=%d/%d, LOW=%d, HIGH=%d\n", bdd,
      // bddlevel2var[LEVEL(bdd)], low, high);
      l = bdd < varcount * 2 ? bdd / 2 - 1 : bddlevel2var[LEVEL (bdd)];

      save = txt[l];
      txt[l] = '0';
      // printf("*L_low=%d\n", l);
      printSet_rec (txt, level + 1, low);
      txt[l] = save;


      save = txt[l];
      txt[l] = '1';
      // printf("*L_high=%d (%d)\n", l, varcount);
      printSet_rec (txt, level + 1, high);
      txt[l] = save;
    }
}

// XXX: we havent considred reordered variables yet!
// stuff like var2level() may be needed in some places when dynamic
// reordering is active!


// --- [ dynamic reordering ]
// --------------------------------------------------
#define MAX_REORDERING_METHODS		5
int reordering_method_table[MAX_REORDERING_METHODS] = {