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

00001 /* Basic BDD routines */
00002 
00003 
00004 #include "bddint.h"
00005 
00006 
00007 /* cmu_bdd_one(bddm) gives the BDD for true. */
00008 
00009 bdd
00010 cmu_bdd_one(cmu_bdd_manager bddm)
00011 {
00012   return (BDD_ONE(bddm));
00013 }
00014 
00015 
00016 /* cmu_bdd_zero(bddm) gives the BDD for false. */
00017 
00018 bdd
00019 cmu_bdd_zero(cmu_bdd_manager bddm)
00020 {
00021   return (BDD_ZERO(bddm));
00022 }
00023 
00024 
00025 bdd
00026 bdd_make_external(bdd f)
00027 {
00028   BDD_SETUP(f);
00029   BDD_INCREFS(f);
00030   BDD_TEMP_DECREFS(f);
00031   return (f);
00032 }
00033 
00034 
00035 long
00036 bdd_find_block(block b, long index)
00037 {
00038   long i, j, k;
00039 
00040   i=0;
00041   j=b->num_children-1;
00042   while (i <= j)
00043     {
00044       k=(i+j)/2;
00045       if (b->children[k]->first_index <= index && b->children[k]->last_index >= index)
00046         return (k);
00047       if (b->children[k]->first_index > index)
00048         j=k-1;
00049       else
00050         i=k+1;
00051     }
00052   return (i);
00053 }
00054 
00055 
00056 void
00057 bdd_block_delta(block b, long delta)
00058 {
00059   long i;
00060 
00061   b->first_index+=delta;
00062   b->last_index+=delta;
00063   for (i=0; i < b->num_children; ++i)
00064     bdd_block_delta(b->children[i], delta);
00065 }
00066 
00067 
00068 static
00069 block
00070 shift_block(cmu_bdd_manager bddm, block b, long index)
00071 {
00072   long i, j;
00073   block p;
00074 
00075   if (b->first_index >= index)
00076     {
00077       bdd_block_delta(b, 1l);
00078       return (b);
00079     }
00080   if (b->last_index < index)
00081     return (b);
00082   b->last_index++;
00083   i=bdd_find_block(b, index);
00084   if (i == b->num_children || b->children[i]->first_index == index)
00085     {
00086       b->children=(block *)mem_resize_block((pointer)b->children, (SIZE_T)(sizeof(block)*(b->num_children+1)));
00087       for (j=b->num_children-1; j >= i; --j)
00088         b->children[j+1]=shift_block(bddm, b->children[j], index);
00089       b->num_children++;
00090       p=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
00091       p->reorderable=0;
00092       p->first_index=index;
00093       p->last_index=index;
00094       p->num_children=0;
00095       p->children=0;
00096       b->children[i]=p;
00097     }
00098   else
00099     while (i < b->num_children)
00100       {
00101         shift_block(bddm, b->children[i], index);
00102         ++i;
00103       }
00104   return (b);
00105 }
00106 
00107 
00108 /* bdd_new_var(bddm, index) creates a new variable with the */
00109 /* specified index.  Existing variables with greater or equal index */
00110 /* have their index incremented. */
00111 
00112 static
00113 bdd
00114 bdd_new_var(cmu_bdd_manager bddm, bdd_index_type index)
00115 {
00116   long i;
00117   long temp;
00118   long oldmax;
00119   assoc_list p;
00120   bdd var;
00121 
00122   if (bddm->vars == BDD_MAX_INDEXINDEX)
00123     cmu_bdd_fatal("bdd_new_var: no more indexes");
00124   if (index > bddm->vars)
00125     cmu_bdd_fatal("bdd_new_var: index out of range");
00126   if (bddm->vars == bddm->maxvars)
00127     {
00128       /* Expand indexing tables and variable associations. */
00129       oldmax=bddm->maxvars;
00130       temp=bddm->maxvars*2;
00131       if (temp > BDD_MAX_INDEXINDEX-1)
00132         temp=BDD_MAX_INDEXINDEX-1;
00133       bddm->maxvars=temp;
00134       bddm->variables=(bdd *)mem_resize_block((pointer)bddm->variables,
00135                                               (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
00136       bddm->indexes=(bdd_index_type *)mem_resize_block((pointer)bddm->indexes,
00137                                                        (SIZE_T)((bddm->maxvars+1)*sizeof(bdd_index_type)));
00138       bddm->indexindexes=
00139         (bdd_indexindex_type *)mem_resize_block((pointer)bddm->indexindexes,
00140                                                 (SIZE_T)(bddm->maxvars*sizeof(bdd_indexindex_type)));
00141       bddm->unique_table.tables=
00142         (var_table *)mem_resize_block((pointer)bddm->unique_table.tables,
00143                                       (SIZE_T)((bddm->maxvars+1)*sizeof(var_table)));
00144       /* Variable associations are padded with nulls in case new variables */
00145       /* are created. */
00146       for (p=bddm->assocs; p; p=p->next)
00147         {
00148           p->va.assoc=(bdd *)mem_resize_block((pointer)p->va.assoc, (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
00149           for (i=oldmax; i < bddm->maxvars; ++i)
00150             p->va.assoc[i+1]=0;
00151         }
00152       bddm->temp_assoc.assoc=(bdd *)mem_resize_block((pointer)bddm->temp_assoc.assoc, (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
00153       for (i=oldmax; i < bddm->maxvars; ++i)
00154         bddm->temp_assoc.assoc[i+1]=0;
00155     }
00156   /* Shift index of following variables. */
00157   if (index != bddm->vars)
00158     for (i=0; i < bddm->vars; ++i)
00159       if (bddm->indexes[i+1] >= index)
00160         bddm->indexes[i+1]++;
00161   for (p=bddm->assocs; p; p=p->next)
00162     if (p->va.last >= index)
00163       p->va.last++;
00164   if (bddm->temp_assoc.last >= index)
00165     bddm->temp_assoc.last++;
00166   /* Shift indexindex values. */
00167   for (i=bddm->vars; i > index; --i)
00168     bddm->indexindexes[i]=bddm->indexindexes[i-1];
00169   /* Make a new variable table. */
00170   bddm->vars++;
00171   bddm->unique_table.tables[bddm->vars]=bdd_new_var_table(bddm);
00172   /* Create the variable. */
00173   var=bdd_find_aux(bddm, (bdd_indexindex_type)bddm->vars, (INT_PTR)BDD_ONE(bddm), (INT_PTR)BDD_ZERO(bddm));
00174   var->refs=BDD_MAX_REFS;
00175   /* Record everything. */
00176   bddm->variables[bddm->vars]=var;
00177   bddm->indexes[bddm->vars]=index;
00178   bddm->indexindexes[index]=bddm->vars;
00179   /* Make a new variable block containing the variable. */
00180   shift_block(bddm, bddm->super_block, (long)index);
00181   return (var);
00182 }
00183 
00184 
00185 /* cmu_bdd_new_var_first(bddm) returns the BDD for a new variable at the */
00186 /* start of the variable order. */
00187 
00188 bdd
00189 cmu_bdd_new_var_first(cmu_bdd_manager bddm)
00190 {
00191   return (bdd_new_var(bddm, (bdd_index_type)0));
00192 }
00193 
00194 
00195 /* cmu_bdd_new_var_last(bddm) returns the BDD for a new variable at the */
00196 /* end of the variable order. */
00197 
00198 bdd
00199 cmu_bdd_new_var_last(cmu_bdd_manager bddm)
00200 {
00201   return (bdd_new_var(bddm, (bdd_index_type)bddm->vars));
00202 }
00203 
00204 
00205 /* cmu_bdd_new_var_before(bddm, var) returns the BDD for a new variable */
00206 /* before the specified one in the variable order. */
00207 
00208 bdd
00209 cmu_bdd_new_var_before(cmu_bdd_manager bddm, bdd var)
00210 {
00211   if (bdd_check_arguments(1, var))
00212     {
00213       BDD_SETUP(var);
00214       if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
00215         {
00216           cmu_bdd_warning("cmu_bdd_new_var_before: argument is not a positive variable");
00217           if (BDD_IS_CONST(var))
00218             return (cmu_bdd_new_var_last(bddm));
00219         }
00220       return (bdd_new_var(bddm, BDD_INDEX(bddm, var)));
00221     }
00222   return ((bdd)0);
00223 }
00224 
00225 
00226 /* cmu_bdd_new_var_after(bddm, var) returns the BDD for a new variable */
00227 /* after the specified one in the variable order. */
00228 
00229 bdd
00230 cmu_bdd_new_var_after(cmu_bdd_manager bddm, bdd var)
00231 {
00232   if (bdd_check_arguments(1, var))
00233     {
00234       BDD_SETUP(var);
00235       if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
00236         {
00237           cmu_bdd_warning("cmu_bdd_new_var_after: argument is not a positive variable");
00238           if (BDD_IS_CONST(var))
00239             return (cmu_bdd_new_var_last(bddm));
00240         }
00241       return (bdd_new_var(bddm, BDD_INDEX(bddm, var)+1));
00242     }
00243   return ((bdd)0);
00244 }
00245 
00246 
00247 /* cmu_bdd_var_with_index(bddm, index) returns the variable with the */
00248 /* specified index, or null if there is no such variable. */
00249 
00250 bdd
00251 cmu_bdd_var_with_index(cmu_bdd_manager bddm, long index)
00252 {
00253   if (index < 0 || index >= bddm->vars)
00254     return ((bdd)0);
00255   return (bddm->variables[bddm->indexindexes[index]]);
00256 }
00257 
00258 
00259 /* cmu_bdd_var_with_id(bddm, id) returns the variable with the specified */
00260 /* id, or null if there is no such variable. */
00261 
00262 bdd
00263 cmu_bdd_var_with_id(cmu_bdd_manager bddm, long indexindex)
00264 {
00265   if (indexindex <= 0 || indexindex > bddm->vars)
00266     return ((bdd)0);
00267   return (bddm->variables[indexindex]);
00268 }
00269 
00270 
00271 static
00272 bdd
00273 cmu_bdd_and_step(cmu_bdd_manager bddm, bdd f, bdd g)
00274 {
00275   bdd_indexindex_type top_indexindex;
00276   bdd f1, f2;
00277   bdd g1, g2;
00278   bdd temp1, temp2;
00279   bdd result;
00280 
00281   BDD_SETUP(f);
00282   BDD_SETUP(g);
00283   if (BDD_IS_CONST(f))
00284     {
00285       if (f == BDD_ZERO(bddm))
00286         return (f);
00287       BDD_TEMP_INCREFS(g);
00288       return (g);
00289     }
00290   /* f is not constant. */
00291   if (BDD_IS_CONST(g))
00292     {
00293       if (g == BDD_ZERO(bddm))
00294         return (g);
00295       BDD_TEMP_INCREFS(f);
00296       return (f);
00297     }
00298   /* f and g are not constant. */
00299   if (BDD_SAME_OR_NEGATIONS(f, g))
00300     {
00301       if (f == g)
00302         {
00303           BDD_TEMP_INCREFS(f);
00304           return (f);
00305         }
00306       return (BDD_ZERO(bddm));
00307     }
00308   /* f and g are not constant and are not equal or negations. */
00309   if (BDD_OUT_OF_ORDER(f, g))
00310     BDD_SWAP(f, g);
00311   if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR *)&result))
00312     return (result);
00313   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00314   BDD_COFACTOR(top_indexindex, f, f1, f2);
00315   BDD_COFACTOR(top_indexindex, g, g1, g2);
00316   temp1=cmu_bdd_and_step(bddm, f1, g1);
00317   temp2=cmu_bdd_and_step(bddm, f2, g2);
00318   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00319   bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR)result);
00320   return (result);
00321 }
00322 
00323 
00324 static
00325 bdd
00326 cmu_bdd_xnor_step(cmu_bdd_manager bddm, bdd f, bdd g)
00327 {
00328   int outneg;
00329   bdd_indexindex_type top_indexindex;
00330   bdd f1, f2;
00331   bdd g1, g2;
00332   bdd temp1, temp2;
00333   bdd result;
00334 
00335   BDD_SETUP(f);
00336   BDD_SETUP(g);
00337   if (BDD_IS_CONST(f))
00338     {
00339       BDD_TEMP_INCREFS(g);
00340       if (f == BDD_ONE(bddm))
00341         return (g);
00342       return (BDD_NOT(g));
00343     }
00344   if (BDD_IS_CONST(g))
00345     {
00346       BDD_TEMP_INCREFS(f);
00347       if (g == BDD_ONE(bddm))
00348         return (f);
00349       return (BDD_NOT(f));
00350     }
00351   /* f and g are not constant. */
00352   if (BDD_SAME_OR_NEGATIONS(f, g))
00353     {
00354       if (f == g)
00355         return (BDD_ONE(bddm));
00356       return (BDD_ZERO(bddm));
00357     }
00358   /* f and g are not constant, not same, not negations. */
00359   if (BDD_OUT_OF_ORDER(f, g))
00360     BDD_SWAP(f, g);
00361   if (BDD_IS_OUTPOS(g))
00362     outneg=0;
00363   else
00364     {
00365       outneg=1;
00366       g=BDD_NOT(g);
00367     }
00368   /* g is an uncomplemented output pointer. */
00369   if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_NOT(g), (INT_PTR *)&result))
00370     return (outneg ? BDD_NOT(result) : result);
00371   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00372   BDD_COFACTOR(top_indexindex, f, f1, f2);
00373   BDD_COFACTOR(top_indexindex, g, g1, g2);
00374   temp1=cmu_bdd_xnor_step(bddm, f1, g1);
00375   temp2=cmu_bdd_xnor_step(bddm, f2, g2);
00376   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00377   bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_NOT(g), (INT_PTR)result);
00378   return (outneg ? BDD_NOT(result) : result);
00379 }
00380 
00381 
00382 bdd
00383 cmu_bdd_ite_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
00384 {
00385   int outneg;
00386   bdd_indexindex_type top_indexindex;
00387   bdd f1, f2;
00388   bdd g1, g2;
00389   bdd h1, h2;
00390   bdd temp1, temp2;
00391   bdd result;
00392 
00393   BDD_SETUP(f);
00394   BDD_SETUP(g);
00395   BDD_SETUP(h);
00396   if (BDD_IS_CONST(f))
00397     {
00398       if (f == BDD_ONE(bddm))
00399         {
00400           BDD_TEMP_INCREFS(g);
00401           return (g);
00402         }
00403       BDD_TEMP_INCREFS(h);
00404       return (h);
00405     }
00406   /* f is not constant. */
00407   if (BDD_SAME_OR_NEGATIONS(f, g))
00408     {
00409       if (f == g)
00410         g=BDD_ONE(bddm);
00411       else
00412         g=BDD_ZERO(bddm);
00413       BDD_RESET(g);
00414     }
00415   if (BDD_SAME_OR_NEGATIONS(f, h))
00416     {
00417       if (f == h)
00418         h=BDD_ZERO(bddm);
00419       else
00420         h=BDD_ONE(bddm);
00421       BDD_RESET(h);
00422     }
00423   if (BDD_IS_CONST(g))
00424     {
00425       if (BDD_IS_CONST(h))
00426         {
00427           if (g == h)
00428             return (g);
00429           BDD_TEMP_INCREFS(f);
00430           if (g == BDD_ONE(bddm))
00431             return (f);
00432           return (BDD_NOT(f));
00433         }
00434       if (g == BDD_ZERO(bddm))
00435         return (cmu_bdd_and_step(bddm, BDD_NOT(f), h));
00436       return (BDD_NOT(cmu_bdd_and_step(bddm, BDD_NOT(f), BDD_NOT(h))));
00437     }
00438   else if (BDD_SAME_OR_NEGATIONS(g, h))
00439     {
00440       if (g == h)
00441         {
00442           BDD_TEMP_INCREFS(g);
00443           return (g);
00444         }
00445       return (cmu_bdd_xnor_step(bddm, f, g));
00446     }
00447   else if (BDD_IS_CONST(h))
00448     {
00449     if (h == BDD_ZERO(bddm))
00450       return (cmu_bdd_and_step(bddm, f, g));
00451     else
00452       return (BDD_NOT(cmu_bdd_and_step(bddm, f, BDD_NOT(g))));
00453     }
00454   /* No special cases; it's a real if-then-else. */
00455   if (!BDD_IS_OUTPOS(f))
00456     {
00457       f=BDD_NOT(f);
00458       BDD_SWAP(g, h);
00459     }
00460   /* f is now an uncomplemented output pointer. */
00461   if (BDD_IS_OUTPOS(g))
00462     outneg=0;
00463   else
00464     {
00465       outneg=1;
00466       g=BDD_NOT(g);
00467       h=BDD_NOT(h);
00468     }
00469   /* g is now an uncomplemented output pointer. */
00470   if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR *)&result))
00471     return (outneg ? BDD_NOT(result) : result);
00472   BDD_TOP_VAR3(top_indexindex, bddm, f, g, h);
00473   BDD_COFACTOR(top_indexindex, f, f1, f2);
00474   BDD_COFACTOR(top_indexindex, g, g1, g2);
00475   BDD_COFACTOR(top_indexindex, h, h1, h2);
00476   temp1=cmu_bdd_ite_step(bddm, f1, g1, h1);
00477   temp2=cmu_bdd_ite_step(bddm, f2, g2, h2);
00478   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00479   bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR)result);
00480   return (outneg ? BDD_NOT(result) : result);
00481 }
00482 
00483 
00484 /* cmu_bdd_ite(bddm, f, g, h) returns the BDD for "if f then g else h". */
00485 
00486 bdd
00487 cmu_bdd_ite(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
00488 {
00489   if (bdd_check_arguments(3, f, g, h))
00490     {
00491       FIREWALL(bddm);
00492       RETURN_BDD(cmu_bdd_ite_step(bddm, f, g, h));
00493     }
00494   return ((bdd)0);
00495 }
00496 
00497 
00498 /* cmu_bdd_and(bddm, f, g) returns the BDD for "f and g". */
00499 
00500 bdd
00501 cmu_bdd_and(cmu_bdd_manager bddm, bdd f, bdd g)
00502 {
00503   return (cmu_bdd_ite(bddm, f, g, BDD_ZERO(bddm)));
00504 }
00505 
00506 
00507 /* cmu_bdd_nand(bddm, f, g) returns the BDD for "f nand g". */
00508 
00509 bdd
00510 cmu_bdd_nand(cmu_bdd_manager bddm, bdd f, bdd g)
00511 {
00512   bdd temp;
00513 
00514   if ((temp=cmu_bdd_and(bddm, f, g)))
00515     return (BDD_NOT(temp));
00516   return ((bdd)0);
00517 }
00518 
00519 
00520 /* cmu_bdd_or(bddm, f, g) returns the BDD for "f or g". */
00521 
00522 bdd
00523 cmu_bdd_or(cmu_bdd_manager bddm, bdd f, bdd g)
00524 {
00525   return (cmu_bdd_ite(bddm, f, BDD_ONE(bddm), g));
00526 }
00527 
00528 
00529 /* cmu_bdd_nor(bddm, f, g) returns the BDD for "f nor g". */
00530 
00531 bdd
00532 cmu_bdd_nor(cmu_bdd_manager bddm, bdd f, bdd g)
00533 {
00534   bdd temp;
00535 
00536   if ((temp=cmu_bdd_or(bddm, f, g)))
00537     return (BDD_NOT(temp));
00538   return ((bdd)0);
00539 }
00540 
00541 
00542 /* cmu_bdd_xor(bddm, f, g) returns the BDD for "f xor g". */
00543 
00544 bdd
00545 cmu_bdd_xor(cmu_bdd_manager bddm, bdd f, bdd g)
00546 {
00547   return (cmu_bdd_ite(bddm, f, BDD_NOT(g), g));
00548 }
00549 
00550 
00551 /* cmu_bdd_xnor(bddm, f, g) returns the BDD for "f xnor g". */
00552 
00553 bdd
00554 cmu_bdd_xnor(cmu_bdd_manager bddm, bdd f, bdd g)
00555 {
00556   bdd temp;
00557 
00558   if ((temp=cmu_bdd_xor(bddm, f, g)))
00559     return (BDD_NOT(temp));
00560   return ((bdd)0);
00561 }
00562 
00563 
00564 /* cmu_bdd_identity(bddm, f) returns the BDD for f.  (The only effect is */
00565 /* to increase the reference count for f.) */
00566 
00567 bdd
00568 cmu_bdd_identity(cmu_bdd_manager bddm, bdd f)
00569 {
00570   if (bdd_check_arguments(1, f))
00571     {
00572       BDD_SETUP(f);
00573       BDD_INCREFS(f);
00574     }
00575   return (f);
00576 }
00577 
00578 
00579 /* cmu_bdd_not(bddm, f) returns the BDD for "not f". */
00580 
00581 bdd
00582 cmu_bdd_not(cmu_bdd_manager bddm, bdd f)
00583 {
00584   if (bdd_check_arguments(1, f))
00585     {
00586       BDD_SETUP(f);
00587       BDD_INCREFS(f);
00588       return (BDD_NOT(f));
00589     }
00590   return ((bdd)0);
00591 }
00592  
00593 
00594 /* cmu_bdd_if(bddm, f) returns the BDD for the variable at the top of f. */
00595 
00596 bdd
00597 cmu_bdd_if(cmu_bdd_manager bddm, bdd f)
00598 {
00599   if (bdd_check_arguments(1, f))
00600     {
00601       BDD_SETUP(f);
00602       if (BDD_IS_CONST(f))
00603         {
00604           cmu_bdd_warning("cmu_bdd_if: argument is a constant");
00605           return (f);
00606         }
00607       FIREWALL(bddm);
00608       RETURN_BDD(BDD_IF(bddm, f));
00609     }
00610   return (f);
00611 }
00612 
00613 
00614 /* cmu_bdd_if_index(bddm, f) returns the index for the variable at the top */
00615 /* of f. */
00616 
00617 long
00618 cmu_bdd_if_index(cmu_bdd_manager bddm, bdd f)
00619 {
00620   if (bdd_check_arguments(1, f))
00621     {
00622       BDD_SETUP(f);
00623       if (BDD_IS_CONST(f))
00624         return (-1l);
00625       return ((long)BDD_INDEX(bddm, f));
00626     }
00627   return (-1l);
00628 }
00629 
00630 
00631 /* cmu_bdd_if_id(bddm, f) returns a unique identifier for the variable at */
00632 /* the top of f. */
00633 
00634 long
00635 cmu_bdd_if_id(cmu_bdd_manager bddm, bdd f)
00636 {
00637   if (bdd_check_arguments(1, f))
00638     {
00639       BDD_SETUP(f);
00640       if (BDD_IS_CONST(f))
00641         return (-1l);
00642       return ((long)BDD_INDEXINDEX(f));
00643     }
00644   return (-1l);
00645 }
00646 
00647 
00648 /* cmu_bdd_then(bddm, f) returns the BDD for the "then" pointer of f. */
00649 
00650 bdd
00651 cmu_bdd_then(cmu_bdd_manager bddm, bdd f)
00652 {
00653   if (bdd_check_arguments(1, f))
00654     {
00655       BDD_SETUP(f);
00656       if (BDD_IS_CONST(f))
00657         {
00658           cmu_bdd_warning("cmu_bdd_then: argument is a constant");
00659           return (f);
00660         }
00661       f=BDD_THEN(f);
00662       BDD_RESET(f);
00663       BDD_INCREFS(f);
00664     }
00665   return (f);
00666 }
00667  
00668 
00669 /* cmu_bdd_else(bddm, f) returns the BDD for the "else" pointer of f. */
00670 
00671 bdd
00672 cmu_bdd_else(cmu_bdd_manager bddm, bdd f)
00673 {
00674   if (bdd_check_arguments(1, f))
00675     {
00676       BDD_SETUP(f);
00677       if (BDD_IS_CONST(f))
00678         {
00679           cmu_bdd_warning("cmu_bdd_else: argument is a constant");
00680           return (f);
00681         }
00682       f=BDD_ELSE(f);
00683       BDD_RESET(f);
00684       BDD_INCREFS(f);
00685     }
00686   return (f);
00687 }
00688 
00689 
00690 static
00691 bdd
00692 cmu_bdd_intersects_step(cmu_bdd_manager bddm, bdd f, bdd g)
00693 {
00694   bdd_indexindex_type top_indexindex;
00695   bdd f1, f2;
00696   bdd g1, g2;
00697   bdd temp;
00698 
00699   BDD_SETUP(f);
00700   BDD_SETUP(g);
00701   if (BDD_IS_CONST(f))
00702     {
00703       if (f == BDD_ZERO(bddm))
00704         return (f);
00705       BDD_TEMP_INCREFS(g);
00706       return (g);
00707     }
00708   /* f is not constant. */
00709   if (BDD_IS_CONST(g))
00710     {
00711       if (g == BDD_ZERO(bddm))
00712         return (g);
00713       BDD_TEMP_INCREFS(f);
00714       return (f);
00715     }
00716   /* f and g are not constant. */
00717   if (BDD_SAME_OR_NEGATIONS(f, g))
00718     {
00719       if (f == g)
00720         {
00721           BDD_TEMP_INCREFS(f);
00722           return (f);
00723         }
00724       return (BDD_ZERO(bddm));
00725     }
00726   /* f and g are not constant and are not equal or negations. */
00727   if (BDD_OUT_OF_ORDER(f, g))
00728     BDD_SWAP(f, g);
00729   if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR *)&temp))
00730     return (temp);
00731   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00732   BDD_COFACTOR(top_indexindex, f, f1, f2);
00733   BDD_COFACTOR(top_indexindex, g, g1, g2);
00734   temp=cmu_bdd_intersects_step(bddm, f1, g1);
00735   if (temp != BDD_ZERO(bddm))
00736     return (bdd_find(bddm, top_indexindex, temp, BDD_ZERO(bddm)));
00737   temp=bdd_find(bddm, top_indexindex, BDD_ZERO(bddm), cmu_bdd_intersects_step(bddm, f2, g2));
00738   if (temp == BDD_ZERO(bddm))
00739     bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR)temp);
00740   return (temp);
00741 }
00742 
00743 
00744 /* cmu_bdd_intersects(bddm, f, g) returns a BDD contained in "f and g", */
00745 /* while building as few nodes as possible.  The idea is that it */
00746 /* gives us a fast test for intersection, and, when f and g do */
00747 /* intersect, we can call cmu_bdd_satisfy or cmu_bdd_satisfy_support on the */
00748 /* result to get a valuation in the intersection. */
00749 
00750 bdd
00751 cmu_bdd_intersects(cmu_bdd_manager bddm, bdd f, bdd g)
00752 {
00753   if (bdd_check_arguments(2, f, g))
00754     {
00755       FIREWALL(bddm);
00756       RETURN_BDD(cmu_bdd_intersects_step(bddm, f, g));
00757     }
00758   return ((bdd)0);
00759 }
00760 
00761 
00762 /* cmu_bdd_implies(bddm, f, g) is analogous to cmu_bdd_intersects, but it */
00763 /* looks for things in "f and not g". */
00764 
00765 bdd
00766 cmu_bdd_implies(cmu_bdd_manager bddm, bdd f, bdd g)
00767 {
00768   if (bdd_check_arguments(2, f, g))
00769     {
00770       FIREWALL(bddm);
00771       RETURN_BDD(cmu_bdd_intersects_step(bddm, f, BDD_NOT(g)));
00772     }
00773   return ((bdd)0);
00774 }
00775 
00776 
00777 int
00778 cmu_bdd_type_aux(cmu_bdd_manager bddm, bdd f)
00779 {
00780   BDD_SETUP(f);
00781   if (BDD_IS_CONST(f))
00782     {
00783       if (f == BDD_ZERO(bddm))
00784         return (BDD_TYPE_ZERO);
00785       if (f == BDD_ONE(bddm))
00786         return (BDD_TYPE_ONE);
00787       return (BDD_TYPE_CONSTANT);
00788     }
00789   if (BDD_THEN(f) == BDD_ONE(bddm) && BDD_ELSE(f) == BDD_ZERO(bddm))
00790     return (BDD_TYPE_POSVAR);
00791   if (BDD_THEN(f) == BDD_ZERO(bddm) && BDD_ELSE(f) == BDD_ONE(bddm))
00792     return (BDD_TYPE_NEGVAR);
00793   return (BDD_TYPE_NONTERMINAL);
00794 }
00795 
00796 
00797 /* cmu_bdd_type(bddm, f) returns BDD_TYPE_ZERO if f is false, BDD_TYPE_ONE */
00798 /* if f is true, BDD_TYPE_CONSTANT if f is an MTBDD constant, */
00799 /* BDD_TYPE_POSVAR is f is an unnegated variable, BDD_TYPE_NEGVAR if */
00800 /* f is a negated variable, BDD_TYPE_OVERFLOW if f is null, and */
00801 /* BDD_TYPE_NONTERMINAL otherwise. */
00802 
00803 int
00804 cmu_bdd_type(cmu_bdd_manager bddm, bdd f)
00805 {
00806   if (bdd_check_arguments(1, f))
00807     return (cmu_bdd_type_aux(bddm, f));
00808   return (BDD_TYPE_OVERFLOW);
00809 }
00810 
00811 
00812 /* cmu_bdd_unfree(bddm, f) increments the reference count for f. */
00813 
00814 void
00815 cmu_bdd_unfree(cmu_bdd_manager bddm, bdd f)
00816 {
00817   if (f)
00818     {
00819       BDD_SETUP(f);
00820       BDD_INCREFS(f);
00821     }
00822 }
00823 
00824 
00825 /* cmu_bdd_free(bddm, f) decrements the reference count for f. */
00826 
00827 void
00828 cmu_bdd_free(cmu_bdd_manager bddm, bdd f)
00829 {
00830   if (f)
00831     {
00832       BDD_SETUP(f);
00833       if (BDD_REFS(f) == 0)
00834         cmu_bdd_fatal("cmu_bdd_free: attempt to free node with zero references");
00835       else
00836         BDD_DECREFS(f);
00837     }
00838 }
00839 
00840 
00841 /* cmu_bdd_vars(bddm) returns the number of variables in existence. */
00842 
00843 long
00844 cmu_bdd_vars(cmu_bdd_manager bddm)
00845 {
00846   return (bddm->vars);
00847 }
00848 
00849 
00850 /* cmu_bdd_total_size(bddm) returns the number of BDD nodes in existence. */
00851 
00852 long
00853 cmu_bdd_total_size(cmu_bdd_manager bddm)
00854 {
00855   return (bddm->unique_table.entries);
00856 }
00857 
00858 
00859 /* cmu_bdd_cache_ratio(bddm, new_ratio) sets the cache size ratio to */
00860 /* new_ratio and returns the old ratio. */
00861 
00862 int
00863 cmu_bdd_cache_ratio(cmu_bdd_manager bddm, int new_ratio)
00864 {
00865   int old_ratio;
00866 
00867   old_ratio=bddm->op_cache.cache_ratio;
00868   if (new_ratio < 1)
00869     new_ratio=1;
00870   else if (new_ratio > 32)
00871     new_ratio=32;
00872   bddm->op_cache.cache_ratio=new_ratio;
00873   return (old_ratio);
00874 }
00875 
00876 
00877 /* cmu_bdd_node_limit(bddm, new_limit) sets the node limit to */
00878 /* new_limit and returns the old limit. */
00879 
00880 long
00881 cmu_bdd_node_limit(cmu_bdd_manager bddm, long new_limit)
00882 {
00883   long old_limit;
00884 
00885   old_limit=bddm->unique_table.node_limit;
00886   if (new_limit < 0)
00887     new_limit=0;
00888   bddm->unique_table.node_limit=new_limit;
00889   if (new_limit && bddm->unique_table.gc_limit > new_limit)
00890     bddm->unique_table.gc_limit=new_limit;
00891   return (old_limit);
00892 }
00893 
00894 
00895 /* cmu_bdd_overflow(bddm) returns 1 if the node limit has been exceeded */
00896 /* and 0 otherwise.  The overflow flag is cleared. */
00897 
00898 int
00899 cmu_bdd_overflow(cmu_bdd_manager bddm)
00900 {
00901   int result;
00902 
00903   result=bddm->overflow;
00904   bddm->overflow=0;
00905   return (result);
00906 }
00907 
00908 
00909 /* cmu_bdd_overflow_closure(bddm, overflow_fn, overflow_env) sets the */
00910 /* closure to be invoked on overflow.  If overflow_fn is null, it */
00911 /* indicates that no function should be called. */
00912 
00913 void
00914 cmu_bdd_overflow_closure(cmu_bdd_manager bddm, void (*overflow_fn)(cmu_bdd_manager, pointer), pointer overflow_env)
00915 {
00916   bddm->overflow_fn=overflow_fn;
00917   bddm->overflow_env=overflow_env;
00918 }
00919 
00920 
00921 /* cmu_bdd_abort_closure(bddm, abort_fn, abort_env) sets a closure to be */
00922 /* invoked when the next find operation is attempted.  This is */
00923 /* intended for aborting BDD operations from signal handlers.  The */
00924 /* handler should set this closure so that invoking it will cause */
00925 /* a longjmp to a recovery routine. */
00926 
00927 void
00928 cmu_bdd_abort_closure(cmu_bdd_manager bddm, void (*abort_fn)(cmu_bdd_manager, pointer), pointer abort_env)
00929 {
00930   bddm->bag_it_fn=abort_fn;
00931   bddm->bag_it_env=abort_env;
00932 }
00933 
00934 
00935 /* cmu_bdd_stats(bddm, fp) prints random statistics to the file indicated */
00936 /* by fp. */
00937 
00938 void
00939 cmu_bdd_stats(cmu_bdd_manager bddm, FILE *fp)
00940 {
00941   long i;
00942   long ue, ce, cs, mem;
00943   SIZE_T alloc;
00944   assoc_list q;
00945 
00946   ue=bddm->unique_table.entries;
00947   ce=bddm->op_cache.entries;
00948   cs=bddm->op_cache.size;
00949   mem=0;
00950   for (i=0; i < bddm->vars; ++i)
00951     {
00952       mem+=sizeof(struct var_table_);
00953       mem+=bddm->unique_table.tables[i]->size*sizeof(bdd);
00954     }
00955   mem=ue*sizeof(struct bdd_);
00956   mem+=cs*sizeof(struct cache_bin_)+ce*sizeof(struct cache_entry_);
00957   mem+=bddm->maxvars*(sizeof(bdd_index_type)+sizeof(bdd_indexindex_type)+sizeof(bdd)+sizeof(var_table));
00958   for (q=bddm->assocs, i=1; q; q=q->next, ++i);
00959   mem+=i*bddm->maxvars*sizeof(bdd);
00960   if ((alloc=mem_allocation()))
00961     /* mem_allocation may be meaningless depending on mem library. */
00962     fprintf(fp, "Memory manager bytes allocated: %ld\n", (long)alloc);
00963   fprintf(fp, "Approximate bytes used: %ld\n", mem);
00964   fprintf(fp, "Number of nodes: %ld\n", ue);
00965   if (bddm->unique_table.node_limit)
00966     fprintf(fp, "Node limit: %ld\n", bddm->unique_table.node_limit);
00967   else
00968     fprintf(fp, "Node limit: ---\n");
00969   fprintf(fp, "Overflow: %s\n", bddm->overflow ? "yes" : "no");
00970   fprintf(fp, "Approximate bytes per node: %-.2f\n", ((double)mem)/ue);
00971   fprintf(fp, "Cache entries: %ld\n", ce);
00972   fprintf(fp, "Cache size: %ld\n", 2*cs);
00973   fprintf(fp, "Cache load factor: %-.2f\n", ((double)ce)/(2*cs));
00974   fprintf(fp, "Cache look ups: %ld\n", bddm->op_cache.lookups);
00975   fprintf(fp, "Cache hits: %ld\n", bddm->op_cache.hits);
00976   if (bddm->op_cache.lookups)
00977     fprintf(fp, "Cache hit rate: %-.2f\n", ((double)(bddm->op_cache.hits))/bddm->op_cache.lookups);
00978   else
00979     fprintf(fp, "Cache hit rate: ---\n");
00980   fprintf(fp, "Cache insertions: %ld\n", bddm->op_cache.inserts);
00981   fprintf(fp, "Cache collisions: %ld\n", bddm->op_cache.collisions);
00982   fprintf(fp, "Number of variables: %ld\n", bddm->vars);
00983   fprintf(fp, "Number of variable associations: %ld\n", i);
00984   fprintf(fp, "Number of garbage collections: %ld\n", bddm->unique_table.gcs);
00985   fprintf(fp, "Number of nodes garbage collected: %ld\n", bddm->unique_table.freed);
00986   fprintf(fp, "Number of find operations: %ld\n", bddm->unique_table.finds);
00987 }
00988 
00989 
00990 static
00991 int
00992 bdd_default_canonical_fn(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2, pointer junk)
00993 {
00994   /* Default transformation is treat the value as a 64-bit integer and to */
00995   /* negate it if it is positive. */
00996   return ((long)value1 > 0 || (!value1 && (long)value2 > 0));
00997 }
00998 
00999 
01000 static
01001 void
01002 bdd_default_transform_fn(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2, INT_PTR *result1, INT_PTR *result2, pointer junk)
01003 {
01004   if (!value2)
01005     /* Will be a carry when taking 2's complement of value2.  Thus, */
01006     /* take 2's complement of high part. */
01007     value1= -(long)value1;
01008   else
01009     {
01010       value2= -(long)value2;
01011       value1= ~value1;
01012     }
01013   *result1=value1;
01014   *result2=value2;
01015 }
01016 
01017 
01018 /* cmu_bdd_init() creates and returns a new BDD manager. */
01019 
01020 cmu_bdd_manager
01021 cmu_bdd_init(void)
01022 {
01023   cmu_bdd_manager bddm;
01024   long i;
01025 
01026   bddm=(cmu_bdd_manager)mem_get_block((SIZE_T)sizeof(struct bdd_manager_));
01027   bddm->overflow=0;
01028   bddm->overflow_fn=0;
01029   bddm->overflow_env=0;
01030   bddm->bag_it_fn=0;
01031   bddm->bag_it_env=0;
01032   bddm->canonical_fn=bdd_default_canonical_fn;
01033   bddm->transform_fn=bdd_default_transform_fn;
01034   bddm->transform_env=0;
01035   bddm->reorder_fn=0;
01036   bddm->reorder_data=0;
01037   bddm->vars=0;
01038   bddm->maxvars=30; 
01039   bddm->check=1;
01040   bddm->variables=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
01041   bddm->indexes=(bdd_index_type *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd_index_type)));
01042   bddm->indexindexes=(bdd_indexindex_type *)mem_get_block((SIZE_T)(bddm->maxvars*sizeof(bdd_indexindex_type)));
01043   bddm->indexes[BDD_CONST_INDEXINDEX]=BDD_MAX_INDEX;
01044   for (i=0; i < REC_MGRS; ++i)
01045     bddm->rms[i]=mem_new_rec_mgr(MIN_REC_SIZE+ALLOC_ALIGNMENT*i);
01046   bddm->temp_assoc.assoc=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
01047   bddm->temp_assoc.last= -1;
01048   for (i=0; i < bddm->maxvars; ++i)
01049     bddm->temp_assoc.assoc[i+1]=0;
01050   bddm->curr_assoc_id= -1;
01051   bddm->curr_assoc= &bddm->temp_assoc;
01052   bddm->assocs=0;
01053   bddm->temp_op= -1;
01054   bddm->super_block=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
01055   bddm->super_block->num_children=0;
01056   bddm->super_block->children=0;
01057   bddm->super_block->reorderable=1;
01058   bddm->super_block->first_index= -1;
01059   bddm->super_block->last_index=0;
01060   cmu_bdd_init_unique(bddm);
01061   cmu_bdd_init_cache(bddm);
01062   bddm->one=bdd_find_terminal(bddm, ~(INT_PTR)0, ~(INT_PTR)0);
01063   bddm->one->refs=BDD_MAX_REFS;
01064   bddm->one->mark=0;
01065   bddm->zero=BDD_NOT(bddm->one);
01066   if (sizeof(double) > 2*sizeof(long))
01067     cmu_bdd_warning("cmu_bdd_init: portability problem for cmu_bdd_satisfying_fraction");
01068   return (bddm);
01069 }
01070 
01071 
01072 /* cmu_bdd_quit(bddm) frees all storage associated with the BDD manager */
01073 /* bddm. */
01074 
01075 void
01076 cmu_bdd_quit(cmu_bdd_manager bddm)
01077 {
01078   int i;
01079   assoc_list p, q;
01080 
01081   cmu_bdd_free_unique(bddm);
01082   cmu_bdd_free_cache(bddm);
01083   mem_free_block((pointer)bddm->variables);
01084   mem_free_block((pointer)bddm->indexes);
01085   mem_free_block((pointer)bddm->indexindexes);
01086   mem_free_block((pointer)bddm->temp_assoc.assoc);
01087   for (p=bddm->assocs; p; p=q)
01088     {
01089       q=p->next;
01090       mem_free_block((pointer)p->va.assoc);
01091       BDD_FREE_REC(bddm, (pointer)p, sizeof(struct assoc_list_));
01092     }
01093   BDD_FREE_REC(bddm, (pointer)bddm->super_block, sizeof(struct block_));
01094   for (i=0; i < REC_MGRS; ++i)
01095     mem_free_rec_mgr(bddm->rms[i]);
01096   mem_free_block((pointer)bddm);
01097 }