source: vis_dev/glu-2.3/src/cmuBdd/bddreorder.c

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

library glu 2.3
File size: 14.0 KB
Line 
1/* BDD dynamic reordering stuff */
2
3
4#include "bddint.h"
5
6
7static
8void
9increfs(bdd f)
10{
11  bdd g;
12
13  BDD_SETUP(f);
14  BDD_INCREFS(f);
15  if (BDD_REFS(f) == 1 && !BDD_TEMP_REFS(f))
16    {
17      g=(bdd)BDD_DATA0(f);
18      {
19        BDD_SETUP(g);
20        BDD_INCREFS(g);
21      }
22      g=(bdd)BDD_DATA1(f);
23      {
24        BDD_SETUP(g);
25        BDD_INCREFS(g);
26      }
27    }
28}
29
30
31static
32void
33decrefs(bdd f)
34{
35  bdd g;
36
37  BDD_SETUP(f);
38  BDD_DECREFS(f);
39  if (!BDD_REFS(f) && !BDD_TEMP_REFS(f))
40    {
41      g=(bdd)BDD_DATA0(f);
42      {
43        BDD_SETUP(g);
44        BDD_DECREFS(g);
45      }
46      g=(bdd)BDD_DATA1(f);
47      {
48        BDD_SETUP(g);
49        BDD_DECREFS(g);
50      }
51    }
52}
53
54
55static
56void
57bdd_exchange_aux(cmu_bdd_manager bddm, bdd f, bdd_indexindex_type next_indexindex)
58{
59  bdd f1, f2;
60  bdd f11, f12, f21, f22;
61  bdd temp1, temp2;
62
63  BDD_SETUP(f);
64  f1=BDD_THEN(f);
65  f2=BDD_ELSE(f);
66  {
67    BDD_SETUP(f1);
68    BDD_SETUP(f2);
69    if (BDD_INDEXINDEX(f1) == next_indexindex)
70      {
71        f11=BDD_THEN(f1);
72        f12=BDD_ELSE(f1);
73      }
74    else
75      {
76        f11=f1;
77        f12=f1;
78      }
79    if (BDD_INDEXINDEX(f2) == next_indexindex)
80      {
81        f21=BDD_THEN(f2);
82        f22=BDD_ELSE(f2);
83      }
84    else
85      {
86        f21=f2;
87        f22=f2;
88      }
89    if (f11 == f21)
90      temp1=f11;
91    else
92      temp1=bdd_find_aux(bddm, BDD_INDEXINDEX(f), (INT_PTR)f11, (INT_PTR)f21);
93    if (f12 == f22)
94      temp2=f12;
95    else if (BDD_IS_OUTPOS(f12))
96      temp2=bdd_find_aux(bddm, BDD_INDEXINDEX(f), (INT_PTR)f12, (INT_PTR)f22);
97    else
98      temp2=BDD_NOT(bdd_find_aux(bddm, BDD_INDEXINDEX(f), (INT_PTR)BDD_NOT(f12), (INT_PTR)BDD_NOT(f22)));
99    BDD_INDEXINDEX(f)=next_indexindex;
100    BDD_DATA0(f)=(INT_PTR)temp1;
101    BDD_DATA1(f)=(INT_PTR)temp2;
102    if (BDD_REFS(f) || BDD_TEMP_REFS(f))
103      {
104        increfs(temp1);
105        increfs(temp2);
106        decrefs(f1);
107        decrefs(f2);
108      }
109    else
110      cmu_bdd_fatal("bdd_exchange_aux: how did this happen?");
111  }
112}
113
114
115static
116void
117fixup_assoc(cmu_bdd_manager bddm, long indexindex1, long indexindex2, var_assoc va)
118{
119  /* Variable with indexindex1 is moving down a spot. */
120  if (va->assoc[indexindex1] && va->last == bddm->indexes[indexindex1])
121    va->last++;
122  else if (!va->assoc[indexindex1] && va->assoc[indexindex2] && va->last == bddm->indexes[indexindex2])
123    va->last--;
124}
125
126
127static
128void
129sweep_var_table(cmu_bdd_manager bddm, long i)
130{
131  long j;
132  var_table table;
133  bdd f, *p;
134
135  table=bddm->unique_table.tables[i];
136  for (j=0; j < table->size; ++j)
137    for (p= &table->table[j], f= *p; f; f= *p)
138      {
139        BDD_SETUP(f);
140        if (BDD_REFS(f) || BDD_TEMP_REFS(f))
141          p= &f->next;
142        else
143          {
144            *p=f->next;
145            BDD_FREE_REC(bddm, (pointer)f, sizeof(struct bdd_));
146            table->entries--;
147            bddm->unique_table.entries--;
148            bddm->unique_table.freed++;
149          }
150      }
151}
152
153
154static
155void
156bdd_exchange(cmu_bdd_manager bddm, long i)
157{
158  bdd_indexindex_type next_indexindex;
159  var_table table, next_table;
160  long j;
161  bdd f, *p;
162  bdd f1, f2;
163  bdd g;
164  long hash;
165  bdd_index_type temp;
166  assoc_list q;
167
168  next_indexindex=bddm->indexindexes[bddm->indexes[i]+1];
169  table=bddm->unique_table.tables[i];
170  next_table=bddm->unique_table.tables[next_indexindex];
171  g=0;
172  for (j=0; j < table->size; ++j)
173    for (p= &table->table[j], f= *p; f; f= *p)
174      {
175        BDD_SETUP(f);
176        if (BDD_REFS(f) || BDD_TEMP_REFS(f))
177          {
178            f1=(bdd)BDD_DATA0(f);
179            f2=(bdd)BDD_DATA1(f);
180            {
181              BDD_SETUP(f1);
182              BDD_SETUP(f2);
183              if (BDD_INDEXINDEX(f1) != next_indexindex && BDD_INDEXINDEX(f2) != next_indexindex)
184                p= &f->next;
185              else
186                {
187                  *p=f->next;
188                  f->next=g;
189                  g=f;
190                }
191            }
192          }
193        else
194          {
195            *p=f->next;
196            BDD_FREE_REC(bddm, (pointer)f, sizeof(struct bdd_));
197            table->entries--;
198            bddm->unique_table.entries--;
199            bddm->unique_table.freed++;
200          }
201      }
202  for (f=g; f; f=g)
203    {
204      bdd_exchange_aux(bddm, f, next_indexindex);
205      g=f->next;
206      hash=HASH_NODE(f->data[0], f->data[1]);
207      BDD_REDUCE(hash, next_table->size);
208      f->next=next_table->table[hash];
209      next_table->table[hash]=f;
210      table->entries--;
211      next_table->entries++;
212      if (4*next_table->size < next_table->entries)
213        bdd_rehash_var_table(next_table, 1);
214    }
215  fixup_assoc(bddm, i, next_indexindex, &bddm->temp_assoc);
216  for (q=bddm->assocs; q; q=q->next)
217    fixup_assoc(bddm, i, next_indexindex, &q->va);
218  sweep_var_table(bddm, next_indexindex);
219  temp=bddm->indexes[i];
220  bddm->indexes[i]=bddm->indexes[next_indexindex];
221  bddm->indexes[next_indexindex]=temp;
222  bddm->indexindexes[temp]=next_indexindex;
223  bddm->indexindexes[bddm->indexes[i]]=i;
224}
225
226
227void
228cmu_bdd_var_block_reorderable(cmu_bdd_manager bddm, block b, int reorderable)
229{
230  b->reorderable=reorderable;
231}
232
233
234static
235void
236bdd_exchange_var_blocks(cmu_bdd_manager bddm, block parent, long bi)
237{
238  block b1, b2;
239  long i, j, k, l;
240  long delta;
241  block temp;
242
243  b1=parent->children[bi];
244  b2=parent->children[bi+1];
245  /* This slides the blocks past each other in a kind of interleaving */
246  /* fashion. */
247  for (i=0; i <= b1->last_index-b1->first_index+b2->last_index-b2->first_index; ++i)
248    {
249      j=i-b1->last_index+b1->first_index;
250      if (j < 0)
251        j=0;
252      k=i;
253      if (k > b2->last_index-b2->first_index)
254        k=b2->last_index-b2->first_index;
255      while (j <= k)
256        {
257          l=b2->first_index+j-i+j;
258          bdd_exchange(bddm, bddm->indexindexes[l-1]);
259          ++j;
260        }
261    }
262  delta=b2->last_index-b2->first_index+1;
263  bdd_block_delta(b1, delta);
264  delta=b1->last_index-b1->first_index+1;
265  bdd_block_delta(b2, -delta);
266  temp=parent->children[bi];
267  parent->children[bi]=parent->children[bi+1];
268  parent->children[bi+1]=temp;
269}
270
271
272static
273int
274cmu_bdd_reorder_window2(cmu_bdd_manager bddm, block b, long i)
275{
276  long size, best_size;
277
278  /* 1 2 */
279  best_size=bddm->unique_table.entries;
280  bdd_exchange_var_blocks(bddm, b, i);
281  /* 2 1 */
282  size=bddm->unique_table.entries;
283  if (size < best_size)
284    return (1);
285  bdd_exchange_var_blocks(bddm, b, i);
286  return (0);
287}
288
289
290static
291int
292cmu_bdd_reorder_window3(cmu_bdd_manager bddm, block b, long i)
293{
294  int best;
295  long size, best_size;
296
297  best=0;
298  /* 1 2 3 */
299  best_size=bddm->unique_table.entries;
300  bdd_exchange_var_blocks(bddm, b, i);
301  /* 2 1 3 */
302  size=bddm->unique_table.entries;
303  if (size < best_size)
304    {
305      best=1;
306      best_size=size;
307    }
308  bdd_exchange_var_blocks(bddm, b, i+1);
309  /* 2 3 1 */
310  size=bddm->unique_table.entries;
311  if (size < best_size)
312    {
313      best=2;
314      best_size=size;
315    }
316  bdd_exchange_var_blocks(bddm, b, i);
317  /* 3 2 1 */
318  size=bddm->unique_table.entries;
319  if (size < best_size)
320    {
321      best=3;
322      best_size=size;
323    }
324  bdd_exchange_var_blocks(bddm, b, i+1);
325  /* 3 1 2 */
326  size=bddm->unique_table.entries;
327  if (size < best_size)
328    {
329      best=4;
330      best_size=size;
331    }
332  bdd_exchange_var_blocks(bddm, b, i);
333  /* 1 3 2 */
334  size=bddm->unique_table.entries;
335  if (size < best_size)
336    {
337      best=5;
338      best_size=size;
339    }
340  switch (best)
341    {
342    case 0:
343      bdd_exchange_var_blocks(bddm, b, i+1);
344      break;
345    case 1:
346      bdd_exchange_var_blocks(bddm, b, i+1);
347      bdd_exchange_var_blocks(bddm, b, i);
348      break;
349    case 2:
350      bdd_exchange_var_blocks(bddm, b, i+1);
351      bdd_exchange_var_blocks(bddm, b, i);
352      bdd_exchange_var_blocks(bddm, b, i+1);
353      break;
354    case 3:
355      bdd_exchange_var_blocks(bddm, b, i);
356      bdd_exchange_var_blocks(bddm, b, i+1);
357      break;
358    case 4:
359      bdd_exchange_var_blocks(bddm, b, i);
360      break;
361    case 5:
362      break;
363    }
364  return (best > 0);
365}
366
367
368static
369void
370cmu_bdd_reorder_stable_window3_aux(cmu_bdd_manager bddm, block b, char *levels)
371{
372  long i;
373  int moved;
374  int any_swapped;
375
376  if (b->reorderable)
377    {
378      for (i=0; i < b->num_children-1; ++i)
379        levels[i]=1;
380      do
381        {
382          any_swapped=0;
383          for (i=0; i < b->num_children-1; ++i)
384            if (levels[i])
385              {
386                if (i < b->num_children-2)
387                  moved=cmu_bdd_reorder_window3(bddm, b, i);
388                else
389                  moved=cmu_bdd_reorder_window2(bddm, b, i);
390                if (moved)
391                  {
392                    if (i > 0)
393                      {
394                        levels[i-1]=1;
395                        if (i > 1)
396                          levels[i-2]=1;
397                      }
398                    levels[i]=1;
399                    levels[i+1]=1;
400                    if (i < b->num_children-2)
401                      {
402                        levels[i+2]=1;
403                        if (i < b->num_children-3)
404                          {
405                            levels[i+3]=1;
406                            if (i < b->num_children-4)
407                              levels[i+4]=1;
408                          }
409                      }
410                    any_swapped=1;
411                  }
412                else
413                  levels[i]=0;
414              }
415        }
416      while (any_swapped);
417    }
418  for (i=0; i < b->num_children; ++i)
419    cmu_bdd_reorder_stable_window3_aux(bddm, b->children[i], levels);
420}
421
422
423void
424cmu_bdd_reorder_stable_window3(cmu_bdd_manager bddm)
425{
426  char *levels;
427
428  levels=(char *)mem_get_block(bddm->vars*sizeof(char));
429  cmu_bdd_reorder_stable_window3_aux(bddm, bddm->super_block, levels);
430  mem_free_block((pointer)levels);
431}
432
433
434static
435void
436bdd_sift_block(cmu_bdd_manager bddm, block b, long start_pos, double max_size_factor)
437{
438  long start_size;
439  long best_size;
440  long best_pos;
441  long curr_size;
442  long curr_pos;
443  long max_size;
444
445  start_size=bddm->unique_table.entries;
446  best_size=start_size;
447  best_pos=start_pos;
448  curr_size=start_size;
449  curr_pos=start_pos;
450  max_size=max_size_factor*start_size;
451  if (bddm->unique_table.node_limit && max_size > bddm->unique_table.node_limit)
452    max_size=bddm->unique_table.node_limit;
453  while (curr_pos < b->num_children-1 && curr_size <= max_size)
454    {
455      bdd_exchange_var_blocks(bddm, b, curr_pos);
456      ++curr_pos;
457      curr_size=bddm->unique_table.entries;
458      if (curr_size < best_size)
459        {
460          best_size=curr_size;
461          best_pos=curr_pos;
462        }
463    }
464  while (curr_pos != start_pos)
465    {
466      --curr_pos;
467      bdd_exchange_var_blocks(bddm, b, curr_pos);
468    }
469  curr_size=start_size;
470  while (curr_pos && curr_size <= max_size)
471    {
472      --curr_pos;
473      bdd_exchange_var_blocks(bddm, b, curr_pos);
474      curr_size=bddm->unique_table.entries;
475      if (curr_size < best_size)
476        {
477          best_size=curr_size;
478          best_pos=curr_pos;
479        }
480    }
481  while (curr_pos != best_pos)
482    {
483      bdd_exchange_var_blocks(bddm, b, curr_pos);
484      ++curr_pos;
485    }
486}
487
488
489static
490void
491cmu_bdd_reorder_sift_aux(cmu_bdd_manager bddm, block b, block *to_sift, double max_size_factor)
492{
493  long i, j, k;
494  long w;
495  long max_w;
496  long widest;
497
498  if (b->reorderable)
499    {
500      for (i=0; i < b->num_children; ++i)
501        to_sift[i]=b->children[i];
502      while (i)
503        {
504          --i;
505          max_w=0;
506          widest=0;
507          for (j=0; j <= i; ++j)
508            {
509              for (w=0, k=to_sift[j]->first_index; k <= to_sift[j]->last_index; ++k)
510                w+=bddm->unique_table.tables[bddm->indexindexes[k]]->entries;
511              w/=to_sift[j]->last_index-to_sift[j]->first_index+1;
512              if (w > max_w)
513                {
514                  max_w=w;
515                  widest=j;
516                }
517            }
518          if (max_w > 1)
519            {
520              for (j=0; b->children[j] != to_sift[widest]; ++j);
521              bdd_sift_block(bddm, b, j, max_size_factor);
522              to_sift[widest]=to_sift[i];
523            }
524          else
525            break;
526        }
527    }
528  for (i=0; i < b->num_children; ++i)
529    cmu_bdd_reorder_sift_aux(bddm, b->children[i], to_sift, max_size_factor);
530}
531
532
533static
534void
535cmu_bdd_reorder_sift_aux1(cmu_bdd_manager bddm, double max_size_factor)
536{
537  block *to_sift;
538
539  to_sift=(block *)mem_get_block(bddm->vars*sizeof(block));
540  cmu_bdd_reorder_sift_aux(bddm, bddm->super_block, to_sift, max_size_factor);
541  mem_free_block((pointer)to_sift);
542}
543
544
545void
546cmu_bdd_reorder_sift(cmu_bdd_manager bddm)
547{
548  cmu_bdd_reorder_sift_aux1(bddm, 2.0);
549}
550
551
552void
553cmu_bdd_reorder_hybrid(cmu_bdd_manager bddm)
554{
555  long nodes;
556  double max_size_factor;
557
558  nodes=bddm->unique_table.entries;
559  max_size_factor= *(double *)bddm->reorder_data;
560  if (max_size_factor > 2.0 || nodes < 10000)
561    max_size_factor=2.0;
562  cmu_bdd_reorder_sift_aux1(bddm, max_size_factor);
563  *(double *)bddm->reorder_data=1.0+(2.0*(nodes-bddm->unique_table.entries))/nodes;
564}
565
566
567/* cmu_bdd_dynamic_reordering(bddm, reorder_fn) sets the dynamic reordering */
568/* method to that specified by reorder_fn. */
569
570void
571cmu_bdd_dynamic_reordering(cmu_bdd_manager bddm, void (*reorder_fn)(cmu_bdd_manager))
572{
573  bddm->reorder_fn=reorder_fn;
574  if (bddm->reorder_data)
575    mem_free_block(bddm->reorder_data);
576  bddm->reorder_data=0;
577  if (reorder_fn == cmu_bdd_reorder_hybrid)
578    {
579      bddm->reorder_data=mem_get_block((SIZE_T)sizeof(double));
580      *(double *)bddm->reorder_data=2.0;
581    }
582}
583
584
585static
586void
587bdd_add_internal_references(cmu_bdd_manager bddm)
588{
589  long i, j;
590  var_table table;
591  bdd *f, g, h;
592
593  for (i=0; i <= bddm->vars; ++i)
594    {
595      if (i == bddm->vars)
596        table=bddm->unique_table.tables[BDD_CONST_INDEXINDEX];
597      else
598        table=bddm->unique_table.tables[bddm->indexindexes[i]];
599      for (j=0; j < table->size; ++j)
600        {
601          f= &table->table[j];
602          while ((g= *f))
603            {
604              BDD_SETUP(g);
605              if (BDD_REFS(g) || BDD_TEMP_REFS(g))
606                {
607                  if (!BDD_IS_CONST(g))
608                    {
609                      h=(bdd)BDD_DATA0(g);
610                      {
611                        BDD_SETUP(h);
612                        BDD_INCREFS(h);
613                      }
614                      h=(bdd)BDD_DATA1(g);
615                      {
616                        BDD_SETUP(h);
617                        BDD_INCREFS(h);
618                      }
619                    }
620                  f= &g->next;
621                }
622              else
623                {
624                  *f=g->next;
625                  if (i == bddm->vars && bddm->unique_table.free_terminal_fn)
626                    (*bddm->unique_table.free_terminal_fn)(bddm,
627                                                           BDD_DATA0(g),
628                                                           BDD_DATA1(g),
629                                                           bddm->unique_table.free_terminal_env);
630                  BDD_FREE_REC(bddm, (pointer)g, sizeof(struct bdd_));
631                  table->entries--;
632                  bddm->unique_table.entries--;
633                  bddm->unique_table.freed++;
634                }
635            }
636        }
637    }
638}
639
640
641static
642void
643bdd_nuke_internal_references(cmu_bdd_manager bddm)
644{
645  long i, j;
646  var_table table;
647  bdd *f, g, h;
648
649  for (i=bddm->vars-1; i >= 0; --i)
650    {
651      table=bddm->unique_table.tables[bddm->indexindexes[i]];
652      for (j=0; j < table->size; ++j)
653        {
654          f= &table->table[j];
655          while ((g= *f))
656            {
657              BDD_SETUP(g);
658              if (BDD_REFS(g) || BDD_TEMP_REFS(g))
659                {
660                  h=(bdd)BDD_DATA0(g);
661                  {
662                    BDD_SETUP(h);
663                    BDD_DECREFS(h);
664                  }
665                  h=(bdd)BDD_DATA1(g);
666                  {
667                    BDD_SETUP(h);
668                    BDD_DECREFS(h);
669                  }
670                  f= &g->next;
671                }
672              else
673                cmu_bdd_fatal("bdd_nuke_internal_references: what happened?");
674            }
675        }
676    }
677}
678
679
680void
681cmu_bdd_reorder_aux(cmu_bdd_manager bddm)
682{
683  if (bddm->reorder_fn)
684    {
685      bdd_flush_all(bddm);
686      bdd_add_internal_references(bddm);
687      (*bddm->reorder_fn)(bddm);
688      bdd_nuke_internal_references(bddm);
689    }
690}
691
692
693/* cmu_bdd_reorder(bddm) invokes the current dynamic reordering method. */
694
695void
696cmu_bdd_reorder(cmu_bdd_manager bddm)
697{
698  cmu_bdd_gc(bddm);
699  cmu_bdd_reorder_aux(bddm);
700}
Note: See TracBrowser for help on using the repository browser.