00001
00002
00003
00004 #include <stdio.h>
00005 #if HAVE_STDARG_H
00006 # include <stdarg.h>
00007 #else
00008 # if HAVE_VARARGS_H
00009 # include <varargs.h>
00010 # else
00011 # error "Need to have HAVE_STDARG_H or HAVE_VARARGS_H defined for variable arguments"
00012 # endif
00013 #endif
00014 #if STDC_HEADERS
00015 # include <stdlib.h>
00016 #endif
00017
00018 #include "bddint.h"
00019
00020
00021 #define VARS 500
00022
00023
00024 #define TT_BITS 32
00025 #define TT_VARS 5
00026
00027
00028
00029
00030 #define ITERATIONS 200
00031
00032
00033 #if defined(__STDC__)
00034 #if STDC_HEADERS
00035 #include <stdlib.h>
00036 #else
00037 extern void srandom(unsigned int);
00038 extern long random(void);
00039 #endif
00040 #if HAVE_UNISTD_H
00041 #include <unistd.h>
00042 #else
00043 extern int unlink(char *);
00044 #endif
00045 #else
00046 extern void srandom();
00047 extern long random();
00048 extern int unlink();
00049 #endif
00050
00051
00052 typedef unsigned long tt;
00053
00054
00055 static cmu_bdd_manager bddm;
00056
00057
00058 static bdd vars[VARS];
00059 static bdd aux_vars[VARS];
00060
00061
00062 static tt cofactor_masks[]=
00063 {
00064 0xffff0000,
00065 0xff00ff00,
00066 0xf0f0f0f0,
00067 0xcccccccc,
00068 0xaaaaaaaa,
00069 };
00070
00071
00072 static
00073 bdd
00074 #if defined(__STDC__)
00075 decode(int var, tt table)
00076 #else
00077 decode(var, table)
00078 int var;
00079 tt table;
00080 #endif
00081 {
00082 bdd temp1, temp2;
00083 bdd result;
00084
00085 if (var == TT_VARS)
00086 return ((table & 1) ? cmu_bdd_one(bddm) : cmu_bdd_zero(bddm));
00087 temp1=decode(var+1, table >> (1 << (TT_VARS-var-1)));
00088 temp2=decode(var+1, table);
00089 result=cmu_bdd_ite(bddm, vars[var], temp1, temp2);
00090 cmu_bdd_free(bddm, temp1);
00091 cmu_bdd_free(bddm, temp2);
00092 return (result);
00093 }
00094
00095
00096 #define encoding_to_bdd(table) (decode(0, (table)))
00097
00098
00099 static union hack_u {
00100 INT_PTR as_double_space[2];
00101 double double_value;
00102 } hack;
00103
00104 static
00105 double
00106 #if defined(__STDC__)
00107 as_double(INT_PTR v1, INT_PTR v2)
00108 #else
00109 as_double(v1, v2)
00110 INT_PTR v1;
00111 INT_PTR v2;
00112 #endif
00113 {
00114 hack.as_double_space[0]=v1;
00115 hack.as_double_space[1]=v2;
00116 return (hack.double_value);
00117 }
00118
00119
00120 static
00121 void
00122 #if defined(__STDC__)
00123 as_INT_PTRs(double n, INT_PTR *r1, INT_PTR *r2)
00124 #else
00125 as_INT_PTRs(n, r1, r2)
00126 double n;
00127 INT_PTR *r1;
00128 INT_PTR *r2;
00129 #endif
00130 {
00131 hack.double_value=n;
00132 *r1=hack.as_double_space[0];
00133 *r2=hack.as_double_space[1];
00134 }
00135
00136
00137 static
00138 char *
00139 #if defined(__STDC__)
00140 terminal_id_fn(cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, pointer junk)
00141 #else
00142 terminal_id_fn(bddm, v1, v2, junk)
00143 cmu_bdd_manager bddm;
00144 INT_PTR v1;
00145 INT_PTR v2;
00146 pointer junk;
00147 #endif
00148 {
00149 static char result[100];
00150
00151 sprintf(result, "%g", as_double(v1, v2));
00152 return (result);
00153 }
00154
00155
00156 static
00157 void
00158 #if defined(__STDC__)
00159 print_bdd(bdd f)
00160 #else
00161 print_bdd(f)
00162 bdd f;
00163 #endif
00164 {
00165 cmu_bdd_print_bdd(bddm, f, bdd_naming_fn_none, terminal_id_fn, (pointer)0, stderr);
00166 }
00167
00168
00169 #if defined(__STDC__)
00170 static
00171 void
00172 error(char *op, bdd result, bdd expected, ...)
00173 {
00174 int i;
00175 va_list ap;
00176 bdd f;
00177
00178 va_start(ap, expected);
00179 fprintf(stderr, "\nError: operation %s:\n", op);
00180 i=0;
00181 while (1)
00182 {
00183 f=va_arg(ap, bdd);
00184 if (f)
00185 {
00186 ++i;
00187 fprintf(stderr, "Argument %d:\n", i);
00188 print_bdd(f);
00189 }
00190 else
00191 break;
00192 }
00193 fprintf(stderr, "Result:\n");
00194 print_bdd(result);
00195 fprintf(stderr, "Expected result:\n");
00196 print_bdd(expected);
00197 va_end(ap);
00198 }
00199 #else
00200 static
00201 void
00202 error(va_alist)
00203 va_dcl
00204 {
00205 int i;
00206 va_list ap;
00207 char *op;
00208 bdd result;
00209 bdd expected;
00210 bdd f;
00211
00212 va_start(ap);
00213 op=va_arg(ap, char *);
00214 result=va_arg(ap, bdd);
00215 expected=va_arg(ap, bdd);
00216 fprintf(stderr, "\nError: operation %s:\n", op);
00217 i=0;
00218 while (1)
00219 {
00220 f=va_arg(ap, bdd);
00221 if (f)
00222 {
00223 ++i;
00224 fprintf(stderr, "Argument %d:\n", i);
00225 print_bdd(f);
00226 }
00227 else
00228 break;
00229 }
00230 fprintf(stderr, "Result:\n");
00231 print_bdd(result);
00232 fprintf(stderr, "Expected result:\n");
00233 print_bdd(expected);
00234 va_end(ap);
00235 }
00236 #endif
00237
00238
00239 static
00240 tt
00241 #if defined(__STDC__)
00242 cofactor(tt table, int var, int value)
00243 #else
00244 cofactor(table, var, value)
00245 tt table;
00246 int var;
00247 int value;
00248 #endif
00249 {
00250 int shift;
00251
00252 shift=1 << (TT_VARS-var-1);
00253 if (value)
00254 {
00255 table&=cofactor_masks[var];
00256 table|=table >> shift;
00257 }
00258 else
00259 {
00260 table&=~cofactor_masks[var];
00261 table|=table << shift;
00262 }
00263 return (table);
00264 }
00265
00266
00267 static
00268 void
00269 #if defined(__STDC__)
00270 test_ite(bdd f1, tt table1, bdd f2, tt table2, bdd f3, tt table3)
00271 #else
00272 test_ite(f1, table1, f2, table2, f3, table3)
00273 bdd f1;
00274 tt table1;
00275 bdd f2;
00276 tt table2;
00277 bdd f3;
00278 tt table3;
00279 #endif
00280 {
00281 bdd result;
00282 tt resulttable;
00283 bdd expected;
00284
00285 result=cmu_bdd_ite(bddm, f1, f2, f3);
00286 resulttable=(table1 & table2) | (~table1 & table3);
00287 expected=encoding_to_bdd(resulttable);
00288 if (result != expected)
00289 error("ITE", result, expected, f1, f2, f3, (bdd)0);
00290 cmu_bdd_free(bddm, result);
00291 cmu_bdd_free(bddm, expected);
00292 }
00293
00294
00295 static
00296 void
00297 #if defined(__STDC__)
00298 test_and(bdd f1, tt table1, bdd f2, tt table2)
00299 #else
00300 test_and(f1, table1, f2, table2)
00301 bdd f1;
00302 tt table1;
00303 bdd f2;
00304 tt table2;
00305 #endif
00306 {
00307 bdd result;
00308 tt resulttable;
00309 bdd expected;
00310
00311 result=cmu_bdd_and(bddm, f1, f2);
00312 resulttable=table1 & table2;
00313 expected=encoding_to_bdd(resulttable);
00314 if (result != expected)
00315 error("and", result, expected, f1, f2, (bdd)0);
00316 cmu_bdd_free(bddm, result);
00317 cmu_bdd_free(bddm, expected);
00318 }
00319
00320
00321 static
00322 void
00323 #if defined(__STDC__)
00324 test_or(bdd f1, tt table1, bdd f2, tt table2)
00325 #else
00326 test_or(f1, table1, f2, table2)
00327 bdd f1;
00328 tt table1;
00329 bdd f2;
00330 tt table2;
00331 #endif
00332 {
00333 bdd result;
00334 tt resulttable;
00335 bdd expected;
00336
00337 result=cmu_bdd_or(bddm, f1, f2);
00338 resulttable=table1 | table2;
00339 expected=encoding_to_bdd(resulttable);
00340 if (result != expected)
00341 error("or", result, expected, f1, f2, (bdd)0);
00342 cmu_bdd_free(bddm, result);
00343 cmu_bdd_free(bddm, expected);
00344 }
00345
00346
00347 static
00348 void
00349 #if defined(__STDC__)
00350 test_xor(bdd f1, tt table1, bdd f2, tt table2)
00351 #else
00352 test_xor(f1, table1, f2, table2)
00353 bdd f1;
00354 tt table1;
00355 bdd f2;
00356 tt table2;
00357 #endif
00358 {
00359 bdd result;
00360 tt resulttable;
00361 bdd expected;
00362
00363 result=cmu_bdd_xor(bddm, f1, f2);
00364 resulttable=table1 ^ table2;
00365 expected=encoding_to_bdd(resulttable);
00366 if (result != expected)
00367 error("xor", result, expected, f1, f2, (bdd)0);
00368 cmu_bdd_free(bddm, result);
00369 cmu_bdd_free(bddm, expected);
00370 }
00371
00372
00373 static
00374 void
00375 #if defined(__STDC__)
00376 test_id_not(bdd f, tt table)
00377 #else
00378 test_id_not(f, table)
00379 bdd f;
00380 tt table;
00381 #endif
00382 {
00383 bdd result;
00384 tt resulttable;
00385 bdd expected;
00386
00387 result=cmu_bdd_not(bddm, f);
00388 resulttable= ~table;
00389 expected=encoding_to_bdd(resulttable);
00390 if (result != expected)
00391 error("not", result, expected, f, (bdd)0);
00392 cmu_bdd_free(bddm, result);
00393 cmu_bdd_free(bddm, expected);
00394 result=cmu_bdd_identity(bddm, f);
00395 resulttable=table;
00396 expected=encoding_to_bdd(resulttable);
00397 if (result != expected)
00398 error("identity", result, expected, f, (bdd)0);
00399 cmu_bdd_free(bddm, result);
00400 cmu_bdd_free(bddm, expected);
00401 }
00402
00403
00404 static
00405 void
00406 #if defined(__STDC__)
00407 test_compose(bdd f1, tt table1, bdd f2, tt table2)
00408 #else
00409 test_compose(f1, table1, f2, table2)
00410 bdd f1;
00411 tt table1;
00412 bdd f2;
00413 tt table2;
00414 #endif
00415 {
00416 int var;
00417 bdd result;
00418 tt resulttable;
00419 bdd expected;
00420
00421 var=((unsigned long)random())%TT_VARS;
00422 result=cmu_bdd_compose(bddm, f1, vars[var], cmu_bdd_one(bddm));
00423 resulttable=cofactor(table1, var, 1);
00424 expected=encoding_to_bdd(resulttable);
00425 if (result != expected)
00426 error("restrict1", result, expected, f1, vars[var], (bdd)0);
00427 cmu_bdd_free(bddm, result);
00428 cmu_bdd_free(bddm, expected);
00429 result=cmu_bdd_compose(bddm, f1, vars[var], cmu_bdd_zero(bddm));
00430 resulttable=cofactor(table1, var, 0);
00431 expected=encoding_to_bdd(resulttable);
00432 if (result != expected)
00433 error("restrict0", result, expected, f1, vars[var], (bdd)0);
00434 cmu_bdd_free(bddm, result);
00435 cmu_bdd_free(bddm, expected);
00436 result=cmu_bdd_compose(bddm, f1, vars[var], f2);
00437 resulttable=(table2 & cofactor(table1, var, 1)) | (~table2 & cofactor(table1, var, 0));
00438 expected=encoding_to_bdd(resulttable);
00439 if (result != expected)
00440 error("compose", result, expected, f1, vars[var], f2, (bdd)0);
00441 cmu_bdd_free(bddm, result);
00442 cmu_bdd_free(bddm, expected);
00443 }
00444
00445
00446 static
00447 void
00448 #if defined(__STDC__)
00449 test_qnt(bdd f, tt table)
00450 #else
00451 test_qnt(f, table)
00452 bdd f;
00453 tt table;
00454 #endif
00455 {
00456 int var1, var2;
00457 bdd assoc[3];
00458 bdd temp;
00459 bdd result;
00460 tt resulttable;
00461 bdd expected;
00462
00463 var1=((unsigned long)random())%TT_VARS;
00464 do
00465 var2=((unsigned long)random())%TT_VARS;
00466 while (var1 == var2);
00467 assoc[0]=vars[var1];
00468 assoc[1]=vars[var2];
00469 assoc[2]=0;
00470 cmu_bdd_temp_assoc(bddm, assoc, 0);
00471 cmu_bdd_assoc(bddm, -1);
00472 if (random()%2)
00473 result=cmu_bdd_exists(bddm, f);
00474 else
00475 {
00476 temp=cmu_bdd_not(bddm, f);
00477 result=cmu_bdd_forall(bddm, temp);
00478 cmu_bdd_free(bddm, temp);
00479 temp=result;
00480 result=cmu_bdd_not(bddm, temp);
00481 cmu_bdd_free(bddm, temp);
00482 }
00483 resulttable=cofactor(table, var1, 1) | cofactor(table, var1, 0);
00484 resulttable=cofactor(resulttable, var2, 1) | cofactor(resulttable, var2, 0);
00485 expected=encoding_to_bdd(resulttable);
00486 if (result != expected)
00487 error("quantification", result, expected, f, vars[var1], vars[var2], (bdd)0);
00488 cmu_bdd_free(bddm, result);
00489 cmu_bdd_free(bddm, expected);
00490 }
00491
00492
00493 static
00494 void
00495 #if defined(__STDC__)
00496 test_rel_prod(bdd f1, tt table1, bdd f2, tt table2)
00497 #else
00498 test_rel_prod(f1, table1, f2, table2)
00499 bdd f1;
00500 tt table1;
00501 bdd f2;
00502 tt table2;
00503 #endif
00504 {
00505 int var1, var2;
00506 bdd assoc[3];
00507 bdd result;
00508 tt resulttable;
00509 bdd expected;
00510
00511 var1=((unsigned long)random())%TT_VARS;
00512 do
00513 var2=((unsigned long)random())%TT_VARS;
00514 while (var1 == var2);
00515 assoc[0]=vars[var1];
00516 assoc[1]=vars[var2];
00517 assoc[2]=0;
00518 cmu_bdd_temp_assoc(bddm, assoc, 0);
00519 cmu_bdd_assoc(bddm, -1);
00520 result=cmu_bdd_rel_prod(bddm, f1, f2);
00521 table1&=table2;
00522 resulttable=cofactor(table1, var1, 1) | cofactor(table1, var1, 0);
00523 resulttable=cofactor(resulttable, var2, 1) | cofactor(resulttable, var2, 0);
00524 expected=encoding_to_bdd(resulttable);
00525 if (result != expected)
00526 error("relational product", result, expected, f1, f2, vars[var1], vars[var2], (bdd)0);
00527 cmu_bdd_free(bddm, result);
00528 cmu_bdd_free(bddm, expected);
00529 }
00530
00531
00532 static
00533 void
00534 #if defined(__STDC__)
00535 test_subst(bdd f1, tt table1, bdd f2, tt table2, bdd f3, tt table3)
00536 #else
00537 test_subst(f1, table1, f2, table2, f3, table3)
00538 bdd f1;
00539 tt table1;
00540 bdd f2;
00541 tt table2;
00542 bdd f3;
00543 tt table3;
00544 #endif
00545 {
00546 int var1, var2;
00547 bdd assoc[6];
00548 bdd result;
00549 tt resulttable;
00550 tt temp1, temp2, temp3, temp4;
00551 bdd expected;
00552
00553 var1=((unsigned long)random())%TT_VARS;
00554 do
00555 var2=((unsigned long)random())%TT_VARS;
00556 while (var1 == var2);
00557 assoc[0]=vars[var1];
00558 assoc[1]=f2;
00559 assoc[2]=vars[var2];
00560 assoc[3]=f3;
00561 assoc[4]=0;
00562 assoc[5]=0;
00563 cmu_bdd_temp_assoc(bddm, assoc, 1);
00564 cmu_bdd_assoc(bddm, -1);
00565 result=cmu_bdd_substitute(bddm, f1);
00566 temp1=cofactor(cofactor(table1, var1, 1), var2, 1);
00567 temp2=cofactor(cofactor(table1, var1, 1), var2, 0);
00568 temp3=cofactor(cofactor(table1, var1, 0), var2, 1);
00569 temp4=cofactor(cofactor(table1, var1, 0), var2, 0);
00570 resulttable=table2 & table3 & temp1;
00571 resulttable|=table2 & ~table3 & temp2;
00572 resulttable|=~table2 & table3 & temp3;
00573 resulttable|=~table2 & ~table3 & temp4;
00574 expected=encoding_to_bdd(resulttable);
00575 if (result != expected)
00576 error("substitute", result, expected, f1, vars[var1], f2, vars[var2], f3, (bdd)0);
00577 cmu_bdd_free(bddm, result);
00578 cmu_bdd_free(bddm, expected);
00579 }
00580
00581
00582 static
00583 void
00584 #if defined(__STDC__)
00585 test_inter_impl(bdd f1, tt table1, bdd f2, tt table2)
00586 #else
00587 test_inter_impl(f1, table1, f2, table2)
00588 bdd f1;
00589 tt table1;
00590 bdd f2;
00591 tt table2;
00592 #endif
00593 {
00594 bdd result;
00595 tt resulttable;
00596 bdd expected;
00597 bdd implies_result;
00598
00599 result=cmu_bdd_intersects(bddm, f1, f2);
00600 resulttable=table1 & table2;
00601 expected=encoding_to_bdd(resulttable);
00602 implies_result=cmu_bdd_implies(bddm, result, expected);
00603 if (implies_result != cmu_bdd_zero(bddm))
00604 {
00605 error("intersection test", result, expected, f1, f2, (bdd)0);
00606 cmu_bdd_free(bddm, implies_result);
00607 }
00608 cmu_bdd_free(bddm, result);
00609 cmu_bdd_free(bddm, expected);
00610 }
00611
00612
00613 static
00614 void
00615 #if defined(__STDC__)
00616 test_sat(bdd f, tt table)
00617 #else
00618 test_sat(f, table)
00619 bdd f;
00620 tt table;
00621 #endif
00622 {
00623 int var1, var2;
00624 bdd assoc[TT_VARS+1];
00625 bdd result;
00626 bdd temp1, temp2, temp3;
00627
00628 if (f == cmu_bdd_zero(bddm))
00629 return;
00630 result=cmu_bdd_satisfy(bddm, f);
00631 temp1=cmu_bdd_not(bddm, f);
00632 temp2=cmu_bdd_intersects(bddm, temp1, result);
00633 if (temp2 != cmu_bdd_zero(bddm))
00634 error("intersection of satisfy result with negated argument", temp2, cmu_bdd_zero(bddm), f, (bdd)0);
00635 cmu_bdd_free(bddm, temp1);
00636 cmu_bdd_free(bddm, temp2);
00637 var1=((unsigned long)random())%TT_VARS;
00638 do
00639 var2=((unsigned long)random())%TT_VARS;
00640 while (var1 == var2);
00641 assoc[0]=vars[var1];
00642 assoc[1]=vars[var2];
00643 assoc[2]=0;
00644 cmu_bdd_temp_assoc(bddm, assoc, 0);
00645 cmu_bdd_assoc(bddm, -1);
00646 temp1=cmu_bdd_satisfy_support(bddm, result);
00647 temp2=cmu_bdd_not(bddm, result);
00648 temp3=cmu_bdd_intersects(bddm, temp2, temp1);
00649 if (temp3 != cmu_bdd_zero(bddm))
00650 error("intersection of satisfy support result with negated argument", temp3, cmu_bdd_zero(bddm), result, (bdd)0);
00651 cmu_bdd_free(bddm, result);
00652 cmu_bdd_free(bddm, temp1);
00653 cmu_bdd_free(bddm, temp2);
00654 cmu_bdd_free(bddm, temp3);
00655 temp1=cmu_bdd_compose(bddm, f, vars[var1], cmu_bdd_zero(bddm));
00656 temp2=cmu_bdd_compose(bddm, f, vars[var1], cmu_bdd_one(bddm));
00657 if (cmu_bdd_satisfying_fraction(bddm, temp1)+cmu_bdd_satisfying_fraction(bddm, temp2) !=
00658 2.0*cmu_bdd_satisfying_fraction(bddm, f))
00659 {
00660 fprintf(stderr, "\nError: operation satisfying fraction:\n");
00661 fprintf(stderr, "Argument:\n");
00662 print_bdd(f);
00663 fprintf(stderr, "Cofactor on:\n");
00664 print_bdd(vars[var1]);
00665 }
00666 cmu_bdd_free(bddm, temp1);
00667 cmu_bdd_free(bddm, temp2);
00668 }
00669
00670
00671 static
00672 void
00673 #if defined(__STDC__)
00674 test_gen_cof(bdd f1, tt table1, bdd f2, tt table2)
00675 #else
00676 test_gen_cof(f1, table1, f2, table2)
00677 bdd f1;
00678 tt table1;
00679 bdd f2;
00680 tt table2;
00681 #endif
00682 {
00683 int var1, var2;
00684 bdd result;
00685 bdd temp1, temp2, temp3;
00686 tt resulttable;
00687 bdd expected;
00688
00689 result=cmu_bdd_cofactor(bddm, f1, f2);
00690 temp1=cmu_bdd_xnor(bddm, result, f1);
00691 temp2=cmu_bdd_not(bddm, f2);
00692 temp3=cmu_bdd_or(bddm, temp1, temp2);
00693 if (temp3 != cmu_bdd_one(bddm))
00694 error("d.c. comparison of generalized cofactor", temp3, cmu_bdd_one(bddm), f1, f2, (bdd)0);
00695 cmu_bdd_free(bddm, result);
00696 cmu_bdd_free(bddm, temp1);
00697 cmu_bdd_free(bddm, temp2);
00698 cmu_bdd_free(bddm, temp3);
00699 var1=((unsigned long)random())%TT_VARS;
00700 do
00701 var2=((unsigned long)random())%TT_VARS;
00702 while (var1 == var2);
00703 temp1=cmu_bdd_not(bddm, vars[var2]);
00704 temp2=cmu_bdd_and(bddm, vars[var1], temp1);
00705 cmu_bdd_free(bddm, temp1);
00706 result=cmu_bdd_cofactor(bddm, f1, temp2);
00707 resulttable=cofactor(cofactor(table1, var1, 1), var2, 0);
00708 expected=encoding_to_bdd(resulttable);
00709 if (result != expected)
00710 error("generalized cofactor", result, expected, f1, temp2, (bdd)0);
00711 cmu_bdd_free(bddm, result);
00712 cmu_bdd_free(bddm, expected);
00713 cmu_bdd_free(bddm, temp2);
00714 }
00715
00716
00717 static
00718 void
00719 #if defined(__STDC__)
00720 test_reduce(bdd f1, tt table1, bdd f2, tt table2)
00721 #else
00722 test_reduce(f1, table1, f2, table2)
00723 bdd f1;
00724 tt table1;
00725 bdd f2;
00726 tt table2;
00727 #endif
00728 {
00729 bdd result;
00730 bdd temp1, temp2, temp3;
00731
00732 result=cmu_bdd_reduce(bddm, f1, f2);
00733 temp1=cmu_bdd_xnor(bddm, result, f1);
00734 temp2=cmu_bdd_not(bddm, f2);
00735 temp3=cmu_bdd_or(bddm, temp1, temp2);
00736 if (temp3 != cmu_bdd_one(bddm))
00737 error("d.c. comparison of reduce", temp3, cmu_bdd_one(bddm), f1, f2, (bdd)0);
00738 cmu_bdd_free(bddm, result);
00739 cmu_bdd_free(bddm, temp1);
00740 cmu_bdd_free(bddm, temp2);
00741 cmu_bdd_free(bddm, temp3);
00742 }
00743
00744
00745 static
00746 bdd
00747 #if defined(__STDC__)
00748 apply_and(cmu_bdd_manager bddm, bdd *f, bdd *g, pointer env)
00749 #else
00750 apply_and(bddm, f, g, env)
00751 cmu_bdd_manager bddm;
00752 bdd *f;
00753 bdd *g;
00754 pointer env;
00755 #endif
00756 {
00757 bdd f1, g1;
00758
00759 f1= *f;
00760 g1= *g;
00761 {
00762 if (f1 == BDD_ZERO(bddm))
00763 return (f1);
00764 if (g1 == BDD_ZERO(bddm))
00765 return (g1);
00766 if (f1 == BDD_ONE(bddm))
00767 return (g1);
00768 if (g1 == BDD_ONE(bddm))
00769 return (f1);
00770 if ((INT_PTR)f1 < (INT_PTR)g1)
00771 {
00772 *f=g1;
00773 *g=f1;
00774 }
00775 return ((bdd)0);
00776 }
00777 }
00778
00779
00780 static
00781 void
00782 #if defined(__STDC__)
00783 test_apply(bdd f1, tt table1, bdd f2, tt table2)
00784 #else
00785 test_apply(f1, table1, f2, table2)
00786 bdd f1;
00787 tt table1;
00788 bdd f2;
00789 tt table2;
00790 #endif
00791 {
00792 bdd result;
00793 tt resulttable;
00794 bdd expected;
00795
00796 result=bdd_apply2(bddm, apply_and, f1, f2, (pointer)0);
00797 resulttable=table1 & table2;
00798 expected=encoding_to_bdd(resulttable);
00799 if (result != expected)
00800 error("apply2", result, expected, f1, f2, (bdd)0);
00801 cmu_bdd_free(bddm, result);
00802 cmu_bdd_free(bddm, expected);
00803 }
00804
00805
00806 static
00807 void
00808 #if defined(__STDC__)
00809 test_size(bdd f1, tt table1, bdd f2, tt table2)
00810 #else
00811 test_size(f1, table1, f2, table2)
00812 bdd f1;
00813 tt table1;
00814 bdd f2;
00815 tt table2;
00816 #endif
00817 {
00818 int i;
00819 long size;
00820 long profile[2*TT_VARS+1];
00821 bdd fs[3];
00822
00823 size=cmu_bdd_size(bddm, f1, 1);
00824 cmu_bdd_profile(bddm, f1, profile, 1);
00825 for (i=0; i < 2*TT_VARS+1; ++i)
00826 size-=profile[i];
00827 if (size)
00828 {
00829 fprintf(stderr, "\nError: size count vs. profile sum:\n");
00830 fprintf(stderr, "Argument:\n");
00831 print_bdd(f1);
00832 }
00833 size=cmu_bdd_size(bddm, f1, 0);
00834 cmu_bdd_profile(bddm, f1, profile, 0);
00835 for (i=0; i < 2*TT_VARS+1; ++i)
00836 size-=profile[i];
00837 if (size)
00838 {
00839 fprintf(stderr, "\nError: no negout size count vs. profile sum:\n");
00840 fprintf(stderr, "Argument:\n");
00841 print_bdd(f1);
00842 }
00843 fs[0]=f1;
00844 fs[1]=f2;
00845 fs[2]=0;
00846 size=cmu_bdd_size_multiple(bddm, fs, 1);
00847 cmu_bdd_profile_multiple(bddm, fs, profile, 1);
00848 for (i=0; i < 2*TT_VARS+1; ++i)
00849 size-=profile[i];
00850 if (size)
00851 {
00852 fprintf(stderr, "\nError: multiple size count vs. multiple profile sum:\n");
00853 fprintf(stderr, "Argument 1:\n");
00854 print_bdd(f1);
00855 fprintf(stderr, "Argument 2:\n");
00856 print_bdd(f2);
00857 }
00858 }
00859
00860
00861 static
00862 int
00863 #if defined(__STDC__)
00864 canonical_fn(cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, pointer env)
00865 #else
00866 canonical_fn(bddm, v1, v2, env)
00867 cmu_bdd_manager bddm;
00868 INT_PTR v1;
00869 INT_PTR v2;
00870 pointer env;
00871 #endif
00872 {
00873 return (as_double(v1, v2) > 0);
00874 }
00875
00876
00877 static
00878 void
00879 #if defined(__STDC__)
00880 transform_fn(cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, INT_PTR *r1, INT_PTR *r2, pointer env)
00881 #else
00882 transform_fn(bddm, v1, v2, r1, r2, env)
00883 cmu_bdd_manager bddm;
00884 INT_PTR v1;
00885 INT_PTR v2;
00886 INT_PTR *r1;
00887 INT_PTR *r2;
00888 pointer env;
00889 #endif
00890 {
00891 as_INT_PTRs(-as_double(v1, v2), r1, r2);
00892 }
00893
00894
00895 static
00896 bdd
00897 #if defined(__STDC__)
00898 terminal(double n)
00899 #else
00900 terminal(n)
00901 double n;
00902 #endif
00903 {
00904 INT_PTR v1, v2;
00905
00906 as_INT_PTRs(n, &v1, &v2);
00907 return (cmu_mtbdd_get_terminal(bddm, v1, v2));
00908 }
00909
00910
00911 static
00912 bdd
00913 #if defined(__STDC__)
00914 walsh_matrix(int n)
00915 #else
00916 walsh_matrix(n)
00917 int n;
00918 #endif
00919 {
00920 bdd temp1, temp2, temp3;
00921 bdd result;
00922
00923 if (n == TT_VARS)
00924 return (terminal(1.0));
00925 temp1=walsh_matrix(n+1);
00926 temp2=mtbdd_transform(bddm, temp1);
00927 temp3=temp2;
00928 temp2=mtcmu_bdd_ite(bddm, aux_vars[n], temp3, temp1);
00929 cmu_bdd_free(bddm, temp3);
00930 result=mtcmu_bdd_ite(bddm, vars[n], temp2, temp1);
00931 cmu_bdd_free(bddm, temp1);
00932 cmu_bdd_free(bddm, temp2);
00933 return (result);
00934 }
00935
00936
00937 #define OP_MULT 1000l
00938 #define OP_ADD 1100l
00939
00940
00941 static
00942 bdd
00943 #if defined(__STDC__)
00944 mtbdd_mult_step(cmu_bdd_manager bddm, bdd f, bdd g)
00945 #else
00946 mtbdd_mult_step(bddm, f, g)
00947 cmu_bdd_manager bddm;
00948 bdd f;
00949 bdd g;
00950 #endif
00951 {
00952 bdd_indexindex_type top_indexindex;
00953 bdd f1, f2;
00954 bdd g1, g2;
00955 bdd temp1, temp2;
00956 bdd result;
00957 INT_PTR u1, u2;
00958 INT_PTR v1, v2;
00959
00960 BDD_SETUP(f);
00961 BDD_SETUP(g);
00962 if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
00963 {
00964 cmu_mtbdd_terminal_value_aux(bddm, f, &u1, &u2);
00965 cmu_mtbdd_terminal_value_aux(bddm, g, &v1, &v2);
00966 as_INT_PTRs(as_double(u1, u2)*as_double(v1, v2), &u1, &u2);
00967 return (bdd_find_terminal(bddm, u1, u2));
00968 }
00969 if (BDD_OUT_OF_ORDER(f, g))
00970 BDD_SWAP(f, g);
00971 if (bdd_lookup_in_cache2(bddm, OP_MULT, f, g, &result))
00972 return (result);
00973 BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00974 BDD_COFACTOR(top_indexindex, f, f1, f2);
00975 BDD_COFACTOR(top_indexindex, g, g1, g2);
00976 temp1=mtbdd_mult_step(bddm, f1, g1);
00977 temp2=mtbdd_mult_step(bddm, f2, g2);
00978 result=bdd_find(bddm, top_indexindex, temp1, temp2);
00979 bdd_insert_in_cache2(bddm, OP_MULT, f, g, result);
00980 return (result);
00981 }
00982
00983
00984 static
00985 bdd
00986 #if defined(__STDC__)
00987 mtbdd_mult(cmu_bdd_manager bddm, bdd f, bdd g)
00988 #else
00989 mtbdd_mult(bddm, f, g)
00990 cmu_bdd_manager bddm;
00991 bdd f;
00992 bdd g;
00993 #endif
00994 {
00995 if (bdd_check_arguments(2, f, g))
00996 {
00997 FIREWALL(bddm);
00998 RETURN_BDD(mtbdd_mult_step(bddm, f, g));
00999 }
01000 return ((bdd)0);
01001 }
01002
01003
01004 static
01005 bdd
01006 #if defined(__STDC__)
01007 mtbdd_add_step(cmu_bdd_manager bddm, bdd f, bdd g)
01008 #else
01009 mtbdd_add_step(bddm, f, g)
01010 cmu_bdd_manager bddm;
01011 bdd f;
01012 bdd g;
01013 #endif
01014 {
01015 bdd_indexindex_type top_indexindex;
01016 bdd f1, f2;
01017 bdd g1, g2;
01018 bdd temp1, temp2;
01019 bdd result;
01020 INT_PTR u1, u2;
01021 INT_PTR v1, v2;
01022
01023 BDD_SETUP(f);
01024 BDD_SETUP(g);
01025 if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
01026 {
01027 cmu_mtbdd_terminal_value_aux(bddm, f, &u1, &u2);
01028 cmu_mtbdd_terminal_value_aux(bddm, g, &v1, &v2);
01029 as_INT_PTRs(as_double(u1, u2)+as_double(v1, v2), &u1, &u2);
01030 return (bdd_find_terminal(bddm, u1, u2));
01031 }
01032 if (BDD_OUT_OF_ORDER(f, g))
01033 BDD_SWAP(f, g);
01034 if (bdd_lookup_in_cache2(bddm, OP_ADD, f, g, &result))
01035 return (result);
01036 BDD_TOP_VAR2(top_indexindex, bddm, f, g);
01037 BDD_COFACTOR(top_indexindex, f, f1, f2);
01038 BDD_COFACTOR(top_indexindex, g, g1, g2);
01039 temp1=mtbdd_add_step(bddm, f1, g1);
01040 temp2=mtbdd_add_step(bddm, f2, g2);
01041 result=bdd_find(bddm, top_indexindex, temp1, temp2);
01042 bdd_insert_in_cache2(bddm, OP_ADD, f, g, result);
01043 return (result);
01044 }
01045
01046
01047 static
01048 bdd
01049 #if defined(__STDC__)
01050 mtbdd_add(cmu_bdd_manager bddm, bdd f, bdd g)
01051 #else
01052 mtbdd_add(bddm, f, g)
01053 cmu_bdd_manager bddm;
01054 bdd f;
01055 bdd g;
01056 #endif
01057 {
01058 if (bdd_check_arguments(2, f, g))
01059 {
01060 FIREWALL(bddm);
01061 RETURN_BDD(mtbdd_add_step(bddm, f, g));
01062 }
01063 return ((bdd)0);
01064 }
01065
01066
01067 static
01068 bdd
01069 #if defined(__STDC__)
01070 transform(bdd f, bdd g, bdd *elim_vars)
01071 #else
01072 transform(f, g, elim_vars)
01073 bdd f;
01074 bdd g;
01075 bdd *elim_vars;
01076 #endif
01077 {
01078 int i;
01079 bdd temp1, temp2;
01080 bdd result;
01081
01082 result=mtbdd_mult(bddm, f, g);
01083 for (i=0; i < TT_VARS; ++i)
01084 {
01085 temp1=cmu_bdd_compose(bddm, result, elim_vars[i], cmu_bdd_one(bddm));
01086 temp2=cmu_bdd_compose(bddm, result, elim_vars[i], cmu_bdd_zero(bddm));
01087 cmu_bdd_free(bddm, result);
01088 result=mtbdd_add(bddm, temp1, temp2);
01089 cmu_bdd_free(bddm, temp1);
01090 cmu_bdd_free(bddm, temp2);
01091 }
01092 return (result);
01093 }
01094
01095
01096 static
01097 void
01098 #if defined(__STDC__)
01099 test_mtbdd(bdd f1, tt table1)
01100 #else
01101 test_mtbdd(f1, table1)
01102 bdd f1;
01103 tt table1;
01104 #endif
01105 {
01106 bdd wm;
01107 bdd temp1, temp2;
01108 bdd result;
01109
01110 wm=walsh_matrix(0);
01111 temp1=transform(wm, f1, vars);
01112 temp2=temp1;
01113 temp1=transform(wm, temp2, aux_vars);
01114 cmu_bdd_free(bddm, wm);
01115 cmu_bdd_free(bddm, temp2);
01116 temp2=terminal(1.0/TT_BITS);
01117 result=mtbdd_mult(bddm, temp1, temp2);
01118 cmu_bdd_free(bddm, temp1);
01119 cmu_bdd_free(bddm, temp2);
01120 if (f1 != result)
01121 error("Walsh transformation and inverse", result, f1, (bdd)0);
01122 cmu_bdd_free(bddm, result);
01123 }
01124
01125
01126 static
01127 void
01128 #if defined(__STDC__)
01129 test_swap(bdd f, tt table)
01130 #else
01131 test_swap(f, table)
01132 bdd f;
01133 tt table;
01134 #endif
01135 {
01136 int var1, var2;
01137 bdd result;
01138 tt resulttable;
01139 tt temp1, temp2, temp3, temp4;
01140 bdd expected;
01141
01142 var1=((unsigned long)random())%TT_VARS;
01143 var2=((unsigned long)random())%TT_VARS;
01144 result=cmu_bdd_swap_vars(bddm, f, vars[var1], vars[var2]);
01145 temp1=cofactor(cofactor(table, var1, 1), var2, 1);
01146 temp2=cofactor(cofactor(table, var1, 1), var2, 0);
01147 temp3=cofactor(cofactor(table, var1, 0), var2, 1);
01148 temp4=cofactor(cofactor(table, var1, 0), var2, 0);
01149 resulttable=cofactor_masks[var2] & cofactor_masks[var1] & temp1;
01150 resulttable|=cofactor_masks[var2] & ~cofactor_masks[var1] & temp2;
01151 resulttable|=~cofactor_masks[var2] & cofactor_masks[var1] & temp3;
01152 resulttable|=~cofactor_masks[var2] & ~cofactor_masks[var1] & temp4;
01153 expected=encoding_to_bdd(resulttable);
01154 if (result != expected)
01155 error("swap variables", result, expected, f, vars[var1], vars[var2], (bdd)0);
01156 cmu_bdd_free(bddm, result);
01157 cmu_bdd_free(bddm, expected);
01158 }
01159
01160
01161 static void
01162 #if defined(__STDC__)
01163 test_dump(bdd f, tt table)
01164 #else
01165 test_dump(f, table)
01166 bdd f;
01167 tt table;
01168 #endif
01169 {
01170 FILE *fp;
01171 int i, j;
01172 bdd dump_vars[TT_VARS+1];
01173 bdd temp;
01174 bdd result;
01175 int err;
01176
01177 if (!(fp=tmpfile()))
01178 {
01179 fprintf(stderr, "could not open temporary file\n");
01180 exit(1);
01181 }
01182 for (i=0; i < TT_VARS; ++i)
01183 dump_vars[i]=vars[i];
01184 dump_vars[i]=0;
01185 for (i=0; i < TT_VARS-1; ++i)
01186 {
01187 j=i+((unsigned long)random())%(TT_VARS-i);
01188 temp=dump_vars[i];
01189 dump_vars[i]=dump_vars[j];
01190 dump_vars[j]=temp;
01191 }
01192 if (!cmu_bdd_dump_bdd(bddm, f, dump_vars, fp))
01193 {
01194 fprintf(stderr, "Error: dump failure:\n");
01195 fprintf(stderr, "Argument:\n");
01196 print_bdd(f);
01197 fclose(fp);
01198 return;
01199 }
01200 rewind(fp);
01201 if (!(result=cmu_bdd_undump_bdd(bddm, dump_vars, fp, &err)) || err)
01202 {
01203 fprintf(stderr, "Error: undump failure: code %d:\n", err);
01204 fprintf(stderr, "Argument:\n");
01205 print_bdd(f);
01206 fclose(fp);
01207 return;
01208 }
01209 fclose(fp);
01210 if (result != f)
01211 error("dump/undump", result, f, f, (bdd)0);
01212 cmu_bdd_free(bddm, result);
01213 }
01214
01215
01216 static
01217 void
01218 #if defined(__STDC__)
01219 check_leak(void)
01220 #else
01221 check_leak()
01222 #endif
01223 {
01224 bdd assoc[1];
01225
01226 assoc[0]=0;
01227 cmu_bdd_temp_assoc(bddm, assoc, 0);
01228 cmu_bdd_gc(bddm);
01229 if (cmu_bdd_total_size(bddm) != 2*TT_VARS+1l)
01230 fprintf(stderr, "Memory leak somewhere...\n");
01231 }
01232
01233
01234 static
01235 void
01236 #if defined(__STDC__)
01237 random_tests(int iterations)
01238 #else
01239 random_tests(iterations)
01240 int iterations;
01241 #endif
01242 {
01243 int i;
01244 tt table1, table2, table3;
01245 bdd f1, f2, f3;
01246 INT_PTR v1, v2;
01247
01248 printf("Random operation tests...\n");
01249 bddm=cmu_bdd_init();
01250 cmu_bdd_node_limit(bddm, 5000);
01251 mtbdd_transform_closure(bddm, canonical_fn, transform_fn, (pointer)0);
01252 as_INT_PTRs(-1.0, &v1, &v2);
01253 mtcmu_bdd_one_data(bddm, v1, v2);
01254 vars[1]=cmu_bdd_new_var_last(bddm);
01255 vars[0]=cmu_bdd_new_var_first(bddm);
01256 vars[4]=cmu_bdd_new_var_after(bddm, vars[1]);
01257 vars[3]=cmu_bdd_new_var_before(bddm, vars[4]);
01258 vars[2]=cmu_bdd_new_var_after(bddm, vars[1]);
01259 for (i=0; i < 5; ++i)
01260 aux_vars[i]=cmu_bdd_new_var_after(bddm, vars[i]);
01261 for (i=0; i < iterations; ++i)
01262 {
01263 if ((i & 0xf) == 0)
01264 {
01265 putchar('.');
01266 fflush(stdout);
01267 }
01268 if ((i & 0x3ff) == 0x3ff)
01269 {
01270 putchar('\n');
01271 fflush(stdout);
01272 check_leak();
01273 }
01274 table1=random();
01275 table2=random();
01276 table3=random();
01277 f1=encoding_to_bdd(table1);
01278 f2=encoding_to_bdd(table2);
01279 f3=encoding_to_bdd(table3);
01280 test_ite(f1, table1, f2, table2, f3, table3);
01281 test_and(f1, table1, f2, table2);
01282 test_or(f1, table1, f2, table2);
01283 test_xor(f1, table1, f2, table2);
01284 test_id_not(f1, table1);
01285 test_compose(f1, table1, f2, table2);
01286 test_qnt(f1, table1);
01287 test_rel_prod(f1, table1, f2, table2);
01288 test_subst(f1, table1, f2, table2, f3, table3);
01289 test_inter_impl(f1, table1, f2, table2);
01290 test_sat(f1, table1);
01291 test_gen_cof(f1, table1, f2, table2);
01292 test_reduce(f1, table1, f2, table2);
01293 test_apply(f1, table1, f2, table2);
01294 test_size(f1, table1, f2, table2);
01295 test_mtbdd(f1, table1);
01296 test_swap(f1, table1);
01297 if (i < 100)
01298 test_dump(f1, table1);
01299 cmu_bdd_free(bddm, f1);
01300 cmu_bdd_free(bddm, f2);
01301 cmu_bdd_free(bddm, f3);
01302 }
01303 putchar('\n');
01304 cmu_bdd_stats(bddm, stdout);
01305 cmu_bdd_quit(bddm);
01306 }
01307
01308
01309 int
01310 #if defined(__STDC__)
01311 main(void)
01312 #else
01313 main()
01314 #endif
01315 {
01316 (void) srandom((unsigned) 1);
01317 random_tests(ITERATIONS);
01318 exit(0);
01319 }
