src/cmuBdd/bddprint.c

Go to the documentation of this file.

/* BDD library print routines */


#include "bddint.h"


static
void
chars(char c, int n, FILE *fp)
{
  int i;

  for (i=0; i < n; ++i)
    fputc(c, fp);
}


static
void
bdd_print_top_var(cmu_bdd_manager bddm,
                  bdd f,
                  char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                  pointer env,
                  FILE *fp)
{
  BDD_SETUP(f);
  fputs(bdd_var_name(bddm, BDD_IF(bddm, f), var_naming_fn, env), fp);
  fputc('\n', fp);
}


static
void
cmu_bdd_print_bdd_step(cmu_bdd_manager bddm,
                   bdd f,
                   char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                   char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer),
                   pointer env,
                   FILE *fp,
                   hash_table h,
                   int indentation)
{
  int negated;
  long *number;

  BDD_SETUP(f);
  chars(' ', indentation, fp);
  switch (cmu_bdd_type_aux(bddm, f))
    {
    case BDD_TYPE_ZERO:
    case BDD_TYPE_ONE:
    case BDD_TYPE_CONSTANT:
      fputs(bdd_terminal_id(bddm, f, terminal_id_fn, env), fp);
      fputc('\n', fp);
      break;
    case BDD_TYPE_NEGVAR:
      fputc('!', fp);
      /* fall through */
    case BDD_TYPE_POSVAR:
      bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
      break;
    case BDD_TYPE_NONTERMINAL:
      if (bdd_lookup_in_hash_table(h, BDD_NOT(f)))
        {
          f=BDD_NOT(f);
          negated=1;
        }
      else
        negated=0;
      number=(long *)bdd_lookup_in_hash_table(h, f);
      if (number && *number < 0)
        {
          if (negated)
            fputc('!', fp);
          fprintf(fp, "subformula %ld\n", -*number-1);
        }
      else
        {
          if (number)
            {
              fprintf(fp, "%ld: ", *number);
              *number= -*number-1;
            }
          fputs("if ", fp);
          bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
          cmu_bdd_print_bdd_step(bddm, BDD_THEN(f), var_naming_fn, terminal_id_fn, env, fp, h, indentation+2);
          chars(' ', indentation, fp);
          fputs("else if !", fp);
          bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
          cmu_bdd_print_bdd_step(bddm, BDD_ELSE(f), var_naming_fn, terminal_id_fn, env, fp, h, indentation+2);
          chars(' ', indentation, fp);
          fputs("endif ", fp);
          bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
        }
      break;
    default:
      cmu_bdd_fatal("cmu_bdd_print_bdd_step: unknown type returned by cmu_bdd_type");
    }
}


/* cmu_bdd_print_bdd(bddm, f, var_naming_fn, terminal_id_fn, env, fp) prints a */
/* human-readable representation of f to the file given by fp.  If */
/* var_naming_fn is non-null, it should be a pointer to a function that */
/* assigns names to BDD variables.  It is passed bddm, a BDD representing */
/* a variable, and the pointer given by env, and should return a string */
/* giving the name of the variable or null.  If terminal_id_fn is */
/* non-null, it should be a pointer to a function that formats terminal */
/* nodes.  It is passed bddm, two longs representing the data value of */
/* the terminal node, and env.  It should return a string for the */
/* terminal node, or null. */

void
cmu_bdd_print_bdd(cmu_bdd_manager bddm,
              bdd f,
              char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
              char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer),
              pointer env,
              FILE *fp)
{
  long next;
  hash_table h;

  if (!bdd_check_arguments(1, f))
    {
      fprintf(fp, "overflow\n");
      return;
    }
  bdd_mark_shared_nodes(bddm, f);
  h=bdd_new_hash_table(bddm, sizeof(long));
  next=0;
  bdd_number_shared_nodes(bddm, f, h, &next);
  cmu_bdd_print_bdd_step(bddm, f, var_naming_fn, terminal_id_fn, env, fp, h, 0);
  cmu_bdd_free_hash_table(h);
}

---