00001
00031 #include "util_hack.h"
00032 #include "cuddInt.h"
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050 #ifndef lint
00051 static char rcsid[] DD_UNUSED = "$Id: cuddApa.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
00052 #endif
00053
00054 static DdNode *background, *zero;
00055
00056
00057
00058
00059
00060
00063
00064
00065
00066
00067 static DdApaNumber cuddApaCountMintermAux ARGS((DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st_table * table));
00068 static enum st_retval cuddApaStCountfree ARGS((char * key, char * value, char * arg));
00069
00073
00074
00075
00076
00077
00093 int
00094 Cudd_ApaNumberOfDigits(
00095 int binaryDigits)
00096 {
00097 int digits;
00098
00099 digits = binaryDigits / DD_APA_BITS;
00100 if ((digits * DD_APA_BITS) != binaryDigits)
00101 digits++;
00102 return(digits);
00103
00104 }
00105
00106
00120 DdApaNumber
00121 Cudd_NewApaNumber(
00122 int digits)
00123 {
00124 return(ALLOC(DdApaDigit, digits));
00125
00126 }
00127
00128
00140 void
00141 Cudd_ApaCopy(
00142 int digits,
00143 DdApaNumber source,
00144 DdApaNumber dest)
00145 {
00146 int i;
00147
00148 for (i = 0; i < digits; i++) {
00149 dest[i] = source[i];
00150 }
00151
00152 }
00153
00154
00167 DdApaDigit
00168 Cudd_ApaAdd(
00169 int digits,
00170 DdApaNumber a,
00171 DdApaNumber b,
00172 DdApaNumber sum)
00173 {
00174 int i;
00175 DdApaDoubleDigit partial = 0;
00176
00177 for (i = digits - 1; i >= 0; i--) {
00178 partial = a[i] + b[i] + DD_MSDIGIT(partial);
00179 sum[i] = (DdApaDigit) DD_LSDIGIT(partial);
00180 }
00181 return(DD_MSDIGIT(partial));
00182
00183 }
00184
00185
00199 DdApaDigit
00200 Cudd_ApaSubtract(
00201 int digits,
00202 DdApaNumber a,
00203 DdApaNumber b,
00204 DdApaNumber diff)
00205 {
00206 int i;
00207 DdApaDoubleDigit partial = DD_APA_BASE;
00208
00209 for (i = digits - 1; i >= 0; i--) {
00210 partial = a[i] - b[i] + DD_MSDIGIT(partial) + DD_APA_MASK;
00211 diff[i] = (DdApaDigit) DD_LSDIGIT(partial);
00212 }
00213 return(DD_MSDIGIT(partial) - 1);
00214
00215 }
00216
00217
00229 DdApaDigit
00230 Cudd_ApaShortDivision(
00231 int digits,
00232 DdApaNumber dividend,
00233 DdApaDigit divisor,
00234 DdApaNumber quotient)
00235 {
00236 int i;
00237 DdApaDigit remainder;
00238 DdApaDoubleDigit partial;
00239
00240 remainder = 0;
00241 for (i = 0; i < digits; i++) {
00242 partial = remainder * DD_APA_BASE + dividend[i];
00243 quotient[i] = (DdApaDigit) (partial/(DdApaDoubleDigit)divisor);
00244 remainder = (DdApaDigit) (partial % divisor);
00245 }
00246
00247 return(remainder);
00248
00249 }
00250
00251
00270 unsigned int
00271 Cudd_ApaIntDivision(
00272 int digits,
00273 DdApaNumber dividend,
00274 unsigned int divisor,
00275 DdApaNumber quotient)
00276 {
00277 int i;
00278 double partial;
00279 unsigned int remainder = 0;
00280 double ddiv = (double) divisor;
00281
00282 for (i = 0; i < digits; i++) {
00283 partial = (double) remainder * DD_APA_BASE + dividend[i];
00284 quotient[i] = (DdApaDigit) (partial / ddiv);
00285 remainder = (unsigned int) (partial - ((double)quotient[i] * ddiv));
00286 }
00287
00288 return(remainder);
00289
00290 }
00291
00292
00307 void
00308 Cudd_ApaShiftRight(
00309 int digits,
00310 DdApaDigit in,
00311 DdApaNumber a,
00312 DdApaNumber b)
00313 {
00314 int i;
00315
00316 for (i = digits - 1; i > 0; i--) {
00317 b[i] = (a[i] >> 1) | ((a[i-1] & 1) << (DD_APA_BITS - 1));
00318 }
00319 b[0] = (a[0] >> 1) | (in << (DD_APA_BITS - 1));
00320
00321 }
00322
00323
00335 void
00336 Cudd_ApaSetToLiteral(
00337 int digits,
00338 DdApaNumber number,
00339 DdApaDigit literal)
00340 {
00341 int i;
00342
00343 for (i = 0; i < digits - 1; i++)
00344 number[i] = 0;
00345 number[digits - 1] = literal;
00346
00347 }
00348
00349
00363 void
00364 Cudd_ApaPowerOfTwo(
00365 int digits,
00366 DdApaNumber number,
00367 int power)
00368 {
00369 int i;
00370 int index;
00371
00372 for (i = 0; i < digits; i++)
00373 number[i] = 0;
00374 i = digits - 1 - power / DD_APA_BITS;
00375 if (i < 0) return;
00376 index = power & (DD_APA_BITS - 1);
00377 number[i] = 1 << index;
00378
00379 }
00380
00381
00395 int
00396 Cudd_ApaCompare(
00397 int digitsFirst,
00398 DdApaNumber first,
00399 int digitsSecond,
00400 DdApaNumber second)
00401 {
00402 int i;
00403 int firstNZ, secondNZ;
00404
00405
00406 for (firstNZ = 0; firstNZ < digitsFirst; firstNZ++)
00407 if (first[firstNZ] != 0) break;
00408 for (secondNZ = 0; secondNZ < digitsSecond; secondNZ++)
00409 if (second[secondNZ] != 0) break;
00410 if (digitsFirst - firstNZ > digitsSecond - secondNZ) return(1);
00411 else if (digitsFirst - firstNZ < digitsSecond - secondNZ) return(-1);
00412 for (i = 0; i < digitsFirst - firstNZ; i++) {
00413 if (first[firstNZ + i] > second[secondNZ + i]) return(1);
00414 else if (first[firstNZ + i] < second[secondNZ + i]) return(-1);
00415 }
00416 return(0);
00417
00418 }
00419
00420
00435 int
00436 Cudd_ApaCompareRatios(
00437 int digitsFirst,
00438 DdApaNumber firstNum,
00439 unsigned int firstDen,
00440 int digitsSecond,
00441 DdApaNumber secondNum,
00442 unsigned int secondDen)
00443 {
00444 int result;
00445 DdApaNumber first, second;
00446 unsigned int firstRem, secondRem;
00447
00448 first = Cudd_NewApaNumber(digitsFirst);
00449 firstRem = Cudd_ApaIntDivision(digitsFirst,firstNum,firstDen,first);
00450 second = Cudd_NewApaNumber(digitsSecond);
00451 secondRem = Cudd_ApaIntDivision(digitsSecond,secondNum,secondDen,second);
00452 result = Cudd_ApaCompare(digitsFirst,first,digitsSecond,second);
00453 if (result == 0) {
00454 if ((double)firstRem/firstDen > (double)secondRem/secondDen)
00455 return(1);
00456 else if ((double)firstRem/firstDen < (double)secondRem/secondDen)
00457 return(-1);
00458 }
00459 return(result);
00460
00461 }
00462
00463
00476 int
00477 Cudd_ApaPrintHex(
00478 FILE * fp,
00479 int digits,
00480 DdApaNumber number)
00481 {
00482 int i, result;
00483
00484 for (i = 0; i < digits; i++) {
00485 result = fprintf(fp,DD_APA_HEXPRINT,number[i]);
00486 if (result == EOF)
00487 return(0);
00488 }
00489 return(1);
00490
00491 }
00492
00493
00506 int
00507 Cudd_ApaPrintDecimal(
00508 FILE * fp,
00509 int digits,
00510 DdApaNumber number)
00511 {
00512 int i, result;
00513 DdApaDigit remainder;
00514 DdApaNumber work;
00515 unsigned char *decimal;
00516 int leadingzero;
00517 int decimalDigits = (int) (digits * log10((double) DD_APA_BASE)) + 1;
00518
00519 work = Cudd_NewApaNumber(digits);
00520 if (work == NULL)
00521 return(0);
00522 decimal = ALLOC(unsigned char, decimalDigits);
00523 if (decimal == NULL) {
00524 FREE(work);
00525 return(0);
00526 }
00527 Cudd_ApaCopy(digits,number,work);
00528 for (i = decimalDigits - 1; i >= 0; i--) {
00529 remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
00530 decimal[i] = remainder;
00531 }
00532 FREE(work);
00533
00534 leadingzero = 1;
00535 for (i = 0; i < decimalDigits; i++) {
00536 leadingzero = leadingzero && (decimal[i] == 0);
00537 if ((!leadingzero) || (i == (decimalDigits - 1))) {
00538 result = fprintf(fp,"%1d",decimal[i]);
00539 if (result == EOF) {
00540 FREE(decimal);
00541 return(0);
00542 }
00543 }
00544 }
00545 FREE(decimal);
00546 return(1);
00547
00548 }
00549
00550
00563 int
00564 Cudd_ApaPrintExponential(
00565 FILE * fp,
00566 int digits,
00567 DdApaNumber number,
00568 int precision)
00569 {
00570 int i, first, last, result;
00571 DdApaDigit remainder;
00572 DdApaNumber work;
00573 unsigned char *decimal;
00574 int decimalDigits = (int) (digits * log10((double) DD_APA_BASE)) + 1;
00575
00576 work = Cudd_NewApaNumber(digits);
00577 if (work == NULL)
00578 return(0);
00579 decimal = ALLOC(unsigned char, decimalDigits);
00580 if (decimal == NULL) {
00581 FREE(work);
00582 return(0);
00583 }
00584 Cudd_ApaCopy(digits,number,work);
00585 first = decimalDigits - 1;
00586 for (i = decimalDigits - 1; i >= 0; i--) {
00587 remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
00588 decimal[i] = remainder;
00589 if (remainder != 0) first = i;
00590 }
00591 FREE(work);
00592 last = ddMin(first + precision, decimalDigits);
00593
00594 for (i = first; i < last; i++) {
00595 result = fprintf(fp,"%s%1d",i == first+1 ? "." : "", decimal[i]);
00596 if (result == EOF) {
00597 FREE(decimal);
00598 return(0);
00599 }
00600 }
00601 FREE(decimal);
00602 result = fprintf(fp,"e+%d",decimalDigits - first - 1);
00603 if (result == EOF) {
00604 return(0);
00605 }
00606 return(1);
00607
00608 }
00609
00610
00628 DdApaNumber
00629 Cudd_ApaCountMinterm(
00630 DdManager * manager,
00631 DdNode * node,
00632 int nvars,
00633 int * digits)
00634 {
00635 DdApaNumber max, min;
00636 st_table *table;
00637 DdApaNumber i,count;
00638
00639 background = manager->background;
00640 zero = Cudd_Not(manager->one);
00641
00642 *digits = Cudd_ApaNumberOfDigits(nvars+1);
00643 max = Cudd_NewApaNumber(*digits);
00644 if (max == NULL) {
00645 return(NULL);
00646 }
00647 Cudd_ApaPowerOfTwo(*digits,max,nvars);
00648 min = Cudd_NewApaNumber(*digits);
00649 if (min == NULL) {
00650 FREE(max);
00651 return(NULL);
00652 }
00653 Cudd_ApaSetToLiteral(*digits,min,0);
00654 table = st_init_table(st_ptrcmp,st_ptrhash);
00655 if (table == NULL) {
00656 FREE(max);
00657 FREE(min);
00658 return(NULL);
00659 }
00660 i = cuddApaCountMintermAux(Cudd_Regular(node),*digits,max,min,table);
00661 if (i == NULL) {
00662 FREE(max);
00663 FREE(min);
00664 st_foreach(table, cuddApaStCountfree, NULL);
00665 st_free_table(table);
00666 return(NULL);
00667 }
00668 count = Cudd_NewApaNumber(*digits);
00669 if (count == NULL) {
00670 FREE(max);
00671 FREE(min);
00672 st_foreach(table, cuddApaStCountfree, NULL);
00673 st_free_table(table);
00674 if (Cudd_Regular(node)->ref == 1) FREE(i);
00675 return(NULL);
00676 }
00677 if (Cudd_IsComplement(node)) {
00678 (void) Cudd_ApaSubtract(*digits,max,i,count);
00679 } else {
00680 Cudd_ApaCopy(*digits,i,count);
00681 }
00682 FREE(max);
00683 FREE(min);
00684 st_foreach(table, cuddApaStCountfree, NULL);
00685 st_free_table(table);
00686 if (Cudd_Regular(node)->ref == 1) FREE(i);
00687 return(count);
00688
00689 }
00690
00691
00705 int
00706 Cudd_ApaPrintMinterm(
00707 FILE * fp,
00708 DdManager * dd,
00709 DdNode * node,
00710 int nvars)
00711 {
00712 int digits;
00713 int result;
00714 DdApaNumber count;
00715
00716 count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
00717 if (count == NULL)
00718 return(0);
00719 result = Cudd_ApaPrintDecimal(fp,digits,count);
00720 FREE(count);
00721 if (fprintf(fp,"\n") == EOF) {
00722 return(0);
00723 }
00724 return(result);
00725
00726 }
00727
00728
00744 int
00745 Cudd_ApaPrintMintermExp(
00746 FILE * fp,
00747 DdManager * dd,
00748 DdNode * node,
00749 int nvars,
00750 int precision)
00751 {
00752 int digits;
00753 int result;
00754 DdApaNumber count;
00755
00756 count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
00757 if (count == NULL)
00758 return(0);
00759 result = Cudd_ApaPrintExponential(fp,digits,count,precision);
00760 FREE(count);
00761 if (fprintf(fp,"\n") == EOF) {
00762 return(0);
00763 }
00764 return(result);
00765
00766 }
00767
00768
00782 int
00783 Cudd_ApaPrintDensity(
00784 FILE * fp,
00785 DdManager * dd,
00786 DdNode * node,
00787 int nvars)
00788 {
00789 int digits;
00790 int result;
00791 DdApaNumber count,density;
00792 unsigned int size, remainder, fractional;
00793
00794 count = Cudd_ApaCountMinterm(dd,node,nvars,&digits);
00795 if (count == NULL)
00796 return(0);
00797 size = Cudd_DagSize(node);
00798 density = Cudd_NewApaNumber(digits);
00799 remainder = Cudd_ApaIntDivision(digits,count,size,density);
00800 result = Cudd_ApaPrintDecimal(fp,digits,density);
00801 FREE(count);
00802 FREE(density);
00803 fractional = (unsigned int)((double)remainder / size * 1000000);
00804 if (fprintf(fp,".%u\n", fractional) == EOF) {
00805 return(0);
00806 }
00807 return(result);
00808
00809 }
00810
00811
00812
00813
00814
00815
00816
00817
00818
00819
00820
00821
00843 static DdApaNumber
00844 cuddApaCountMintermAux(
00845 DdNode * node,
00846 int digits,
00847 DdApaNumber max,
00848 DdApaNumber min,
00849 st_table * table)
00850 {
00851 DdNode *Nt, *Ne;
00852 DdApaNumber mint, mint1, mint2;
00853 DdApaDigit carryout;
00854
00855 if (cuddIsConstant(node)) {
00856 if (node == background || node == zero) {
00857 return(min);
00858 } else {
00859 return(max);
00860 }
00861 }
00862 if (node->ref > 1 && st_lookup(table, (char *)node, (char **)&mint)) {
00863 return(mint);
00864 }
00865
00866 Nt = cuddT(node); Ne = cuddE(node);
00867
00868 mint1 = cuddApaCountMintermAux(Nt, digits, max, min, table);
00869 if (mint1 == NULL) return(NULL);
00870 mint2 = cuddApaCountMintermAux(Cudd_Regular(Ne), digits, max, min, table);
00871 if (mint2 == NULL) {
00872 if (Nt->ref == 1) FREE(mint1);
00873 return(NULL);
00874 }
00875 mint = Cudd_NewApaNumber(digits);
00876 if (mint == NULL) {
00877 if (Nt->ref == 1) FREE(mint1);
00878 if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
00879 return(NULL);
00880 }
00881 if (Cudd_IsComplement(Ne)) {
00882 (void) Cudd_ApaSubtract(digits,max,mint2,mint);
00883 carryout = Cudd_ApaAdd(digits,mint1,mint,mint);
00884 } else {
00885 carryout = Cudd_ApaAdd(digits,mint1,mint2,mint);
00886 }
00887 Cudd_ApaShiftRight(digits,carryout,mint,mint);
00888
00889
00890
00891 if (Nt->ref == 1) FREE(mint1);
00892 if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
00893
00894 if (node->ref > 1) {
00895 if (st_insert(table, (char *)node, (char *)mint) == ST_OUT_OF_MEM) {
00896 FREE(mint);
00897 return(NULL);
00898 }
00899 }
00900 return(mint);
00901
00902 }
00903
00904
00916 static enum st_retval
00917 cuddApaStCountfree(
00918 char * key,
00919 char * value,
00920 char * arg)
00921 {
00922 DdApaNumber d;
00923
00924 d = (DdApaNumber) value;
00925 FREE(d);
00926 return(ST_CONTINUE);
00927
00928 }
00929
00930
