00001
00073 #include "util.h"
00074 #include "cuddInt.h"
00075
00076
00077
00078
00079
00080
00081
00082
00083
00084
00085
00086
00087
00088
00089
00090
00091
00092 #ifndef lint
00093 static char rcsid[] DD_UNUSED = "$Id: cuddApa.c,v 1.19 2009/03/08 01:27:50 fabio Exp $";
00094 #endif
00095
00096 static DdNode *background, *zero;
00097
00098
00099
00100
00101
00102 #ifdef __cplusplus
00103 extern "C" {
00104 #endif
00105
00108
00109
00110
00111
00112 static DdApaNumber cuddApaCountMintermAux (DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st_table * table);
00113 static enum st_retval cuddApaStCountfree (char * key, char * value, char * arg);
00114
00117 #ifdef __cplusplus
00118 }
00119 #endif
00120
00121
00122
00123
00124
00125
00126
00142 int
00143 Cudd_ApaNumberOfDigits(
00144 int binaryDigits)
00145 {
00146 int digits;
00147
00148 digits = binaryDigits / DD_APA_BITS;
00149 if ((digits * DD_APA_BITS) != binaryDigits)
00150 digits++;
00151 return(digits);
00152
00153 }
00154
00155
00169 DdApaNumber
00170 Cudd_NewApaNumber(
00171 int digits)
00172 {
00173 return(ALLOC(DdApaDigit, digits));
00174
00175 }
00176
00177
00189 void
00190 Cudd_ApaCopy(
00191 int digits,
00192 DdApaNumber source,
00193 DdApaNumber dest)
00194 {
00195 int i;
00196
00197 for (i = 0; i < digits; i++) {
00198 dest[i] = source[i];
00199 }
00200
00201 }
00202
00203
00216 DdApaDigit
00217 Cudd_ApaAdd(
00218 int digits,
00219 DdApaNumber a,
00220 DdApaNumber b,
00221 DdApaNumber sum)
00222 {
00223 int i;
00224 DdApaDoubleDigit partial = 0;
00225
00226 for (i = digits - 1; i >= 0; i--) {
00227 partial = a[i] + b[i] + DD_MSDIGIT(partial);
00228 sum[i] = (DdApaDigit) DD_LSDIGIT(partial);
00229 }
00230 return((DdApaDigit) DD_MSDIGIT(partial));
00231
00232 }
00233
00234
00248 DdApaDigit
00249 Cudd_ApaSubtract(
00250 int digits,
00251 DdApaNumber a,
00252 DdApaNumber b,
00253 DdApaNumber diff)
00254 {
00255 int i;
00256 DdApaDoubleDigit partial = DD_APA_BASE;
00257
00258 for (i = digits - 1; i >= 0; i--) {
00259 partial = DD_MSDIGIT(partial) + DD_APA_MASK + a[i] - b[i];
00260 diff[i] = (DdApaDigit) DD_LSDIGIT(partial);
00261 }
00262 return((DdApaDigit) DD_MSDIGIT(partial) - 1);
00263
00264 }
00265
00266
00278 DdApaDigit
00279 Cudd_ApaShortDivision(
00280 int digits,
00281 DdApaNumber dividend,
00282 DdApaDigit divisor,
00283 DdApaNumber quotient)
00284 {
00285 int i;
00286 DdApaDigit remainder;
00287 DdApaDoubleDigit partial;
00288
00289 remainder = 0;
00290 for (i = 0; i < digits; i++) {
00291 partial = remainder * DD_APA_BASE + dividend[i];
00292 quotient[i] = (DdApaDigit) (partial/(DdApaDoubleDigit)divisor);
00293 remainder = (DdApaDigit) (partial % divisor);
00294 }
00295
00296 return(remainder);
00297
00298 }
00299
00300
00319 unsigned int
00320 Cudd_ApaIntDivision(
00321 int digits,
00322 DdApaNumber dividend,
00323 unsigned int divisor,
00324 DdApaNumber quotient)
00325 {
00326 int i;
00327 double partial;
00328 unsigned int remainder = 0;
00329 double ddiv = (double) divisor;
00330
00331 for (i = 0; i < digits; i++) {
00332 partial = (double) remainder * DD_APA_BASE + dividend[i];
00333 quotient[i] = (DdApaDigit) (partial / ddiv);
00334 remainder = (unsigned int) (partial - ((double)quotient[i] * ddiv));
00335 }
00336
00337 return(remainder);
00338
00339 }
00340
00341
00356 void
00357 Cudd_ApaShiftRight(
00358 int digits,
00359 DdApaDigit in,
00360 DdApaNumber a,
00361 DdApaNumber b)
00362 {
00363 int i;
00364
00365 for (i = digits - 1; i > 0; i--) {
00366 b[i] = (a[i] >> 1) | ((a[i-1] & 1) << (DD_APA_BITS - 1));
00367 }
00368 b[0] = (a[0] >> 1) | (in << (DD_APA_BITS - 1));
00369
00370 }
00371
00372
00384 void
00385 Cudd_ApaSetToLiteral(
00386 int digits,
00387 DdApaNumber number,
00388 DdApaDigit literal)
00389 {
00390 int i;
00391
00392 for (i = 0; i < digits - 1; i++)
00393 number[i] = 0;
00394 number[digits - 1] = literal;
00395
00396 }
00397
00398
00412 void
00413 Cudd_ApaPowerOfTwo(
00414 int digits,
00415 DdApaNumber number,
00416 int power)
00417 {
00418 int i;
00419 int index;
00420
00421 for (i = 0; i < digits; i++)
00422 number[i] = 0;
00423 i = digits - 1 - power / DD_APA_BITS;
00424 if (i < 0) return;
00425 index = power & (DD_APA_BITS - 1);
00426 number[i] = 1 << index;
00427
00428 }
00429
00430
00444 int
00445 Cudd_ApaCompare(
00446 int digitsFirst,
00447 DdApaNumber first,
00448 int digitsSecond,
00449 DdApaNumber second)
00450 {
00451 int i;
00452 int firstNZ, secondNZ;
00453
00454
00455 for (firstNZ = 0; firstNZ < digitsFirst; firstNZ++)
00456 if (first[firstNZ] != 0) break;
00457 for (secondNZ = 0; secondNZ < digitsSecond; secondNZ++)
00458 if (second[secondNZ] != 0) break;
00459 if (digitsFirst - firstNZ > digitsSecond - secondNZ) return(1);
00460 else if (digitsFirst - firstNZ < digitsSecond - secondNZ) return(-1);
00461 for (i = 0; i < digitsFirst - firstNZ; i++) {
00462 if (first[firstNZ + i] > second[secondNZ + i]) return(1);
00463 else if (first[firstNZ + i] < second[secondNZ + i]) return(-1);
00464 }
00465 return(0);
00466
00467 }
00468
00469
00484 int
00485 Cudd_ApaCompareRatios(
00486 int digitsFirst,
00487 DdApaNumber firstNum,
00488 unsigned int firstDen,
00489 int digitsSecond,
00490 DdApaNumber secondNum,
00491 unsigned int secondDen)
00492 {
00493 int result;
00494 DdApaNumber first, second;
00495 unsigned int firstRem, secondRem;
00496
00497 first = Cudd_NewApaNumber(digitsFirst);
00498 firstRem = Cudd_ApaIntDivision(digitsFirst,firstNum,firstDen,first);
00499 second = Cudd_NewApaNumber(digitsSecond);
00500 secondRem = Cudd_ApaIntDivision(digitsSecond,secondNum,secondDen,second);
00501 result = Cudd_ApaCompare(digitsFirst,first,digitsSecond,second);
00502 FREE(first);
00503 FREE(second);
00504 if (result == 0) {
00505 if ((double)firstRem/firstDen > (double)secondRem/secondDen)
00506 return(1);
00507 else if ((double)firstRem/firstDen < (double)secondRem/secondDen)
00508 return(-1);
00509 }
00510 return(result);
00511
00512 }
00513
00514
00527 int
00528 Cudd_ApaPrintHex(
00529 FILE * fp,
00530 int digits,
00531 DdApaNumber number)
00532 {
00533 int i, result;
00534
00535 for (i = 0; i < digits; i++) {
00536 result = fprintf(fp,DD_APA_HEXPRINT,number[i]);
00537 if (result == EOF)
00538 return(0);
00539 }
00540 return(1);
00541
00542 }
00543
00544
00557 int
00558 Cudd_ApaPrintDecimal(
00559 FILE * fp,
00560 int digits,
00561 DdApaNumber number)
00562 {
00563 int i, result;
00564 DdApaDigit remainder;
00565 DdApaNumber work;
00566 unsigned char *decimal;
00567 int leadingzero;
00568 int decimalDigits = (int) (digits * log10((double) DD_APA_BASE)) + 1;
00569
00570 work = Cudd_NewApaNumber(digits);
00571 if (work == NULL)
00572 return(0);
00573 decimal = ALLOC(unsigned char, decimalDigits);
00574 if (decimal == NULL) {
00575 FREE(work);
00576 return(0);
00577 }
00578 Cudd_ApaCopy(digits,number,work);
00579 for (i = decimalDigits - 1; i >= 0; i--) {
00580 remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
00581 decimal[i] = (unsigned char) remainder;
00582 }
00583 FREE(work);
00584
00585 leadingzero = 1;
00586 for (i = 0; i < decimalDigits; i++) {
00587 leadingzero = leadingzero && (decimal[i] == 0);
00588 if ((!leadingzero) || (i == (decimalDigits - 1))) {
00589 result = fprintf(fp,"%1d",decimal[i]);
00590 if (result == EOF) {
00591 FREE(decimal);
00592 return(0);
00593 }
00594 }
00595 }
00596 FREE(decimal);
00597 return(1);
00598
00599 }
00600
00601
00614 int
00615 Cudd_ApaPrintExponential(
00616 FILE * fp,
00617 int digits,
00618 DdApaNumber number,
00619 int precision)
00620 {
00621 int i, first, last, result;
00622 DdApaDigit remainder;
00623 DdApaNumber work;
00624 unsigned char *decimal;
00625 int decimalDigits = (int) (digits * log10((double) DD_APA_BASE)) + 1;
00626
00627 work = Cudd_NewApaNumber(digits);
00628 if (work == NULL)
00629 return(0);
00630 decimal = ALLOC(unsigned char, decimalDigits);
00631 if (decimal == NULL) {
00632 FREE(work);
00633 return(0);
00634 }
00635 Cudd_ApaCopy(digits,number,work);
00636 first = decimalDigits - 1;
00637 for (i = decimalDigits - 1; i >= 0; i--) {
00638 remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
00639 decimal[i] = (unsigned char) remainder;
00640 if (remainder != 0) first = i;
00641 }
00642 FREE(work);
00643 last = ddMin(first + precision, decimalDigits);
00644
00645 for (i = first; i < last; i++) {
00646 result = fprintf(fp,"%s%1d",i == first+1 ? "." : "", decimal[i]);
00647 if (result == EOF) {
00648 FREE(decimal);
00649 return(0);
00650 }
00651 }
00652 FREE(decimal);
00653 result = fprintf(fp,"e+%d",decimalDigits - first - 1);
00654 if (result == EOF) {
00655 return(0);
00656 }
00657 return(1);
00658
00659 }
00660
00661
00679 DdApaNumber
00680 Cudd_ApaCountMinterm(
00681 DdManager * manager,
00682 DdNode * node,
00683 int nvars,
00684 int * digits)
00685 {
00686 DdApaNumber max, min;
00687 st_table *table;
00688 DdApaNumber i,count;
00689
00690 background = manager->background;
00691 zero = Cudd_Not(manager->one);
00692
00693 *digits = Cudd_ApaNumberOfDigits(nvars+1);
00694 max = Cudd_NewApaNumber(*digits);
00695 if (max == NULL) {
00696 return(NULL);
00697 }
00698 Cudd_ApaPowerOfTwo(*digits,max,nvars);
00699 min = Cudd_NewApaNumber(*digits);
00700 if (min == NULL) {
00701 FREE(max);
00702 return(NULL);
00703 }
00704 Cudd_ApaSetToLiteral(*digits,min,0);
00705 table = st_init_table(st_ptrcmp,st_ptrhash);
00706 if (table == NULL) {
00707 FREE(max);
00708 FREE(min);
00709 return(NULL);
00710 }
00711 i = cuddApaCountMintermAux(Cudd_Regular(node),*digits,max,min,table);
00712 if (i == NULL) {
00713 FREE(max);
00714 FREE(min);
00715 st_foreach(table, cuddApaStCountfree, NULL);
00716 st_free_table(table);
00717 return(NULL);
00718 }
00719 count = Cudd_NewApaNumber(*digits);
00720 if (count == NULL) {
00721 FREE(max);
00722 FREE(min);
00723 st_foreach(table, cuddApaStCountfree, NULL);
00724 st_free_table(table);
00725 if (Cudd_Regular(node)->ref == 1) FREE(i);
00726 return(NULL);
00727 }
00728 if (Cudd_IsComplement(node)) {
00729 (void) Cudd_ApaSubtract(*digits,max,i,count);
00730 } else {
00731 Cudd_ApaCopy(*digits,i,count);
00732 }
00733 FREE(max);
00734 FREE(min);
00735 st_foreach(table, cuddApaStCountfree, NULL);
00736 st_free_table(table);
00737 if (Cudd_Regular(node)->ref == 1) FREE(i);
00738 return(count);
00739
00740 }
00741
00742
00756 int
00757 Cudd_ApaPrintMinterm(
00758 FILE * fp,
00759 DdManager * dd,
00760 DdNode * node,
00761 int nvars)
00762 {
00763 int digits;
00764 int result;
00765 DdApaNumber count;
00766
00767 count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
00768 if (count == NULL)
00769 return(0);
00770 result = Cudd_ApaPrintDecimal(fp,digits,count);
00771 FREE(count);
00772 if (fprintf(fp,"\n") == EOF) {
00773 return(0);
00774 }
00775 return(result);
00776
00777 }
00778
00779
00795 int
00796 Cudd_ApaPrintMintermExp(
00797 FILE * fp,
00798 DdManager * dd,
00799 DdNode * node,
00800 int nvars,
00801 int precision)
00802 {
00803 int digits;
00804 int result;
00805 DdApaNumber count;
00806
00807 count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
00808 if (count == NULL)
00809 return(0);
00810 result = Cudd_ApaPrintExponential(fp,digits,count,precision);
00811 FREE(count);
00812 if (fprintf(fp,"\n") == EOF) {
00813 return(0);
00814 }
00815 return(result);
00816
00817 }
00818
00819
00833 int
00834 Cudd_ApaPrintDensity(
00835 FILE * fp,
00836 DdManager * dd,
00837 DdNode * node,
00838 int nvars)
00839 {
00840 int digits;
00841 int result;
00842 DdApaNumber count,density;
00843 unsigned int size, remainder, fractional;
00844
00845 count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
00846 if (count == NULL)
00847 return(0);
00848 size = Cudd_DagSize(node);
00849 density = Cudd_NewApaNumber(digits);
00850 remainder = Cudd_ApaIntDivision(digits,count,size,density);
00851 result = Cudd_ApaPrintDecimal(fp,digits,density);
00852 FREE(count);
00853 FREE(density);
00854 fractional = (unsigned int)((double)remainder / size * 1000000);
00855 if (fprintf(fp,".%u\n", fractional) == EOF) {
00856 return(0);
00857 }
00858 return(result);
00859
00860 }
00861
00862
00863
00864
00865
00866
00867
00868
00869
00870
00871
00872
00894 static DdApaNumber
00895 cuddApaCountMintermAux(
00896 DdNode * node,
00897 int digits,
00898 DdApaNumber max,
00899 DdApaNumber min,
00900 st_table * table)
00901 {
00902 DdNode *Nt, *Ne;
00903 DdApaNumber mint, mint1, mint2;
00904 DdApaDigit carryout;
00905
00906 if (cuddIsConstant(node)) {
00907 if (node == background || node == zero) {
00908 return(min);
00909 } else {
00910 return(max);
00911 }
00912 }
00913 if (node->ref > 1 && st_lookup(table, node, &mint)) {
00914 return(mint);
00915 }
00916
00917 Nt = cuddT(node); Ne = cuddE(node);
00918
00919 mint1 = cuddApaCountMintermAux(Nt, digits, max, min, table);
00920 if (mint1 == NULL) return(NULL);
00921 mint2 = cuddApaCountMintermAux(Cudd_Regular(Ne), digits, max, min, table);
00922 if (mint2 == NULL) {
00923 if (Nt->ref == 1) FREE(mint1);
00924 return(NULL);
00925 }
00926 mint = Cudd_NewApaNumber(digits);
00927 if (mint == NULL) {
00928 if (Nt->ref == 1) FREE(mint1);
00929 if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
00930 return(NULL);
00931 }
00932 if (Cudd_IsComplement(Ne)) {
00933 (void) Cudd_ApaSubtract(digits,max,mint2,mint);
00934 carryout = Cudd_ApaAdd(digits,mint1,mint,mint);
00935 } else {
00936 carryout = Cudd_ApaAdd(digits,mint1,mint2,mint);
00937 }
00938 Cudd_ApaShiftRight(digits,carryout,mint,mint);
00939
00940
00941
00942 if (Nt->ref == 1) FREE(mint1);
00943 if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
00944
00945 if (node->ref > 1) {
00946 if (st_insert(table, (char *)node, (char *)mint) == ST_OUT_OF_MEM) {
00947 FREE(mint);
00948 return(NULL);
00949 }
00950 }
00951 return(mint);
00952
00953 }
00954
00955
00967 static enum st_retval
00968 cuddApaStCountfree(
00969 char * key,
00970 char * value,
00971 char * arg)
00972 {
00973 DdApaNumber d;
00974
00975 d = (DdApaNumber) value;
00976 FREE(d);
00977 return(ST_CONTINUE);
00978
00979 }
