src/cmuBdd/bddprprofile.c

Go to the documentation of this file.

/* BDD library profile printing routines */


#include "bddint.h"
#if STDC_HEADERS
#include <string.h>
#endif

static char profile_width[]="XXXXXXXXX";


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

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


/* cmu_bdd_print_profile_aux(bddm, level_counts, var_naming_fn, line_length, */
/* env, fp) prints a profile to the file given by fp.  The var_naming_fn */
/* is as in cmu_bdd_print_bdd.  line_length gives the line width to scale the */
/* profile to. */

void
cmu_bdd_print_profile_aux(cmu_bdd_manager bddm,
                      long *level_counts,
                      char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                      pointer env,
                      int line_length,
                      FILE *fp)
{
  long i, n;
  int l;
  char *name;
  int max_prefix_len;
  int max_profile_width;
  int histogram_column;
  int histogram_width;
  int profile_scale;
  long total;

  n=bddm->vars;
  /* max_... initialized with values for leaf nodes */
  max_prefix_len=5;
  max_profile_width=level_counts[n];
  total=level_counts[n];
  for (i=0; i < n; ++i)
    if (level_counts[i])
      {
        sprintf(profile_width, "%ld", level_counts[i]);
        l=strlen(bdd_var_name(bddm, bddm->variables[bddm->indexindexes[i]], var_naming_fn, env))+strlen(profile_width);
        if (l > max_prefix_len)
          max_prefix_len=l;
        if (level_counts[i] > max_profile_width)
          max_profile_width=level_counts[i];
        total+=level_counts[i];
      }
  histogram_column=max_prefix_len+3;
  histogram_width=line_length-histogram_column-1;
  if (histogram_width < 20)
    histogram_width=20;         /* Random minimum width */
  if (histogram_width >= max_profile_width)
    profile_scale=1;
  else
    profile_scale=(max_profile_width+histogram_width-1)/histogram_width;
  for (i=0; i < n; ++i)
    if (level_counts[i])
      {
        name=bdd_var_name(bddm, bddm->variables[bddm->indexindexes[i]], var_naming_fn, env);
        fputs(name, fp);
        fputc(':', fp);
        sprintf(profile_width, "%ld", level_counts[i]);
        chars(' ', (int)(max_prefix_len-strlen(name)-strlen(profile_width)+1), fp);
        fputs(profile_width, fp);
        fputc(' ', fp);
        chars('#', level_counts[i]/profile_scale, fp);
        fputc('\n', fp);
      }
  fputs("leaf:", fp);
  sprintf(profile_width, "%ld", level_counts[n]);
  chars(' ', (int)(max_prefix_len-4-strlen(profile_width)+1), fp);
  fputs(profile_width, fp);
  fputc(' ', fp);
  chars('#', level_counts[n]/profile_scale, fp);
  fputc('\n', fp);
  fprintf(fp, "Total: %ld\n", total);
}


/* cmu_bdd_print_profile(bddm, f, var_naming_fn, env, line_length, fp) displays */
/* the node profile for f on fp.  line_length specifies the maximum line */
/* length.  var_naming_fn is as in cmu_bdd_print_bdd. */

void
cmu_bdd_print_profile(cmu_bdd_manager bddm,
                  bdd f,
                  char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                  pointer env,
                  int line_length,
                  FILE *fp)
{
  long *level_counts;

  if (bdd_check_arguments(1, f))
    {
      level_counts=(long *)mem_get_block((SIZE_T)((bddm->vars+1)*sizeof(long)));
      cmu_bdd_profile(bddm, f, level_counts, 1);
      cmu_bdd_print_profile_aux(bddm, level_counts, var_naming_fn, env, line_length, fp);
      mem_free_block((pointer)level_counts);
    }
  else
    fputs("overflow\n", fp);
}


/* cmu_bdd_print_profile_multiple is like cmu_bdd_print_profile except it displays */
/* the profile for a set of BDDs. */

void
cmu_bdd_print_profile_multiple(cmu_bdd_manager bddm,
                           bdd* fs,
                           char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                           pointer env,
                           int line_length,
                           FILE *fp)
{
  long *level_counts;

  bdd_check_array(fs);
  level_counts=(long *)mem_get_block((SIZE_T)((bddm->vars+1)*sizeof(long)));
  cmu_bdd_profile_multiple(bddm, fs, level_counts, 1);
  cmu_bdd_print_profile_aux(bddm, level_counts, var_naming_fn, env, line_length, fp);
  mem_free_block((pointer)level_counts);
}


/* cmu_bdd_print_function_profile is like cmu_bdd_print_profile except it displays */
/* a function profile for f. */

void
cmu_bdd_print_function_profile(cmu_bdd_manager bddm,
                           bdd f,
                           char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                           pointer env,
                           int line_length,
                           FILE *fp)
{
  long *level_counts;

  if (bdd_check_arguments(1, f))
    {
      level_counts=(long *)mem_get_block((SIZE_T)((bddm->vars+1)*sizeof(long)));
      cmu_bdd_function_profile(bddm, f, level_counts);
      cmu_bdd_print_profile_aux(bddm, level_counts, var_naming_fn, env, line_length, fp);
      mem_free_block((pointer)level_counts);
    }
  else
    fputs("overflow\n", fp);
}


/* cmu_bdd_print_function_profile_multiple is like cmu_bdd_print_function_profile */
/* except for multiple BDDs. */

void
cmu_bdd_print_function_profile_multiple(cmu_bdd_manager bddm,
                                    bdd* fs,
                                    char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
                                    pointer env,
                                    int line_length,
                                    FILE *fp)
{
  long *level_counts;

  bdd_check_array(fs);
  level_counts=(long *)mem_get_block((SIZE_T)((bddm->vars+1)*sizeof(long)));
  cmu_bdd_function_profile_multiple(bddm, fs, level_counts);
  cmu_bdd_print_profile_aux(bddm, level_counts, var_naming_fn, env, line_length, fp);
  mem_free_block((pointer)level_counts);
}

---