1/*======================================================================== 2 Copyright (C) 1996-2001 by Jorn Lind-Nielsen 3 All rights reserved 4 5 Permission is hereby granted, without written agreement and without 6 license or royalty fees, to use, reproduce, prepare derivative 7 works, distribute, and display this software and its documentation 8 for any purpose, provided that (1) the above copyright notice and 9 the following two paragraphs appear in all copies of the source code 10 and (2) redistributions, including without limitation binaries, 11 reproduce these notices in the supporting documentation. Substantial 12 modifications to this software may be copyrighted by their authors 13 and need not follow the licensing terms described here, provided 14 that the new terms are clearly indicated in all files where they apply. 15 16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 21 22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 27 MODIFICATIONS. 28========================================================================*/ 29 30/************************************************************************* 31 $Header$ 32 FILE: fdd.c 33 DESCR: Finite domain extensions to BDD package 34 AUTH: Jorn Lind 35 DATE: (C) june 1997 36 37 NOTE: If V1,...,Vn is BDD vars for a FDD, then Vn is the Least Sign. Bit 38*************************************************************************/ 39#include <stdlib.h> 40#include <string.h> 41#include "kernel.h" 42#include "fdd.h" 43 44 45static void fdd_printset_rec(FILE *, int, int *); 46 47/*======================================================================*/ 48/* NOTE: ALL FDD operations works with LSB in top of the variable order */ 49/* and in index zero of the domain tables */ 50/*======================================================================*/ 51 52typedef struct s_Domain 53{ 54 int realsize; /* The specified domain (0...N-1) */ 55 int binsize; /* The number of BDD variables representing the domain */ 56 int *ivar; /* Variable indeces for the variable set */ 57 BDD var; /* The BDD variable set */ 58} Domain; 59 60 61static void Domain_allocate(Domain*, int); 62static void Domain_done(Domain*); 63 64static int firstbddvar; 65static int fdvaralloc; /* Number of allocated domains */ 66static int fdvarnum; /* Number of defined domains */ 67static Domain *domain; /* Table of domain sizes */ 68 69static bddfilehandler filehandler; 70 71/************************************************************************* 72 Domain definition 73*************************************************************************/ 74 75void bdd_fdd_init(void) 76{ 77 domain = NULL; 78 fdvarnum = fdvaralloc = 0; 79 firstbddvar = 0; 80} 81 82 83void bdd_fdd_done(void) 84{ 85 int n; 86 87 if (domain != NULL) 88 { 89 for (n=0 ; n<fdvarnum ; n++) 90 Domain_done(&domain[n]); 91 free(domain); 92 } 93 94 domain = NULL; 95} 96 97 98/* 99NAME {* fdd\_extdomain *} 100SECTION {* fdd *} 101SHORT {* adds another set of finite domain blocks *} 102PROTO {* int fdd_extdomain(int *dom, int num) *} 103DESCR {* Extends the set of finite domain blocks with the {\tt num} 104 domains in 105 {\tt dom}. Each entry in {\tt dom} defines the size of a new 106 finite domain which later on can be used for finite state machine 107 traversal and other operations on finte domains. Each domain 108 allocates $\log_2(|dom[i]|)$ BDD variables to be used later. 109 The ordering is interleaved for the domains defined in each 110 call to {\tt bdd\_extdomain}. This means that assuming domain 111 $D_0$ needs 2 BDD variables $x_1$ and $x_2$, and another domain 112 $D_1$ needs 4 BDD variables $y_1,y_2,y_3$ and $y_4$, then the 113 order will be $x_1,y_1,x_2,y_2,y_3,y_4$. The index of the first 114 domain in {\tt dom} is returned. The index of the other domains 115 are offset from this index with the same offset as in {\tt dom}. 116 117 The BDD variables needed to encode the domain are created for the 118 purpose and do not interfere with the BDD variables already in 119 use. *} 120RETURN {* The index of the first domain or a negative error code. *} 121ALSO {* fdd\_ithvar, fdd\_equals, fdd\_overlapdomain *} 122*/ 123int fdd_extdomain(int *dom, int num) 124{ 125 int offset = fdvarnum; 126 int binoffset; 127 int extravars = 0; 128 int n, bn, more; 129 130 if (!bddrunning) 131 return bdd_error(BDD_RUNNING); 132 133 /* Build domain table */ 134 if (domain == NULL) /* First time */ 135 { 136 fdvaralloc = num; 137 if ((domain=(Domain*)malloc(sizeof(Domain)*num)) == NULL) 138 return bdd_error(BDD_MEMORY); 139 } 140 else /* Allocated before */ 141 { 142 if (fdvarnum + num > fdvaralloc) 143 { 144 fdvaralloc += (num > fdvaralloc) ? num : fdvaralloc; 145 146 domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc); 147 if (domain == NULL) 148 return bdd_error(BDD_MEMORY); 149 } 150 } 151 152 /* Create bdd variable tables */ 153 for (n=0 ; n<num ; n++) 154 { 155 Domain_allocate(&domain[n+fdvarnum], dom[n]); 156 extravars += domain[n+fdvarnum].binsize; 157 } 158 159 binoffset = firstbddvar; 160 if (firstbddvar + extravars > bddvarnum) 161 bdd_setvarnum(firstbddvar + extravars); 162 163 /* Set correct variable sequence (interleaved) */ 164 for (bn=0,more=1 ; more ; bn++) 165 { 166 more = 0; 167 168 for (n=0 ; n<num ; n++) 169 if (bn < domain[n+fdvarnum].binsize) 170 { 171 more = 1; 172 domain[n+fdvarnum].ivar[bn] = binoffset++; 173 } 174 } 175 176 for (n=0 ; n<num ; n++) 177 { 178 domain[n+fdvarnum].var = bdd_makeset(domain[n+fdvarnum].ivar, 179 domain[n+fdvarnum].binsize); 180 bdd_addref(domain[n+fdvarnum].var); 181 } 182 183 fdvarnum += num; 184 firstbddvar += extravars; 185 186 return offset; 187} 188 189 190/* 191NAME {* fdd\_overlapdomain *} 192SECTION {* fdd *} 193SHORT {* combine two FDD blocks into one *} 194PROTO {* int fdd_overlapdomain(int v1, int v2) *} 195DESCR {* This function takes two FDD blocks and merges them into a new one, 196 such that the new one is encoded using both sets of BDD variables. 197 If {\tt v1} is encoded using the BDD variables $a_1, \ldots, 198 a_n$ and has a domain of $[0,N_1]$, and {\tt v2} is encoded using 199 $b_1, \ldots, b_n$ and has a domain of $[0,N_2]$, then the result 200 will be encoded using the BDD variables $a_1, \ldots, a_n, b_1, 201 \ldots, b_n$ and have the domain $[0,N_1*N_2]$. The use of this 202 function may result in some strange output from 203 {\tt fdd\_printset}. *} 204RETURN {* The index of the finite domain block *} 205ALSO {* fdd\_extdomain *} 206*/ 207int fdd_overlapdomain(int v1, int v2) 208{ 209 Domain *d; 210 int n; 211 212 if (!bddrunning) 213 return bdd_error(BDD_RUNNING); 214 215 if (v1 < 0 || v1 >= fdvarnum || v2 < 0 || v2 >= fdvarnum) 216 return bdd_error(BDD_VAR); 217 218 if (fdvarnum + 1 > fdvaralloc) 219 { 220 fdvaralloc += fdvaralloc; 221 222 domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc); 223 if (domain == NULL) 224 return bdd_error(BDD_MEMORY); 225 } 226 227 d = &domain[fdvarnum]; 228 d->realsize = domain[v1].realsize * domain[v2].realsize; 229 d->binsize = domain[v1].binsize + domain[v2].binsize; 230 d->ivar = (int *)malloc(sizeof(int)*d->binsize); 231 232 for (n=0 ; n<domain[v1].binsize ; n++) 233 d->ivar[n] = domain[v1].ivar[n]; 234 for (n=0 ; n<domain[v2].binsize ; n++) 235 d->ivar[domain[v1].binsize+n] = domain[v2].ivar[n]; 236 237 d->var = bdd_makeset(d->ivar, d->binsize); 238 bdd_addref(d->var); 239 240 return fdvarnum++; 241} 242 243 244/* 245NAME {* fdd\_clearall *} 246SECTION {* fdd *} 247SHORT {* clear all allocated FDD blocks *} 248PROTO {* void fdd_clearall(void) *} 249DESCR {* Removes all defined finite domain blocks defined by 250 {\tt fdd\_extdomain()} and {\tt fdd\_overlapdomain()} *} 251*/ 252void fdd_clearall(void) 253{ 254 bdd_fdd_done(); 255 bdd_fdd_init(); 256} 257 258 259/************************************************************************* 260 FDD helpers 261*************************************************************************/ 262 263/* 264NAME {* fdd\_domainnum *} 265SECTION {* fdd *} 266SHORT {* number of defined finite domain blocks *} 267PROTO {* int fdd_domainnum(void) *} 268DESCR {* Returns the number of finite domain blocks define by calls to 269 {\tt bdd\_extdomain}. *} 270RETURN {* The number of defined finite domain blocks 271 or a negative error code *} 272ALSO {* fdd\_domainsize, fdd\_extdomain *} 273*/ 274int fdd_domainnum(void) 275{ 276 if (!bddrunning) 277 return bdd_error(BDD_RUNNING); 278 279 return fdvarnum; 280} 281 282 283/* 284NAME {* fdd\_domainsize *} 285SECTION {* fdd *} 286SHORT {* real size of a finite domain block *} 287PROTO {* int fdd_domainsize(int var) *} 288DESCR {* Returns the size of the domain for the finite domain 289 block {\tt var}. *} 290RETURN {* The size or a negative error code *} 291ALSO {* fdd\_domainnum *} 292*/ 293int fdd_domainsize(int v) 294{ 295 if (!bddrunning) 296 return bdd_error(BDD_RUNNING); 297 298 if (v < 0 || v >= fdvarnum) 299 return bdd_error(BDD_VAR); 300 return domain[v].realsize; 301} 302 303 304/* 305NAME {* fdd\_varnum *} 306SECTION {* fdd *} 307SHORT {* binary size of a finite domain block *} 308PROTO {* int fdd_varnum(int var) *} 309DESCR {* Returns the number of BDD variables used for the finite domain 310 block {\tt var}. *} 311RETURN {* The number of variables or a negative error code *} 312ALSO {* fdd\_vars *} 313*/ 314int fdd_varnum(int v) 315{ 316 if (!bddrunning) 317 return bdd_error(BDD_RUNNING); 318 319 if (v >= fdvarnum || v < 0) 320 return bdd_error(BDD_VAR); 321 return domain[v].binsize; 322} 323 324 325/* 326NAME {* fdd\_vars *} 327SECTION {* fdd *} 328SHORT {* all BDD variables associated with a finite domain block *} 329PROTO {* int *fdd_vars(int var) *} 330DESCR {* Returns an integer array containing the BDD variables used to 331 define the finite domain block {\tt var}. The size of the array 332 is the number of variables used to define the finite domain block. 333 The array will have the Least Significant Bit at pos 0. The 334 array must {\em not} be deallocated. *} 335RETURN {* Integer array contaning the variable numbers or NULL if 336 {\tt v} is an unknown block. *} 337ALSO {* fdd\_varnum *} 338*/ 339int *fdd_vars(int v) 340{ 341 if (!bddrunning) 342 { 343 bdd_error(BDD_RUNNING); 344 return NULL; 345 } 346 347 if (v >= fdvarnum || v < 0) 348 { 349 bdd_error(BDD_VAR); 350 return NULL; 351 } 352 353 return domain[v].ivar; 354} 355 356 357 358/************************************************************************* 359 FDD primitives 360*************************************************************************/ 361 362/* 363NAME {* fdd\_ithvar *} 364SECTION {* fdd *} 365SHORT {* the BDD for the i'th FDD set to a specific value *} 366PROTO {* BDD fdd_ithvar(int var, int val) *} 367DESCR {* Returns the BDD that defines the value {\tt val} for the 368 finite domain block {\tt var}. The encoding places the 369 Least Significant Bit at the top of the BDD tree 370 (which means they will have the lowest variable index). 371 The returned BDD will be $V_0 \conj V_1 \conj \ldots 372 \conj V_N$ where each $V_i$ will be in positive or negative form 373 depending on the value of {\tt val}. *} 374RETURN {* The correct BDD or the constant false BDD on error. *} 375ALSO {* fdd\_ithset *} 376*/ 377BDD fdd_ithvar(int var, int val) 378{ 379 int n; 380 int v=1, tmp; 381 382 if (!bddrunning) 383 { 384 bdd_error(BDD_RUNNING); 385 return bddfalse; 386 } 387 388 if (var < 0 || var >= fdvarnum) 389 { 390 bdd_error(BDD_VAR); 391 return bddfalse; 392 } 393 394 if (val < 0 || val >= domain[var].realsize) 395 { 396 bdd_error(BDD_RANGE); 397 return bddfalse; 398 } 399 400 for (n=0 ; n<domain[var].binsize ; n++) 401 { 402 bdd_addref(v); 403 404 if (val & 0x1) 405 tmp = bdd_apply(bdd_ithvar(domain[var].ivar[n]), v, bddop_and); 406 else 407 tmp = bdd_apply(bdd_nithvar(domain[var].ivar[n]), v, bddop_and); 408 409 bdd_delref(v); 410 v = tmp; 411 val >>= 1; 412 } 413 414 return v; 415} 416 417 418/* 419NAME {* fdd\_scanvar *} 420SECTION {* fdd *} 421SHORT {* Finds one satisfying value of a FDD variable *} 422PROTO {* int fdd_scanvar(BDD r, int var) *} 423DESCR {* Finds one satisfying assignment of the FDD variable {\tt var} in the 424 BDD {\tt r} and returns this value. *} 425RETURN {* The value of a satisfying assignment of {\tt var}. If {\tt r} is 426 the trivially false BDD, then a negative value is returned. *} 427ALSO {* fdd\_scanallvar *} 428*/ 429int fdd_scanvar(BDD r, int var) 430{ 431 int *allvar; 432 int res; 433 434 CHECK(r); 435 if (r == bddfalse) 436 return -1; 437 if (var < 0 || var >= fdvarnum) 438 return bdd_error(BDD_VAR); 439 440 allvar = fdd_scanallvar(r); 441 res = allvar[var]; 442 free(allvar); 443 444 return res; 445} 446 447 448/* 449NAME {* fdd\_scanallvar *} 450SECTION {* fdd *} 451SHORT {* Finds one satisfying value of all FDD variables *} 452PROTO {* int* fdd_scanallvar(BDD r) *} 453DESCR {* Finds one satisfying assignment in {\tt r} of all the defined 454 FDD variables. Each value is stored in an array which is 455 returned. The size of this array is exactly the number of 456 FDD variables defined. It is the user's responsibility to 457 free this array using {\tt free()}. *} 458RETURN {* An array with all satisfying values. If {\tt r} is the trivially 459 false BDD, then NULL is returned. *} 460ALSO {* fdd\_scanvar *} 461*/ 462int* fdd_scanallvar(BDD r) 463{ 464 int n; 465 char *store; 466 int *res; 467 BDD p = r; 468 469 CHECKa(r,NULL); 470 if (r == bddfalse) 471 return NULL; 472 473 store = NEW(char,bddvarnum); 474 for (n=0 ; n<bddvarnum ; n++) 475 store[n] = 0; 476 477 while (!ISCONST(p)) 478 { 479 if (!ISZERO(LOW(p))) 480 { 481 store[bddlevel2var[LEVEL(p)]] = 0; 482 p = LOW(p); 483 } 484 else 485 { 486 store[bddlevel2var[LEVEL(p)]] = 1; 487 p = HIGH(p); 488 } 489 } 490 491 res = NEW(int, fdvarnum); 492 493 for (n=0 ; n<fdvarnum ; n++) 494 { 495 int m; 496 int val=0; 497 498 for (m=domain[n].binsize-1 ; m>=0 ; m--) 499 if ( store[domain[n].ivar[m]] ) 500 val = val*2 + 1; 501 else 502 val = val*2; 503 504 res[n] = val; 505 } 506 507 free(store); 508 509 return res; 510} 511 512/* 513NAME {* fdd\_ithset *} 514SECTION {* fdd *} 515SHORT {* the variable set for the i'th finite domain block *} 516PROTO {* BDD fdd_ithset(int var) *} 517DESCR {* Returns the variable set that contains the variables used to 518 define the finite domain block {\tt var}. *} 519RETURN {* The variable set or the constant false BDD on error. *} 520ALSO {* fdd\_ithvar *} 521*/ 522BDD fdd_ithset(int var) 523{ 524 if (!bddrunning) 525 { 526 bdd_error(BDD_RUNNING); 527 return bddfalse; 528 } 529 530 if (var < 0 || var >= fdvarnum) 531 { 532 bdd_error(BDD_VAR); 533 return bddfalse; 534 } 535 536 return domain[var].var; 537} 538 539/* 540NAME {* fdd\_domain *} 541SECTION {* fdd *} 542SHORT {* BDD encoding of the domain of a FDD variable *} 543PROTO {* BDD fdd_domain(int var) *} 544DESCR {* Returns what corresponds to a disjunction of all possible 545 values of the variable {\tt var}. 546 This is more efficient than doing 547 {\tt fdd\_ithvar(var,0) OR fdd\_ithvar(var,1) ...} explicitely 548 for all values in the domain of {\tt var}. *} 549RETURN {* The encoding of the domain*} 550*/ 551BDD fdd_domain(int var) 552{ 553 int n,val; 554 Domain *dom; 555 BDD d; 556 557 if (!bddrunning) 558 { 559 bdd_error(BDD_RUNNING); 560 return bddfalse; 561 } 562 563 if (var < 0 || var >= fdvarnum) 564 { 565 bdd_error(BDD_VAR); 566 return bddfalse; 567 } 568 569 /* Encode V<=X-1. V is the variables in 'var' and X is the domain size */ 570 571 dom = &domain[var]; 572 val = dom->realsize-1; 573 d = bddtrue; 574 575 for (n=0 ; n<dom->binsize ; n++) 576 { 577 BDD tmp; 578 579 if (val & 0x1) 580 tmp = bdd_apply( bdd_nithvar(dom->ivar[n]), d, bddop_or ); 581 else 582 tmp = bdd_apply( bdd_nithvar(dom->ivar[n]), d, bddop_and ); 583 584 val >>= 1; 585 586 bdd_addref(tmp); 587 bdd_delref(d); 588 d = tmp; 589 } 590 591 return d; 592} 593 594 595/* 596NAME {* fdd\_equals *} 597SECTION {* fdd *} 598SHORT {* returns a BDD setting two FD. blocks equal *} 599PROTO {* BDD fdd_equals(int f, int g) *} 600DESCR {* Builds a BDD which is true for all the possible assignments to 601 the variable blocks {\tt f} and {\tt g} that makes the blocks 602 equal. This is more or less just a shorthand for calling 603 {\tt fdd\_equ()}. *} 604RETURN {* The correct BDD or the constant false on errors. *} 605*/ 606BDD fdd_equals(int left, int right) 607{ 608 BDD e = bddtrue, tmp1, tmp2; 609 int n; 610 611 if (!bddrunning) 612 { 613 bdd_error(BDD_RUNNING); 614 return bddfalse; 615 } 616 617 if (left < 0 || left >= fdvarnum || right < 0 || right >= fdvarnum) 618 { 619 bdd_error(BDD_VAR); 620 return bddfalse; 621 } 622 if (domain[left].realsize != domain[right].realsize) 623 { 624 bdd_error(BDD_RANGE); 625 return bddfalse; 626 } 627 628 for (n=0 ; n<domain[left].binsize ; n++) 629 { 630 tmp1 = bdd_addref( bdd_apply(bdd_ithvar(domain[left].ivar[n]), 631 bdd_ithvar(domain[right].ivar[n]), 632 bddop_biimp) ); 633 634 tmp2 = bdd_addref( bdd_apply(e, tmp1, bddop_and) ); 635 bdd_delref(tmp1); 636 bdd_delref(e); 637 e = tmp2; 638 } 639 640 bdd_delref(e); 641 return e; 642} 643 644 645/************************************************************************* 646 File IO 647*************************************************************************/ 648 649/* 650NAME {* fdd\_file\_hook *} 651SECTION {* fdd *} 652SHORT {* Specifies a printing callback handler *} 653PROTO {* bddfilehandler fdd_file_hook(bddfilehandler handler) *} 654DESCR {* A printing callback handler for use with FDDs is used to 655 convert the FDD integer identifier into something readable by the 656 end user. Typically the handler will print a string name 657 instead of the identifier. A handler could look like this: 658 \begin{verbatim} 659void printhandler(FILE *o, int var) 660{ 661 extern char **names; 662 fprintf(o, "%s", names[var]); 663} 664\end{verbatim} 665 666 \noindent 667 The handler can then be passed to BuDDy like this: 668 {\tt fdd\_file\_hook(printhandler)}. 669 670 No default handler is supplied. The argument {\tt handler} may be 671 NULL if no handler is needed. *} 672RETURN {* The old handler *} 673ALSO {* fdd\_printset, bdd\_file\_hook *} 674*/ 675bddfilehandler fdd_file_hook(bddfilehandler h) 676{ 677 bddfilehandler old = filehandler; 678 filehandler = h; 679 return old; 680} 681 682/* 683NAME {* fdd\_printset *} 684EXTRA {* fdd\_fprintset *} 685SECTION {* fdd *} 686SHORT {* prints a BDD for a finite domain block *} 687PROTO {* void fdd_printset(BDD r) 688void fdd_fprintset(FILE *ofile, BDD f) *} 689DESCR {* Prints the BDD {\tt f} using a set notation as in 690 {\tt bdd\_printset} but with the index of the finite domain blocks 691 included instead of the BDD variables. It is possible to specify 692 a printing callback function with {\tt fdd\_file\_hook} or 693 {\tt fdd\_strm\_hook} which can be used to print the FDD 694 identifier in a readable form. *} 695ALSO {* bdd\_printset, fdd\_file\_hook, fdd\_strm\_hook *} 696*/ 697void fdd_printset(BDD r) 698{ 699 CHECKn(r); 700 fdd_fprintset(stdout, r); 701} 702 703 704void fdd_fprintset(FILE *ofile, BDD r) 705{ 706 int *set; 707 708 if (!bddrunning) 709 { 710 bdd_error(BDD_RUNNING); 711 return; 712 } 713 714 if (r < 2) 715 { 716 fprintf(ofile, "%s", r == 0 ? "F" : "T"); 717 return; 718 } 719 720 set = (int *)malloc(sizeof(int)*bddvarnum); 721 if (set == NULL) 722 { 723 bdd_error(BDD_MEMORY); 724 return; 725 } 726 727 memset(set, 0, sizeof(int) * bddvarnum); 728 fdd_printset_rec(ofile, r, set); 729 free(set); 730} 731 732 733static void fdd_printset_rec(FILE *ofile, int r, int *set) 734{ 735 int n,m,i; 736 int used = 0; 737 int *var; 738 int *binval; 739 int ok, first; 740 741 if (r == 0) 742 return; 743 else 744 if (r == 1) 745 { 746 fprintf(ofile, "<"); 747 first=1; 748 749 for (n=0 ; n<fdvarnum ; n++) 750 { 751 int firstval=1; 752 used = 0; 753 754 for (m=0 ; m<domain[n].binsize ; m++) 755 if (set[domain[n].ivar[m]] != 0) 756 used = 1; 757 758 if (used) 759 { 760 if (!first) 761 fprintf(ofile, ", "); 762 first = 0; 763 if (filehandler) 764 filehandler(ofile, n); 765 else 766 fprintf(ofile, "%d", n); 767 printf(":"); 768 769 var = domain[n].ivar; 770 771 for (m=0 ; m<(1<<domain[n].binsize) ; m++) 772 { 773 binval = fdddec2bin(n, m); 774 ok=1; 775 776 for (i=0 ; i<domain[n].binsize && ok ; i++) 777 if (set[var[i]] == 1 && binval[i] != 0) 778 ok = 0; 779 else 780 if (set[var[i]] == 2 && binval[i] != 1) 781 ok = 0; 782 783 if (ok) 784 { 785 if (firstval) 786 fprintf(ofile, "%d", m); 787 else 788 fprintf(ofile, "/%d", m); 789 firstval = 0; 790 } 791 792 free(binval); 793 } 794 } 795 } 796 797 fprintf(ofile, ">"); 798 } 799 else 800 { 801 set[bddlevel2var[LEVEL(r)]] = 1; 802 fdd_printset_rec(ofile, LOW(r), set); 803 804 set[bddlevel2var[LEVEL(r)]] = 2; 805 fdd_printset_rec(ofile, HIGH(r), set); 806 807 set[bddlevel2var[LEVEL(r)]] = 0; 808 } 809} 810 811 812/*======================================================================*/ 813 814/* 815NAME {* fdd\_scanset *} 816SECTION {* fdd *} 817SHORT {* scans a variable set *} 818PROTO {* int fdd_scanset(BDD r, int **varset, int *varnum) *} 819DESCR {* Scans the BDD {\tt r} to find all occurences of FDD variables 820 and then stores these in {\tt varset}. {\tt varset} will be set 821 to point to an array of size {\tt varnum} which will contain 822 the indices of the found FDD variables. It is the users 823 responsibility to free {\tt varset} after use. *} 824RETURN {* Zero on success or a negative error code on error. *} 825ALSO {* fdd\_makeset *} 826*/ 827int fdd_scanset(BDD r, int **varset, int *varnum) 828{ 829 int *fv, fn; 830 int num,n,m,i; 831 832 if (!bddrunning) 833 return bdd_error(BDD_RUNNING); 834 835 if ((n=bdd_scanset(r, &fv, &fn)) < 0) 836 return n; 837 838 for (n=0,num=0 ; n<fdvarnum ; n++) 839 { 840 int found=0; 841 842 for (m=0 ; m<domain[n].binsize && !found ; m++) 843 { 844 for (i=0 ; i<fn && !found ; i++) 845 if (domain[n].ivar[m] == fv[i]) 846 { 847 num++; 848 found=1; 849 } 850 } 851 } 852 853 if ((*varset=(int*)malloc(sizeof(int)*num)) == NULL) 854 return bdd_error(BDD_MEMORY); 855 856 for (n=0,num=0 ; n<fdvarnum ; n++) 857 { 858 int found=0; 859 860 for (m=0 ; m<domain[n].binsize && !found ; m++) 861 { 862 for (i=0 ; i<fn && !found ; i++) 863 if (domain[n].ivar[m] == fv[i]) 864 { 865 (*varset)[num++] = n; 866 found=1; 867 } 868 } 869 } 870 871 *varnum = num; 872 873 return 0; 874} 875 876 877/*======================================================================*/ 878 879/* 880NAME {* fdd\_makeset *} 881SECTION {* fdd *} 882SHORT {* creates a variable set for N finite domain blocks *} 883PROTO {* BDD fdd_makeset(int *varset, int varnum) *} 884DESCR {* Returns a BDD defining all the variable sets used to define 885 the variable blocks in the array {\tt varset}. The argument 886 {\tt varnum} defines the size of {\tt varset}. *} 887RETURN {* The correct BDD or the constant false on errors. *} 888ALSO {* fdd\_ithset, bdd\_makeset *} 889*/ 890BDD fdd_makeset(int *varset, int varnum) 891{ 892 BDD res=bddtrue, tmp; 893 int n; 894 895 if (!bddrunning) 896 { 897 bdd_error(BDD_RUNNING); 898 return bddfalse; 899 } 900 901 for (n=0 ; n<varnum ; n++) 902 if (varset[n] < 0 || varset[n] >= fdvarnum) 903 { 904 bdd_error(BDD_VAR); 905 return bddfalse; 906 } 907 908 for (n=0 ; n<varnum ; n++) 909 { 910 bdd_addref(res); 911 tmp = bdd_apply(domain[varset[n]].var, res, bddop_and); 912 bdd_delref(res); 913 res = tmp; 914 } 915 916 return res; 917} 918 919 920/* 921NAME {* fdd\_intaddvarblock *} 922SECTION {* fdd *} 923SHORT {* adds a new variable block for reordering *} 924PROTO {* int fdd_intaddvarblock(int first, int last, int fixed) *} 925DESCR {* Works exactly like {\tt bdd\_addvarblock} except that 926 {\tt fdd\_intaddvarblock} takes a range of FDD variables 927 instead of BDD variables. *} 928RETURN {* Zero on success, otherwise a negative error code. *} 929ALSO {* bdd\_addvarblock, bdd\_intaddvarblock, bdd\_reorder *} 930*/ 931int fdd_intaddvarblock(int first, int last, int fixed) 932{ 933 bdd res = bddtrue, tmp; 934 int n, err; 935 936 if (!bddrunning) 937 return bdd_error(BDD_RUNNING); 938 939 if (first > last || first < 0 || last >= fdvarnum) 940 return bdd_error(BDD_VARBLK); 941 942 for (n=first ; n<=last ; n++) 943 { 944 bdd_addref(res); 945 tmp = bdd_apply(domain[n].var, res, bddop_and); 946 bdd_delref(res); 947 res = tmp; 948 } 949 950 err = bdd_addvarblock(res, fixed); 951 952 bdd_delref(res); 953 return err; 954} 955 956 957/* 958NAME {* fdd\_setpair *} 959SECTION {* fdd *} 960SHORT {* defines a pair for two finite domain blocks *} 961PROTO {* int fdd_setpair(bddPair *pair, int p1, int p2) *} 962DESCR {* Defines each variable in the finite domain block {\tt p1} to 963 be paired with the corresponding variable in {\tt p2}. The result 964 is stored in {\tt pair} which must be allocated using 965 {\tt bdd\_makepair}. *} 966RETURN {* Zero on success or a negative error code on error. *} 967ALSO {* fdd\_setpairs *} 968*/ 969int fdd_setpair(bddPair *pair, int p1, int p2) 970{ 971 int n,e; 972 973 if (!bddrunning) 974 return bdd_error(BDD_RUNNING); 975 976 if (p1<0 || p1>=fdvarnum || p2<0 || p2>=fdvarnum) 977 return bdd_error(BDD_VAR); 978 979 if (domain[p1].binsize != domain[p2].binsize) 980 return bdd_error(BDD_VARNUM); 981 982 for (n=0 ; n<domain[p1].binsize ; n++) 983 if ((e=bdd_setpair(pair, domain[p1].ivar[n], domain[p2].ivar[n])) < 0) 984 return e; 985 986 return 0; 987} 988 989 990/* 991NAME {* fdd\_setpairs *} 992SECTION {* fdd *} 993SHORT {* defines N pairs for finite domain blocks *} 994PROTO {* int fdd_setpairs(bddPair *pair, int *p1, int *p2, int size) *} 995DESCR {* Defines each variable in all the finite domain blocks listed in 996 the array {\tt p1} to be paired with the corresponding variable 997 in {\tt p2}. The result 998 is stored in {\tt pair} which must be allocated using 999 {\tt bdd\_makeset}.*} 1000RETURN {* Zero on success or a negative error code on error. *} 1001ALSO {* bdd\_setpair *} 1002*/ 1003int fdd_setpairs(bddPair *pair, int *p1, int *p2, int size) 1004{ 1005 int n,e; 1006 1007 if (!bddrunning) 1008 return bdd_error(BDD_RUNNING); 1009 1010 for (n=0 ; n<size ; n++) 1011 if (p1[n]<0 || p1[n]>=fdvarnum || p2[n]<0 || p2[n]>=fdvarnum) 1012 return bdd_error(BDD_VAR); 1013 1014 for (n=0 ; n<size ; n++) 1015 if ((e=fdd_setpair(pair, p1[n], p2[n])) < 0) 1016 return e; 1017 1018 return 0; 1019} 1020 1021 1022/************************************************************************* 1023 Domain storage "class" 1024*************************************************************************/ 1025 1026static void Domain_done(Domain* d) 1027{ 1028 free(d->ivar); 1029 bdd_delref(d->var); 1030} 1031 1032 1033static void Domain_allocate(Domain* d, int range) 1034{ 1035 int calcsize = 2; 1036 1037 if (range <= 0 || range > INT_MAX/2) 1038 { 1039 bdd_error(BDD_RANGE); 1040 return; 1041 } 1042 1043 d->realsize = range; 1044 d->binsize = 1; 1045 1046 while (calcsize < range) 1047 { 1048 d->binsize++; 1049 calcsize <<= 1; 1050 } 1051 1052 d->ivar = (int *)malloc(sizeof(int)*d->binsize); 1053 d->var = bddtrue; 1054} 1055 1056 1057int *fdddec2bin(int var, int val) 1058{ 1059 int *res; 1060 int n = 0; 1061 1062 res = (int *)malloc(sizeof(int)*domain[var].binsize); 1063 memset(res, 0, sizeof(int)*domain[var].binsize); 1064 1065 while (val > 0) 1066 { 1067 if (val & 0x1) 1068 res[n] = 1; 1069 val >>= 1; 1070 n++; 1071 } 1072 1073 return res; 1074} 1075 1076 1077/* EOF */ 1078