source: vis_dev/glu-2.3/src/cmuBdd/mtbdd.c @ 23

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

library glu 2.3

File size: 6.1 KB
Line 
1/* Basic multi-terminal BDD routines */
2
3
4#include "bddint.h"
5
6
7/* mtbdd_transform_closure(bddm, canonical_fn, transform_fn, env) sets */
8/* the transformation for MTBDD terminal values for the "negative-output" */
9/* pointer flag.  The canonical_fn receives the BDD manager, two longs */
10/* representing the input value, and the value of env.  It should return */
11/* a non-zero value if the result needs to be transformed.  The */
12/* transform_fn receives the BDD manager, two longs (the input value), */
13/* pointers to two longs (for the output) and the value of env.  This */
14/* should not be called after any MTBDD terminals are created. */
15
16void
17mtbdd_transform_closure(cmu_bdd_manager bddm,
18                        int (*canonical_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer),
19                        void (*transform_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *, pointer),
20                        pointer transform_env)
21{
22  bddm->transform_fn=transform_fn;
23  bddm->transform_env=transform_env;
24  bddm->canonical_fn=canonical_fn;
25}
26
27
28/* mtcmu_bdd_one_data(bddm, value1, value2) sets the MTBDD value for TRUE. */
29/* This should not be called after MTBDD terminals have been created. */
30
31void
32mtcmu_bdd_one_data(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
33{
34  var_table table;
35  long hash;
36
37  table=bddm->unique_table.tables[BDD_CONST_INDEXINDEX];
38  if (table->entries != 1)
39    cmu_bdd_fatal("mtcmu_bdd_one_data: other terminal nodes already exist");
40  hash=HASH_NODE(bddm->one->data[0], bddm->one->data[1]);
41  BDD_REDUCE(hash, table->size);
42  table->table[hash]=0;
43  bddm->one->data[0]=value1;
44  bddm->one->data[1]=value2;
45  hash=HASH_NODE(bddm->one->data[0], bddm->one->data[1]);
46  BDD_REDUCE(hash, table->size);
47  table->table[hash]=bddm->one;
48}
49
50
51/* cmu_mtbdd_free_terminal_closure(bddm, free_terminal_fn, free_terminal_env) */
52/* sets the closure to be invoked on when freeing MTBDD terminals.  If */
53/* free_terminal_fn is null, it indicates that no function should be */
54/* called.  The free_terminal_fn gets the BDD manager, two longs */
55/* holding the data for the terminal, and the value of free_terminal_env. */
56
57void
58cmu_mtbdd_free_terminal_closure(cmu_bdd_manager bddm,
59                            void (*free_terminal_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer),
60                            pointer free_terminal_env)
61{
62  bddm->unique_table.free_terminal_fn=free_terminal_fn;
63  bddm->unique_table.free_terminal_env=free_terminal_env;
64}
65
66
67/* cmu_mtbdd_get_terminal(bddm, value1, value2) returns the multi-terminal */
68/* BDD for a constant. */
69
70bdd
71cmu_mtbdd_get_terminal(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
72{
73  FIREWALL(bddm);
74  RETURN_BDD(bdd_find_terminal(bddm, value1, value2));
75}
76
77
78/* cmu_mtbdd_terminal_value(bddm, f, value1, value2) returns the data value */
79/* for the terminal node f. */
80
81void
82cmu_mtbdd_terminal_value(cmu_bdd_manager bddm, bdd f, INT_PTR *value1, INT_PTR *value2)
83{
84  if (bdd_check_arguments(1, f))
85    {
86      BDD_SETUP(f);
87      if (!BDD_IS_CONST(f))
88        {
89          cmu_bdd_warning("mtbdd_terminal_data: argument is terminal node");
90          *value1=0;
91          *value2=0;
92          return;
93        }
94      cmu_mtbdd_terminal_value_aux(bddm, f, value1, value2);
95    }
96}
97
98
99static
100bdd
101mtcmu_bdd_ite_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
102{
103  bdd_indexindex_type top_indexindex;
104  bdd f1, f2;
105  bdd g1, g2;
106  bdd h1, h2;
107  bdd temp1, temp2;
108  bdd result;
109
110  BDD_SETUP(f);
111  BDD_SETUP(g);
112  BDD_SETUP(h);
113  if (BDD_IS_CONST(f))
114    {
115      if (f == BDD_ONE(bddm))
116        {
117          BDD_TEMP_INCREFS(g);
118          return (g);
119        }
120      BDD_TEMP_INCREFS(h);
121      return (h);
122    }
123  /* f is not constant. */
124  if (g == h)
125    {
126      BDD_TEMP_INCREFS(g);
127      return (g);
128    }
129  /* f is not constant, g and h are distinct. */
130  if (!BDD_IS_OUTPOS(f))
131    {
132      f=BDD_NOT(f);
133      BDD_SWAP(g, h);
134    }
135  /* f is now an uncomplemented output pointer. */
136  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR *)&result))
137    return (result);
138  BDD_TOP_VAR3(top_indexindex, bddm, f, g, h);
139  BDD_COFACTOR(top_indexindex, f, f1, f2);
140  BDD_COFACTOR(top_indexindex, g, g1, g2);
141  BDD_COFACTOR(top_indexindex, h, h1, h2);
142  temp1=mtcmu_bdd_ite_step(bddm, f1, g1, h1);
143  temp2=mtcmu_bdd_ite_step(bddm, f2, g2, h2);
144  result=bdd_find(bddm, top_indexindex, temp1, temp2);
145  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR)result);
146  return (result);
147}
148
149
150/* mtcmu_bdd_ite(bddm, f, g, h) returns the BDD for "if f then g else h", */
151/* where g and h are multi-terminal BDDs. */
152
153bdd
154mtcmu_bdd_ite(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
155{
156  if (bdd_check_arguments(3, f, g, h))
157    {
158      FIREWALL(bddm);
159      RETURN_BDD(mtcmu_bdd_ite_step(bddm, f, g, h));
160    }
161  return ((bdd)0);
162}
163
164
165/* mtcmu_bdd_substitute(bddm, f) does the analog of cmu_bdd_substitute for MTBDDs. */
166
167bdd
168mtcmu_bdd_substitute(cmu_bdd_manager bddm, bdd f)
169{
170  long op;
171
172  if (bdd_check_arguments(1, f))
173    {
174      FIREWALL(bddm);
175      if (bddm->curr_assoc_id == -1)
176        op=bddm->temp_op--;
177      else
178        op=OP_SUBST+bddm->curr_assoc_id;
179      RETURN_BDD(cmu_bdd_substitute_step(bddm, f, op, mtcmu_bdd_ite_step, bddm->curr_assoc));
180    }
181  return ((bdd)0);
182}
183
184
185static
186bdd
187cmu_mtbdd_equal_step(cmu_bdd_manager bddm, bdd f, bdd g)
188{
189  bdd_indexindex_type top_indexindex;
190  bdd f1, f2;
191  bdd g1, g2;
192  bdd temp1, temp2;
193  bdd result;
194
195  BDD_SETUP(f);
196  BDD_SETUP(g);
197  if (f == g)
198    return (BDD_ONE(bddm));
199  if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
200    return (BDD_ZERO(bddm));
201  if (BDD_OUT_OF_ORDER(f, g))
202    BDD_SWAP(f, g);
203  if (bdd_lookup_in_cache2(bddm, OP_EQUAL, f, g, &result))
204    return (result);
205  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
206  BDD_COFACTOR(top_indexindex, f, f1, f2);
207  BDD_COFACTOR(top_indexindex, g, g1, g2);
208  temp1=cmu_mtbdd_equal_step(bddm, f1, g1);
209  temp2=cmu_mtbdd_equal_step(bddm, f2, g2);
210  result=bdd_find(bddm, top_indexindex, temp1, temp2);
211  bdd_insert_in_cache2(bddm, OP_EQUAL, f, g, result);
212  return (result);
213}
214
215
216/* cmu_mtbdd_equal(bddm, f, g) returns a BDD indicating when the */
217/* multi-terminal BDDs f and g are equal. */
218
219bdd
220cmu_mtbdd_equal(cmu_bdd_manager bddm, bdd f, bdd g)
221{
222  if (bdd_check_arguments(2, f, g))
223    {
224      FIREWALL(bddm);
225      RETURN_BDD(cmu_mtbdd_equal_step(bddm, f, g));
226    }
227  return ((bdd)0);
228}
Note: See TracBrowser for help on using the repository browser.