distr/cudd/cuddApa.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddApa.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Arbitrary precision arithmetic functions.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_ApaNumberOfDigits()
  12                 <li> Cudd_NewApaNumber()
  13                 <li> Cudd_ApaCopy()
  14                 <li> Cudd_ApaAdd()
  15                 <li> Cudd_ApaSubtract()
  16                 <li> Cudd_ApaShortDivision()
  17                 <li> Cudd_ApaIntDivision()
  18                 <li> Cudd_ApaShiftRight()
  19                 <li> Cudd_ApaSetToLiteral()
  20                 <li> Cudd_ApaPowerOfTwo()
  21                 <li> Cudd_ApaCompare()
  22                 <li> Cudd_ApaCompareRatios()
  23                 <li> Cudd_ApaPrintHex()
  24                 <li> Cudd_ApaPrintDecimal()
  25                 <li> Cudd_ApaPrintExponential()
  26                 <li> Cudd_ApaCountMinterm()
  27                 <li> Cudd_ApaPrintMinterm()
  28                 <li> Cudd_ApaPrintMintermExp()
  29                 <li> Cudd_ApaPrintDensity()
  30                 </ul>
  31         Static procedures included in this module:
  32                 <ul>
  33                 <li> cuddApaCountMintermAux()
  34                 <li> cuddApaStCountfree()
  35                 </ul>]
  36
  37   Author      [Fabio Somenzi]
  38
  39   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  40
  41   All rights reserved.
  42
  43   Redistribution and use in source and binary forms, with or without
  44   modification, are permitted provided that the following conditions
  45   are met:
  46
  47   Redistributions of source code must retain the above copyright
  48   notice, this list of conditions and the following disclaimer.
  49
  50   Redistributions in binary form must reproduce the above copyright
  51   notice, this list of conditions and the following disclaimer in the
  52   documentation and/or other materials provided with the distribution.
  53
  54   Neither the name of the University of Colorado nor the names of its
  55   contributors may be used to endorse or promote products derived from
  56   this software without specific prior written permission.
  57
  58   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  59   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  60   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  61   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  62   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  63   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  64   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  65   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  66   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  67   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  68   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  69   POSSIBILITY OF SUCH DAMAGE.]
  70
  71 ******************************************************************************/
  72
  73 #include "util.h"
  74 #include "cuddInt.h"
  75
  76 /*---------------------------------------------------------------------------*/
  77 /* Constant declarations                                                     */
  78 /*---------------------------------------------------------------------------*/
  79
  80 /*---------------------------------------------------------------------------*/
  81 /* Stucture declarations                                                     */
  82 /*---------------------------------------------------------------------------*/
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Type declarations                                                         */
  86 /*---------------------------------------------------------------------------*/
  87
  88 /*---------------------------------------------------------------------------*/
  89 /* Variable declarations                                                     */
  90 /*---------------------------------------------------------------------------*/
  91
  92 #ifndef lint
  93 static char rcsid[] DD_UNUSED = "$Id: cuddApa.c,v 1.19 2009/03/08 01:27:50 fabio Exp $";
  94 #endif
  95
  96 static  DdNode  *background, *zero;
  97
  98 /*---------------------------------------------------------------------------*/
  99 /* Macro declarations                                                        */
 100 /*---------------------------------------------------------------------------*/
 101
 102 #ifdef __cplusplus
 103 extern "C" {
 104 #endif
 105
 106 /**AutomaticStart*************************************************************/
 107
 108 /*---------------------------------------------------------------------------*/
 109 /* Static function prototypes                                                */
 110 /*---------------------------------------------------------------------------*/
 111
 112 static DdApaNumber cuddApaCountMintermAux (DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st_table * table);
 113 static enum st_retval cuddApaStCountfree (char * key, char * value, char * arg);
 114
 115 /**AutomaticEnd***************************************************************/
 116
 117 #ifdef __cplusplus
 118 } /* end of extern "C" */
 119 #endif
 120
 121
 122 /*---------------------------------------------------------------------------*/
 123 /* Definition of exported functions                                          */
 124 /*---------------------------------------------------------------------------*/
 125
 126
 127 /**Function********************************************************************
 128
 129   Synopsis    [Finds the number of digits for an arbitrary precision
 130   integer.]
 131
 132   Description [Finds the number of digits for an arbitrary precision
 133   integer given the maximum number of binary digits.  The number of
 134   binary digits should be positive. Returns the number of digits if
 135   successful; 0 otherwise.]
 136
 137   SideEffects [None]
 138
 139   SeeAlso     []
 140
 141 ******************************************************************************/
 142 int
 143 Cudd_ApaNumberOfDigits(
 144   int  binaryDigits)
 145 {
 146     int digits;
 147
 148     digits = binaryDigits / DD_APA_BITS;
 149     if ((digits * DD_APA_BITS) != binaryDigits)
 150         digits++;
 151     return(digits);
 152
 153 } /* end of Cudd_ApaNumberOfDigits */
 154
 155
 156 /**Function********************************************************************
 157
 158   Synopsis    [Allocates memory for an arbitrary precision integer.]
 159
 160   Description [Allocates memory for an arbitrary precision
 161   integer. Returns a pointer to the allocated memory if successful;
 162   NULL otherwise.]
 163
 164   SideEffects [None]
 165
 166   SeeAlso     []
 167
 168 ******************************************************************************/
 169 DdApaNumber
 170 Cudd_NewApaNumber(
 171   int  digits)
 172 {
 173     return(ALLOC(DdApaDigit, digits));
 174
 175 } /* end of Cudd_NewApaNumber */
 176
 177
 178 /**Function********************************************************************
 179
 180   Synopsis    [Makes a copy of an arbitrary precision integer.]
 181
 182   Description [Makes a copy of an arbitrary precision integer.]
 183
 184   SideEffects [Changes parameter <code>dest</code>.]
 185
 186   SeeAlso     []
 187
 188 ******************************************************************************/
 189 void
 190 Cudd_ApaCopy(
 191   int  digits,
 192   DdApaNumber  source,
 193   DdApaNumber  dest)
 194 {
 195     int i;
 196
 197     for (i = 0; i < digits; i++) {
 198         dest[i] = source[i];
 199     }
 200
 201 } /* end of Cudd_ApaCopy */
 202
 203
 204 /**Function********************************************************************
 205
 206   Synopsis    [Adds two arbitrary precision integers.]
 207
 208   Description [Adds two arbitrary precision integers.  Returns the
 209   carry out of the most significant digit.]
 210
 211   SideEffects [The result of the sum is stored in parameter <code>sum</code>.]
 212
 213   SeeAlso     []
 214
 215 ******************************************************************************/
 216 DdApaDigit
 217 Cudd_ApaAdd(
 218   int  digits,
 219   DdApaNumber  a,
 220   DdApaNumber  b,
 221   DdApaNumber  sum)
 222 {
 223     int i;
 224     DdApaDoubleDigit partial = 0;
 225
 226     for (i = digits - 1; i >= 0; i--) {
 227         partial = a[i] + b[i] + DD_MSDIGIT(partial);
 228         sum[i] = (DdApaDigit) DD_LSDIGIT(partial);
 229     }
 230     return((DdApaDigit) DD_MSDIGIT(partial));
 231
 232 } /* end of Cudd_ApaAdd */
 233
 234
 235 /**Function********************************************************************
 236
 237   Synopsis    [Subtracts two arbitrary precision integers.]
 238
 239   Description [Subtracts two arbitrary precision integers.  Returns the
 240   borrow out of the most significant digit.]
 241
 242   SideEffects [The result of the subtraction is stored in parameter
 243   <code>diff</code>.]
 244
 245   SeeAlso     []
 246
 247 ******************************************************************************/
 248 DdApaDigit
 249 Cudd_ApaSubtract(
 250   int  digits,
 251   DdApaNumber  a,
 252   DdApaNumber  b,
 253   DdApaNumber  diff)
 254 {
 255     int i;
 256     DdApaDoubleDigit partial = DD_APA_BASE;
 257
 258     for (i = digits - 1; i >= 0; i--) {
 259         partial = DD_MSDIGIT(partial) + DD_APA_MASK + a[i] - b[i];
 260         diff[i] = (DdApaDigit) DD_LSDIGIT(partial);
 261     }
 262     return((DdApaDigit) DD_MSDIGIT(partial) - 1);
 263
 264 } /* end of Cudd_ApaSubtract */
 265
 266
 267 /**Function********************************************************************
 268
 269   Synopsis    [Divides an arbitrary precision integer by a digit.]
 270
 271   Description [Divides an arbitrary precision integer by a digit.]
 272
 273   SideEffects [The quotient is returned in parameter <code>quotient</code>.]
 274
 275   SeeAlso     []
 276
 277 ******************************************************************************/
 278 DdApaDigit
 279 Cudd_ApaShortDivision(
 280   int  digits,
 281   DdApaNumber  dividend,
 282   DdApaDigit  divisor,
 283   DdApaNumber  quotient)
 284 {
 285     int i;
 286     DdApaDigit remainder;
 287     DdApaDoubleDigit partial;
 288
 289     remainder = 0;
 290     for (i = 0; i < digits; i++) {
 291         partial = remainder * DD_APA_BASE + dividend[i];
 292         quotient[i] = (DdApaDigit) (partial/(DdApaDoubleDigit)divisor);
 293         remainder = (DdApaDigit) (partial % divisor);
 294     }
 295
 296     return(remainder);
 297
 298 } /* end of Cudd_ApaShortDivision */
 299
 300
 301 /**Function********************************************************************
 302
 303   Synopsis    [Divides an arbitrary precision integer by an integer.]
 304
 305   Description [Divides an arbitrary precision integer by a 32-bit
 306   unsigned integer. Returns the remainder of the division. This
 307   procedure relies on the assumption that the number of bits of a
 308   DdApaDigit plus the number of bits of an unsigned int is less the
 309   number of bits of the mantissa of a double. This guarantees that the
 310   product of a DdApaDigit and an unsigned int can be represented
 311   without loss of precision by a double. On machines where this
 312   assumption is not satisfied, this procedure will malfunction.]
 313
 314   SideEffects [The quotient is returned in parameter <code>quotient</code>.]
 315
 316   SeeAlso     [Cudd_ApaShortDivision]
 317
 318 ******************************************************************************/
 319 unsigned int
 320 Cudd_ApaIntDivision(
 321   int  digits,
 322   DdApaNumber dividend,
 323   unsigned int divisor,
 324   DdApaNumber quotient)
 325 {
 326     int i;
 327     double partial;
 328     unsigned int remainder = 0;
 329     double ddiv = (double) divisor;
 330
 331     for (i = 0; i < digits; i++) {
 332         partial = (double) remainder * DD_APA_BASE + dividend[i];
 333         quotient[i] = (DdApaDigit) (partial / ddiv);
 334         remainder = (unsigned int) (partial - ((double)quotient[i] * ddiv));
 335     }
 336
 337     return(remainder);
 338
 339 } /* end of Cudd_ApaIntDivision */
 340
 341
 342 /**Function********************************************************************
 343
 344   Synopsis [Shifts right an arbitrary precision integer by one binary
 345   place.]
 346
 347   Description [Shifts right an arbitrary precision integer by one
 348   binary place. The most significant binary digit of the result is
 349   taken from parameter <code>in</code>.]
 350
 351   SideEffects [The result is returned in parameter <code>b</code>.]
 352
 353   SeeAlso     []
 354
 355 ******************************************************************************/
 356 void
 357 Cudd_ApaShiftRight(
 358   int  digits,
 359   DdApaDigit  in,
 360   DdApaNumber  a,
 361   DdApaNumber  b)
 362 {
 363     int i;
 364
 365     for (i = digits - 1; i > 0; i--) {
 366         b[i] = (a[i] >> 1) | ((a[i-1] & 1) << (DD_APA_BITS - 1));
 367     }
 368     b[0] = (a[0] >> 1) | (in << (DD_APA_BITS - 1));
 369
 370 } /* end of Cudd_ApaShiftRight */
 371
 372
 373 /**Function********************************************************************
 374
 375   Synopsis    [Sets an arbitrary precision integer to a one-digit literal.]
 376
 377   Description [Sets an arbitrary precision integer to a one-digit literal.]
 378
 379   SideEffects [The result is returned in parameter <code>number</code>.]
 380
 381   SeeAlso     []
 382
 383 ******************************************************************************/
 384 void
 385 Cudd_ApaSetToLiteral(
 386   int  digits,
 387   DdApaNumber  number,
 388   DdApaDigit  literal)
 389 {
 390     int i;
 391
 392     for (i = 0; i < digits - 1; i++)
 393         number[i] = 0;
 394     number[digits - 1] = literal;
 395
 396 } /* end of Cudd_ApaSetToLiteral */
 397
 398
 399 /**Function********************************************************************
 400
 401   Synopsis    [Sets an arbitrary precision integer to a power of two.]
 402
 403   Description [Sets an arbitrary precision integer to a power of
 404   two. If the power of two is too large to be represented, the number
 405   is set to 0.]
 406
 407   SideEffects [The result is returned in parameter <code>number</code>.]
 408
 409   SeeAlso     []
 410
 411 ******************************************************************************/
 412 void
 413 Cudd_ApaPowerOfTwo(
 414   int  digits,
 415   DdApaNumber  number,
 416   int  power)
 417 {
 418     int i;
 419     int index;
 420
 421     for (i = 0; i < digits; i++)
 422         number[i] = 0;
 423     i = digits - 1 - power / DD_APA_BITS;
 424     if (i < 0) return;
 425     index = power & (DD_APA_BITS - 1);
 426     number[i] = 1 << index;
 427
 428 } /* end of Cudd_ApaPowerOfTwo */
 429
 430
 431 /**Function********************************************************************
 432
 433   Synopsis    [Compares two arbitrary precision integers.]
 434
 435   Description [Compares two arbitrary precision integers. Returns 1 if
 436   the first number is larger; 0 if they are equal; -1 if the second
 437   number is larger.]
 438
 439   SideEffects [None]
 440
 441   SeeAlso     []
 442
 443 ******************************************************************************/
 444 int
 445 Cudd_ApaCompare(
 446   int digitsFirst,
 447   DdApaNumber  first,
 448   int digitsSecond,
 449   DdApaNumber  second)
 450 {
 451     int i;
 452     int firstNZ, secondNZ;
 453
 454     /* Find first non-zero in both numbers. */
 455     for (firstNZ = 0; firstNZ < digitsFirst; firstNZ++)
 456         if (first[firstNZ] != 0) break;
 457     for (secondNZ = 0; secondNZ < digitsSecond; secondNZ++)
 458         if (second[secondNZ] != 0) break;
 459     if (digitsFirst - firstNZ > digitsSecond - secondNZ) return(1);
 460     else if (digitsFirst - firstNZ < digitsSecond - secondNZ) return(-1);
 461     for (i = 0; i < digitsFirst - firstNZ; i++) {
 462         if (first[firstNZ + i] > second[secondNZ + i]) return(1);
 463         else if (first[firstNZ + i] < second[secondNZ + i]) return(-1);
 464     }
 465     return(0);
 466
 467 } /* end of Cudd_ApaCompare */
 468
 469
 470 /**Function********************************************************************
 471
 472   Synopsis    [Compares the ratios of two arbitrary precision integers to two
 473   unsigned ints.]
 474
 475   Description [Compares the ratios of two arbitrary precision integers
 476   to two unsigned ints. Returns 1 if the first number is larger; 0 if
 477   they are equal; -1 if the second number is larger.]
 478
 479   SideEffects [None]
 480
 481   SeeAlso     []
 482
 483 ******************************************************************************/
 484 int
 485 Cudd_ApaCompareRatios(
 486   int digitsFirst,
 487   DdApaNumber firstNum,
 488   unsigned int firstDen,
 489   int digitsSecond,
 490   DdApaNumber secondNum,
 491   unsigned int secondDen)
 492 {
 493     int result;
 494     DdApaNumber first, second;
 495     unsigned int firstRem, secondRem;
 496
 497     first = Cudd_NewApaNumber(digitsFirst);
 498     firstRem = Cudd_ApaIntDivision(digitsFirst,firstNum,firstDen,first);
 499     second = Cudd_NewApaNumber(digitsSecond);
 500     secondRem = Cudd_ApaIntDivision(digitsSecond,secondNum,secondDen,second);
 501     result = Cudd_ApaCompare(digitsFirst,first,digitsSecond,second);
 502     FREE(first);
 503     FREE(second);
 504     if (result == 0) {
 505         if ((double)firstRem/firstDen > (double)secondRem/secondDen)
 506             return(1);
 507         else if ((double)firstRem/firstDen < (double)secondRem/secondDen)
 508             return(-1);
 509     }
 510     return(result);
 511
 512 } /* end of Cudd_ApaCompareRatios */
 513
 514
 515 /**Function********************************************************************
 516
 517   Synopsis    [Prints an arbitrary precision integer in hexadecimal format.]
 518
 519   Description [Prints an arbitrary precision integer in hexadecimal format.
 520   Returns 1 if successful; 0 otherwise.]
 521
 522   SideEffects [None]
 523
 524   SeeAlso     [Cudd_ApaPrintDecimal Cudd_ApaPrintExponential]
 525
 526 ******************************************************************************/
 527 int
 528 Cudd_ApaPrintHex(
 529   FILE * fp,
 530   int  digits,
 531   DdApaNumber  number)
 532 {
 533     int i, result;
 534
 535     for (i = 0; i < digits; i++) {
 536         result = fprintf(fp,DD_APA_HEXPRINT,number[i]);
 537         if (result == EOF)
 538             return(0);
 539     }
 540     return(1);
 541
 542 } /* end of Cudd_ApaPrintHex */
 543
 544
 545 /**Function********************************************************************
 546
 547   Synopsis    [Prints an arbitrary precision integer in decimal format.]
 548
 549   Description [Prints an arbitrary precision integer in decimal format.
 550   Returns 1 if successful; 0 otherwise.]
 551
 552   SideEffects [None]
 553
 554   SeeAlso     [Cudd_ApaPrintHex Cudd_ApaPrintExponential]
 555
 556 ******************************************************************************/
 557 int
 558 Cudd_ApaPrintDecimal(
 559   FILE * fp,
 560   int  digits,
 561   DdApaNumber  number)
 562 {
 563     int i, result;
 564     DdApaDigit remainder;
 565     DdApaNumber work;
 566     unsigned char *decimal;
 567     int leadingzero;
 568     int decimalDigits = (int) (digits * log10((double) DD_APA_BASE)) + 1;
 569
 570     work = Cudd_NewApaNumber(digits);
 571     if (work == NULL)
 572         return(0);
 573     decimal = ALLOC(unsigned char, decimalDigits);
 574     if (decimal == NULL) {
 575         FREE(work);
 576         return(0);
 577     }
 578     Cudd_ApaCopy(digits,number,work);
 579     for (i = decimalDigits - 1; i >= 0; i--) {
 580         remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
 581         decimal[i] = (unsigned char) remainder;
 582     }
 583     FREE(work);
 584
 585     leadingzero = 1;
 586     for (i = 0; i < decimalDigits; i++) {
 587         leadingzero = leadingzero && (decimal[i] == 0);
 588         if ((!leadingzero) || (i == (decimalDigits - 1))) {
 589             result = fprintf(fp,"%1d",decimal[i]);
 590             if (result == EOF) {
 591                 FREE(decimal);
 592                 return(0);
 593             }
 594         }
 595     }
 596     FREE(decimal);
 597     return(1);
 598
 599 } /* end of Cudd_ApaPrintDecimal */
 600
 601
 602 /**Function********************************************************************
 603
 604   Synopsis    [Prints an arbitrary precision integer in exponential format.]
 605
 606   Description [Prints an arbitrary precision integer in exponential format.
 607   Returns 1 if successful; 0 otherwise.]
 608
 609   SideEffects [None]
 610
 611   SeeAlso     [Cudd_ApaPrintHex Cudd_ApaPrintDecimal]
 612
 613 ******************************************************************************/
 614 int
 615 Cudd_ApaPrintExponential(
 616   FILE * fp,
 617   int  digits,
 618   DdApaNumber  number,
 619   int precision)
 620 {
 621     int i, first, last, result;
 622     DdApaDigit remainder;
 623     DdApaNumber work;
 624     unsigned char *decimal;
 625     int decimalDigits = (int) (digits * log10((double) DD_APA_BASE)) + 1;
 626
 627     work = Cudd_NewApaNumber(digits);
 628     if (work == NULL)
 629         return(0);
 630     decimal = ALLOC(unsigned char, decimalDigits);
 631     if (decimal == NULL) {
 632         FREE(work);
 633         return(0);
 634     }
 635     Cudd_ApaCopy(digits,number,work);
 636     first = decimalDigits - 1;
 637     for (i = decimalDigits - 1; i >= 0; i--) {
 638         remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
 639         decimal[i] = (unsigned char) remainder;
 640         if (remainder != 0) first = i; /* keep track of MS non-zero */
 641     }
 642     FREE(work);
 643     last = ddMin(first + precision, decimalDigits);
 644
 645     for (i = first; i < last; i++) {
 646         result = fprintf(fp,"%s%1d",i == first+1 ? "." : "", decimal[i]);
 647         if (result == EOF) {
 648             FREE(decimal);
 649             return(0);
 650         }
 651     }
 652     FREE(decimal);
 653     result = fprintf(fp,"e+%d",decimalDigits - first - 1);
 654     if (result == EOF) {
 655         return(0);
 656     }
 657     return(1);
 658
 659 } /* end of Cudd_ApaPrintExponential */
 660
 661
 662 /**Function********************************************************************
 663
 664   Synopsis    [Counts the number of minterms of a DD.]
 665
 666   Description [Counts the number of minterms of a DD. The function is
 667   assumed to depend on nvars variables. The minterm count is
 668   represented as an arbitrary precision unsigned integer, to allow for
 669   any number of variables CUDD supports.  Returns a pointer to the
 670   array representing the number of minterms of the function rooted at
 671   node if successful; NULL otherwise.]
 672
 673   SideEffects [The number of digits of the result is returned in
 674   parameter <code>digits</code>.]
 675
 676   SeeAlso     [Cudd_CountMinterm]
 677
 678 ******************************************************************************/
 679 DdApaNumber
 680 Cudd_ApaCountMinterm(
 681   DdManager * manager,
 682   DdNode * node,
 683   int  nvars,
 684   int * digits)
 685 {
 686     DdApaNumber max, min;
 687     st_table    *table;
 688     DdApaNumber i,count;
 689
 690     background = manager->background;
 691     zero = Cudd_Not(manager->one);
 692
 693     *digits = Cudd_ApaNumberOfDigits(nvars+1);
 694     max = Cudd_NewApaNumber(*digits);
 695     if (max == NULL) {
 696         return(NULL);
 697     }
 698     Cudd_ApaPowerOfTwo(*digits,max,nvars);
 699     min = Cudd_NewApaNumber(*digits);
 700     if (min == NULL) {
 701         FREE(max);
 702         return(NULL);
 703     }
 704     Cudd_ApaSetToLiteral(*digits,min,0);
 705     table = st_init_table(st_ptrcmp,st_ptrhash);
 706     if (table == NULL) {
 707         FREE(max);
 708         FREE(min);
 709         return(NULL);
 710     }
 711     i = cuddApaCountMintermAux(Cudd_Regular(node),*digits,max,min,table);
 712     if (i == NULL) {
 713         FREE(max);
 714         FREE(min);
 715         st_foreach(table, cuddApaStCountfree, NULL);
 716         st_free_table(table);
 717         return(NULL);
 718     }
 719     count = Cudd_NewApaNumber(*digits);
 720     if (count == NULL) {
 721         FREE(max);
 722         FREE(min);
 723         st_foreach(table, cuddApaStCountfree, NULL);
 724         st_free_table(table);
 725         if (Cudd_Regular(node)->ref == 1) FREE(i);
 726         return(NULL);
 727     }
 728     if (Cudd_IsComplement(node)) {
 729         (void) Cudd_ApaSubtract(*digits,max,i,count);
 730     } else {
 731         Cudd_ApaCopy(*digits,i,count);
 732     }
 733     FREE(max);
 734     FREE(min);
 735     st_foreach(table, cuddApaStCountfree, NULL);
 736     st_free_table(table);
 737     if (Cudd_Regular(node)->ref == 1) FREE(i);
 738     return(count);
 739
 740 } /* end of Cudd_ApaCountMinterm */
 741
 742
 743 /**Function********************************************************************
 744
 745   Synopsis    [Prints the number of minterms of a BDD or ADD using
 746   arbitrary precision arithmetic.]
 747
 748   Description [Prints the number of minterms of a BDD or ADD using
 749   arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.]
 750
 751   SideEffects [None]
 752
 753   SeeAlso     [Cudd_ApaPrintMintermExp]
 754
 755 ******************************************************************************/
 756 int
 757 Cudd_ApaPrintMinterm(
 758   FILE * fp,
 759   DdManager * dd,
 760   DdNode * node,
 761   int  nvars)
 762 {
 763     int digits;
 764     int result;
 765     DdApaNumber count;
 766
 767     count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
 768     if (count == NULL)
 769         return(0);
 770     result = Cudd_ApaPrintDecimal(fp,digits,count);
 771     FREE(count);
 772     if (fprintf(fp,"\n") == EOF) {
 773         return(0);
 774     }
 775     return(result);
 776
 777 } /* end of Cudd_ApaPrintMinterm */
 778
 779
 780 /**Function********************************************************************
 781
 782   Synopsis    [Prints the number of minterms of a BDD or ADD in exponential
 783   format using arbitrary precision arithmetic.]
 784
 785   Description [Prints the number of minterms of a BDD or ADD in
 786   exponential format using arbitrary precision arithmetic. Parameter
 787   precision controls the number of signficant digits printed. Returns
 788   1 if successful; 0 otherwise.]
 789
 790   SideEffects [None]
 791
 792   SeeAlso     [Cudd_ApaPrintMinterm]
 793
 794 ******************************************************************************/
 795 int
 796 Cudd_ApaPrintMintermExp(
 797   FILE * fp,
 798   DdManager * dd,
 799   DdNode * node,
 800   int  nvars,
 801   int precision)
 802 {
 803     int digits;
 804     int result;
 805     DdApaNumber count;
 806
 807     count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
 808     if (count == NULL)
 809         return(0);
 810     result = Cudd_ApaPrintExponential(fp,digits,count,precision);
 811     FREE(count);
 812     if (fprintf(fp,"\n") == EOF) {
 813         return(0);
 814     }
 815     return(result);
 816
 817 } /* end of Cudd_ApaPrintMintermExp */
 818
 819
 820 /**Function********************************************************************
 821
 822   Synopsis    [Prints the density of a BDD or ADD using
 823   arbitrary precision arithmetic.]
 824
 825   Description [Prints the density of a BDD or ADD using
 826   arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.]
 827
 828   SideEffects [None]
 829
 830   SeeAlso     []
 831
 832 ******************************************************************************/
 833 int
 834 Cudd_ApaPrintDensity(
 835   FILE * fp,
 836   DdManager * dd,
 837   DdNode * node,
 838   int  nvars)
 839 {
 840     int digits;
 841     int result;
 842     DdApaNumber count,density;
 843     unsigned int size, remainder, fractional;
 844
 845     count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
 846     if (count == NULL)
 847         return(0);
 848     size = Cudd_DagSize(node);
 849     density = Cudd_NewApaNumber(digits);
 850     remainder = Cudd_ApaIntDivision(digits,count,size,density);
 851     result = Cudd_ApaPrintDecimal(fp,digits,density);
 852     FREE(count);
 853     FREE(density);
 854     fractional = (unsigned int)((double)remainder / size * 1000000);
 855     if (fprintf(fp,".%u\n", fractional) == EOF) {
 856         return(0);
 857     }
 858     return(result);
 859
 860 } /* end of Cudd_ApaPrintDensity */
 861
 862
 863 /*---------------------------------------------------------------------------*/
 864 /* Definition of internal functions                                          */
 865 /*---------------------------------------------------------------------------*/
 866
 867
 868 /*---------------------------------------------------------------------------*/
 869 /* Definition of static functions                                            */
 870 /*---------------------------------------------------------------------------*/
 871
 872
 873 /**Function********************************************************************
 874
 875   Synopsis    [Performs the recursive step of Cudd_ApaCountMinterm.]
 876
 877   Description [Performs the recursive step of Cudd_ApaCountMinterm.
 878   It is based on the following identity. Let |f| be the
 879   number of minterms of f. Then:
 880   <xmp>
 881     |f| = (|f0|+|f1|)/2
 882   </xmp>
 883   where f0 and f1 are the two cofactors of f.
 884   Uses the identity <code>|f'| = max - |f|</code>.
 885   The procedure expects the argument "node" to be a regular pointer, and
 886   guarantees this condition is met in the recursive calls.
 887   For efficiency, the result of a call is cached only if the node has
 888   a reference count greater than 1.
 889   Returns the number of minterms of the function rooted at node.]
 890
 891   SideEffects [None]
 892
 893 ******************************************************************************/
 894 static DdApaNumber
 895 cuddApaCountMintermAux(
 896   DdNode * node,
 897   int  digits,
 898   DdApaNumber  max,
 899   DdApaNumber  min,
 900   st_table * table)
 901 {
 902     DdNode      *Nt, *Ne;
 903     DdApaNumber mint, mint1, mint2;
 904     DdApaDigit  carryout;
 905
 906     if (cuddIsConstant(node)) {
 907         if (node == background || node == zero) {
 908             return(min);
 909         } else {
 910             return(max);
 911         }
 912     }
 913     if (node->ref > 1 && st_lookup(table, node, &mint)) {
 914         return(mint);
 915     }
 916
 917     Nt = cuddT(node); Ne = cuddE(node);
 918
 919     mint1 = cuddApaCountMintermAux(Nt,  digits, max, min, table);
 920     if (mint1 == NULL) return(NULL);
 921     mint2 = cuddApaCountMintermAux(Cudd_Regular(Ne), digits, max, min, table);
 922     if (mint2 == NULL) {
 923         if (Nt->ref == 1) FREE(mint1);
 924         return(NULL);
 925     }
 926     mint = Cudd_NewApaNumber(digits);
 927     if (mint == NULL) {
 928         if (Nt->ref == 1) FREE(mint1);
 929         if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
 930         return(NULL);
 931     }
 932     if (Cudd_IsComplement(Ne)) {
 933         (void) Cudd_ApaSubtract(digits,max,mint2,mint);
 934         carryout = Cudd_ApaAdd(digits,mint1,mint,mint);
 935     } else {
 936         carryout = Cudd_ApaAdd(digits,mint1,mint2,mint);
 937     }
 938     Cudd_ApaShiftRight(digits,carryout,mint,mint);
 939     /* If the refernce count of a child is 1, its minterm count
 940     ** hasn't been stored in table.  Therefore, it must be explicitly
 941     ** freed here. */
 942     if (Nt->ref == 1) FREE(mint1);
 943     if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
 944
 945     if (node->ref > 1) {
 946         if (st_insert(table, (char *)node, (char *)mint) == ST_OUT_OF_MEM) {
 947             FREE(mint);
 948             return(NULL);
 949         }
 950     }
 951     return(mint);
 952
 953 } /* end of cuddApaCountMintermAux */
 954
 955
 956 /**Function********************************************************************
 957
 958   Synopsis [Frees the memory used to store the minterm counts recorded
 959   in the visited table.]
 960
 961   Description [Frees the memory used to store the minterm counts
 962   recorded in the visited table. Returns ST_CONTINUE.]
 963
 964   SideEffects [None]
 965
 966 ******************************************************************************/
 967 static enum st_retval
 968 cuddApaStCountfree(
 969   char * key,
 970   char * value,
 971   char * arg)
 972 {
 973     DdApaNumber d;
 974
 975     d = (DdApaNumber) value;
 976     FREE(d);
 977     return(ST_CONTINUE);
 978
 979 } /* end of cuddApaStCountfree */