distr/cudd/cuddCache.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddCache.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for cache insertion and lookup.]
   8
   9   Description [Internal procedures included in this module:
  10                 <ul>
  11                 <li> cuddInitCache()
  12                 <li> cuddCacheInsert()
  13                 <li> cuddCacheInsert2()
  14                 <li> cuddCacheLookup()
  15                 <li> cuddCacheLookupZdd()
  16                 <li> cuddCacheLookup2()
  17                 <li> cuddCacheLookup2Zdd()
  18                 <li> cuddConstantLookup()
  19                 <li> cuddCacheProfile()
  20                 <li> cuddCacheResize()
  21                 <li> cuddCacheFlush()
  22                 <li> cuddComputeFloorLog2()
  23                 </ul>
  24             Static procedures included in this module:
  25                 <ul>
  26                 </ul> ]
  27
  28   SeeAlso     []
  29
  30   Author      [Fabio Somenzi]
  31
  32   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  33
  34   All rights reserved.
  35
  36   Redistribution and use in source and binary forms, with or without
  37   modification, are permitted provided that the following conditions
  38   are met:
  39
  40   Redistributions of source code must retain the above copyright
  41   notice, this list of conditions and the following disclaimer.
  42
  43   Redistributions in binary form must reproduce the above copyright
  44   notice, this list of conditions and the following disclaimer in the
  45   documentation and/or other materials provided with the distribution.
  46
  47   Neither the name of the University of Colorado nor the names of its
  48   contributors may be used to endorse or promote products derived from
  49   this software without specific prior written permission.
  50
  51   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  52   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  53   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  54   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  55   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  56   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  57   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  58   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  59   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  60   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  61   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  62   POSSIBILITY OF SUCH DAMAGE.]
  63
  64 ******************************************************************************/
  65
  66 #include "util.h"
  67 #include "cuddInt.h"
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Constant declarations                                                     */
  71 /*---------------------------------------------------------------------------*/
  72
  73 #ifdef DD_CACHE_PROFILE
  74 #define DD_HYSTO_BINS 8
  75 #endif
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Stucture declarations                                                     */
  79 /*---------------------------------------------------------------------------*/
  80
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Type declarations                                                         */
  84 /*---------------------------------------------------------------------------*/
  85
  86
  87 /*---------------------------------------------------------------------------*/
  88 /* Variable declarations                                                     */
  89 /*---------------------------------------------------------------------------*/
  90
  91 #ifndef lint
  92 static char rcsid[] DD_UNUSED = "$Id: cuddCache.c,v 1.34 2009/02/19 16:17:50 fabio Exp $";
  93 #endif
  94
  95 /*---------------------------------------------------------------------------*/
  96 /* Macro declarations                                                        */
  97 /*---------------------------------------------------------------------------*/
  98
  99
 100 /**AutomaticStart*************************************************************/
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Static function prototypes                                                */
 104 /*---------------------------------------------------------------------------*/
 105
 106
 107 /**AutomaticEnd***************************************************************/
 108
 109
 110 /*---------------------------------------------------------------------------*/
 111 /* Definition of exported functions                                          */
 112 /*---------------------------------------------------------------------------*/
 113
 114 /*---------------------------------------------------------------------------*/
 115 /* Definition of internal functions                                          */
 116 /*---------------------------------------------------------------------------*/
 117
 118
 119 /**Function********************************************************************
 120
 121   Synopsis    [Initializes the computed table.]
 122
 123   Description [Initializes the computed table. It is called by
 124   Cudd_Init. Returns 1 in case of success; 0 otherwise.]
 125
 126   SideEffects [None]
 127
 128   SeeAlso     [Cudd_Init]
 129
 130 ******************************************************************************/
 131 int
 132 cuddInitCache(
 133   DdManager * unique /* unique table */,
 134   unsigned int cacheSize /* initial size of the cache */,
 135   unsigned int maxCacheSize /* cache size beyond which no resizing occurs */)
 136 {
 137     int i;
 138     unsigned int logSize;
 139 #ifndef DD_CACHE_PROFILE
 140     DdNodePtr *mem;
 141     ptruint offset;
 142 #endif
 143
 144     /* Round cacheSize to largest power of 2 not greater than the requested
 145     ** initial cache size. */
 146     logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
 147     cacheSize = 1 << logSize;
 148     unique->acache = ALLOC(DdCache,cacheSize+1);
 149     if (unique->acache == NULL) {
 150         unique->errorCode = CUDD_MEMORY_OUT;
 151         return(0);
 152     }
 153     /* If the size of the cache entry is a power of 2, we want to
 154     ** enforce alignment to that power of two. This happens when
 155     ** DD_CACHE_PROFILE is not defined. */
 156 #ifdef DD_CACHE_PROFILE
 157     unique->cache = unique->acache;
 158     unique->memused += (cacheSize) * sizeof(DdCache);
 159 #else
 160     mem = (DdNodePtr *) unique->acache;
 161     offset = (ptruint) mem & (sizeof(DdCache) - 1);
 162     mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr);
 163     unique->cache = (DdCache *) mem;
 164     assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0);
 165     unique->memused += (cacheSize+1) * sizeof(DdCache);
 166 #endif
 167     unique->cacheSlots = cacheSize;
 168     unique->cacheShift = sizeof(int) * 8 - logSize;
 169     unique->maxCacheHard = maxCacheSize;
 170     /* If cacheSlack is non-negative, we can resize. */
 171     unique->cacheSlack = (int) ddMin(maxCacheSize,
 172         DD_MAX_CACHE_TO_SLOTS_RATIO*unique->slots) -
 173         2 * (int) cacheSize;
 174     Cudd_SetMinHit(unique,DD_MIN_HIT);
 175     /* Initialize to avoid division by 0 and immediate resizing. */
 176     unique->cacheMisses = (double) (int) (cacheSize * unique->minHit + 1);
 177     unique->cacheHits = 0;
 178     unique->totCachehits = 0;
 179     /* The sum of cacheMisses and totCacheMisses is always correct,
 180     ** even though cacheMisses is larger than it should for the reasons
 181     ** explained above. */
 182     unique->totCacheMisses = -unique->cacheMisses;
 183     unique->cachecollisions = 0;
 184     unique->cacheinserts = 0;
 185     unique->cacheLastInserts = 0;
 186     unique->cachedeletions = 0;
 187
 188     /* Initialize the cache */
 189     for (i = 0; (unsigned) i < cacheSize; i++) {
 190         unique->cache[i].h = 0; /* unused slots */
 191         unique->cache[i].data = NULL; /* invalid entry */
 192 #ifdef DD_CACHE_PROFILE
 193         unique->cache[i].count = 0;
 194 #endif
 195     }
 196
 197     return(1);
 198
 199 } /* end of cuddInitCache */
 200
 201
 202 /**Function********************************************************************
 203
 204   Synopsis    [Inserts a result in the cache.]
 205
 206   Description []
 207
 208   SideEffects [None]
 209
 210   SeeAlso     [cuddCacheInsert2 cuddCacheInsert1]
 211
 212 ******************************************************************************/
 213 void
 214 cuddCacheInsert(
 215   DdManager * table,
 216   ptruint op,
 217   DdNode * f,
 218   DdNode * g,
 219   DdNode * h,
 220   DdNode * data)
 221 {
 222     int posn;
 223     register DdCache *entry;
 224     ptruint uf, ug, uh;
 225
 226     uf = (ptruint) f | (op & 0xe);
 227     ug = (ptruint) g | (op >> 4);
 228     uh = (ptruint) h;
 229
 230     posn = ddCHash2(uh,uf,ug,table->cacheShift);
 231     entry = &table->cache[posn];
 232
 233     table->cachecollisions += entry->data != NULL;
 234     table->cacheinserts++;
 235
 236     entry->f    = (DdNode *) uf;
 237     entry->g    = (DdNode *) ug;
 238     entry->h    = uh;
 239     entry->data = data;
 240 #ifdef DD_CACHE_PROFILE
 241     entry->count++;
 242 #endif
 243
 244 } /* end of cuddCacheInsert */
 245
 246
 247 /**Function********************************************************************
 248
 249   Synopsis    [Inserts a result in the cache for a function with two
 250   operands.]
 251
 252   Description []
 253
 254   SideEffects [None]
 255
 256   SeeAlso     [cuddCacheInsert cuddCacheInsert1]
 257
 258 ******************************************************************************/
 259 void
 260 cuddCacheInsert2(
 261   DdManager * table,
 262   DD_CTFP op,
 263   DdNode * f,
 264   DdNode * g,
 265   DdNode * data)
 266 {
 267     int posn;
 268     register DdCache *entry;
 269
 270     posn = ddCHash2(op,f,g,table->cacheShift);
 271     entry = &table->cache[posn];
 272
 273     if (entry->data != NULL) {
 274         table->cachecollisions++;
 275     }
 276     table->cacheinserts++;
 277
 278     entry->f = f;
 279     entry->g = g;
 280     entry->h = (ptruint) op;
 281     entry->data = data;
 282 #ifdef DD_CACHE_PROFILE
 283     entry->count++;
 284 #endif
 285
 286 } /* end of cuddCacheInsert2 */
 287
 288
 289 /**Function********************************************************************
 290
 291   Synopsis    [Inserts a result in the cache for a function with two
 292   operands.]
 293
 294   Description []
 295
 296   SideEffects [None]
 297
 298   SeeAlso     [cuddCacheInsert cuddCacheInsert2]
 299
 300 ******************************************************************************/
 301 void
 302 cuddCacheInsert1(
 303   DdManager * table,
 304   DD_CTFP1 op,
 305   DdNode * f,
 306   DdNode * data)
 307 {
 308     int posn;
 309     register DdCache *entry;
 310
 311     posn = ddCHash2(op,f,f,table->cacheShift);
 312     entry = &table->cache[posn];
 313
 314     if (entry->data != NULL) {
 315         table->cachecollisions++;
 316     }
 317     table->cacheinserts++;
 318
 319     entry->f = f;
 320     entry->g = f;
 321     entry->h = (ptruint) op;
 322     entry->data = data;
 323 #ifdef DD_CACHE_PROFILE
 324     entry->count++;
 325 #endif
 326
 327 } /* end of cuddCacheInsert1 */
 328
 329
 330 /**Function********************************************************************
 331
 332   Synopsis    [Looks up in the cache for the result of op applied to f,
 333   g, and h.]
 334
 335   Description [Returns the result if found; it returns NULL if no
 336   result is found.]
 337
 338   SideEffects [None]
 339
 340   SeeAlso     [cuddCacheLookup2 cuddCacheLookup1]
 341
 342 ******************************************************************************/
 343 DdNode *
 344 cuddCacheLookup(
 345   DdManager * table,
 346   ptruint op,
 347   DdNode * f,
 348   DdNode * g,
 349   DdNode * h)
 350 {
 351     int posn;
 352     DdCache *en,*cache;
 353     DdNode *data;
 354     ptruint uf, ug, uh;
 355
 356     uf = (ptruint) f | (op & 0xe);
 357     ug = (ptruint) g | (op >> 4);
 358     uh = (ptruint) h;
 359
 360     cache = table->cache;
 361 #ifdef DD_DEBUG
 362     if (cache == NULL) {
 363         return(NULL);
 364     }
 365 #endif
 366
 367     posn = ddCHash2(uh,uf,ug,table->cacheShift);
 368     en = &cache[posn];
 369     if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
 370         en->h==uh) {
 371         data = Cudd_Regular(en->data);
 372         table->cacheHits++;
 373         if (data->ref == 0) {
 374             cuddReclaim(table,data);
 375         }
 376         return(en->data);
 377     }
 378
 379     /* Cache miss: decide whether to resize. */
 380     table->cacheMisses++;
 381
 382     if (table->cacheSlack >= 0 &&
 383         table->cacheHits > table->cacheMisses * table->minHit) {
 384         cuddCacheResize(table);
 385     }
 386
 387     return(NULL);
 388
 389 } /* end of cuddCacheLookup */
 390
 391
 392 /**Function********************************************************************
 393
 394   Synopsis    [Looks up in the cache for the result of op applied to f,
 395   g, and h.]
 396
 397   Description [Returns the result if found; it returns NULL if no
 398   result is found.]
 399
 400   SideEffects [None]
 401
 402   SeeAlso     [cuddCacheLookup2Zdd cuddCacheLookup1Zdd]
 403
 404 ******************************************************************************/
 405 DdNode *
 406 cuddCacheLookupZdd(
 407   DdManager * table,
 408   ptruint op,
 409   DdNode * f,
 410   DdNode * g,
 411   DdNode * h)
 412 {
 413     int posn;
 414     DdCache *en,*cache;
 415     DdNode *data;
 416     ptruint uf, ug, uh;
 417
 418     uf = (ptruint) f | (op & 0xe);
 419     ug = (ptruint) g | (op >> 4);
 420     uh = (ptruint) h;
 421
 422     cache = table->cache;
 423 #ifdef DD_DEBUG
 424     if (cache == NULL) {
 425         return(NULL);
 426     }
 427 #endif
 428
 429     posn = ddCHash2(uh,uf,ug,table->cacheShift);
 430     en = &cache[posn];
 431     if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
 432         en->h==uh) {
 433         data = Cudd_Regular(en->data);
 434         table->cacheHits++;
 435         if (data->ref == 0) {
 436             cuddReclaimZdd(table,data);
 437         }
 438         return(en->data);
 439     }
 440
 441     /* Cache miss: decide whether to resize. */
 442     table->cacheMisses++;
 443
 444     if (table->cacheSlack >= 0 &&
 445         table->cacheHits > table->cacheMisses * table->minHit) {
 446         cuddCacheResize(table);
 447     }
 448
 449     return(NULL);
 450
 451 } /* end of cuddCacheLookupZdd */
 452
 453
 454 /**Function********************************************************************
 455
 456   Synopsis    [Looks up in the cache for the result of op applied to f
 457   and g.]
 458
 459   Description [Returns the result if found; it returns NULL if no
 460   result is found.]
 461
 462   SideEffects [None]
 463
 464   SeeAlso     [cuddCacheLookup cuddCacheLookup1]
 465
 466 ******************************************************************************/
 467 DdNode *
 468 cuddCacheLookup2(
 469   DdManager * table,
 470   DD_CTFP op,
 471   DdNode * f,
 472   DdNode * g)
 473 {
 474     int posn;
 475     DdCache *en,*cache;
 476     DdNode *data;
 477
 478     cache = table->cache;
 479 #ifdef DD_DEBUG
 480     if (cache == NULL) {
 481         return(NULL);
 482     }
 483 #endif
 484
 485     posn = ddCHash2(op,f,g,table->cacheShift);
 486     en = &cache[posn];
 487     if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
 488         data = Cudd_Regular(en->data);
 489         table->cacheHits++;
 490         if (data->ref == 0) {
 491             cuddReclaim(table,data);
 492         }
 493         return(en->data);
 494     }
 495
 496     /* Cache miss: decide whether to resize. */
 497     table->cacheMisses++;
 498
 499     if (table->cacheSlack >= 0 &&
 500         table->cacheHits > table->cacheMisses * table->minHit) {
 501         cuddCacheResize(table);
 502     }
 503
 504     return(NULL);
 505
 506 } /* end of cuddCacheLookup2 */
 507
 508
 509 /**Function********************************************************************
 510
 511   Synopsis [Looks up in the cache for the result of op applied to f.]
 512
 513   Description [Returns the result if found; it returns NULL if no
 514   result is found.]
 515
 516   SideEffects [None]
 517
 518   SeeAlso     [cuddCacheLookup cuddCacheLookup2]
 519
 520 ******************************************************************************/
 521 DdNode *
 522 cuddCacheLookup1(
 523   DdManager * table,
 524   DD_CTFP1 op,
 525   DdNode * f)
 526 {
 527     int posn;
 528     DdCache *en,*cache;
 529     DdNode *data;
 530
 531     cache = table->cache;
 532 #ifdef DD_DEBUG
 533     if (cache == NULL) {
 534         return(NULL);
 535     }
 536 #endif
 537
 538     posn = ddCHash2(op,f,f,table->cacheShift);
 539     en = &cache[posn];
 540     if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
 541         data = Cudd_Regular(en->data);
 542         table->cacheHits++;
 543         if (data->ref == 0) {
 544             cuddReclaim(table,data);
 545         }
 546         return(en->data);
 547     }
 548
 549     /* Cache miss: decide whether to resize. */
 550     table->cacheMisses++;
 551
 552     if (table->cacheSlack >= 0 &&
 553         table->cacheHits > table->cacheMisses * table->minHit) {
 554         cuddCacheResize(table);
 555     }
 556
 557     return(NULL);
 558
 559 } /* end of cuddCacheLookup1 */
 560
 561
 562 /**Function********************************************************************
 563
 564   Synopsis [Looks up in the cache for the result of op applied to f
 565   and g.]
 566
 567   Description [Returns the result if found; it returns NULL if no
 568   result is found.]
 569
 570   SideEffects [None]
 571
 572   SeeAlso     [cuddCacheLookupZdd cuddCacheLookup1Zdd]
 573
 574 ******************************************************************************/
 575 DdNode *
 576 cuddCacheLookup2Zdd(
 577   DdManager * table,
 578   DD_CTFP op,
 579   DdNode * f,
 580   DdNode * g)
 581 {
 582     int posn;
 583     DdCache *en,*cache;
 584     DdNode *data;
 585
 586     cache = table->cache;
 587 #ifdef DD_DEBUG
 588     if (cache == NULL) {
 589         return(NULL);
 590     }
 591 #endif
 592
 593     posn = ddCHash2(op,f,g,table->cacheShift);
 594     en = &cache[posn];
 595     if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
 596         data = Cudd_Regular(en->data);
 597         table->cacheHits++;
 598         if (data->ref == 0) {
 599             cuddReclaimZdd(table,data);
 600         }
 601         return(en->data);
 602     }
 603
 604     /* Cache miss: decide whether to resize. */
 605     table->cacheMisses++;
 606
 607     if (table->cacheSlack >= 0 &&
 608         table->cacheHits > table->cacheMisses * table->minHit) {
 609         cuddCacheResize(table);
 610     }
 611
 612     return(NULL);
 613
 614 } /* end of cuddCacheLookup2Zdd */
 615
 616
 617 /**Function********************************************************************
 618
 619   Synopsis [Looks up in the cache for the result of op applied to f.]
 620
 621   Description [Returns the result if found; it returns NULL if no
 622   result is found.]
 623
 624   SideEffects [None]
 625
 626   SeeAlso     [cuddCacheLookupZdd cuddCacheLookup2Zdd]
 627
 628 ******************************************************************************/
 629 DdNode *
 630 cuddCacheLookup1Zdd(
 631   DdManager * table,
 632   DD_CTFP1 op,
 633   DdNode * f)
 634 {
 635     int posn;
 636     DdCache *en,*cache;
 637     DdNode *data;
 638
 639     cache = table->cache;
 640 #ifdef DD_DEBUG
 641     if (cache == NULL) {
 642         return(NULL);
 643     }
 644 #endif
 645
 646     posn = ddCHash2(op,f,f,table->cacheShift);
 647     en = &cache[posn];
 648     if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
 649         data = Cudd_Regular(en->data);
 650         table->cacheHits++;
 651         if (data->ref == 0) {
 652             cuddReclaimZdd(table,data);
 653         }
 654         return(en->data);
 655     }
 656
 657     /* Cache miss: decide whether to resize. */
 658     table->cacheMisses++;
 659
 660     if (table->cacheSlack >= 0  &&
 661         table->cacheHits > table->cacheMisses * table->minHit) {
 662         cuddCacheResize(table);
 663     }
 664
 665     return(NULL);
 666
 667 } /* end of cuddCacheLookup1Zdd */
 668
 669
 670 /**Function********************************************************************
 671
 672   Synopsis [Looks up in the cache for the result of op applied to f,
 673   g, and h.]
 674
 675   Description [Looks up in the cache for the result of op applied to f,
 676   g, and h. Assumes that the calling procedure (e.g.,
 677   Cudd_bddIteConstant) is only interested in whether the result is
 678   constant or not. Returns the result if found (possibly
 679   DD_NON_CONSTANT); otherwise it returns NULL.]
 680
 681   SideEffects [None]
 682
 683   SeeAlso     [cuddCacheLookup]
 684
 685 ******************************************************************************/
 686 DdNode *
 687 cuddConstantLookup(
 688   DdManager * table,
 689   ptruint op,
 690   DdNode * f,
 691   DdNode * g,
 692   DdNode * h)
 693 {
 694     int posn;
 695     DdCache *en,*cache;
 696     ptruint uf, ug, uh;
 697
 698     uf = (ptruint) f | (op & 0xe);
 699     ug = (ptruint) g | (op >> 4);
 700     uh = (ptruint) h;
 701
 702     cache = table->cache;
 703 #ifdef DD_DEBUG
 704     if (cache == NULL) {
 705         return(NULL);
 706     }
 707 #endif
 708     posn = ddCHash2(uh,uf,ug,table->cacheShift);
 709     en = &cache[posn];
 710
 711     /* We do not reclaim here because the result should not be
 712      * referenced, but only tested for being a constant.
 713      */
 714     if (en->data != NULL &&
 715         en->f == (DdNodePtr)uf && en->g == (DdNodePtr)ug && en->h == uh) {
 716         table->cacheHits++;
 717         return(en->data);
 718     }
 719
 720     /* Cache miss: decide whether to resize. */
 721     table->cacheMisses++;
 722
 723     if (table->cacheSlack >= 0 &&
 724         table->cacheHits > table->cacheMisses * table->minHit) {
 725         cuddCacheResize(table);
 726     }
 727
 728     return(NULL);
 729
 730 } /* end of cuddConstantLookup */
 731
 732
 733 /**Function********************************************************************
 734
 735   Synopsis    [Computes and prints a profile of the cache usage.]
 736
 737   Description [Computes and prints a profile of the cache usage.
 738   Returns 1 if successful; 0 otherwise.]
 739
 740   SideEffects [None]
 741
 742   SeeAlso     []
 743
 744 ******************************************************************************/
 745 int
 746 cuddCacheProfile(
 747   DdManager * table,
 748   FILE * fp)
 749 {
 750     DdCache *cache = table->cache;
 751     int slots = table->cacheSlots;
 752     int nzeroes = 0;
 753     int i, retval;
 754     double exUsed;
 755
 756 #ifdef DD_CACHE_PROFILE
 757     double count, mean, meansq, stddev, expected;
 758     long max, min;
 759     int imax, imin;
 760     double *hystogramQ, *hystogramR; /* histograms by quotient and remainder */
 761     int nbins = DD_HYSTO_BINS;
 762     int bin;
 763     long thiscount;
 764     double totalcount, exStddev;
 765
 766     meansq = mean = expected = 0.0;
 767     max = min = (long) cache[0].count;
 768     imax = imin = 0;
 769     totalcount = 0.0;
 770
 771     hystogramQ = ALLOC(double, nbins);
 772     if (hystogramQ == NULL) {
 773         table->errorCode = CUDD_MEMORY_OUT;
 774         return(0);
 775     }
 776     hystogramR = ALLOC(double, nbins);
 777     if (hystogramR == NULL) {
 778         FREE(hystogramQ);
 779         table->errorCode = CUDD_MEMORY_OUT;
 780         return(0);
 781     }
 782     for (i = 0; i < nbins; i++) {
 783         hystogramQ[i] = 0;
 784         hystogramR[i] = 0;
 785     }
 786
 787     for (i = 0; i < slots; i++) {
 788         thiscount = (long) cache[i].count;
 789         if (thiscount > max) {
 790             max = thiscount;
 791             imax = i;
 792         }
 793         if (thiscount < min) {
 794             min = thiscount;
 795             imin = i;
 796         }
 797         if (thiscount == 0) {
 798             nzeroes++;
 799         }
 800         count = (double) thiscount;
 801         mean += count;
 802         meansq += count * count;
 803         totalcount += count;
 804         expected += count * (double) i;
 805         bin = (i * nbins) / slots;
 806         hystogramQ[bin] += (double) thiscount;
 807         bin = i % nbins;
 808         hystogramR[bin] += (double) thiscount;
 809     }
 810     mean /= (double) slots;
 811     meansq /= (double) slots;
 812
 813     /* Compute the standard deviation from both the data and the
 814     ** theoretical model for a random distribution. */
 815     stddev = sqrt(meansq - mean*mean);
 816     exStddev = sqrt((1 - 1/(double) slots) * totalcount / (double) slots);
 817
 818     retval = fprintf(fp,"Cache average accesses = %g\n",  mean);
 819     if (retval == EOF) return(0);
 820     retval = fprintf(fp,"Cache access standard deviation = %g ", stddev);
 821     if (retval == EOF) return(0);
 822     retval = fprintf(fp,"(expected = %g)\n", exStddev);
 823     if (retval == EOF) return(0);
 824     retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
 825     if (retval == EOF) return(0);
 826     retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
 827     if (retval == EOF) return(0);
 828     exUsed = 100.0 * (1.0 - exp(-totalcount / (double) slots));
 829     retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
 830                      100.0 - (double) nzeroes * 100.0 / (double) slots,
 831                      exUsed);
 832     if (retval == EOF) return(0);
 833
 834     if (totalcount > 0) {
 835         expected /= totalcount;
 836         retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
 837         if (retval == EOF) return(0);
 838         retval = fprintf(fp," (expected bin value = %g)\nBy quotient:",
 839                          expected);
 840         if (retval == EOF) return(0);
 841         for (i = nbins - 1; i>=0; i--) {
 842             retval = fprintf(fp," %.0f", hystogramQ[i]);
 843             if (retval == EOF) return(0);
 844         }
 845         retval = fprintf(fp,"\nBy residue: ");
 846         if (retval == EOF) return(0);
 847         for (i = nbins - 1; i>=0; i--) {
 848             retval = fprintf(fp," %.0f", hystogramR[i]);
 849             if (retval == EOF) return(0);
 850         }
 851         retval = fprintf(fp,"\n");
 852         if (retval == EOF) return(0);
 853     }
 854
 855     FREE(hystogramQ);
 856     FREE(hystogramR);
 857 #else
 858     for (i = 0; i < slots; i++) {
 859         nzeroes += cache[i].h == 0;
 860     }
 861     exUsed = 100.0 *
 862         (1.0 - exp(-(table->cacheinserts - table->cacheLastInserts) /
 863                    (double) slots));
 864     retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
 865                      100.0 - (double) nzeroes * 100.0 / (double) slots,
 866                      exUsed);
 867     if (retval == EOF) return(0);
 868 #endif
 869     return(1);
 870
 871 } /* end of cuddCacheProfile */
 872
 873
 874 /**Function********************************************************************
 875
 876   Synopsis    [Resizes the cache.]
 877
 878   Description []
 879
 880   SideEffects [None]
 881
 882   SeeAlso     []
 883
 884 ******************************************************************************/
 885 void
 886 cuddCacheResize(
 887   DdManager * table)
 888 {
 889     DdCache *cache, *oldcache, *oldacache, *entry, *old;
 890     int i;
 891     int posn, shift;
 892     unsigned int slots, oldslots;
 893     double offset;
 894     int moved = 0;
 895     extern DD_OOMFP MMoutOfMemory;
 896     DD_OOMFP saveHandler;
 897 #ifndef DD_CACHE_PROFILE
 898     ptruint misalignment;
 899     DdNodePtr *mem;
 900 #endif
 901
 902     oldcache = table->cache;
 903     oldacache = table->acache;
 904     oldslots = table->cacheSlots;
 905     slots = table->cacheSlots = oldslots << 1;
 906
 907 #ifdef DD_VERBOSE
 908     (void) fprintf(table->err,"Resizing the cache from %d to %d entries\n",
 909                    oldslots, slots);
 910     (void) fprintf(table->err,
 911                    "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
 912                    table->cacheHits, table->cacheMisses,
 913                    table->cacheHits / (table->cacheHits + table->cacheMisses));
 914 #endif
 915
 916     saveHandler = MMoutOfMemory;
 917     MMoutOfMemory = Cudd_OutOfMem;
 918     table->acache = cache = ALLOC(DdCache,slots+1);
 919     MMoutOfMemory = saveHandler;
 920     /* If we fail to allocate the new table we just give up. */
 921     if (cache == NULL) {
 922 #ifdef DD_VERBOSE
 923         (void) fprintf(table->err,"Resizing failed. Giving up.\n");
 924 #endif
 925         table->cacheSlots = oldslots;
 926         table->acache = oldacache;
 927         /* Do not try to resize again. */
 928         table->maxCacheHard = oldslots - 1;
 929         table->cacheSlack = - (int) (oldslots + 1);
 930         return;
 931     }
 932     /* If the size of the cache entry is a power of 2, we want to
 933     ** enforce alignment to that power of two. This happens when
 934     ** DD_CACHE_PROFILE is not defined. */
 935 #ifdef DD_CACHE_PROFILE
 936     table->cache = cache;
 937 #else
 938     mem = (DdNodePtr *) cache;
 939     misalignment = (ptruint) mem & (sizeof(DdCache) - 1);
 940     mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr);
 941     table->cache = cache = (DdCache *) mem;
 942     assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0);
 943 #endif
 944     shift = --(table->cacheShift);
 945     table->memused += (slots - oldslots) * sizeof(DdCache);
 946     table->cacheSlack -= slots; /* need these many slots to double again */
 947
 948     /* Clear new cache. */
 949     for (i = 0; (unsigned) i < slots; i++) {
 950         cache[i].data = NULL;
 951         cache[i].h = 0;
 952 #ifdef DD_CACHE_PROFILE
 953         cache[i].count = 0;
 954 #endif
 955     }
 956
 957     /* Copy from old cache to new one. */
 958     for (i = 0; (unsigned) i < oldslots; i++) {
 959         old = &oldcache[i];
 960         if (old->data != NULL) {
 961             posn = ddCHash2(old->h,old->f,old->g,shift);
 962             entry = &cache[posn];
 963             entry->f = old->f;
 964             entry->g = old->g;
 965             entry->h = old->h;
 966             entry->data = old->data;
 967 #ifdef DD_CACHE_PROFILE
 968             entry->count = 1;
 969 #endif
 970             moved++;
 971         }
 972     }
 973
 974     FREE(oldacache);
 975
 976     /* Reinitialize measurements so as to avoid division by 0 and
 977     ** immediate resizing.
 978     */
 979     offset = (double) (int) (slots * table->minHit + 1);
 980     table->totCacheMisses += table->cacheMisses - offset;
 981     table->cacheMisses = offset;
 982     table->totCachehits += table->cacheHits;
 983     table->cacheHits = 0;
 984     table->cacheLastInserts = table->cacheinserts - (double) moved;
 985
 986 } /* end of cuddCacheResize */
 987
 988
 989 /**Function********************************************************************
 990
 991   Synopsis    [Flushes the cache.]
 992
 993   Description []
 994
 995   SideEffects [None]
 996
 997   SeeAlso     []
 998
 999 ******************************************************************************/
