source: vis_dev/glu-2.3/src/cmuBdd/bddprint.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 3.5 KB
RevLine 
[13]1/* BDD library print routines */
2
3
4#include "bddint.h"
5
6
7static
8void
9chars(char c, int n, FILE *fp)
10{
11  int i;
12
13  for (i=0; i < n; ++i)
14    fputc(c, fp);
15}
16
17
18static
19void
20bdd_print_top_var(cmu_bdd_manager bddm,
21                  bdd f,
22                  char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
23                  pointer env,
24                  FILE *fp)
25{
26  BDD_SETUP(f);
27  fputs(bdd_var_name(bddm, BDD_IF(bddm, f), var_naming_fn, env), fp);
28  fputc('\n', fp);
29}
30
31
32static
33void
34cmu_bdd_print_bdd_step(cmu_bdd_manager bddm,
35                   bdd f,
36                   char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
37                   char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer),
38                   pointer env,
39                   FILE *fp,
40                   hash_table h,
41                   int indentation)
42{
43  int negated;
44  long *number;
45
46  BDD_SETUP(f);
47  chars(' ', indentation, fp);
48  switch (cmu_bdd_type_aux(bddm, f))
49    {
50    case BDD_TYPE_ZERO:
51    case BDD_TYPE_ONE:
52    case BDD_TYPE_CONSTANT:
53      fputs(bdd_terminal_id(bddm, f, terminal_id_fn, env), fp);
54      fputc('\n', fp);
55      break;
56    case BDD_TYPE_NEGVAR:
57      fputc('!', fp);
58      /* fall through */
59    case BDD_TYPE_POSVAR:
60      bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
61      break;
62    case BDD_TYPE_NONTERMINAL:
63      if (bdd_lookup_in_hash_table(h, BDD_NOT(f)))
64        {
65          f=BDD_NOT(f);
66          negated=1;
67        }
68      else
69        negated=0;
70      number=(long *)bdd_lookup_in_hash_table(h, f);
71      if (number && *number < 0)
72        {
73          if (negated)
74            fputc('!', fp);
75          fprintf(fp, "subformula %ld\n", -*number-1);
76        }
77      else
78        {
79          if (number)
80            {
81              fprintf(fp, "%ld: ", *number);
82              *number= -*number-1;
83            }
84          fputs("if ", fp);
85          bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
86          cmu_bdd_print_bdd_step(bddm, BDD_THEN(f), var_naming_fn, terminal_id_fn, env, fp, h, indentation+2);
87          chars(' ', indentation, fp);
88          fputs("else if !", fp);
89          bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
90          cmu_bdd_print_bdd_step(bddm, BDD_ELSE(f), var_naming_fn, terminal_id_fn, env, fp, h, indentation+2);
91          chars(' ', indentation, fp);
92          fputs("endif ", fp);
93          bdd_print_top_var(bddm, f, var_naming_fn, env, fp);
94        }
95      break;
96    default:
97      cmu_bdd_fatal("cmu_bdd_print_bdd_step: unknown type returned by cmu_bdd_type");
98    }
99}
100
101
102/* cmu_bdd_print_bdd(bddm, f, var_naming_fn, terminal_id_fn, env, fp) prints a */
103/* human-readable representation of f to the file given by fp.  If */
104/* var_naming_fn is non-null, it should be a pointer to a function that */
105/* assigns names to BDD variables.  It is passed bddm, a BDD representing */
106/* a variable, and the pointer given by env, and should return a string */
107/* giving the name of the variable or null.  If terminal_id_fn is */
108/* non-null, it should be a pointer to a function that formats terminal */
109/* nodes.  It is passed bddm, two longs representing the data value of */
110/* the terminal node, and env.  It should return a string for the */
111/* terminal node, or null. */
112
113void
114cmu_bdd_print_bdd(cmu_bdd_manager bddm,
115              bdd f,
116              char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer),
117              char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer),
118              pointer env,
119              FILE *fp)
120{
121  long next;
122  hash_table h;
123
124  if (!bdd_check_arguments(1, f))
125    {
126      fprintf(fp, "overflow\n");
127      return;
128    }
129  bdd_mark_shared_nodes(bddm, f);
130  h=bdd_new_hash_table(bddm, sizeof(long));
131  next=0;
132  bdd_number_shared_nodes(bddm, f, h, &next);
133  cmu_bdd_print_bdd_step(bddm, f, var_naming_fn, terminal_id_fn, env, fp, h, 0);
134  cmu_bdd_free_hash_table(h);
135}
Note: See TracBrowser for help on using the repository browser.