source: vis_dev/glu-2.3/src/cmuBdd/bddassoc.c @ 15

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

library glu 2.3

File size: 6.2 KB
Line 
1/* BDD variable association routines */
2
3
4#include "bddint.h"
5
6
7static
8int
9cmu_bdd_assoc_eq(cmu_bdd_manager bddm, bdd *p, bdd *q)
10{
11  bdd_indexindex_type i;
12
13  for (i=0; i < bddm->maxvars; ++i)
14    if (p[i+1] != q[i+1])
15      return (0);
16  return (1);
17}
18
19
20static
21int
22check_assoc(cmu_bdd_manager bddm, bdd *assoc_info, int pairs)
23{
24  bdd_check_array(assoc_info);
25  if (pairs)
26    while (assoc_info[0] && assoc_info[1])
27      {
28        if (cmu_bdd_type_aux(bddm, assoc_info[0]) != BDD_TYPE_POSVAR)
29          {
30            cmu_bdd_warning("check_assoc: first element in pair is not a positive variable");
31            return (0);
32          }
33        assoc_info+=2;
34      }
35  return (1);
36}
37
38 
39/* cmu_bdd_new_assoc(bddm, assoc_info, pairs) creates or finds a variable */
40/* association given by assoc_info.  pairs is 0 if the information */
41/* represents only a list of variables rather than a full association. */
42
43int
44cmu_bdd_new_assoc(cmu_bdd_manager bddm, bdd *assoc_info, int pairs)
45{
46  long i;
47  assoc_list p, *q;
48  bdd f;
49  bdd *assoc;
50  bdd_indexindex_type j;
51  long last;
52
53  if (!check_assoc(bddm, assoc_info, pairs))
54    return (-1);
55  assoc=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
56  /* Unpack the association. */
57  for (i=0; i < bddm->maxvars; ++i)
58    assoc[i+1]=0;
59  if (pairs)
60    for (i=0; (f=assoc_info[i]) && assoc_info[i+1]; i+=2)
61      {
62        BDD_SETUP(f);
63        assoc[BDD_INDEXINDEX(f)]=assoc_info[i+1];
64      }
65  else
66    for (i=0; (f=assoc_info[i]); ++i)
67      {
68        BDD_SETUP(f);
69        assoc[BDD_INDEXINDEX(f)]=BDD_ONE(bddm);
70      }
71  /* Check for existence. */
72  for (p=bddm->assocs; p; p=p->next)
73    if (cmu_bdd_assoc_eq(bddm, p->va.assoc, assoc))
74      {
75        mem_free_block((pointer)assoc);
76        p->refs++;
77        return (p->id);
78      }
79  /* Find the first unused id. */
80  for (q= &bddm->assocs, p= *q, i=0; p && p->id == i; q= &p->next, p= *q, ++i);
81  p=(assoc_list)BDD_NEW_REC(bddm, sizeof(struct assoc_list_));
82  p->id=i;
83  p->next= *q;
84  *q=p;
85  p->va.assoc=assoc;
86  last= -1;
87  if (pairs)
88    for (i=0; (f=assoc_info[i]) && assoc_info[i+1]; i+=2)
89      {
90        BDD_SETUP(f);
91        j=BDD_INDEXINDEX(f);
92        if ((long)bddm->indexes[j] > last)
93          last=bddm->indexes[j];
94      }
95  else
96    for (i=0; (f=assoc_info[i]); ++i)
97      {
98        BDD_SETUP(f);
99        j=BDD_INDEXINDEX(f);
100        if ((long)bddm->indexes[j] > last)
101          last=bddm->indexes[j];
102      }
103  p->va.last=last;
104  p->refs=1;
105  /* Protect BDDs in the association. */
106  if (pairs)
107    for (i=0; assoc_info[i] && (f=assoc_info[i+1]); i+=2)
108      {
109        BDD_SETUP(f);
110        BDD_INCREFS(f);
111      }
112  return (p->id);
113}
114
115
116static
117int
118bdd_flush_id_entries(cmu_bdd_manager bddm, cache_entry p, pointer closure)
119{
120  int (*flush_fn)(cmu_bdd_manager, cache_entry, pointer);
121
122  flush_fn=bddm->op_cache.flush_fn[TAG(p)];
123  if (flush_fn)
124    return ((*flush_fn)(bddm, CACHE_POINTER(p), closure));
125  return (0);
126}
127
128
129/* cmu_bdd_free_assoc(bddm, id) deletes the variable association given by */
130/* id. */
131
132void
133cmu_bdd_free_assoc(cmu_bdd_manager bddm, int assoc_id)
134{
135  bdd_indexindex_type i;
136  bdd f;
137  assoc_list p, *q;
138
139  if (bddm->curr_assoc_id == assoc_id)
140    {
141      bddm->curr_assoc_id= -1;
142      bddm->curr_assoc= &bddm->temp_assoc;
143    }
144  for (q= &bddm->assocs, p= *q; p; q= &p->next, p= *q)
145    if (p->id == assoc_id)
146      {
147        p->refs--;
148        if (!p->refs)
149          {
150            /* Unprotect the BDDs in the association. */
151            for (i=0; i < bddm->vars; ++i)
152              if ((f=p->va.assoc[i+1]))
153                {
154                  BDD_SETUP(f);
155                  BDD_DECREFS(f);
156                }
157            /* Flush old cache entries. */
158            bdd_flush_cache(bddm, bdd_flush_id_entries, (pointer)((long)assoc_id));
159            *q=p->next;
160            mem_free_block((pointer)(p->va.assoc));
161            BDD_FREE_REC(bddm, (pointer)p, sizeof(struct assoc_list_));
162          }
163        return;
164      }
165  cmu_bdd_warning("cmu_bdd_free_assoc: no variable association with specified ID");
166}
167
168
169/* cmu_bdd_augment_temp_assoc(bddm, assoc_info, pairs) adds to the temporary */
170/* variable association as specified by assoc_info.  pairs is 0 if the */
171/* information represents only a list of variables rather than a full */
172/* association. */
173
174void
175cmu_bdd_augment_temp_assoc(cmu_bdd_manager bddm, bdd *assoc_info, int pairs)
176{
177  long i;
178  bdd_indexindex_type j;
179  bdd f;
180  long last;
181
182  if (check_assoc(bddm, assoc_info, pairs))
183    {
184      last=bddm->temp_assoc.last;
185      if (pairs)
186        for (i=0; (f=assoc_info[i]) && assoc_info[i+1]; i+=2)
187          {
188            BDD_SETUP(f);
189            j=BDD_INDEXINDEX(f);
190            if ((long)bddm->indexes[j] > last)
191              last=bddm->indexes[j];
192            if ((f=bddm->temp_assoc.assoc[j]))
193              {
194                BDD_SETUP(f);
195                BDD_DECREFS(f);
196              }
197            f=assoc_info[i+1];
198            BDD_RESET(f);
199            bddm->temp_assoc.assoc[j]=f;
200            /* Protect BDDs in the association. */
201            BDD_INCREFS(f);
202          }
203      else
204        for (i=0; (f=assoc_info[i]); ++i)
205          {
206            BDD_SETUP(f);
207            j=BDD_INDEXINDEX(f);
208            if ((long)bddm->indexes[j] > last)
209              last=bddm->indexes[j];
210            if ((f=bddm->temp_assoc.assoc[j]))
211              {
212                BDD_SETUP(f);
213                BDD_DECREFS(f);
214              }
215            bddm->temp_assoc.assoc[j]=BDD_ONE(bddm);
216          }
217      bddm->temp_assoc.last=last;
218    }
219}
220
221
222/* cmu_bdd_temp_assoc(bddm, assoc_info, pairs) sets the temporary variable */
223/* association as specified by assoc_info.  pairs is 0 if the */
224/* information represents only a list of variables rather than a full */
225/* association. */
226
227void
228cmu_bdd_temp_assoc(cmu_bdd_manager bddm, bdd *assoc_info, int pairs)
229{
230  long i;
231  bdd f;
232
233  /* Clean up old temporary association. */
234  for (i=0; i < bddm->vars; ++i)
235    {
236      if ((f=bddm->temp_assoc.assoc[i+1]))
237        {
238          BDD_SETUP(f);
239          BDD_DECREFS(f);
240        }
241      bddm->temp_assoc.assoc[i+1]=0;
242    }
243  bddm->temp_assoc.last= -1;
244  cmu_bdd_augment_temp_assoc(bddm, assoc_info, pairs);
245}
246
247
248/* cmu_bdd_assoc(bddm, id) sets the current variable association to the */
249/* one given by id and returns the ID of the old association.  An */
250/* id of -1 indicates the temporary association. */
251
252int
253cmu_bdd_assoc(cmu_bdd_manager bddm, int assoc_id)
254{
255  int old_assoc;
256  assoc_list p;
257
258  old_assoc=bddm->curr_assoc_id;
259  if (assoc_id != -1)
260    {
261      for (p=bddm->assocs; p; p=p->next)
262        if (p->id == assoc_id)
263          {
264            bddm->curr_assoc_id=p->id;
265            bddm->curr_assoc= &p->va;
266            return (old_assoc);
267          }
268      cmu_bdd_warning("cmu_bdd_assoc: no variable association with specified ID");
269    }
270  bddm->curr_assoc_id= -1;
271  bddm->curr_assoc= &bddm->temp_assoc;
272  return (old_assoc);
273}
Note: See TracBrowser for help on using the repository browser.