buddy.ffi.c (17000B)
1 /* Generated from buddy.ffi */ 2 3 #include "../pico.h" 4 5 #include "bdd.h" 6 7 any cfun_bdd_init(any ex) { 8 any x = ex, y; 9 x = cdr(x); 10 y = EVAL(car(x)); 11 NeedNum(ex, y); 12 int b1 = (int) unBox(y); 13 x = cdr(x); 14 y = EVAL(car(x)); 15 NeedNum(ex, y); 16 int b2 = (int) unBox(y); 17 int z = bdd_init(b1, b2); 18 return box(z); 19 } 20 21 any cfun_bdd_done(any ex __attribute__((unused))) { 22 bdd_done(); 23 return Nil; 24 } 25 26 any cfun_bdd_setvarnum(any ex) { 27 any x = ex, y; 28 x = cdr(x); 29 y = EVAL(car(x)); 30 NeedNum(ex, y); 31 int b1 = (int) unBox(y); 32 int z = bdd_setvarnum(b1); 33 return box(z); 34 } 35 36 any cfun_bdd_extvarnum(any ex) { 37 any x = ex, y; 38 x = cdr(x); 39 y = EVAL(car(x)); 40 NeedNum(ex, y); 41 int b1 = (int) unBox(y); 42 int z = bdd_extvarnum(b1); 43 return box(z); 44 } 45 46 any cfun_bdd_isrunning(any ex __attribute__((unused))) { 47 int z = bdd_isrunning(); 48 return box(z); 49 } 50 51 any cfun_bdd_setmaxnodenum(any ex) { 52 any x = ex, y; 53 x = cdr(x); 54 y = EVAL(car(x)); 55 NeedNum(ex, y); 56 int b1 = (int) unBox(y); 57 int z = bdd_setmaxnodenum(b1); 58 return box(z); 59 } 60 61 any cfun_bdd_setmaxincrease(any ex) { 62 any x = ex, y; 63 x = cdr(x); 64 y = EVAL(car(x)); 65 NeedNum(ex, y); 66 int b1 = (int) unBox(y); 67 int z = bdd_setmaxincrease(b1); 68 return box(z); 69 } 70 71 any cfun_bdd_setminfreenodes(any ex) { 72 any x = ex, y; 73 x = cdr(x); 74 y = EVAL(car(x)); 75 NeedNum(ex, y); 76 int b1 = (int) unBox(y); 77 int z = bdd_setminfreenodes(b1); 78 return box(z); 79 } 80 81 any cfun_bdd_getnodenum(any ex __attribute__((unused))) { 82 int z = bdd_getnodenum(); 83 return box(z); 84 } 85 86 any cfun_bdd_getallocnum(any ex __attribute__((unused))) { 87 int z = bdd_getallocnum(); 88 return box(z); 89 } 90 91 any cfun_bdd_versionstr(any ex __attribute__((unused))) { 92 char* z = bdd_versionstr(); 93 return mkStr(z); 94 } 95 96 any cfun_bdd_versionnum(any ex __attribute__((unused))) { 97 int z = bdd_versionnum(); 98 return box(z); 99 } 100 101 any cfun_bdd_printstat(any ex __attribute__((unused))) { 102 bdd_printstat(); 103 return Nil; 104 } 105 106 any cfun_bdd_default_errhandler(any ex) { 107 any x = ex, y; 108 x = cdr(x); 109 y = EVAL(car(x)); 110 NeedNum(ex, y); 111 int b1 = (int) unBox(y); 112 bdd_default_errhandler(b1); 113 return Nil; 114 } 115 116 any cfun_bdd_errstring(any ex) { 117 any x = ex, y; 118 x = cdr(x); 119 y = EVAL(car(x)); 120 NeedNum(ex, y); 121 int b1 = (int) unBox(y); 122 char* z = bdd_errstring(b1); 123 return mkStr(z); 124 } 125 126 any cfun_bdd_clear_error(any ex __attribute__((unused))) { 127 bdd_clear_error(); 128 return Nil; 129 } 130 131 any cfun_bdd_true(any ex __attribute__((unused))) { 132 int z = bdd_true(); 133 return box(z); 134 } 135 136 any cfun_bdd_false(any ex __attribute__((unused))) { 137 int z = bdd_false(); 138 return box(z); 139 } 140 141 any cfun_bdd_varnum(any ex __attribute__((unused))) { 142 int z = bdd_varnum(); 143 return box(z); 144 } 145 146 any cfun_bdd_ithvar(any ex) { 147 any x = ex, y; 148 x = cdr(x); 149 y = EVAL(car(x)); 150 NeedNum(ex, y); 151 int b1 = (int) unBox(y); 152 BDD z = bdd_ithvar(b1); 153 return box(z); 154 } 155 156 any cfun_bdd_nithvar(any ex) { 157 any x = ex, y; 158 x = cdr(x); 159 y = EVAL(car(x)); 160 NeedNum(ex, y); 161 int b1 = (int) unBox(y); 162 BDD z = bdd_nithvar(b1); 163 return box(z); 164 } 165 166 any cfun_bdd_var(any ex) { 167 any x = ex, y; 168 x = cdr(x); 169 y = EVAL(car(x)); 170 NeedNum(ex, y); 171 BDD b1 = (BDD) unBox(y); 172 int z = bdd_var(b1); 173 return box(z); 174 } 175 176 any cfun_bdd_low(any ex) { 177 any x = ex, y; 178 x = cdr(x); 179 y = EVAL(car(x)); 180 NeedNum(ex, y); 181 BDD b1 = (BDD) unBox(y); 182 BDD z = bdd_low(b1); 183 return box(z); 184 } 185 186 any cfun_bdd_high(any ex) { 187 any x = ex, y; 188 x = cdr(x); 189 y = EVAL(car(x)); 190 NeedNum(ex, y); 191 BDD b1 = (BDD) unBox(y); 192 BDD z = bdd_high(b1); 193 return box(z); 194 } 195 196 any cfun_bdd_addref(any ex) { 197 any x = ex, y; 198 x = cdr(x); 199 y = EVAL(car(x)); 200 NeedNum(ex, y); 201 BDD b1 = (BDD) unBox(y); 202 BDD z = bdd_addref(b1); 203 return box(z); 204 } 205 206 any cfun_bdd_delref(any ex) { 207 any x = ex, y; 208 x = cdr(x); 209 y = EVAL(car(x)); 210 NeedNum(ex, y); 211 BDD b1 = (BDD) unBox(y); 212 BDD z = bdd_delref(b1); 213 return box(z); 214 } 215 216 any cfun_bdd_gbc(any ex __attribute__((unused))) { 217 bdd_gbc(); 218 return Nil; 219 } 220 221 any cfun_bdd_newpair(any ex __attribute__((unused))) { 222 bddPair* z = bdd_newpair(); 223 return box(z); 224 } 225 226 any cfun_bdd_setpair(any ex) { 227 any x = ex, y; 228 x = cdr(x); 229 y = EVAL(car(x)); 230 NeedNum(ex, y); 231 bddPair* b1 = (bddPair*) unBox(y); 232 x = cdr(x); 233 y = EVAL(car(x)); 234 NeedNum(ex, y); 235 int b2 = (int) unBox(y); 236 x = cdr(x); 237 y = EVAL(car(x)); 238 NeedNum(ex, y); 239 int b3 = (int) unBox(y); 240 int z = bdd_setpair(b1, b2, b3); 241 return box(z); 242 } 243 244 any cfun_bdd_setbddpair(any ex) { 245 any x = ex, y; 246 x = cdr(x); 247 y = EVAL(car(x)); 248 NeedNum(ex, y); 249 bddPair* b1 = (bddPair*) unBox(y); 250 x = cdr(x); 251 y = EVAL(car(x)); 252 NeedNum(ex, y); 253 int b2 = (int) unBox(y); 254 x = cdr(x); 255 y = EVAL(car(x)); 256 NeedNum(ex, y); 257 BDD b3 = (BDD) unBox(y); 258 int z = bdd_setbddpair(b1, b2, b3); 259 return box(z); 260 } 261 262 any cfun_bdd_resetpair(any ex) { 263 any x = ex, y; 264 x = cdr(x); 265 y = EVAL(car(x)); 266 NeedNum(ex, y); 267 bddPair* b1 = (bddPair*) unBox(y); 268 bdd_resetpair(b1); 269 return Nil; 270 } 271 272 any cfun_bdd_freepair(any ex) { 273 any x = ex, y; 274 x = cdr(x); 275 y = EVAL(car(x)); 276 NeedNum(ex, y); 277 bddPair* b1 = (bddPair*) unBox(y); 278 bdd_freepair(b1); 279 return Nil; 280 } 281 282 any cfun_bdd_setcacheratio(any ex) { 283 any x = ex, y; 284 x = cdr(x); 285 y = EVAL(car(x)); 286 NeedNum(ex, y); 287 int b1 = (int) unBox(y); 288 int z = bdd_setcacheratio(b1); 289 return box(z); 290 } 291 292 any cfun_bdd_not(any ex) { 293 any x = ex, y; 294 x = cdr(x); 295 y = EVAL(car(x)); 296 NeedNum(ex, y); 297 BDD b1 = (BDD) unBox(y); 298 BDD z = bdd_not(b1); 299 return box(z); 300 } 301 302 any cfun_bdd_apply(any ex) { 303 any x = ex, y; 304 x = cdr(x); 305 y = EVAL(car(x)); 306 NeedNum(ex, y); 307 BDD b1 = (BDD) unBox(y); 308 x = cdr(x); 309 y = EVAL(car(x)); 310 NeedNum(ex, y); 311 BDD b2 = (BDD) unBox(y); 312 x = cdr(x); 313 y = EVAL(car(x)); 314 NeedNum(ex, y); 315 int b3 = (int) unBox(y); 316 BDD z = bdd_apply(b1, b2, b3); 317 return box(z); 318 } 319 320 any cfun_bdd_and(any ex) { 321 any x = ex, y; 322 x = cdr(x); 323 y = EVAL(car(x)); 324 NeedNum(ex, y); 325 BDD b1 = (BDD) unBox(y); 326 x = cdr(x); 327 y = EVAL(car(x)); 328 NeedNum(ex, y); 329 BDD b2 = (BDD) unBox(y); 330 BDD z = bdd_and(b1, b2); 331 return box(z); 332 } 333 334 any cfun_bdd_or(any ex) { 335 any x = ex, y; 336 x = cdr(x); 337 y = EVAL(car(x)); 338 NeedNum(ex, y); 339 BDD b1 = (BDD) unBox(y); 340 x = cdr(x); 341 y = EVAL(car(x)); 342 NeedNum(ex, y); 343 BDD b2 = (BDD) unBox(y); 344 BDD z = bdd_or(b1, b2); 345 return box(z); 346 } 347 348 any cfun_bdd_xor(any ex) { 349 any x = ex, y; 350 x = cdr(x); 351 y = EVAL(car(x)); 352 NeedNum(ex, y); 353 BDD b1 = (BDD) unBox(y); 354 x = cdr(x); 355 y = EVAL(car(x)); 356 NeedNum(ex, y); 357 BDD b2 = (BDD) unBox(y); 358 BDD z = bdd_xor(b1, b2); 359 return box(z); 360 } 361 362 any cfun_bdd_imp(any ex) { 363 any x = ex, y; 364 x = cdr(x); 365 y = EVAL(car(x)); 366 NeedNum(ex, y); 367 BDD b1 = (BDD) unBox(y); 368 x = cdr(x); 369 y = EVAL(car(x)); 370 NeedNum(ex, y); 371 BDD b2 = (BDD) unBox(y); 372 BDD z = bdd_imp(b1, b2); 373 return box(z); 374 } 375 376 any cfun_bdd_biimp(any ex) { 377 any x = ex, y; 378 x = cdr(x); 379 y = EVAL(car(x)); 380 NeedNum(ex, y); 381 BDD b1 = (BDD) unBox(y); 382 x = cdr(x); 383 y = EVAL(car(x)); 384 NeedNum(ex, y); 385 BDD b2 = (BDD) unBox(y); 386 BDD z = bdd_biimp(b1, b2); 387 return box(z); 388 } 389 390 any cfun_bdd_ite(any ex) { 391 any x = ex, y; 392 x = cdr(x); 393 y = EVAL(car(x)); 394 NeedNum(ex, y); 395 BDD b1 = (BDD) unBox(y); 396 x = cdr(x); 397 y = EVAL(car(x)); 398 NeedNum(ex, y); 399 BDD b2 = (BDD) unBox(y); 400 x = cdr(x); 401 y = EVAL(car(x)); 402 NeedNum(ex, y); 403 BDD b3 = (BDD) unBox(y); 404 BDD z = bdd_ite(b1, b2, b3); 405 return box(z); 406 } 407 408 any cfun_bdd_restrict(any ex) { 409 any x = ex, y; 410 x = cdr(x); 411 y = EVAL(car(x)); 412 NeedNum(ex, y); 413 BDD b1 = (BDD) unBox(y); 414 x = cdr(x); 415 y = EVAL(car(x)); 416 NeedNum(ex, y); 417 BDD b2 = (BDD) unBox(y); 418 BDD z = bdd_restrict(b1, b2); 419 return box(z); 420 } 421 422 any cfun_bdd_constrain(any ex) { 423 any x = ex, y; 424 x = cdr(x); 425 y = EVAL(car(x)); 426 NeedNum(ex, y); 427 BDD b1 = (BDD) unBox(y); 428 x = cdr(x); 429 y = EVAL(car(x)); 430 NeedNum(ex, y); 431 BDD b2 = (BDD) unBox(y); 432 BDD z = bdd_constrain(b1, b2); 433 return box(z); 434 } 435 436 any cfun_bdd_replace(any ex) { 437 any x = ex, y; 438 x = cdr(x); 439 y = EVAL(car(x)); 440 NeedNum(ex, y); 441 BDD b1 = (BDD) unBox(y); 442 x = cdr(x); 443 y = EVAL(car(x)); 444 NeedNum(ex, y); 445 bddPair* b2 = (bddPair*) unBox(y); 446 BDD z = bdd_replace(b1, b2); 447 return box(z); 448 } 449 450 any cfun_bdd_compose(any ex) { 451 any x = ex, y; 452 x = cdr(x); 453 y = EVAL(car(x)); 454 NeedNum(ex, y); 455 BDD b1 = (BDD) unBox(y); 456 x = cdr(x); 457 y = EVAL(car(x)); 458 NeedNum(ex, y); 459 BDD b2 = (BDD) unBox(y); 460 x = cdr(x); 461 y = EVAL(car(x)); 462 NeedNum(ex, y); 463 BDD b3 = (BDD) unBox(y); 464 BDD z = bdd_compose(b1, b2, b3); 465 return box(z); 466 } 467 468 any cfun_bdd_veccompose(any ex) { 469 any x = ex, y; 470 x = cdr(x); 471 y = EVAL(car(x)); 472 NeedNum(ex, y); 473 BDD b1 = (BDD) unBox(y); 474 x = cdr(x); 475 y = EVAL(car(x)); 476 NeedNum(ex, y); 477 bddPair* b2 = (bddPair*) unBox(y); 478 BDD z = bdd_veccompose(b1, b2); 479 return box(z); 480 } 481 482 any cfun_bdd_simplify(any ex) { 483 any x = ex, y; 484 x = cdr(x); 485 y = EVAL(car(x)); 486 NeedNum(ex, y); 487 BDD b1 = (BDD) unBox(y); 488 x = cdr(x); 489 y = EVAL(car(x)); 490 NeedNum(ex, y); 491 BDD b2 = (BDD) unBox(y); 492 BDD z = bdd_simplify(b1, b2); 493 return box(z); 494 } 495 496 any cfun_bdd_exist(any ex) { 497 any x = ex, y; 498 x = cdr(x); 499 y = EVAL(car(x)); 500 NeedNum(ex, y); 501 BDD b1 = (BDD) unBox(y); 502 x = cdr(x); 503 y = EVAL(car(x)); 504 NeedNum(ex, y); 505 BDD b2 = (BDD) unBox(y); 506 BDD z = bdd_exist(b1, b2); 507 return box(z); 508 } 509 510 any cfun_bdd_forall(any ex) { 511 any x = ex, y; 512 x = cdr(x); 513 y = EVAL(car(x)); 514 NeedNum(ex, y); 515 BDD b1 = (BDD) unBox(y); 516 x = cdr(x); 517 y = EVAL(car(x)); 518 NeedNum(ex, y); 519 BDD b2 = (BDD) unBox(y); 520 BDD z = bdd_forall(b1, b2); 521 return box(z); 522 } 523 524 any cfun_bdd_unique(any ex) { 525 any x = ex, y; 526 x = cdr(x); 527 y = EVAL(car(x)); 528 NeedNum(ex, y); 529 BDD b1 = (BDD) unBox(y); 530 x = cdr(x); 531 y = EVAL(car(x)); 532 NeedNum(ex, y); 533 BDD b2 = (BDD) unBox(y); 534 BDD z = bdd_unique(b1, b2); 535 return box(z); 536 } 537 538 any cfun_bdd_appex(any ex) { 539 any x = ex, y; 540 x = cdr(x); 541 y = EVAL(car(x)); 542 NeedNum(ex, y); 543 BDD b1 = (BDD) unBox(y); 544 x = cdr(x); 545 y = EVAL(car(x)); 546 NeedNum(ex, y); 547 BDD b2 = (BDD) unBox(y); 548 x = cdr(x); 549 y = EVAL(car(x)); 550 NeedNum(ex, y); 551 int b3 = (int) unBox(y); 552 x = cdr(x); 553 y = EVAL(car(x)); 554 NeedNum(ex, y); 555 BDD b4 = (BDD) unBox(y); 556 BDD z = bdd_appex(b1, b2, b3, b4); 557 return box(z); 558 } 559 560 any cfun_bdd_appall(any ex) { 561 any x = ex, y; 562 x = cdr(x); 563 y = EVAL(car(x)); 564 NeedNum(ex, y); 565 BDD b1 = (BDD) unBox(y); 566 x = cdr(x); 567 y = EVAL(car(x)); 568 NeedNum(ex, y); 569 BDD b2 = (BDD) unBox(y); 570 x = cdr(x); 571 y = EVAL(car(x)); 572 NeedNum(ex, y); 573 int b3 = (int) unBox(y); 574 x = cdr(x); 575 y = EVAL(car(x)); 576 NeedNum(ex, y); 577 BDD b4 = (BDD) unBox(y); 578 BDD z = bdd_appall(b1, b2, b3, b4); 579 return box(z); 580 } 581 582 any cfun_bdd_appuni(any ex) { 583 any x = ex, y; 584 x = cdr(x); 585 y = EVAL(car(x)); 586 NeedNum(ex, y); 587 BDD b1 = (BDD) unBox(y); 588 x = cdr(x); 589 y = EVAL(car(x)); 590 NeedNum(ex, y); 591 BDD b2 = (BDD) unBox(y); 592 x = cdr(x); 593 y = EVAL(car(x)); 594 NeedNum(ex, y); 595 int b3 = (int) unBox(y); 596 x = cdr(x); 597 y = EVAL(car(x)); 598 NeedNum(ex, y); 599 BDD b4 = (BDD) unBox(y); 600 BDD z = bdd_appuni(b1, b2, b3, b4); 601 return box(z); 602 } 603 604 any cfun_bdd_support(any ex) { 605 any x = ex, y; 606 x = cdr(x); 607 y = EVAL(car(x)); 608 NeedNum(ex, y); 609 BDD b1 = (BDD) unBox(y); 610 BDD z = bdd_support(b1); 611 return box(z); 612 } 613 614 any cfun_bdd_satone(any ex) { 615 any x = ex, y; 616 x = cdr(x); 617 y = EVAL(car(x)); 618 NeedNum(ex, y); 619 BDD b1 = (BDD) unBox(y); 620 BDD z = bdd_satone(b1); 621 return box(z); 622 } 623 624 any cfun_bdd_satoneset(any ex) { 625 any x = ex, y; 626 x = cdr(x); 627 y = EVAL(car(x)); 628 NeedNum(ex, y); 629 BDD b1 = (BDD) unBox(y); 630 x = cdr(x); 631 y = EVAL(car(x)); 632 NeedNum(ex, y); 633 BDD b2 = (BDD) unBox(y); 634 x = cdr(x); 635 y = EVAL(car(x)); 636 NeedNum(ex, y); 637 BDD b3 = (BDD) unBox(y); 638 BDD z = bdd_satoneset(b1, b2, b3); 639 return box(z); 640 } 641 642 any cfun_bdd_fullsatone(any ex) { 643 any x = ex, y; 644 x = cdr(x); 645 y = EVAL(car(x)); 646 NeedNum(ex, y); 647 BDD b1 = (BDD) unBox(y); 648 BDD z = bdd_fullsatone(b1); 649 return box(z); 650 } 651 652 any cfun_bdd_nodecount(any ex) { 653 any x = ex, y; 654 x = cdr(x); 655 y = EVAL(car(x)); 656 NeedNum(ex, y); 657 BDD b1 = (BDD) unBox(y); 658 int z = bdd_nodecount(b1); 659 return box(z); 660 } 661 662 any cfun_bdd_printall(any ex __attribute__((unused))) { 663 bdd_printall(); 664 return Nil; 665 } 666 667 any cfun_bdd_printtable(any ex) { 668 any x = ex, y; 669 x = cdr(x); 670 y = EVAL(car(x)); 671 NeedNum(ex, y); 672 BDD b1 = (BDD) unBox(y); 673 bdd_printtable(b1); 674 return Nil; 675 } 676 677 any cfun_bdd_printset(any ex) { 678 any x = ex, y; 679 x = cdr(x); 680 y = EVAL(car(x)); 681 NeedNum(ex, y); 682 BDD b1 = (BDD) unBox(y); 683 bdd_printset(b1); 684 return Nil; 685 } 686 687 any cfun_bdd_fnprintdot(any ex) { 688 any x = ex, y; 689 x = cdr(x); 690 y = EVAL(car(x)); 691 any y1s = xSym(y); 692 char b1[bufSize(y1s)]; 693 bufString(y1s, b1); 694 x = cdr(x); 695 y = EVAL(car(x)); 696 NeedNum(ex, y); 697 BDD b2 = (BDD) unBox(y); 698 int z = bdd_fnprintdot(b1, b2); 699 return box(z); 700 } 701 702 any cfun_bdd_printdot(any ex) { 703 any x = ex, y; 704 x = cdr(x); 705 y = EVAL(car(x)); 706 NeedNum(ex, y); 707 BDD b1 = (BDD) unBox(y); 708 bdd_printdot(b1); 709 return Nil; 710 } 711 712 any cfun_bdd_fnsave(any ex) { 713 any x = ex, y; 714 x = cdr(x); 715 y = EVAL(car(x)); 716 any y1s = xSym(y); 717 char b1[bufSize(y1s)]; 718 bufString(y1s, b1); 719 x = cdr(x); 720 y = EVAL(car(x)); 721 NeedNum(ex, y); 722 BDD b2 = (BDD) unBox(y); 723 int z = bdd_fnsave(b1, b2); 724 return box(z); 725 } 726 727 any cfun_bdd_swapvar(any ex) { 728 any x = ex, y; 729 x = cdr(x); 730 y = EVAL(car(x)); 731 NeedNum(ex, y); 732 int b1 = (int) unBox(y); 733 x = cdr(x); 734 y = EVAL(car(x)); 735 NeedNum(ex, y); 736 int b2 = (int) unBox(y); 737 int z = bdd_swapvar(b1, b2); 738 return box(z); 739 } 740 741 any cfun_bdd_default_reohandler(any ex) { 742 any x = ex, y; 743 x = cdr(x); 744 y = EVAL(car(x)); 745 NeedNum(ex, y); 746 int b1 = (int) unBox(y); 747 bdd_default_reohandler(b1); 748 return Nil; 749 } 750 751 any cfun_bdd_reorder(any ex) { 752 any x = ex, y; 753 x = cdr(x); 754 y = EVAL(car(x)); 755 NeedNum(ex, y); 756 int b1 = (int) unBox(y); 757 bdd_reorder(b1); 758 return Nil; 759 } 760 761 any cfun_bdd_reorder_gain(any ex __attribute__((unused))) { 762 int z = bdd_reorder_gain(); 763 return box(z); 764 } 765 766 any cfun_bdd_clrvarblocks(any ex __attribute__((unused))) { 767 bdd_clrvarblocks(); 768 return Nil; 769 } 770 771 any cfun_bdd_addvarblock(any ex) { 772 any x = ex, y; 773 x = cdr(x); 774 y = EVAL(car(x)); 775 NeedNum(ex, y); 776 BDD b1 = (BDD) unBox(y); 777 x = cdr(x); 778 y = EVAL(car(x)); 779 NeedNum(ex, y); 780 int b2 = (int) unBox(y); 781 int z = bdd_addvarblock(b1, b2); 782 return box(z); 783 } 784 785 any cfun_bdd_intaddvarblock(any ex) { 786 any x = ex, y; 787 x = cdr(x); 788 y = EVAL(car(x)); 789 NeedNum(ex, y); 790 int b1 = (int) unBox(y); 791 x = cdr(x); 792 y = EVAL(car(x)); 793 NeedNum(ex, y); 794 int b2 = (int) unBox(y); 795 x = cdr(x); 796 y = EVAL(car(x)); 797 NeedNum(ex, y); 798 int b3 = (int) unBox(y); 799 int z = bdd_intaddvarblock(b1, b2, b3); 800 return box(z); 801 } 802 803 any cfun_bdd_varblockall(any ex __attribute__((unused))) { 804 bdd_varblockall(); 805 return Nil; 806 } 807 808 any cfun_bdd_autoreorder(any ex) { 809 any x = ex, y; 810 x = cdr(x); 811 y = EVAL(car(x)); 812 NeedNum(ex, y); 813 int b1 = (int) unBox(y); 814 int z = bdd_autoreorder(b1); 815 return box(z); 816 } 817 818 any cfun_bdd_autoreorder_times(any ex) { 819 any x = ex, y; 820 x = cdr(x); 821 y = EVAL(car(x)); 822 NeedNum(ex, y); 823 int b1 = (int) unBox(y); 824 x = cdr(x); 825 y = EVAL(car(x)); 826 NeedNum(ex, y); 827 int b2 = (int) unBox(y); 828 int z = bdd_autoreorder_times(b1, b2); 829 return box(z); 830 } 831 832 any cfun_bdd_var2level(any ex) { 833 any x = ex, y; 834 x = cdr(x); 835 y = EVAL(car(x)); 836 NeedNum(ex, y); 837 int b1 = (int) unBox(y); 838 int z = bdd_var2level(b1); 839 return box(z); 840 } 841 842 any cfun_bdd_level2var(any ex) { 843 any x = ex, y; 844 x = cdr(x); 845 y = EVAL(car(x)); 846 NeedNum(ex, y); 847 int b1 = (int) unBox(y); 848 int z = bdd_level2var(b1); 849 return box(z); 850 } 851 852 any cfun_bdd_getreorder_times(any ex __attribute__((unused))) { 853 int z = bdd_getreorder_times(); 854 return box(z); 855 } 856 857 any cfun_bdd_getreorder_method(any ex __attribute__((unused))) { 858 int z = bdd_getreorder_method(); 859 return box(z); 860 } 861 862 any cfun_bdd_enable_reorder(any ex __attribute__((unused))) { 863 bdd_enable_reorder(); 864 return Nil; 865 } 866 867 any cfun_bdd_disable_reorder(any ex __attribute__((unused))) { 868 bdd_disable_reorder(); 869 return Nil; 870 } 871 872 any cfun_bdd_reorder_verbose(any ex) { 873 any x = ex, y; 874 x = cdr(x); 875 y = EVAL(car(x)); 876 NeedNum(ex, y); 877 int b1 = (int) unBox(y); 878 int z = bdd_reorder_verbose(b1); 879 return box(z); 880 } 881 882 any cfun_bdd_printorder(any ex __attribute__((unused))) { 883 bdd_printorder(); 884 return Nil; 885 }