1 /**CFile***********************************************************************
7 Synopsis [Arbitrary precision arithmetic functions.]
9 Description [External procedures included in this module:
11 <li> Cudd_ApaNumberOfDigits()
12 <li> Cudd_NewApaNumber()
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()
31 Static procedures included in this module:
33 <li> cuddApaCountMintermAux()
34 <li> cuddApaStCountfree()
37 Author [Fabio Somenzi]
39 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
43 Redistribution and use in source and binary forms, with or without
44 modification, are permitted provided that the following conditions
47 Redistributions of source code must retain the above copyright
48 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
71 ******************************************************************************/
76 /*---------------------------------------------------------------------------*/
77 /* Constant declarations */
78 /*---------------------------------------------------------------------------*/
80 /*---------------------------------------------------------------------------*/
81 /* Stucture declarations */
82 /*---------------------------------------------------------------------------*/
84 /*---------------------------------------------------------------------------*/
85 /* Type declarations */
86 /*---------------------------------------------------------------------------*/
88 /*---------------------------------------------------------------------------*/
89 /* Variable declarations */
90 /*---------------------------------------------------------------------------*/
93 static char rcsid
[] DD_UNUSED
= "$Id: cuddApa.c,v 1.19 2009/03/08 01:27:50 fabio Exp $";
96 static DdNode
*background
, *zero
;
98 /*---------------------------------------------------------------------------*/
99 /* Macro declarations */
100 /*---------------------------------------------------------------------------*/
106 /**AutomaticStart*************************************************************/
108 /*---------------------------------------------------------------------------*/
109 /* Static function prototypes */
110 /*---------------------------------------------------------------------------*/
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
);
115 /**AutomaticEnd***************************************************************/
118 } /* end of extern "C" */
122 /*---------------------------------------------------------------------------*/
123 /* Definition of exported functions */
124 /*---------------------------------------------------------------------------*/
127 /**Function********************************************************************
129 Synopsis [Finds the number of digits for an arbitrary precision
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.]
141 ******************************************************************************/
143 Cudd_ApaNumberOfDigits(
148 digits
= binaryDigits
/ DD_APA_BITS
;
149 if ((digits
* DD_APA_BITS
) != binaryDigits
)
153 } /* end of Cudd_ApaNumberOfDigits */
156 /**Function********************************************************************
158 Synopsis [Allocates memory for an arbitrary precision integer.]
160 Description [Allocates memory for an arbitrary precision
161 integer. Returns a pointer to the allocated memory if successful;
168 ******************************************************************************/
173 return(ALLOC(DdApaDigit
, digits
));
175 } /* end of Cudd_NewApaNumber */
178 /**Function********************************************************************
180 Synopsis [Makes a copy of an arbitrary precision integer.]
182 Description [Makes a copy of an arbitrary precision integer.]
184 SideEffects [Changes parameter <code>dest</code>.]
188 ******************************************************************************/
197 for (i
= 0; i
< digits
; i
++) {
201 } /* end of Cudd_ApaCopy */
204 /**Function********************************************************************
206 Synopsis [Adds two arbitrary precision integers.]
208 Description [Adds two arbitrary precision integers. Returns the
209 carry out of the most significant digit.]
211 SideEffects [The result of the sum is stored in parameter <code>sum</code>.]
215 ******************************************************************************/
224 DdApaDoubleDigit partial
= 0;
226 for (i
= digits
- 1; i
>= 0; i
--) {
227 partial
= a
[i
] + b
[i
] + DD_MSDIGIT(partial
);
228 sum
[i
] = (DdApaDigit
) DD_LSDIGIT(partial
);
230 return((DdApaDigit
) DD_MSDIGIT(partial
));
232 } /* end of Cudd_ApaAdd */
235 /**Function********************************************************************
237 Synopsis [Subtracts two arbitrary precision integers.]
239 Description [Subtracts two arbitrary precision integers. Returns the
240 borrow out of the most significant digit.]
242 SideEffects [The result of the subtraction is stored in parameter
247 ******************************************************************************/
256 DdApaDoubleDigit partial
= DD_APA_BASE
;
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
);
262 return((DdApaDigit
) DD_MSDIGIT(partial
) - 1);
264 } /* end of Cudd_ApaSubtract */
267 /**Function********************************************************************
269 Synopsis [Divides an arbitrary precision integer by a digit.]
271 Description [Divides an arbitrary precision integer by a digit.]
273 SideEffects [The quotient is returned in parameter <code>quotient</code>.]
277 ******************************************************************************/
279 Cudd_ApaShortDivision(
281 DdApaNumber dividend
,
283 DdApaNumber quotient
)
286 DdApaDigit remainder
;
287 DdApaDoubleDigit partial
;
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
);
298 } /* end of Cudd_ApaShortDivision */
301 /**Function********************************************************************
303 Synopsis [Divides an arbitrary precision integer by an integer.]
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.]
314 SideEffects [The quotient is returned in parameter <code>quotient</code>.]
316 SeeAlso [Cudd_ApaShortDivision]
318 ******************************************************************************/
322 DdApaNumber dividend
,
323 unsigned int divisor
,
324 DdApaNumber quotient
)
328 unsigned int remainder
= 0;
329 double ddiv
= (double) divisor
;
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
));
339 } /* end of Cudd_ApaIntDivision */
342 /**Function********************************************************************
344 Synopsis [Shifts right an arbitrary precision integer by one binary
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>.]
351 SideEffects [The result is returned in parameter <code>b</code>.]
355 ******************************************************************************/
365 for (i
= digits
- 1; i
> 0; i
--) {
366 b
[i
] = (a
[i
] >> 1) | ((a
[i
-1] & 1) << (DD_APA_BITS
- 1));
368 b
[0] = (a
[0] >> 1) | (in
<< (DD_APA_BITS
- 1));
370 } /* end of Cudd_ApaShiftRight */
373 /**Function********************************************************************
375 Synopsis [Sets an arbitrary precision integer to a one-digit literal.]
377 Description [Sets an arbitrary precision integer to a one-digit literal.]
379 SideEffects [The result is returned in parameter <code>number</code>.]
383 ******************************************************************************/
385 Cudd_ApaSetToLiteral(
392 for (i
= 0; i
< digits
- 1; i
++)
394 number
[digits
- 1] = literal
;
396 } /* end of Cudd_ApaSetToLiteral */
399 /**Function********************************************************************
401 Synopsis [Sets an arbitrary precision integer to a power of two.]
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
407 SideEffects [The result is returned in parameter <code>number</code>.]
411 ******************************************************************************/
421 for (i
= 0; i
< digits
; i
++)
423 i
= digits
- 1 - power
/ DD_APA_BITS
;
425 index
= power
& (DD_APA_BITS
- 1);
426 number
[i
] = 1 << index
;
428 } /* end of Cudd_ApaPowerOfTwo */
431 /**Function********************************************************************
433 Synopsis [Compares two arbitrary precision integers.]
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
443 ******************************************************************************/
452 int firstNZ
, secondNZ
;
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);
467 } /* end of Cudd_ApaCompare */
470 /**Function********************************************************************
472 Synopsis [Compares the ratios of two arbitrary precision integers to two
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.]
483 ******************************************************************************/
485 Cudd_ApaCompareRatios(
487 DdApaNumber firstNum
,
488 unsigned int firstDen
,
490 DdApaNumber secondNum
,
491 unsigned int secondDen
)
494 DdApaNumber first
, second
;
495 unsigned int firstRem
, secondRem
;
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
);
505 if ((double)firstRem
/firstDen
> (double)secondRem
/secondDen
)
507 else if ((double)firstRem
/firstDen
< (double)secondRem
/secondDen
)
512 } /* end of Cudd_ApaCompareRatios */
515 /**Function********************************************************************
517 Synopsis [Prints an arbitrary precision integer in hexadecimal format.]
519 Description [Prints an arbitrary precision integer in hexadecimal format.
520 Returns 1 if successful; 0 otherwise.]
524 SeeAlso [Cudd_ApaPrintDecimal Cudd_ApaPrintExponential]
526 ******************************************************************************/
535 for (i
= 0; i
< digits
; i
++) {
536 result
= fprintf(fp
,DD_APA_HEXPRINT
,number
[i
]);
542 } /* end of Cudd_ApaPrintHex */
545 /**Function********************************************************************
547 Synopsis [Prints an arbitrary precision integer in decimal format.]
549 Description [Prints an arbitrary precision integer in decimal format.
550 Returns 1 if successful; 0 otherwise.]
554 SeeAlso [Cudd_ApaPrintHex Cudd_ApaPrintExponential]
556 ******************************************************************************/
558 Cudd_ApaPrintDecimal(
564 DdApaDigit remainder
;
566 unsigned char *decimal
;
568 int decimalDigits
= (int) (digits
* log10((double) DD_APA_BASE
)) + 1;
570 work
= Cudd_NewApaNumber(digits
);
573 decimal
= ALLOC(unsigned char, decimalDigits
);
574 if (decimal
== NULL
) {
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
;
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
]);
599 } /* end of Cudd_ApaPrintDecimal */
602 /**Function********************************************************************
604 Synopsis [Prints an arbitrary precision integer in exponential format.]
606 Description [Prints an arbitrary precision integer in exponential format.
607 Returns 1 if successful; 0 otherwise.]
611 SeeAlso [Cudd_ApaPrintHex Cudd_ApaPrintDecimal]
613 ******************************************************************************/
615 Cudd_ApaPrintExponential(
621 int i
, first
, last
, result
;
622 DdApaDigit remainder
;
624 unsigned char *decimal
;
625 int decimalDigits
= (int) (digits
* log10((double) DD_APA_BASE
)) + 1;
627 work
= Cudd_NewApaNumber(digits
);
630 decimal
= ALLOC(unsigned char, decimalDigits
);
631 if (decimal
== NULL
) {
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 */
643 last
= ddMin(first
+ precision
, decimalDigits
);
645 for (i
= first
; i
< last
; i
++) {
646 result
= fprintf(fp
,"%s%1d",i
== first
+1 ? "." : "", decimal
[i
]);
653 result
= fprintf(fp
,"e+%d",decimalDigits
- first
- 1);
659 } /* end of Cudd_ApaPrintExponential */
662 /**Function********************************************************************
664 Synopsis [Counts the number of minterms of a DD.]
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.]
673 SideEffects [The number of digits of the result is returned in
674 parameter <code>digits</code>.]
676 SeeAlso [Cudd_CountMinterm]
678 ******************************************************************************/
680 Cudd_ApaCountMinterm(
686 DdApaNumber max
, min
;
690 background
= manager
->background
;
691 zero
= Cudd_Not(manager
->one
);
693 *digits
= Cudd_ApaNumberOfDigits(nvars
+1);
694 max
= Cudd_NewApaNumber(*digits
);
698 Cudd_ApaPowerOfTwo(*digits
,max
,nvars
);
699 min
= Cudd_NewApaNumber(*digits
);
704 Cudd_ApaSetToLiteral(*digits
,min
,0);
705 table
= st_init_table(st_ptrcmp
,st_ptrhash
);
711 i
= cuddApaCountMintermAux(Cudd_Regular(node
),*digits
,max
,min
,table
);
715 st_foreach(table
, cuddApaStCountfree
, NULL
);
716 st_free_table(table
);
719 count
= Cudd_NewApaNumber(*digits
);
723 st_foreach(table
, cuddApaStCountfree
, NULL
);
724 st_free_table(table
);
725 if (Cudd_Regular(node
)->ref
== 1) FREE(i
);
728 if (Cudd_IsComplement(node
)) {
729 (void) Cudd_ApaSubtract(*digits
,max
,i
,count
);
731 Cudd_ApaCopy(*digits
,i
,count
);
735 st_foreach(table
, cuddApaStCountfree
, NULL
);
736 st_free_table(table
);
737 if (Cudd_Regular(node
)->ref
== 1) FREE(i
);
740 } /* end of Cudd_ApaCountMinterm */
743 /**Function********************************************************************
745 Synopsis [Prints the number of minterms of a BDD or ADD using
746 arbitrary precision arithmetic.]
748 Description [Prints the number of minterms of a BDD or ADD using
749 arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.]
753 SeeAlso [Cudd_ApaPrintMintermExp]
755 ******************************************************************************/
757 Cudd_ApaPrintMinterm(
767 count
= Cudd_ApaCountMinterm(dd
,node
,nvars
,&digits
);
770 result
= Cudd_ApaPrintDecimal(fp
,digits
,count
);
772 if (fprintf(fp
,"\n") == EOF
) {
777 } /* end of Cudd_ApaPrintMinterm */
780 /**Function********************************************************************
782 Synopsis [Prints the number of minterms of a BDD or ADD in exponential
783 format using arbitrary precision arithmetic.]
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.]
792 SeeAlso [Cudd_ApaPrintMinterm]
794 ******************************************************************************/
796 Cudd_ApaPrintMintermExp(
807 count
= Cudd_ApaCountMinterm(dd
,node
,nvars
,&digits
);
810 result
= Cudd_ApaPrintExponential(fp
,digits
,count
,precision
);
812 if (fprintf(fp
,"\n") == EOF
) {
817 } /* end of Cudd_ApaPrintMintermExp */
820 /**Function********************************************************************
822 Synopsis [Prints the density of a BDD or ADD using
823 arbitrary precision arithmetic.]
825 Description [Prints the density of a BDD or ADD using
826 arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.]
832 ******************************************************************************/
834 Cudd_ApaPrintDensity(
842 DdApaNumber count
,density
;
843 unsigned int size
, remainder
, fractional
;
845 count
= Cudd_ApaCountMinterm(dd
,node
,nvars
,&digits
);
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
);
854 fractional
= (unsigned int)((double)remainder
/ size
* 1000000);
855 if (fprintf(fp
,".%u\n", fractional
) == EOF
) {
860 } /* end of Cudd_ApaPrintDensity */
863 /*---------------------------------------------------------------------------*/
864 /* Definition of internal functions */
865 /*---------------------------------------------------------------------------*/
868 /*---------------------------------------------------------------------------*/
869 /* Definition of static functions */
870 /*---------------------------------------------------------------------------*/
873 /**Function********************************************************************
875 Synopsis [Performs the recursive step of Cudd_ApaCountMinterm.]
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:
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.]
893 ******************************************************************************/
895 cuddApaCountMintermAux(
903 DdApaNumber mint
, mint1
, mint2
;
906 if (cuddIsConstant(node
)) {
907 if (node
== background
|| node
== zero
) {
913 if (node
->ref
> 1 && st_lookup(table
, node
, &mint
)) {
917 Nt
= cuddT(node
); Ne
= cuddE(node
);
919 mint1
= cuddApaCountMintermAux(Nt
, digits
, max
, min
, table
);
920 if (mint1
== NULL
) return(NULL
);
921 mint2
= cuddApaCountMintermAux(Cudd_Regular(Ne
), digits
, max
, min
, table
);
923 if (Nt
->ref
== 1) FREE(mint1
);
926 mint
= Cudd_NewApaNumber(digits
);
928 if (Nt
->ref
== 1) FREE(mint1
);
929 if (Cudd_Regular(Ne
)->ref
== 1) FREE(mint2
);
932 if (Cudd_IsComplement(Ne
)) {
933 (void) Cudd_ApaSubtract(digits
,max
,mint2
,mint
);
934 carryout
= Cudd_ApaAdd(digits
,mint1
,mint
,mint
);
936 carryout
= Cudd_ApaAdd(digits
,mint1
,mint2
,mint
);
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
942 if (Nt
->ref
== 1) FREE(mint1
);
943 if (Cudd_Regular(Ne
)->ref
== 1) FREE(mint2
);
946 if (st_insert(table
, (char *)node
, (char *)mint
) == ST_OUT_OF_MEM
) {
953 } /* end of cuddApaCountMintermAux */
956 /**Function********************************************************************
958 Synopsis [Frees the memory used to store the minterm counts recorded
959 in the visited table.]
961 Description [Frees the memory used to store the minterm counts
962 recorded in the visited table. Returns ST_CONTINUE.]
966 ******************************************************************************/
967 static enum st_retval
975 d
= (DdApaNumber
) value
;
979 } /* end of cuddApaStCountfree */