source: vis_dev/glu-2.3/src/cmuBdd/bddmisc.c @ 43

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

library glu 2.3

File size: 2.2 KB
Line 
1/* Support functions need by miscellaneous BDD routines */
2
3
4#include "bddint.h"
5
6
7void
8bdd_mark_shared_nodes(cmu_bdd_manager bddm, bdd f)
9{
10  BDD_SETUP(f);
11  f=BDD_OUTPOS(f);
12  if (BDD_IS_CONST(f) || cmu_bdd_type_aux(bddm, f) == BDD_TYPE_POSVAR)
13    return;
14  if (BDD_MARK(f))
15    {
16      if (BDD_MARK(f) == 1)
17        BDD_MARK(f)=2;
18      return;
19    }
20  BDD_MARK(f)=1;
21  bdd_mark_shared_nodes(bddm, BDD_THEN(f));
22  bdd_mark_shared_nodes(bddm, BDD_ELSE(f));
23}
24
25
26void
27bdd_number_shared_nodes(cmu_bdd_manager bddm, bdd f, hash_table h, long *next)
28{
29  BDD_SETUP(f);
30  if (BDD_IS_CONST(f) || ((1 << cmu_bdd_type_aux(bddm, f)) & ((1 << BDD_TYPE_POSVAR) | (1 << BDD_TYPE_NEGVAR))))
31    return;
32  if (BDD_MARK(f) == 0)
33    return;
34  if (BDD_MARK(f) == 2)
35    {
36      bdd_insert_in_hash_table(h, f, (pointer)next);
37      ++*next;
38    }
39  BDD_MARK(f)=0;
40  bdd_number_shared_nodes(bddm, BDD_THEN(f), h, next);
41  bdd_number_shared_nodes(bddm, BDD_ELSE(f), h, next);
42}
43
44
45static char default_terminal_id[]="terminal XXXXXXXXXX XXXXXXXXXX";
46static char default_var_name[]="var.XXXXXXXXXX";
47
48
49char *
50bdd_terminal_id(cmu_bdd_manager bddm, bdd f, char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer), pointer env)
51{
52  char *id;
53  INT_PTR v1, v2;
54
55  cmu_mtbdd_terminal_value_aux(bddm, f, &v1, &v2);
56  if (terminal_id_fn)
57    id=(*terminal_id_fn)(bddm, v1, v2, env);
58  else
59    id=0;
60  if (!id)
61    {
62      if (f == BDD_ONE(bddm))
63        return ("1");
64      if (f == BDD_ZERO(bddm))
65        return ("0");
66      sprintf(default_terminal_id, "terminal %ld %ld", (long)v1, (long)v2);
67      id=default_terminal_id;
68    }
69  return (id);
70}
71
72
73char *
74bdd_var_name(cmu_bdd_manager bddm, bdd v, char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer), pointer env)
75{
76  char *name;
77
78  if (var_naming_fn)
79    name=(*var_naming_fn)(bddm, v, env);
80  else
81    name=0;
82  if (!name)
83    {
84      BDD_SETUP(v);
85      sprintf(default_var_name, "var.%d", BDD_INDEX(bddm, v));
86      name=default_var_name;
87    }
88  return (name);
89}
90
91
92void
93cmu_mtbdd_terminal_value_aux(cmu_bdd_manager bddm, bdd f, INT_PTR *value1, INT_PTR *value2)
94{
95  BDD_SETUP(f);
96  if (BDD_IS_OUTPOS(f))
97    {
98      *value1=BDD_DATA0(f);
99      *value2=BDD_DATA1(f);
100    }
101  else
102    (*bddm->transform_fn)(bddm, BDD_DATA0(f), BDD_DATA1(f), value1, value2, bddm->transform_env);
103}
Note: See TracBrowser for help on using the repository browser.