1/* Copyright (C) 1997-2001 by Ken Friis Larsen and Jakob Lichtenberg. */ 2#include <stdlib.h> 3#include <stdio.h> 4#include <string.h> 5 6/* BDD stuff */ 7#include <bdd.h> 8#include <fdd.h> 9#include <bvec.h> 10 11/* Mosml stuff */ 12#include <mosml/mlvalues.h> 13#include <mosml/fail.h> 14#include <mosml/alloc.h> 15#include <mosml/memory.h> 16#include <mosml/str.h> 17 18 19/* Reduced Ordered Binary Decision Diagrams: interface to 20 J�rn Lind-Nielsen's <buddy@it.edu> BuDDy library. 21 Made by Ken Friis Larsen <ken@friislarsen.net> 22 23 The type bdd.bdd of a Binary Decision Diagram is an abstract type; 24 really a BDD structure. This will contain an integer which is a 25 root number. The root number cannot just be treated as an ordinary 26 int for two reasons: 27 28 1. The gc cannot understand the root number (it would be confused 29 by the untagged integer field) 30 31 2. The (camlrunm) gc don't know how to garbage collect a bdd 32 (call bdd_delref from the bdd lib.) 33 34 This raises the question how to deallocate the bdd structure when 35 it is no longer reachable. One possibility is to use finalized 36 objects, calling the bdd_delref function explicitly whenever a bdd 37 value is about to be garbage-collected by the camlrunm runtime 38 system. 39 40 A bdd should be a finalized object: a pair, 41 42 header with Final_tag 43 0: finalization function mlbdd_finalize 44 1: the bdd's root number 45 46 whose component 0 is a pointer to the finalizing function 47 mlbdd_finalize, and whose component 1 is a root number. The 48 finalization function should apply bdd_delref to the second 49 component of the pair: */ 50 51/* To make DLL on Windows we need non-standard annotations */ 52#ifdef WIN32 53#define EXTERNML __declspec(dllexport) 54#else 55#define EXTERNML 56#endif 57 58/* Sometimes it is nice to raise the Domain exception 59 */ 60#include <mosml/globals.h> 61#ifndef SMLEXN_DOMAIN /* SMLEXN_DOMAIN is not defined in mosml 2.00 */ 62#define RAISE_DOMAIN raiseprimitive0(SYS__EXN_DOMAIN) 63#else 64#define RAISE_DOMAIN mlraise(Atom(SMLEXN_DOMAIN)) 65#endif 66 67 68 69/* A nice macro to have */ 70#define Bdd_val(x) (Field(x, 1)) 71 72/* I don't want to adjust the GC so I've made my own alloc_final, 73 stolen from alloc.c 74*/ 75value mlbdd_alloc_final(mlsize_t len, final_fun fun) 76{ 77 value result; 78 result = alloc_shr(len, Final_tag); 79 Final_fun(result) = fun; 80 return result; 81} 82 83void mlbdd_errorhandler(int errorcode) 84{ 85 /* printf("mlbdd error: %d\n",errorcode); */ 86 failwith((char *) bdd_errstring(errorcode)); 87} 88 89static char* pregc = NULL; 90static char* postgc = NULL; 91static int printgc = 0; /* Invariant: if printgc != 0 then will the 92 two strings above point to valid strings */ 93void mlbdd_gc(int num, bddGbcStat* foo) 94{ 95 if(num==1 && printgc) { printf (pregc); fflush(stdout); } 96 else if(num==0 && printgc) { printf(postgc); fflush(stdout); } 97} 98 99static void mlbdd_freegcstrings() { 100 if(printgc) { 101 stat_free(pregc); 102 stat_free(postgc); 103 printgc = 0; 104 } 105} 106 107static void mlbdd_copy2cstring(value from, char* to){ 108 char* fromp; 109 int len; 110 111 fromp = String_val(from); 112 len = string_length(from); 113 114 to = stat_alloc(len + 1); 115 strcpy(to, fromp); 116} 117 118/* ML type: bool -> string -> string -> unit */ 119EXTERNML value mlbdd_setprintgc(value print, value pre, value post) /* ML */ 120{ 121 mlbdd_freegcstrings(); 122 123 if(Bool_val(print)) { 124 mlbdd_copy2cstring(pre, pregc); 125 mlbdd_copy2cstring(post, postgc); 126 printgc = 1; 127 } 128 129 return Val_unit; 130} 131 132/* ML type: int -> int -> unit */ 133EXTERNML value mlbdd_bdd_init(value nodes, value cachesize) /* ML */ 134{ 135 /* setup the our error handler */ 136 bdd_error_hook(&mlbdd_errorhandler); 137 bdd_init(Int_val(nodes), Int_val(cachesize)); 138 bdd_error_hook(&mlbdd_errorhandler); 139 /* bdd_gbc_hook(NULL); */ 140 bdd_gbc_hook(mlbdd_gc); 141 return Val_unit; 142} 143 144/* ML type: unit -> unit */ 145EXTERNML value mlbdd_bdd_done(value nill) /* ML */ 146{ 147 bdd_done(); 148 mlbdd_freegcstrings(); 149 return Val_unit; 150} 151 152/* ML type: unit -> bool */ 153EXTERNML value mlbdd_bdd_isrunning(value nill) /* ML */ 154{ 155 return bdd_isrunning() ? Val_true : Val_false; 156} 157 158/* ML type: int -> unit */ 159EXTERNML value mlbdd_bdd_setvarnum(value n) /* ML */ 160{ 161 bdd_setvarnum(Int_val(n)); 162 return Val_unit; 163} 164 165/* ML type: unit -> int */ 166EXTERNML value mlbdd_getvarnum(value dummy) /* ML */ 167{ 168 return Val_long(bdd_varnum()); 169} 170 171 172/* When the bdd becomes unreachable from the ML process, it will be 173 garbage-collected, mlbdd_finalize() will be called on the bdd, 174 which will do the necessary bdd-bookkeeping. */ 175void mlbdd_finalize(value obj) 176{ 177 bdd_delref(Bdd_val(obj)); 178} 179 180/* Creation of a bdd makes a finalized pair (mlbdd_finalize, root) as 181 described above. */ 182EXTERNML value mlbdd_make(BDD root) 183{ 184 value res; 185 bdd_addref(root); 186 res = mlbdd_alloc_final(2, &mlbdd_finalize); 187 Bdd_val(res) = root; /* Hopefully a BDD fits in a long */ 188 return res; 189} 190 191/* FOR INTERNAL USAGE */ 192/* ML type: bdd -> int */ 193EXTERNML value mlbdd_root(value r) /* ML */ 194{ 195 return Val_int(Bdd_val(r)); 196} 197 198/* ML type: varnum -> bdd */ 199EXTERNML value mlbdd_bdd_ithvar(value i) /* ML */ 200{ 201 return mlbdd_make(bdd_ithvar(Int_val(i))); 202} 203 204/* ML type: varnum-> bdd */ 205EXTERNML value mlbdd_bdd_nithvar(value i) /* ML */ 206{ 207 return mlbdd_make(bdd_nithvar(Int_val(i))); 208} 209 210/* ML type: bool -> bdd */ 211EXTERNML value mlbdd_fromBool(value b) /* ML */ 212{ 213 return mlbdd_make(Bool_val(b) ? bddtrue : bddfalse); 214} 215 216/* ML type: bdd -> bool */ 217EXTERNML value mlbdd_toBool(value obj) /* ML */ 218{ 219 BDD root; 220 root = Bdd_val(obj); 221 if(root == bddtrue) return Val_true; 222 else if(root == bddfalse) return Val_false; 223 else { 224 RAISE_DOMAIN; 225 return Val_unit; /* unreachable, here to prevent warnings */ 226 } 227} 228 229/* ML type: bdd -> varnum */ 230EXTERNML value mlbdd_bdd_var(value r) /* ML */ 231{ 232 return Val_int(bdd_var(Bdd_val(r))); 233} 234 235/* ML type: bdd -> bdd */ 236EXTERNML value mlbdd_bdd_low(value r) /* ML */ 237{ 238 return mlbdd_make(bdd_low(Bdd_val(r))); 239} 240 241/* ML type: bdd -> bdd */ 242EXTERNML value mlbdd_bdd_high(value r) /* ML */ 243{ 244 return mlbdd_make(bdd_high(Bdd_val(r))); 245} 246 247/* Pass the opr constants from <bdd.h> to ML */ 248/* ML type: unit -> int * int * int * int * int * int * int * int * int *int * int * int * int * int * int * int * int * int */ 249EXTERNML value mlbdd_constants(value unit) /* ML */ 250{ 251 value res = alloc_tuple(18); 252 Field(res, 0) = Val_long(bddop_and); 253 Field(res, 1) = Val_long(bddop_xor); 254 Field(res, 2) = Val_long(bddop_or); 255 Field(res, 3) = Val_long(bddop_nand); 256 Field(res, 4) = Val_long(bddop_nor); 257 Field(res, 5) = Val_long(bddop_imp); 258 Field(res, 6) = Val_long(bddop_biimp); 259 Field(res, 7) = Val_long(bddop_diff); 260 Field(res, 8) = Val_long(bddop_less); 261 Field(res, 9) = Val_long(bddop_invimp); 262 Field(res, 10) = Val_long(BDD_REORDER_FIXED); 263 Field(res, 11) = Val_long(BDD_REORDER_FREE); 264 Field(res, 12) = Val_long(BDD_REORDER_WIN2); 265 Field(res, 13) = Val_long(BDD_REORDER_WIN2ITE); 266 Field(res, 14) = Val_long(BDD_REORDER_SIFT); 267 Field(res, 15) = Val_long(BDD_REORDER_SIFTITE); 268 Field(res, 16) = Val_long(BDD_REORDER_RANDOM); 269 Field(res, 17) = Val_long(BDD_REORDER_NONE); 270 271 return res; 272} 273 274 275/* ML type: bdd -> bdd -> int -> bdd */ 276EXTERNML value mlbdd_bdd_apply(value left, value right, value opr) /* ML */ 277{ 278 return mlbdd_make(bdd_apply(Bdd_val(left),Bdd_val(right), 279 Int_val(opr))); 280} 281 282/* ML type: bdd -> bdd */ 283EXTERNML value mlbdd_bdd_not(value r) /* ML */ 284{ 285 return mlbdd_make(bdd_not(Bdd_val(r))); 286} 287 288/* ML type: bdd -> bdd -> bdd -> bdd */ 289EXTERNML value mlbdd_bdd_ite(value x, value y, value z) /* ML */ 290{ 291 return mlbdd_make(bdd_ite(Bdd_val(x), Bdd_val(y), Bdd_val(z))); 292} 293 294 295/* ML type: bdd -> bdd -> bool */ 296EXTERNML value mlbdd_equal(value left, value right) /* ML */ 297{ 298 return ((Bdd_val(left) == Bdd_val(right)) ? Val_true : Val_false); 299} 300 301/* ML type: bdd -> bdd -> bdd */ 302EXTERNML value mlbdd_bdd_restrict(value r, value var) /* ML */ 303{ 304 return mlbdd_make(bdd_restrict(Bdd_val(r),Bdd_val(var))); 305} 306 307/* ML type: bdd -> bdd -> int -> bdd */ 308EXTERNML value mlbdd_bdd_compose(value f, value g, value var) /* ML */ 309{ 310 return mlbdd_make(bdd_compose(Bdd_val(f),Bdd_val(g),Int_val(var))); 311} 312 313 314 315/* ML type: bdd -> bdd -> bdd */ 316EXTERNML value mlbdd_bdd_simplify(value f, value d) /* ML */ 317{ 318 return mlbdd_make(bdd_simplify(Bdd_val(f), Bdd_val(d))); 319} 320 321/* ML type: bdd -> unit */ 322EXTERNML value mlbdd_bdd_printdot(value r) /* ML */ 323{ 324 bdd_printdot(Bdd_val(r)); 325 return Val_unit; 326} 327 328/* ML type: bdd -> unit */ 329EXTERNML value mlbdd_bdd_printset(value r) /* ML */ 330{ 331 bdd_printset(Bdd_val(r)); 332 fflush(stdout); 333 return Val_unit; 334} 335 336/* ML type: string -> bdd -> unit */ 337EXTERNML value mlbdd_bdd_fnprintset(value filename, value r) /* ML */ 338{ 339 char *fname; 340 FILE *ofile; 341 fname = String_val(filename); 342 ofile = fopen(fname, "w"); 343 if (ofile == NULL) 344 failwith("Unable to open file"); 345 else { 346 bdd_fprintset(ofile, Bdd_val(r)); 347 fclose(ofile); 348 } 349 return Val_unit; 350} 351 352 353/* ML type: string -> bdd -> unit */ 354EXTERNML value mlbdd_bdd_fnprintdot(value filename, value r) /* ML */ 355{ 356 bdd_fnprintdot(String_val(filename), Bdd_val(r)); 357 return Val_unit; 358} 359 360/* ML type: unit -> unit */ 361EXTERNML value mlbdd_bdd_printall(value nill) /* ML */ 362{ 363 bdd_printall(); 364 return nill; 365} 366 367/* ML type: string -> bdd -> unit */ 368EXTERNML value mlbdd_bdd_fnsave(value filename, value r) /* ML */ 369{ 370 bdd_fnsave(String_val(filename), Bdd_val(r)); 371 return Val_unit; 372} 373 374/* ML type: string -> bdd */ 375EXTERNML value mlbdd_bdd_fnload(value filename) /* ML */ 376{ 377 BDD res; 378 bdd_fnload(String_val(filename), &res); 379 return mlbdd_make(res); 380 381} 382 383/* ML type: unit -> int * int * int * int * int * int * int * int */ 384EXTERNML value mlbdd_bdd_stats(value nill) 385{ 386 static bddStat stat; 387 value result = alloc_tuple(8); 388 389 bdd_stats(& stat); 390 391 Field(result, 0) = Val_long(stat.produced); 392 Field(result, 1) = Val_long(stat.nodenum); 393 Field(result, 2) = Val_long(stat.maxnodenum); 394 Field(result, 3) = Val_long(stat.freenodes); 395 Field(result, 4) = Val_long(stat.minfreenodes); 396 Field(result, 5) = Val_long(stat.varnum); 397 Field(result, 6) = Val_long(stat.cachesize); 398 Field(result, 7) = Val_long(stat.gbcnum); 399 400 return result; 401} 402 403/* ML type: bdd -> real */ 404EXTERNML value mlbdd_bdd_satcount(value r) /* ML */ 405{ 406 return copy_double(bdd_satcount(Bdd_val(r))); 407} 408 409/* ML type: bdd -> varSet */ 410EXTERNML value mlbdd_bdd_satone(value r) /* ML */ 411{ 412 return mlbdd_make(bdd_satone(Bdd_val(r))); 413} 414 415/* ML type: bdd -> varSet */ 416EXTERNML value mlbdd_bdd_fullsatone(value r) /* ML */ 417{ 418 return mlbdd_make(bdd_fullsatone(Bdd_val(r))); 419} 420 421/* ML type: bdd -> int */ 422EXTERNML value mlbdd_bdd_nodecount(value r) /* ML */ 423{ 424 return Val_int(bdd_nodecount(Bdd_val(r))); 425} 426 427/* ML type: int -> int */ 428EXTERNML value mlbdd_bdd_setmaxincrease(value n) /* ML */ 429{ 430 return Val_int(bdd_setmaxincrease(Int_val(n))); 431} 432 433/* ML type: int -> int */ 434EXTERNML value mlbdd_bdd_setcacheratio(value n) /* ML */ 435{ 436 return Val_int(bdd_setcacheratio(Int_val(n))); 437} 438 439 440/* Some helper functions for creating variable sets, these will be 441 represented as BDD's on the C side but as a different type (varSet) on 442 the ML side. 443*/ 444 445/* ML type: varnum vector -> varSet */ 446EXTERNML value mlbdd_makeset(value varvector) /* ML */ 447{ 448 int size, i, *v; 449 value result; 450 451 size = Wosize_val(varvector); 452 453 /* we use stat_alloc which guarantee that we get the memory (or it 454 will raise an exception). */ 455 v = (int *) stat_alloc(sizeof(int) * size); 456 for (i=0; i<size; i++) { 457 v[i] = Int_val(Field(varvector, i)); 458 } 459 460 /* we assume that vector is sorted on the ML side */ 461 result = mlbdd_make(bdd_makeset(v, size)); 462 463 /* memory allocated with stat_alloc, should be freed with 464 stat_free.*/ 465 stat_free((char *) v); 466 467 return result; 468} 469 470/* ML type: varSet -> varnum vector */ 471EXTERNML value mlbdd_bdd_scanset(value varset) 472{ 473 value result; 474 int *v, n, i; 475 476 if(bdd_scanset(Bdd_val(varset), &v, &n)) { 477 RAISE_DOMAIN; 478 return Val_unit; /* unreachable, here to prevent warnings */ 479 } else { 480 if(n == 0) 481 result = Atom(0); /* The empty vector */ 482 else { 483 result = n < Max_young_wosize ? alloc(n, 0) : alloc_shr(n, 0); 484 for (i = 0; i < n; i++) { 485 Field(result, i) = Val_long(v[i]); 486 } 487 free(v); 488 } 489 } 490 return result; 491} 492 493/* ML type: bdd -> varSet */ 494EXTERNML value mlbdd_bdd_support(value b) /* ML */ 495{ 496 return mlbdd_make(bdd_support(Bdd_val(b))); 497} 498 499/* ML type: bdd -> varSet -> bdd */ 500EXTERNML value mlbdd_bdd_exist(value b1, value varset) /* ML */ 501{ 502 return mlbdd_make(bdd_exist(Bdd_val(b1),Bdd_val(varset))); 503} 504 505/* ML type: bdd -> varSet -> bdd */ 506EXTERNML value mlbdd_bdd_forall(value b1, value varset) /* ML */ 507{ 508 return mlbdd_make(bdd_forall(Bdd_val(b1),Bdd_val(varset))); 509} 510 511/* ML type: bdd -> bdd -> int -> varSet -> bdd */ 512EXTERNML value mlbdd_bdd_appall(value left, value right, 513 value opr, value varset) /* ML */ 514{ 515 return mlbdd_make(bdd_appall(Bdd_val(left),Bdd_val(right), 516 Int_val(opr), Bdd_val(varset))); 517} 518 519/* ML type: bdd -> bdd -> int -> varSet -> bdd */ 520EXTERNML value mlbdd_bdd_appex(value left, value right, 521 value opr, value varset) /* ML */ 522{ 523 return mlbdd_make(bdd_appex(Bdd_val(left),Bdd_val(right), 524 Int_val(opr), Bdd_val(varset))); 525} 526 527 528/* Some helper for making BddPairs, which on the ML side is called 529 pairSet. pairSet is implemented very similar to bdd, i.e. as 530 finalized objects. */ 531#define PairSet_val(x) (((bddPair **) (x)) [1]) // Also an l-value 532 533 534void mlbdd_pair_finalize(value pairset) 535{ 536 bdd_freepair(PairSet_val(pairset)); 537} 538 539/* ML type: varnum vector -> varnum vector -> pairSet */ 540EXTERNML value mlbdd_makepairset(value oldvar, value newvar) /* ML */ 541{ 542 int size, i, *o, *n; 543 bddPair *pairs; 544 value result; 545 546 size = Wosize_val(oldvar); 547 548 /* we use stat_alloc which guarantee that we get the memory (or it 549 will raise an exception). */ 550 o = (int *) stat_alloc(sizeof(int) * size); 551 n = (int *) stat_alloc(sizeof(int) * size); 552 553 for (i=0; i<size; i++) { 554 o[i] = Int_val(Field(oldvar, i)); 555 n[i] = Int_val(Field(newvar, i)); 556 } 557 558 pairs = bdd_newpair(); 559 bdd_setpairs(pairs, o, n, size); 560 561 /* memory allocated with stat_alloc, should be freed with 562 stat_free.*/ 563 stat_free((char *) o); 564 stat_free((char *) n); 565 566 result = mlbdd_alloc_final(2, &mlbdd_pair_finalize); 567 PairSet_val(result) = pairs; 568 569 return result; 570} 571 572 573/* ML type: varnum vector -> bdd vector -> pairSet */ 574EXTERNML value mlbdd_makebddpairset(value oldvar, value newvar) /* ML */ 575{ 576 int size, i, *o, *n; 577 bddPair *pairs; 578 value result; 579 580 size = Wosize_val(oldvar); 581 582 /* we use stat_alloc which guarantee that we get the memory (or it 583 will raise an exception). */ 584 o = (int *) stat_alloc(sizeof(int) * size); 585 n = (BDD *) stat_alloc(sizeof(int) * size); 586 587 for (i=0; i<size; i++) { 588 o[i] = Int_val(Field(oldvar, i)); 589 n[i] = Bdd_val(Field(newvar, i)); 590 } 591 592 pairs = bdd_newpair(); 593 bdd_setbddpairs(pairs, o, n, size); 594 595 /* memory allocated with stat_alloc, should be freed with 596 stat_free.*/ 597 stat_free((char *) o); 598 stat_free((char *) n); 599 600 result = mlbdd_alloc_final(2, &mlbdd_pair_finalize); 601 PairSet_val(result) = pairs; 602 603 return result; 604} 605 606 607 608/* ML type: bdd -> pairSet -> bdd */ 609EXTERNML value mlbdd_bdd_replace(value r, value pair) /* ML */ 610{ 611 return mlbdd_make(bdd_replace(Bdd_val(r), PairSet_val(pair))); 612} 613 614 615/* ML type: pairSet -> bdd -> bdd */ 616EXTERNML value mlbdd_bdd_veccompose(value pair, value r) /* ML */ 617{ 618 return mlbdd_make(bdd_veccompose(Bdd_val(r), PairSet_val(pair))); 619} 620 621 622/* REORDER FUNCTIONS */ 623 624/* ML type: varnum -> varnum -> fixed -> unit */ 625EXTERNML value mlbdd_bdd_intaddvarblock(value first, value last, value fixed) /* ML */ 626{ 627 bdd_intaddvarblock(Int_val(first), Int_val(last), Int_val(fixed)); 628 return Val_unit; 629} 630 631/* ML type: unit -> unit */ 632EXTERNML value mlbdd_bdd_clrvarblocks(value dummy) /* ML */ 633{ 634 bdd_clrvarblocks(); 635 return dummy; 636} 637 638/* ML type: method -> unit */ 639EXTERNML value mlbdd_bdd_reorder(value method) /* ML */ 640{ 641 bdd_reorder(Int_val(method)); 642 return Val_unit; 643} 644 645/* ML type: method -> method */ 646EXTERNML value mlbdd_bdd_autoreorder(value method) /* ML */ 647{ 648 return Val_long(bdd_autoreorder(Int_val(method))); 649} 650 651/* ML type: method -> int -> method */ 652EXTERNML value mlbdd_bdd_autoreorder_times(value method, value times) /* ML */ 653{ 654 return Val_long(bdd_autoreorder_times(Int_val(method), Int_val(times))); 655} 656 657 658/* ML type: unit -> method */ 659EXTERNML value mlbdd_bdd_getreorder_method(value dummy) /* ML */ 660{ 661 return Val_long(bdd_getreorder_method()); 662 663} 664 665/* ML type: unit -> int */ 666EXTERNML value mlbdd_bdd_getreorder_times(value dummy) /* ML */ 667{ 668 return Val_long(bdd_getreorder_times()); 669} 670 671 672/* ML type: unit -> unit */ 673EXTERNML value mlbdd_bdd_disable_reorder(value dummy) /* ML */ 674{ 675 bdd_disable_reorder(); 676 return dummy; 677} 678 679/* ML type: unit -> unit */ 680EXTERNML value mlbdd_bdd_enable_reorder(value dummy) /* ML */ 681{ 682 bdd_enable_reorder(); 683 return dummy; 684} 685 686 687/* ML type: varnum -> level */ 688EXTERNML value mlbdd_bdd_var2level(value num) /* ML */ 689{ 690 return Val_long(bdd_var2level(Int_val(num))); 691} 692 693/* ML type: level -> varnum */ 694EXTERNML value mlbdd_bdd_level2var(value lev) /* ML */ 695{ 696 return Val_long(bdd_level2var(Int_val(lev))); 697} 698 699/* FDD FUNCTIONS */ 700 701/* ML type: int vector -> fddvar */ 702EXTERNML value mlfdd_extdomain(value vector) /* ML */ 703{ 704 int size, i, *v,k; 705 value result; 706 707 size = Wosize_val(vector); 708 709 /* we use stat_alloc which guarantee that we get the memory (or it 710 will raise an exception). */ 711 v = (int *) stat_alloc(sizeof(int) * size); 712 for (i=0; i<size; i++) { 713 v[i] = Int_val(Field(vector, i)); 714 } 715 k = fdd_extdomain(v, size); 716 result = Val_int(k); 717 718 /* memory allocated with stat_alloc, should be freed with 719 stat_free.*/ 720 stat_free((char *) v); 721 722 return result; 723} 724 725/* ML type: unit -> unit */ 726EXTERNML value mlfdd_clearall(value foo) /* ML */ 727{ 728 fdd_clearall(); 729 730 return Val_unit; 731} 732 733/* ML type: unit -> int */ 734EXTERNML value mlfdd_domainnum(value foo) /* ML */ 735{ 736 return Val_int(fdd_domainnum()); 737} 738 739/* ML type: fddvar -> int */ 740EXTERNML value mlfdd_domainsize(value var) /* ML */ 741{ 742 return Val_int(fdd_domainsize(Int_val(var))); 743} 744 745/* ML type: fddvar -> int */ 746EXTERNML value mlfdd_varnum(value var) /* ML */ 747{ 748 return Val_int(fdd_varnum(Int_val(var))); 749} 750 751/* ML type: fddvar -> varnum vector */ 752EXTERNML value mlfdd_vars(value var) /* ML */ 753{ 754 value result; 755 int *v, n, i; 756 757 n = fdd_varnum(Int_val(var)); 758 v = fdd_vars(Int_val(var)); 759 760 if(n == 0) 761 result = Atom(0); /* The empty vector */ 762 else { 763 result = n < Max_young_wosize ? alloc(n, 0) : alloc_shr(n, 0); 764 for (i = 0; i < n; i++) { 765 Field(result, i) = Val_long(v[i]); 766 } 767 free(v); 768 } 769 770 return result; 771} 772 773/* ML type: fddvar -> varSet */ 774EXTERNML value mlfdd_ithset(value var) /* ML */ 775{ 776 return mlbdd_make(fdd_ithset(Int_val(var))); 777} 778 779/* ML type: fddvar -> bdd */ 780EXTERNML value mlfdd_domain(value var) /* ML */ 781{ 782 return mlbdd_make(fdd_domain(Int_val(var))); 783} 784 785/* ML type: fddvar vector -> varSet */ 786EXTERNML value mlfdd_makeset(value vector) /* ML */ 787{ 788 int size, i, *v; 789 value result; 790 791 size = Wosize_val(vector); 792 793 /* we use stat_alloc which guarantee that we get the memory (or it 794 will raise an exception). */ 795 v = (int *) stat_alloc(sizeof(int) * size); 796 for (i=0; i<size; i++) { 797 v[i] = Int_val(Field(vector, i)); 798 } 799 800 result = mlbdd_make(fdd_makeset(v, size)); 801 802 /* memory allocated with stat_alloc, should be freed with 803 stat_free.*/ 804 stat_free((char *) v); 805 806 return result; 807} 808 809 810/* ML type: fddvar vector -> fddvar vector -> pairSet */ 811EXTERNML value mlfdd_setpairs(value oldvar, value newvar) /* ML */ 812{ 813 int size, i, *o, *n; 814 bddPair *pairs; 815 value result; 816 817 size = Wosize_val(oldvar); 818 819 /* we use stat_alloc which guarantee that we get the memory (or it 820 will raise an exception). */ 821 o = (int *) stat_alloc(sizeof(int) * size); 822 n = (int *) stat_alloc(sizeof(int) * size); 823 824 for (i=0; i<size; i++) { 825 o[i] = Int_val(Field(oldvar, i)); 826 n[i] = Int_val(Field(newvar, i)); 827 } 828 829 pairs = bdd_newpair(); 830 fdd_setpairs(pairs, o, n, size); 831 832 /* memory allocated with stat_alloc, should be freed with 833 stat_free.*/ 834 stat_free((char *) o); 835 stat_free((char *) n); 836 837 result = mlbdd_alloc_final(2, &mlbdd_pair_finalize); 838 PairSet_val(result) = pairs; 839 840 return result; 841} 842 843/* BVEC FUNCTIONS */ 844 845#define bvecbitnum_val(x) (((int*) (x)) [1]) 846#define bvecbitvec_val(x) (((BDD**) (x)) [2]) 847 848BVEC BVEC_val(value obj) { 849 BVEC t; 850 t.bitnum=bvecbitnum_val(obj); 851 t.bitvec=bvecbitvec_val(obj); 852 return t; 853} 854 855/* When the bvec becomes unreachable from the ML process, it will be 856 garbage-collected, mlbdd_finalize_bvec() will be called on the bvec, 857 which will do the necessary bvec-bookkeeping. */ 858void mlbdd_finalize_bvec(value obj) 859{ 860 bvec_free(BVEC_val(obj)); 861} 862 863/* Creation of a bvec makes a finalized pair (mlbdd_finalize, bitnum, bitvec) */ 864EXTERNML value mlbdd_make_bvec(BVEC v) 865{ 866 value res; 867 res = mlbdd_alloc_final(3, &mlbdd_finalize_bvec); 868 bvecbitnum_val(res) = v.bitnum; 869 bvecbitvec_val(res) = v.bitvec; /* Hopefully a pointer fits in a long */ 870 return res; 871} 872 873/* ML type: precision -> bvec */ 874EXTERNML value mlbvec_true(value bits) { 875 return mlbdd_make_bvec(bvec_true(Int_val(bits))); 876} 877 878/* ML type: precision -> bvec */ 879EXTERNML value mlbvec_false(value bits) { 880 return mlbdd_make_bvec(bvec_false(Int_val(bits))); 881} 882 883/* ML type: precision -> const -> bvec */ 884EXTERNML value mlbvec_con(value bits, value val) /* ML */ 885{ 886 return mlbdd_make_bvec(bvec_con(Int_val(bits), Int_val(val))); 887} 888 889/* ML type: precision -> varnum -> int -> bvec */ 890EXTERNML value mlbvec_var(value bits, value var, value step) /* ML */ 891{ 892 return mlbdd_make_bvec(bvec_var(Int_val(bits), Int_val(var), Int_val(step))); 893} 894 895/* ML type: bvecvar -> bvec */ 896EXTERNML value mlbvec_varfdd(value var) /* ML */ 897{ 898 return mlbdd_make_bvec(bvec_varfdd(Int_val(var))); 899} 900 901/* ML type: precision -> bvec -> bvec */ 902EXTERNML value mlbvec_coerce(value bits, value v) /* ML */ 903{ 904 return mlbdd_make_bvec(bvec_coerce(Int_val(bits), BVEC_val(v))); 905} 906 907/* ML type: bvec -> bool */ 908EXTERNML value mlbvec_isconst(value v) /* ML */ 909{ 910 return bvec_isconst(BVEC_val(v)) ? Val_true : Val_false; 911} 912 913/* ML type: bvec -> bool */ 914EXTERNML value mlbvec_getconst(value v) /* ML */ 915{ 916 if(bvec_isconst(BVEC_val(v))) { 917 return Val_int(bvec_val(BVEC_val(v))); 918 } 919 else { 920 RAISE_DOMAIN; 921 return Val_unit; /* unreachable, here to prevent warnings */ 922 } 923} 924 925/* ML type: bvec -> bvec -> bvec */ 926EXTERNML value mlbvec_add(value s1, value s2) /* ML */ 927{ 928 return mlbdd_make_bvec(bvec_add(BVEC_val(s1), BVEC_val(s2))); 929} 930 931/* ML type: bvec -> bvec -> bvec */ 932EXTERNML value mlbvec_sub(value s1, value s2) /* ML */ 933{ 934 return mlbdd_make_bvec(bvec_sub(BVEC_val(s1), BVEC_val(s2))); 935} 936 937/* ML type: bvec -> const -> bvec */ 938EXTERNML value mlbvec_mulfixed(value s1, value con) /* ML */ 939{ 940 return mlbdd_make_bvec(bvec_mulfixed(BVEC_val(s1), Int_val(con))); 941} 942 943/* ML type: bvec -> bvec -> bvec */ 944EXTERNML value mlbvec_mul(value s1, value s2) /* ML */ 945{ 946 return mlbdd_make_bvec(bvec_mul(BVEC_val(s1), BVEC_val(s2))); 947} 948 949 950/* ML type: bvec -> const -> bvec * bvec */ 951EXTERNML value mlbvec_divfixed(value s1, value con) /* ML */ 952{ 953 BVEC res, rem; 954 Push_roots(result, 1); 955 bvec_divfixed(BVEC_val(s1), Int_val(con), &res, &rem); 956 result[0] = alloc_tuple(2); 957 Field(result[0], 0) = mlbdd_make_bvec(res); 958 Field(result[0], 0) = mlbdd_make_bvec(rem); 959 Pop_roots(); 960 return result[0]; 961} 962 963/* ML type: bvec -> bvec -> bvec * bvec */ 964EXTERNML value mlbvec_div(value s1, value s2) /* ML */ 965{ 966 BVEC res, rem; 967 Push_roots(result, 1); 968 bvec_div(BVEC_val(s1), BVEC_val(s2), &res, &rem); 969 result[0] = alloc_tuple(2); 970 Field(result[0], 0) = mlbdd_make_bvec(res); 971 Field(result[0], 0) = mlbdd_make_bvec(rem); 972 Pop_roots(); 973 return result[0]; 974} 975 976 977 978/* ML type: bvec -> bvec -> bdd -> bvec */ 979EXTERNML value mlbvec_shl(value s1, value c, value b) /* ML */ 980{ 981 return mlbdd_make_bvec(bvec_shl(BVEC_val(s1), BVEC_val(c), Bdd_val(b))); 982} 983 984/* ML type: bvec -> const -> bdd -> bvec */ 985EXTERNML value mlbvec_shlfixed(value s1, value c, value b) /* ML */ 986{ 987 return mlbdd_make_bvec(bvec_shlfixed(BVEC_val(s1), Int_val(c), Bdd_val(b))); 988} 989 990/* ML type: bvec -> bvec -> bdd -> bvec */ 991EXTERNML value mlbvec_shr(value s1, value c, value b) /* ML */ 992{ 993 return mlbdd_make_bvec(bvec_shr(BVEC_val(s1), BVEC_val(c), Bdd_val(b))); 994} 995 996/* ML type: bvec -> const -> bdd -> bvec */ 997EXTERNML value mlbvec_shrfixed(value s1, value c, value b) /* ML */ 998{ 999 return mlbdd_make_bvec(bvec_shrfixed(BVEC_val(s1), Int_val(c), Bdd_val(b))); 1000} 1001 1002/* ML type: bvec -> bvec -> bdd */ 1003EXTERNML value mlbvec_lth(value s1, value s2) /* ML */ 1004{ 1005 return mlbdd_make(bvec_lth(BVEC_val(s1), BVEC_val(s2))); 1006} 1007 1008/* ML type: bvec -> bvec -> bdd */ 1009EXTERNML value mlbvec_lte(value s1, value s2) /* ML */ 1010{ 1011 return mlbdd_make(bvec_lte(BVEC_val(s1), BVEC_val(s2))); 1012} 1013 1014/* ML type: bvec -> bvec -> bdd */ 1015EXTERNML value mlbvec_gth(value s1, value s2) /* ML */ 1016{ 1017 return mlbdd_make(bvec_gth(BVEC_val(s1), BVEC_val(s2))); 1018} 1019 1020/* ML type: bvec -> bvec -> bdd */ 1021EXTERNML value mlbvec_gte(value s1, value s2) /* ML */ 1022{ 1023 return mlbdd_make(bvec_gte(BVEC_val(s1), BVEC_val(s2))); 1024} 1025 1026/* ML type: bvec -> bvec -> bdd */ 1027EXTERNML value mlbvec_equ(value s1, value s2) /* ML */ 1028{ 1029 return mlbdd_make(bvec_equ(BVEC_val(s1), BVEC_val(s2))); 1030} 1031 1032/* ML type: bvec -> bvec -> bdd */ 1033EXTERNML value mlbvec_neq(value s1, value s2) /* ML */ 1034{ 1035 return mlbdd_make(bvec_neq(BVEC_val(s1), BVEC_val(s2))); 1036} 1037