glu-2.2: src/cmuBdd/bddreorder.c Source File

00001 /* BDD dynamic reordering stuff */
00002 
00003 
00004 #include "bddint.h"
00005 
00006 
00007 static
00008 void
00009 increfs(bdd f)
00010 {
00011   bdd g;
00012 
00013   BDD_SETUP(f);
00014   BDD_INCREFS(f);
00015   if (BDD_REFS(f) == 1 && !BDD_TEMP_REFS(f))
00016     {
00017       g=(bdd)BDD_DATA0(f);
00018       {
00019         BDD_SETUP(g);
00020         BDD_INCREFS(g);
00021       }
00022       g=(bdd)BDD_DATA1(f);
00023       {
00024         BDD_SETUP(g);
00025         BDD_INCREFS(g);
00026       }
00027     }
00028 }
00029 
00030 
00031 static
00032 void
00033 decrefs(bdd f)
00034 {
00035   bdd g;
00036 
00037   BDD_SETUP(f);
00038   BDD_DECREFS(f);
00039   if (!BDD_REFS(f) && !BDD_TEMP_REFS(f))
00040     {
00041       g=(bdd)BDD_DATA0(f);
00042       {
00043         BDD_SETUP(g);
00044         BDD_DECREFS(g);
00045       }
00046       g=(bdd)BDD_DATA1(f);
00047       {
00048         BDD_SETUP(g);
00049         BDD_DECREFS(g);
00050       }
00051     }
00052 }
00053 
00054 
00055 static
00056 void
00057 bdd_exchange_aux(cmu_bdd_manager bddm, bdd f, bdd_indexindex_type next_indexindex)
00058 {
00059   bdd f1, f2;
00060   bdd f11, f12, f21, f22;
00061   bdd temp1, temp2;
00062 
00063   BDD_SETUP(f);
00064   f1=BDD_THEN(f);
00065   f2=BDD_ELSE(f);
00066   {
00067     BDD_SETUP(f1);
00068     BDD_SETUP(f2);
00069     if (BDD_INDEXINDEX(f1) == next_indexindex)
00070       {
00071         f11=BDD_THEN(f1);
00072         f12=BDD_ELSE(f1);
00073       }
00074     else
00075       {
00076         f11=f1;
00077         f12=f1;
00078       }
00079     if (BDD_INDEXINDEX(f2) == next_indexindex)
00080       {
00081         f21=BDD_THEN(f2);
00082         f22=BDD_ELSE(f2);
00083       }
00084     else
00085       {
00086         f21=f2;
00087         f22=f2;
00088       }
00089     if (f11 == f21)
00090       temp1=f11;
00091     else
00092       temp1=bdd_find_aux(bddm, BDD_INDEXINDEX(f), (INT_PTR)f11, (INT_PTR)f21);
00093     if (f12 == f22)
00094       temp2=f12;
00095     else if (BDD_IS_OUTPOS(f12))
00096       temp2=bdd_find_aux(bddm, BDD_INDEXINDEX(f), (INT_PTR)f12, (INT_PTR)f22);
00097     else
00098       temp2=BDD_NOT(bdd_find_aux(bddm, BDD_INDEXINDEX(f), (INT_PTR)BDD_NOT(f12), (INT_PTR)BDD_NOT(f22)));
00099     BDD_INDEXINDEX(f)=next_indexindex;
00100     BDD_DATA0(f)=(INT_PTR)temp1;
00101     BDD_DATA1(f)=(INT_PTR)temp2;
00102     if (BDD_REFS(f) || BDD_TEMP_REFS(f))
00103       {
00104         increfs(temp1);
00105         increfs(temp2);
00106         decrefs(f1);
00107         decrefs(f2);
00108       }
00109     else
00110       cmu_bdd_fatal("bdd_exchange_aux: how did this happen?");
00111   }
00112 }
00113 
00114 
00115 static
00116 void
00117 fixup_assoc(cmu_bdd_manager bddm, long indexindex1, long indexindex2, var_assoc va)
00118 {
00119   /* Variable with indexindex1 is moving down a spot. */
00120   if (va->assoc[indexindex1] && va->last == bddm->indexes[indexindex1])
00121     va->last++;
00122   else if (!va->assoc[indexindex1] && va->assoc[indexindex2] && va->last == bddm->indexes[indexindex2])
00123     va->last--;
00124 }
00125 
00126 
00127 static
00128 void
00129 sweep_var_table(cmu_bdd_manager bddm, long i)
00130 {
00131   long j;
00132   var_table table;
00133   bdd f, *p;
00134 
00135   table=bddm->unique_table.tables[i];
00136   for (j=0; j < table->size; ++j)
00137     for (p= &table->table[j], f= *p; f; f= *p)
00138       {
00139         BDD_SETUP(f);
00140         if (BDD_REFS(f) || BDD_TEMP_REFS(f))
00141           p= &f->next;
00142         else
00143           {
00144             *p=f->next;
00145             BDD_FREE_REC(bddm, (pointer)f, sizeof(struct bdd_));
00146             table->entries--;
00147             bddm->unique_table.entries--;
00148             bddm->unique_table.freed++;
00149           }
00150       }
00151 }
00152 
00153 
00154 static
00155 void
00156 bdd_exchange(cmu_bdd_manager bddm, long i)
00157 {
00158   bdd_indexindex_type next_indexindex;
00159   var_table table, next_table;
00160   long j;
00161   bdd f, *p;
00162   bdd f1, f2;
00163   bdd g;
00164   long hash;
00165   bdd_index_type temp;
00166   assoc_list q;
00167 
00168   next_indexindex=bddm->indexindexes[bddm->indexes[i]+1];
00169   table=bddm->unique_table.tables[i];
00170   next_table=bddm->unique_table.tables[next_indexindex];
00171   g=0;
00172   for (j=0; j < table->size; ++j)
00173     for (p= &table->table[j], f= *p; f; f= *p)
00174       {
00175         BDD_SETUP(f);
00176         if (BDD_REFS(f) || BDD_TEMP_REFS(f))
00177           {
00178             f1=(bdd)BDD_DATA0(f);
00179             f2=(bdd)BDD_DATA1(f);
00180             {
00181               BDD_SETUP(f1);
00182               BDD_SETUP(f2);
00183               if (BDD_INDEXINDEX(f1) != next_indexindex && BDD_INDEXINDEX(f2) != next_indexindex)
00184                 p= &f->next;
00185               else
00186                 {
00187                   *p=f->next;
00188                   f->next=g;
00189                   g=f;
00190                 }
00191             }
00192           }
00193         else
00194           {
00195             *p=f->next;
00196             BDD_FREE_REC(bddm, (pointer)f, sizeof(struct bdd_));
00197             table->entries--;
00198             bddm->unique_table.entries--;
00199             bddm->unique_table.freed++;
00200           }
00201       }
00202   for (f=g; f; f=g)
00203     {
00204       bdd_exchange_aux(bddm, f, next_indexindex);
00205       g=f->next;
00206       hash=HASH_NODE(f->data[0], f->data[1]);
00207       BDD_REDUCE(hash, next_table->size);
00208       f->next=next_table->table[hash];
00209       next_table->table[hash]=f;
00210       table->entries--;
00211       next_table->entries++;
00212       if (4*next_table->size < next_table->entries)
00213         bdd_rehash_var_table(next_table, 1);
00214     }
00215   fixup_assoc(bddm, i, next_indexindex, &bddm->temp_assoc);
00216   for (q=bddm->assocs; q; q=q->next)
00217     fixup_assoc(bddm, i, next_indexindex, &q->va);
00218   sweep_var_table(bddm, next_indexindex);
00219   temp=bddm->indexes[i];
00220   bddm->indexes[i]=bddm->indexes[next_indexindex];
00221   bddm->indexes[next_indexindex]=temp;
00222   bddm->indexindexes[temp]=next_indexindex;
00223   bddm->indexindexes[bddm->indexes[i]]=i;
00224 }
00225 
00226 
00227 void
00228 cmu_bdd_var_block_reorderable(cmu_bdd_manager bddm, block b, int reorderable)
00229 {
00230   b->reorderable=reorderable;
00231 }
00232 
00233 
00234 static
00235 void
00236 bdd_exchange_var_blocks(cmu_bdd_manager bddm, block parent, long bi)
00237 {
00238   block b1, b2;
00239   long i, j, k, l;
00240   long delta;
00241   block temp;
00242 
00243   b1=parent->children[bi];
00244   b2=parent->children[bi+1];
00245   /* This slides the blocks past each other in a kind of interleaving */
00246   /* fashion. */
00247   for (i=0; i <= b1->last_index-b1->first_index+b2->last_index-b2->first_index; ++i)
00248     {
00249       j=i-b1->last_index+b1->first_index;
00250       if (j < 0)
00251         j=0;
00252       k=i;
00253       if (k > b2->last_index-b2->first_index)
00254         k=b2->last_index-b2->first_index;
00255       while (j <= k)
00256         {
00257           l=b2->first_index+j-i+j;
00258           bdd_exchange(bddm, bddm->indexindexes[l-1]);
00259           ++j;
00260         }
00261     }
00262   delta=b2->last_index-b2->first_index+1;
00263   bdd_block_delta(b1, delta);
00264   delta=b1->last_index-b1->first_index+1;
00265   bdd_block_delta(b2, -delta);
00266   temp=parent->children[bi];
00267   parent->children[bi]=parent->children[bi+1];
00268   parent->children[bi+1]=temp;
00269 }
00270 
00271 
00272 static
00273 int
00274 cmu_bdd_reorder_window2(cmu_bdd_manager bddm, block b, long i)
00275 {
00276   long size, best_size;
00277 
00278   /* 1 2 */
00279   best_size=bddm->unique_table.entries;
00280   bdd_exchange_var_blocks(bddm, b, i);
00281   /* 2 1 */
00282   size=bddm->unique_table.entries;
00283   if (size < best_size)
00284     return (1);
00285   bdd_exchange_var_blocks(bddm, b, i);
00286   return (0);
00287 }
00288 
00289 
00290 static
00291 int
00292 cmu_bdd_reorder_window3(cmu_bdd_manager bddm, block b, long i)
00293 {
00294   int best;
00295   long size, best_size;
00296 
00297   best=0;
00298   /* 1 2 3 */
00299   best_size=bddm->unique_table.entries;
00300   bdd_exchange_var_blocks(bddm, b, i);
00301   /* 2 1 3 */
00302   size=bddm->unique_table.entries;
00303   if (size < best_size)
00304     {
00305       best=1;
00306       best_size=size;
00307     }
00308   bdd_exchange_var_blocks(bddm, b, i+1);
00309   /* 2 3 1 */
00310   size=bddm->unique_table.entries;
00311   if (size < best_size)
00312     {
00313       best=2;
00314       best_size=size;
00315     }
00316   bdd_exchange_var_blocks(bddm, b, i);
00317   /* 3 2 1 */
00318   size=bddm->unique_table.entries;
00319   if (size < best_size)
00320     {
00321       best=3;
00322       best_size=size;
00323     }
00324   bdd_exchange_var_blocks(bddm, b, i+1);
00325   /* 3 1 2 */
00326   size=bddm->unique_table.entries;
00327   if (size < best_size)
00328     {
00329       best=4;
00330       best_size=size;
00331     }
00332   bdd_exchange_var_blocks(bddm, b, i);
00333   /* 1 3 2 */
00334   size=bddm->unique_table.entries;
00335   if (size < best_size)
00336     {
00337       best=5;
00338       best_size=size;
00339     }
00340   switch (best)
00341     {
00342     case 0:
00343       bdd_exchange_var_blocks(bddm, b, i+1);
00344       break;
00345     case 1:
00346       bdd_exchange_var_blocks(bddm, b, i+1);
00347       bdd_exchange_var_blocks(bddm, b, i);
00348       break;
00349     case 2:
00350       bdd_exchange_var_blocks(bddm, b, i+1);
00351       bdd_exchange_var_blocks(bddm, b, i);
00352       bdd_exchange_var_blocks(bddm, b, i+1);
00353       break;
00354     case 3:
00355       bdd_exchange_var_blocks(bddm, b, i);
00356       bdd_exchange_var_blocks(bddm, b, i+1);
00357       break;
00358     case 4:
00359       bdd_exchange_var_blocks(bddm, b, i);
00360       break;
00361     case 5:
00362       break;
00363     }
00364   return (best > 0);
00365 }
00366 
00367 
00368 static
00369 void
00370 cmu_bdd_reorder_stable_window3_aux(cmu_bdd_manager bddm, block b, char *levels)
00371 {
00372   long i;
00373   int moved;
00374   int any_swapped;
00375 
00376   if (b->reorderable)
00377     {
00378       for (i=0; i < b->num_children-1; ++i)
00379         levels[i]=1;
00380       do
00381         {
00382           any_swapped=0;
00383           for (i=0; i < b->num_children-1; ++i)
00384             if (levels[i])
00385               {
00386                 if (i < b->num_children-2)
00387                   moved=cmu_bdd_reorder_window3(bddm, b, i);
00388                 else
00389                   moved=cmu_bdd_reorder_window2(bddm, b, i);
00390                 if (moved)
00391                   {
00392                     if (i > 0)
00393                       {
00394                         levels[i-1]=1;
00395                         if (i > 1)
00396                           levels[i-2]=1;
00397                       }
00398                     levels[i]=1;
00399                     levels[i+1]=1;
00400                     if (i < b->num_children-2)
00401                       {
00402                         levels[i+2]=1;
00403                         if (i < b->num_children-3)
00404                           {
00405                             levels[i+3]=1;
00406                             if (i < b->num_children-4)
00407                               levels[i+4]=1;
00408                           }
00409                       }
00410                     any_swapped=1;
00411                   }
00412                 else
00413                   levels[i]=0;
00414               }
00415         }
00416       while (any_swapped);
00417     }
00418   for (i=0; i < b->num_children; ++i)
00419     cmu_bdd_reorder_stable_window3_aux(bddm, b->children[i], levels);
00420 }
00421 
00422 
00423 void
00424 cmu_bdd_reorder_stable_window3(cmu_bdd_manager bddm)
00425 {
00426   char *levels;
00427 
00428   levels=(char *)mem_get_block(bddm->vars*sizeof(char));
00429   cmu_bdd_reorder_stable_window3_aux(bddm, bddm->super_block, levels);
00430   mem_free_block((pointer)levels);
00431 }
00432 
00433 
00434 static
00435 void
00436 bdd_sift_block(cmu_bdd_manager bddm, block b, long start_pos, double max_size_factor)
00437 {
00438   long start_size;
00439   long best_size;
00440   long best_pos;
00441   long curr_size;
00442   long curr_pos;
00443   long max_size;
00444 
00445   start_size=bddm->unique_table.entries;
00446   best_size=start_size;
00447   best_pos=start_pos;
00448   curr_size=start_size;
00449   curr_pos=start_pos;
00450   max_size=max_size_factor*start_size;
00451   if (bddm->unique_table.node_limit && max_size > bddm->unique_table.node_limit)
00452     max_size=bddm->unique_table.node_limit;
00453   while (curr_pos < b->num_children-1 && curr_size <= max_size)
00454     {
00455       bdd_exchange_var_blocks(bddm, b, curr_pos);
00456       ++curr_pos;
00457       curr_size=bddm->unique_table.entries;
00458       if (curr_size < best_size)
00459         {
00460           best_size=curr_size;
00461           best_pos=curr_pos;
00462         }
00463     }
00464   while (curr_pos != start_pos)
00465     {
00466       --curr_pos;
00467       bdd_exchange_var_blocks(bddm, b, curr_pos);
00468     }
00469   curr_size=start_size;
00470   while (curr_pos && curr_size <= max_size)
00471     {
00472       --curr_pos;
00473       bdd_exchange_var_blocks(bddm, b, curr_pos);
00474       curr_size=bddm->unique_table.entries;
00475       if (curr_size < best_size)
00476         {
00477           best_size=curr_size;
00478           best_pos=curr_pos;
00479         }
00480     }
00481   while (curr_pos != best_pos)
00482     {
00483       bdd_exchange_var_blocks(bddm, b, curr_pos);
00484       ++curr_pos;
00485     }
00486 }
00487 
00488 
00489 static
00490 void
00491 cmu_bdd_reorder_sift_aux(cmu_bdd_manager bddm, block b, block *to_sift, double max_size_factor)
00492 {
00493   long i, j, k;
00494   long w;
00495   long max_w;
00496   long widest;
00497 
00498   if (b->reorderable)
00499     {
00500       for (i=0; i < b->num_children; ++i)
00501         to_sift[i]=b->children[i];
00502       while (i)
00503         {
00504           --i;
00505           max_w=0;
00506           widest=0;
00507           for (j=0; j <= i; ++j)
00508             {
00509               for (w=0, k=to_sift[j]->first_index; k <= to_sift[j]->last_index; ++k)
00510                 w+=bddm->unique_table.tables[bddm->indexindexes[k]]->entries;
00511               w/=to_sift[j]->last_index-to_sift[j]->first_index+1;
00512               if (w > max_w)
00513                 {
00514                   max_w=w;
00515                   widest=j;
00516                 }
00517             }
00518           if (max_w > 1)
00519             {
00520               for (j=0; b->children[j] != to_sift[widest]; ++j);
00521               bdd_sift_block(bddm, b, j, max_size_factor);
00522               to_sift[widest]=to_sift[i];
00523             }
00524           else
00525             break;
00526         }
00527     }
00528   for (i=0; i < b->num_children; ++i)
00529     cmu_bdd_reorder_sift_aux(bddm, b->children[i], to_sift, max_size_factor);
00530 }
00531 
00532 
00533 static
00534 void
00535 cmu_bdd_reorder_sift_aux1(cmu_bdd_manager bddm, double max_size_factor)
00536 {
00537   block *to_sift;
00538 
00539   to_sift=(block *)mem_get_block(bddm->vars*sizeof(block));
00540   cmu_bdd_reorder_sift_aux(bddm, bddm->super_block, to_sift, max_size_factor);
00541   mem_free_block((pointer)to_sift);
00542 }
00543 
00544 
00545 void
00546 cmu_bdd_reorder_sift(cmu_bdd_manager bddm)
00547 {
00548   cmu_bdd_reorder_sift_aux1(bddm, 2.0);
00549 }
00550 
00551 
00552 void
00553 cmu_bdd_reorder_hybrid(cmu_bdd_manager bddm)
00554 {
00555   long nodes;
00556   double max_size_factor;
00557 
00558   nodes=bddm->unique_table.entries;
00559   max_size_factor= *(double *)bddm->reorder_data;
00560   if (max_size_factor > 2.0 || nodes < 10000)
00561     max_size_factor=2.0;
00562   cmu_bdd_reorder_sift_aux1(bddm, max_size_factor);
00563   *(double *)bddm->reorder_data=1.0+(2.0*(nodes-bddm->unique_table.entries))/nodes;
00564 }
00565 
00566 
00567 /* cmu_bdd_dynamic_reordering(bddm, reorder_fn) sets the dynamic reordering */
00568 /* method to that specified by reorder_fn. */
00569 
00570 void
00571 cmu_bdd_dynamic_reordering(cmu_bdd_manager bddm, void (*reorder_fn)(cmu_bdd_manager))
00572 {
00573   bddm->reorder_fn=reorder_fn;
00574   if (bddm->reorder_data)
00575     mem_free_block(bddm->reorder_data);
00576   bddm->reorder_data=0;
00577   if (reorder_fn == cmu_bdd_reorder_hybrid)
00578     {
00579       bddm->reorder_data=mem_get_block((SIZE_T)sizeof(double));
00580       *(double *)bddm->reorder_data=2.0;
00581     }
00582 }
00583 
00584 
00585 static
00586 void
00587 bdd_add_internal_references(cmu_bdd_manager bddm)
00588 {
00589   long i, j;
00590   var_table table;
00591   bdd *f, g, h;
00592 
00593   for (i=0; i <= bddm->vars; ++i)
00594     {
00595       if (i == bddm->vars)
00596         table=bddm->unique_table.tables[BDD_CONST_INDEXINDEX];
00597       else
00598         table=bddm->unique_table.tables[bddm->indexindexes[i]];
00599       for (j=0; j < table->size; ++j)
00600         {
00601           f= &table->table[j];
00602           while ((g= *f))
00603             {
00604               BDD_SETUP(g);
00605               if (BDD_REFS(g) || BDD_TEMP_REFS(g))
00606                 {
00607                   if (!BDD_IS_CONST(g))
00608                     {
00609                       h=(bdd)BDD_DATA0(g);
00610                       {
00611                         BDD_SETUP(h);
00612                         BDD_INCREFS(h);
00613                       }
00614                       h=(bdd)BDD_DATA1(g);
00615                       {
00616                         BDD_SETUP(h);
00617                         BDD_INCREFS(h);
00618                       }
00619                     }
00620                   f= &g->next;
00621                 }
00622               else
00623                 {
00624                   *f=g->next;
00625                   if (i == bddm->vars && bddm->unique_table.free_terminal_fn)
00626                     (*bddm->unique_table.free_terminal_fn)(bddm,
00627                                                            BDD_DATA0(g),
00628                                                            BDD_DATA1(g),
00629                                                            bddm->unique_table.free_terminal_env);
00630                   BDD_FREE_REC(bddm, (pointer)g, sizeof(struct bdd_));
00631                   table->entries--;
00632                   bddm->unique_table.entries--;
00633                   bddm->unique_table.freed++;
00634                 }
00635             }
00636         }
00637     }
00638 }
00639 
00640 
00641 static
00642 void
00643 bdd_nuke_internal_references(cmu_bdd_manager bddm)
00644 {
00645   long i, j;
00646   var_table table;
00647   bdd *f, g, h;
00648 
00649   for (i=bddm->vars-1; i >= 0; --i)
00650     {
00651       table=bddm->unique_table.tables[bddm->indexindexes[i]];
00652       for (j=0; j < table->size; ++j)
00653         {
00654           f= &table->table[j];
00655           while ((g= *f))
00656             {
00657               BDD_SETUP(g);
00658               if (BDD_REFS(g) || BDD_TEMP_REFS(g))
00659                 {
00660                   h=(bdd)BDD_DATA0(g);
00661                   {
00662                     BDD_SETUP(h);
00663                     BDD_DECREFS(h);
00664                   }
00665                   h=(bdd)BDD_DATA1(g);
00666                   {
00667                     BDD_SETUP(h);
00668                     BDD_DECREFS(h);
00669                   }
00670                   f= &g->next;
00671                 }
00672               else
00673                 cmu_bdd_fatal("bdd_nuke_internal_references: what happened?");
00674             }
00675         }
00676     }
00677 }
00678 
00679 
00680 void
00681 cmu_bdd_reorder_aux(cmu_bdd_manager bddm)
00682 {
00683   if (bddm->reorder_fn)
00684     {
00685       bdd_flush_all(bddm);
00686       bdd_add_internal_references(bddm);
00687       (*bddm->reorder_fn)(bddm);
00688       bdd_nuke_internal_references(bddm);
00689     }
00690 }
00691 
00692 
00693 /* cmu_bdd_reorder(bddm) invokes the current dynamic reordering method. */
00694 
00695 void
00696 cmu_bdd_reorder(cmu_bdd_manager bddm)
00697 {
00698   cmu_bdd_gc(bddm);
00699   cmu_bdd_reorder_aux(bddm);
00700 }