1000 void
1001 cuddCacheFlush(
1002   DdManager * table)
1003 {
1004     int i, slots;
1005     DdCache *cache;
1006
1007     slots = table->cacheSlots;
1008     cache = table->cache;
1009     for (i = 0; i < slots; i++) {
1010         table->cachedeletions += cache[i].data != NULL;
1011         cache[i].data = NULL;
1012     }
1013     table->cacheLastInserts = table->cacheinserts;
1014
1015     return;
1016
1017 } /* end of cuddCacheFlush */
1018
1019
1020 /**Function********************************************************************
1021
1022   Synopsis    [Returns the floor of the logarithm to the base 2.]
1023
1024   Description [Returns the floor of the logarithm to the base 2.
1025   The input value is assumed to be greater than 0.]
1026
1027   SideEffects [None]
1028
1029   SeeAlso     []
1030
1031 ******************************************************************************/
1032 int
1033 cuddComputeFloorLog2(
1034   unsigned int value)
1035 {
1036     int floorLog = 0;
1037 #ifdef DD_DEBUG
1038     assert(value > 0);
1039 #endif
1040     while (value > 1) {
1041         floorLog++;
1042         value >>= 1;
1043     }
1044     return(floorLog);
1045
1046 } /* end of cuddComputeFloorLog2 */
1047
1048 /*---------------------------------------------------------------------------*/
1049 /* Definition of static functions                                            */
1050 /*---------------------------------------------------------------------------*/