view release on metacpan or  search on metacpan

XS.xs  view on Meta::CPAN

  // DONT USE ´ret = bdd_makeset(body + offset, size);´ (it uses index
  // not variables)

  bdd_addref (ret);
  for (i = size - 1; i >= 0; i--)
    {

      CHECK_BDD (body[offset + i]);

      tmp = bdd_apply (ret, body[offset + i], bddop_and);
      bdd_addref (tmp);
      bdd_delref (ret);
      ret = tmp;
    }

  return ret;
}

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;
    }
}

XS.xs  view on Meta::CPAN

PROTOTYPES: DISABLE

void 
reorder_setMethod(method)
   int method
PPCODE:
{
  if (method >= 0 && method < MAX_REORDERING_METHODS)
    current_reordering_method = reordering_method_table[method];
}

void reorder_now()
PPCODE:
{
  bdd_reorder (current_reordering_method);
}

void reorder_createVariableGroup(first, last, fix)
   int first
   int last
   int fix
PPCODE:
{
  bdd_intaddvarblock (first, last,
		      fix ? BDD_REORDER_FIXED : BDD_REORDER_FREE);
}

int internal_index(bdd) 
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  RETVAL = (bdd < varcount * 2) ? (bdd / 2 - 1) : bddlevel2var[LEVEL (bdd)];
}
OUTPUT:
RETVAL

void printSet(bdd)
   int bdd;
PPCODE:
{

  char *txt;
  int i;


  CHECK_BDD (bdd);


  if (bdd < 2)
    {
      printf ("\n%s\n", bdd == 0 ? "False" : "True");
      return;
    }

  txt = (char *) malloc (bddvarnum + 2);
  if (!txt)
    {
      bdd_error (BDD_MEMORY);
      return;
    }

  for (i = 0; i < varcount; i++)
    txt[i] = '-';
  txt[i] = '\0';

  printf ("\n");
  printSet_rec (txt, 0, bdd);

  free (txt);
  fflush(stdout);
}

void init(varnum_, node_count)
   int varnum_
   int node_count
PPCODE:
{
  int ok;
  long nodenum, cachesize;

  if (node_count < MIN_NODES)
    node_count = MIN_NODES;
  else if (node_count > MAX_NODES)
    {
      fprintf (stderr,
	       "[JBDD:init()] Number of nodes should be between %d and %d	nodes\n",
	       MIN_NODES, MAX_NODES);
      exit (20);
    }

  nodenum = node_count;
  cachesize = nodenum / 8;	// WAS: 10


  if (has_bdd)
    {
      fprintf (stderr,
	       "A BDD package exist while you are trying to create another one\n"
	       "The BDD package is SINGLETON!\n");

      exit (20);
    }

  ok = bdd_init (nodenum, cachesize);
  if (ok == 0)
    {
      varnum = varnum_;
      varcount = 0;

      bdd_setmaxincrease (MAX_NODE_INCREASE);
      bdd_setvarnum (2 + 2 * varnum);
      has_bdd = 1;


       if (bdd_false () != 0 || bdd_true () != 1)
	{
	  fprintf (stderr, " INTERNAL ERROR : false = %d, true = %d\n",
		   bdd_false (), bdd_true ());
	  exit (20);
	}

    }
  else
    {
      fprintf (stderr, "bdd_init(%ld,%ld) Failed\n (error code %d)\n",
	       nodenum, cachesize, ok);
      exit (20);
    }
}

void kill ()
PPCODE:
{
  if (has_bdd)
    {
      bdd_done ();
      has_bdd = 0;
    }
  else
    fprintf (stderr, "Killing already dead BDD class :(\n");
}


int getOne()
CODE:
{
  BDD ret = bdd_true ();

  CHECK_BDD (ret);

  RETVAL = ret;
}
OUTPUT:
RETVAL

int getZero()
CODE:
{
  BDD ret = bdd_false ();

  CHECK_BDD (ret);

  RETVAL=ret;
}
OUTPUT:
RETVAL


int createBDD()
CODE:
{
  BDD ret;

  if (varcount >= varnum)
    {
      fprintf (stderr, "Maximum var count (%d) reached!!\n", varnum);
      exit (20);
    }

  ret = bdd_ithvar (varcount++);
  // bddnodes[ret].refcou = 1;	// why does BuDDy sets the initial
  // refcount to MAXREF (0x3FF) ?

  RETVAL=ret;
}