src/cmuBdd/bddprint.c File Reference

#include "bddint.h"

Include dependency graph for bddprint.c:

Go to the source code of this file.

Functions
static void	chars (char c, int n, FILE *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)
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)
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)

---

Function Documentation

static void bdd_print_top_var	(	cmu_bdd_manager	bddm,
		bdd	f,
		char *(*)(cmu_bdd_manager, bdd, pointer)	var_naming_fn,
		pointer	env,
		FILE *	fp
	)			[static]

Definition at line 20 of file bddprint.c.

{
  BDD_SETUP(f);
  fputs(bdd_var_name(bddm, BDD_IF(bddm, f), var_naming_fn, env), fp);
  fputc('\n', fp);
}

static void chars	(	char	c,
		int	n,
		FILE *	fp
	)			[static]

Definition at line 9 of file bddprint.c.

{
  int i;

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

void cmu_bdd_print_bdd	(	cmu_bdd_manager	bddm,
		bdd	f,
		char *(*)(cmu_bdd_manager, bdd, pointer)	var_naming_fn,
		char *(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer)	terminal_id_fn,
		pointer	env,
		FILE *	fp
	)

Definition at line 114 of file bddprint.c.

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

static void cmu_bdd_print_bdd_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		char *(*)(cmu_bdd_manager, bdd, pointer)	var_naming_fn,
		char *(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer)	terminal_id_fn,
		pointer	env,
		FILE *	fp,
		hash_table	h,
		int	indentation
	)			[static]

Definition at line 34 of file bddprint.c.

{
  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");
    }
}