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

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

library glu 2.3
File size: 9.1 KB
Line 
1/* BDD unique table routines */
2
3
4#include "bddint.h"
5
6
7#define MIN_GC_LIMIT 10000
8
9
10void
11bdd_rehash_var_table(var_table table, int grow)
12{
13  long i;
14  long hash;
15  long oldsize;
16  bdd *newtable;
17  bdd p, q;
18
19  oldsize=table->size;
20  if (grow)
21    table->size_index++;
22  else
23    table->size_index--;
24  table->size=TABLE_SIZE(table->size_index);
25  newtable=(bdd *)mem_get_block((SIZE_T)(table->size*sizeof(bdd)));
26  for (i=0; i < table->size; ++i)
27    newtable[i]=0;
28  for (i=0; i < oldsize; ++i)
29    for (p=table->table[i]; p; p=q)
30      {
31        q=p->next;
32        hash=HASH_NODE(p->data[0], p->data[1]);
33        BDD_REDUCE(hash, table->size);
34        p->next=newtable[hash];
35        newtable[hash]=p;
36      }
37  mem_free_block((pointer)table->table);
38  table->table=newtable;
39}
40
41
42static
43void
44bdd_mark(cmu_bdd_manager bddm)
45{
46  long i, j;
47  var_table table;
48  bdd f, g;
49
50  for (i=0; i <= bddm->vars; ++i)
51    {
52      if (i == bddm->vars)
53        table=bddm->unique_table.tables[BDD_CONST_INDEXINDEX];
54      else
55        table=bddm->unique_table.tables[bddm->indexindexes[i]];
56      for (j=0; j < table->size; ++j)
57        for (f=table->table[j]; f; f=f->next)
58          {
59            BDD_SETUP(f);
60            if (BDD_REFS(f) || BDD_TEMP_REFS(f))
61              BDD_MARK(f)|=BDD_GC_MARK;
62            if (BDD_IS_USED(f) && !BDD_IS_CONST(f))
63              {
64                g=(bdd)BDD_DATA0(f);
65                {
66                  BDD_SETUP(g);
67                  BDD_MARK(g)|=BDD_GC_MARK;
68                }
69                g=(bdd)BDD_DATA1(f);
70                {
71                  BDD_SETUP(g);
72                  BDD_MARK(g)|=BDD_GC_MARK;
73                }
74              }
75          }
76    }
77}
78
79
80void
81bdd_sweep_var_table(cmu_bdd_manager bddm, long i, int maybe_rehash)
82{
83  long j;
84  var_table table;
85  bdd f, *p;
86
87  table=bddm->unique_table.tables[i];
88  for (j=0; j < table->size; ++j)
89    for (p= &table->table[j], f= *p; f; f= *p)
90      {
91        BDD_SETUP(f);
92        if (BDD_IS_USED(f))
93          {
94            BDD_SETUP(f);
95            BDD_MARK(f)&=~BDD_GC_MARK;
96            p= &f->next;
97          }
98        else
99          {
100            *p=f->next;
101            if (i == BDD_CONST_INDEXINDEX && bddm->unique_table.free_terminal_fn)
102              (*bddm->unique_table.free_terminal_fn)(bddm,
103                                                     BDD_DATA0(f),
104                                                     BDD_DATA1(f),
105                                                     bddm->unique_table.free_terminal_env);
106            BDD_FREE_REC(bddm, (pointer)f, sizeof(struct bdd_));
107            table->entries--;
108            bddm->unique_table.entries--;
109            bddm->unique_table.freed++;
110          }
111      }
112  if (maybe_rehash && table->size > table->entries && table->size_index > 3)
113    bdd_rehash_var_table(table, 0);
114}
115
116
117void
118bdd_sweep(cmu_bdd_manager bddm)
119{
120  long i;
121
122  for (i=0; i <= bddm->vars; ++i)
123    bdd_sweep_var_table(bddm, i, 1);
124}
125
126
127/* cmu_bdd_gc(bddm) performs a garbage collection. */
128
129void
130cmu_bdd_gc(cmu_bdd_manager bddm)
131{
132  bdd_mark(bddm);
133  bdd_purge_cache(bddm);
134  bdd_sweep(bddm);
135  bddm->unique_table.gcs++;
136}
137
138
139static
140void
141bdd_set_gc_limit(cmu_bdd_manager bddm)
142{
143  bddm->unique_table.gc_limit=2*bddm->unique_table.entries;
144  if (bddm->unique_table.gc_limit < MIN_GC_LIMIT)
145    bddm->unique_table.gc_limit=MIN_GC_LIMIT;
146  if (bddm->unique_table.node_limit &&
147      bddm->unique_table.gc_limit > bddm->unique_table.node_limit)
148    bddm->unique_table.gc_limit=bddm->unique_table.node_limit;
149}
150
151
152void
153bdd_clear_temps(cmu_bdd_manager bddm)
154{
155  long i, j;
156  var_table table;
157  bdd f;
158
159  for (i=0; i <= bddm->vars; ++i)
160    {
161      table=bddm->unique_table.tables[i];
162      for (j=0; j < table->size; ++j)
163        for (f=table->table[j]; f; f=f->next)
164          {
165            BDD_SETUP(f);
166            BDD_TEMP_REFS(f)=0;
167          }
168    }
169  cmu_bdd_gc(bddm);
170  bdd_set_gc_limit(bddm);
171} 
172
173
174void
175bdd_cleanup(cmu_bdd_manager bddm, int code)
176{
177  bdd_clear_temps(bddm);
178  switch (code)
179    {
180    case BDD_ABORTED:
181      (*bddm->bag_it_fn)(bddm, bddm->bag_it_env);
182      break;
183    case BDD_OVERFLOWED:
184      if (bddm->overflow_fn)
185        (*bddm->overflow_fn)(bddm, bddm->overflow_env);
186      break;
187    }
188}
189
190
191bdd
192bdd_find_aux(cmu_bdd_manager bddm, bdd_indexindex_type indexindex, INT_PTR d1, INT_PTR d2)
193{
194  var_table table;
195  long hash;
196  bdd temp;
197
198  table=bddm->unique_table.tables[indexindex];
199  hash=HASH_NODE(d1, d2);
200  BDD_REDUCE(hash, table->size);
201  for (temp=table->table[hash]; temp; temp=temp->next)
202    if (temp->data[0] == d1 && temp->data[1] == d2)
203      break;
204  if (!temp)
205    {
206      /* Not found; make a new node. */
207      temp=(bdd)BDD_NEW_REC(bddm, sizeof(struct bdd_));
208      temp->indexindex=indexindex;
209      temp->refs=0;
210      temp->mark=0;
211      temp->data[0]=d1;
212      temp->data[1]=d2;
213      temp->next=table->table[hash];
214      table->table[hash]=temp;
215      table->entries++;
216      bddm->unique_table.entries++;
217      if (4*table->size < table->entries)
218        bdd_rehash_var_table(table, 1);
219    }
220  bddm->unique_table.finds++;
221  return (temp);
222}
223
224
225static
226void
227bdd_check(cmu_bdd_manager bddm)
228{
229  long nodes;
230
231  bddm->check=100;
232  /* When bag_it_fn set, clean up and abort immediately. */
233  if (bddm->bag_it_fn)
234    longjmp(bddm->abort.context, BDD_ABORTED);
235  if (bddm->unique_table.entries > bddm->unique_table.gc_limit)
236    {
237      cmu_bdd_gc(bddm);
238      /* Table full. */
239      nodes=bddm->unique_table.entries;
240      if (3*nodes > 2*bddm->unique_table.gc_limit && bddm->allow_reordering && bddm->reorder_fn)
241        {
242          cmu_bdd_reorder_aux(bddm);
243          if (4*bddm->unique_table.entries > 3*nodes && 3*nodes > 4*bddm->nodes_at_start)
244            /* If we didn't save much, but we have created a reasonable number */
245            /* of nodes, then don't bother reordering next time. */
246            bddm->allow_reordering=0;
247          /* Go try again. */
248          bdd_set_gc_limit(bddm);
249          longjmp(bddm->abort.context, BDD_REORDERED);
250        }
251      bdd_set_gc_limit(bddm);
252      if (bddm->unique_table.node_limit &&
253          bddm->unique_table.entries >= bddm->unique_table.node_limit-1000)
254        {
255          /* Out of memory; go clean up. */
256          bddm->overflow=1;
257          longjmp(bddm->abort.context, BDD_OVERFLOWED);
258        }
259    }
260  /* Maybe increase cache size if it's getting full. */
261  if (3*bddm->op_cache.size < 2*bddm->op_cache.entries &&
262      32*bddm->op_cache.size < bddm->op_cache.cache_ratio*bddm->unique_table.entries)
263    bdd_rehash_cache(bddm, 1);
264}
265
266
267/* bdd_find(bddm, indexindex, f, g) creates or finds a node with the */
268/* given indexindex, "then" pointer, and "else" pointer. */
269
270bdd
271bdd_find(cmu_bdd_manager bddm, bdd_indexindex_type indexindex, bdd f, bdd g)
272{
273  bdd temp;
274
275  BDD_SETUP(f);
276  BDD_SETUP(g);
277  if (f == g)
278    {
279      BDD_TEMP_DECREFS(f);
280      temp=f;
281    }
282  else
283    {
284      if (BDD_IS_OUTPOS(f))
285        temp=bdd_find_aux(bddm, indexindex, (INT_PTR)f, (INT_PTR)g);
286      else
287        temp=BDD_NOT(bdd_find_aux(bddm, indexindex, (INT_PTR)BDD_NOT(f), (INT_PTR)BDD_NOT(g)));
288      {
289        BDD_SETUP(temp);
290        BDD_TEMP_INCREFS(temp);
291      }
292      BDD_TEMP_DECREFS(f);
293      BDD_TEMP_DECREFS(g);
294    }
295  bddm->check--;
296  if (!bddm->check)
297    bdd_check(bddm);
298  return (temp);
299}
300
301
302/* bdd_find_terminal(bddm, value1, value2) creates or finds a terminal */
303/* node with the given data value. */
304
305bdd
306bdd_find_terminal(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
307{
308  bdd temp;
309
310  if ((*bddm->canonical_fn)(bddm, value1, value2, bddm->transform_env))
311    {
312      (*bddm->transform_fn)(bddm, value1, value2, &value1, &value2, bddm->transform_env);
313      temp=BDD_NOT(bdd_find_aux(bddm, BDD_CONST_INDEXINDEX, value1, value2));
314    }
315  else
316    temp=bdd_find_aux(bddm, BDD_CONST_INDEXINDEX, value1, value2);
317  {
318    BDD_SETUP(temp);
319    BDD_TEMP_INCREFS(temp);
320  }
321  bddm->check--;
322  if (!bddm->check)
323    bdd_check(bddm);
324  return (temp);
325}
326
327
328/* cmu_bdd_clear_refs(bddm) sets the reference count of all nodes to 0. */
329
330void
331cmu_bdd_clear_refs(cmu_bdd_manager bddm)
332{
333  long i, j;
334  var_table table;
335  bdd f;
336  assoc_list q;
337
338  for (i=0; i <= bddm->vars; ++i)
339    {
340      table=bddm->unique_table.tables[i];
341      for (j=0; j < table->size; ++j)
342        for (f=table->table[j]; f; f=f->next)
343          {
344            BDD_SETUP(f);
345            BDD_REFS(f)=0;
346          }
347    }
348  for (i=0; i < bddm->vars; ++i)
349    bddm->variables[i+1]->refs=BDD_MAX_REFS;
350  bddm->one->refs=BDD_MAX_REFS;
351  for (q=bddm->assocs; q; q=q->next)
352    for (i=0; i < bddm->vars; ++i)
353      if ((f=q->va.assoc[i+1]))
354        {
355          BDD_SETUP(f);
356          BDD_INCREFS(f);
357        }
358}
359
360
361var_table
362bdd_new_var_table(cmu_bdd_manager bddm)
363{
364  long i;
365  var_table table;
366
367  table=(var_table)BDD_NEW_REC(bddm, sizeof(struct var_table_));
368  table->size_index=3;
369  table->size=TABLE_SIZE(table->size_index);
370  table->entries=0;
371  table->table=(bdd *)mem_get_block((SIZE_T)(table->size*sizeof(bdd)));
372  for (i=0; i < table->size; ++i)
373    table->table[i]=0;
374  return (table);
375}
376
377
378void
379cmu_bdd_init_unique(cmu_bdd_manager bddm)
380{
381  bddm->unique_table.tables=(var_table *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(var_table)));
382  bddm->unique_table.tables[BDD_CONST_INDEXINDEX]=bdd_new_var_table(bddm);
383  bddm->unique_table.gc_limit=MIN_GC_LIMIT;
384  bddm->unique_table.node_limit=0;
385  bddm->unique_table.entries=0;
386  bddm->unique_table.freed=0;
387  bddm->unique_table.gcs=0;
388  bddm->unique_table.finds=0;
389  bddm->unique_table.free_terminal_fn=0;
390  bddm->unique_table.free_terminal_env=0;
391}
392
393
394void
395cmu_bdd_free_unique(cmu_bdd_manager bddm)
396{
397  long i, j;
398  var_table table;
399  bdd p, q;
400
401  for (i=0; i <= bddm->vars; ++i)
402    {
403      table=bddm->unique_table.tables[i];
404      for (j=0; j < table->size; ++j)
405        for (p=table->table[j]; p; p=q)
406          {
407            q=p->next;
408            BDD_FREE_REC(bddm, (pointer)p, sizeof(struct bdd_));
409          }
410      mem_free_block((pointer)table->table);
411      BDD_FREE_REC(bddm, (pointer)table, sizeof(struct var_table_));
412    }
413  mem_free_block((pointer)bddm->unique_table.tables);
414}
Note: See TracBrowser for help on using the repository browser.