source: vis_dev/glu-2.3/src/cuBdd/cuddApa.c @ 104

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

library glu 2.3
File size: 27.3 KB
Line 
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
93static char rcsid[] DD_UNUSED = "$Id: cuddApa.c,v 1.19 2009/03/08 01:27:50 fabio Exp $";
94#endif
95
96static  DdNode  *background, *zero;
97
98/*---------------------------------------------------------------------------*/
99/* Macro declarations                                                        */
100/*---------------------------------------------------------------------------*/
101
102#ifdef __cplusplus
103extern "C" {
104#endif
105
106/**AutomaticStart*************************************************************/
107
108/*---------------------------------------------------------------------------*/
109/* Static function prototypes                                                */
110/*---------------------------------------------------------------------------*/
111
112static DdApaNumber cuddApaCountMintermAux (DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st_table * table);
113static 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******************************************************************************/
142int
143Cudd_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******************************************************************************/
169DdApaNumber
170Cudd_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******************************************************************************/
189void
190Cudd_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******************************************************************************/
216DdApaDigit
217Cudd_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******************************************************************************/
248DdApaDigit
249Cudd_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******************************************************************************/
278DdApaDigit
279Cudd_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******************************************************************************/
319unsigned int
320Cudd_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******************************************************************************/
356void
357Cudd_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******************************************************************************/
384void
385Cudd_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******************************************************************************/
412void
413Cudd_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******************************************************************************/
444int
445Cudd_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******************************************************************************/
484int
485Cudd_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******************************************************************************/
527int
528Cudd_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******************************************************************************/
557int
558Cudd_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******************************************************************************/
614int
615Cudd_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******************************************************************************/
679DdApaNumber
680Cudd_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******************************************************************************/
756int
757Cudd_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******************************************************************************/
795int
796Cudd_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******************************************************************************/
833int
834Cudd_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******************************************************************************/
894static DdApaNumber
895cuddApaCountMintermAux(
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******************************************************************************/
967static enum st_retval
968cuddApaStCountfree(
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 */
Note: See TracBrowser for help on using the repository browser.