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: bddop.c 33 DESCR: BDD operators 34 AUTH: Jorn Lind 35 DATE: (C) nov 1997 36*************************************************************************/ 37#include <stdlib.h> 38#include <string.h> 39#include <math.h> 40#include <time.h> 41#include <assert.h> 42 43#include "kernel.h" 44#include "cache.h" 45 46 /* Hash value modifiers to distinguish between entries in misccache */ 47#define CACHEID_CONSTRAIN 0x0 48#define CACHEID_RESTRICT 0x1 49#define CACHEID_SATCOU 0x2 50#define CACHEID_SATCOULN 0x3 51#define CACHEID_PATHCOU 0x4 52 53 /* Hash value modifiers for replace/compose */ 54#define CACHEID_REPLACE 0x0 55#define CACHEID_COMPOSE 0x1 56#define CACHEID_VECCOMPOSE 0x2 57 58 /* Hash value modifiers for quantification */ 59#define CACHEID_EXIST 0x0 60#define CACHEID_FORALL 0x1 61#define CACHEID_UNIQUE 0x2 62#define CACHEID_APPEX 0x3 63#define CACHEID_APPAL 0x4 64#define CACHEID_APPUN 0x5 65 66 67 /* Number of boolean operators */ 68#define OPERATOR_NUM 11 69 70 /* Operator results - entry = left<<1 | right (left,right in {0,1}) */ 71static int oprres[OPERATOR_NUM][4] = 72{ {0,0,0,1}, /* and ( & ) */ 73 {0,1,1,0}, /* xor ( ^ ) */ 74 {0,1,1,1}, /* or ( | ) */ 75 {1,1,1,0}, /* nand */ 76 {1,0,0,0}, /* nor */ 77 {1,1,0,1}, /* implication ( >> ) */ 78 {1,0,0,1}, /* bi-implication */ 79 {0,0,1,0}, /* difference /greater than ( - ) ( > ) */ 80 {0,1,0,0}, /* less than ( < ) */ 81 {1,0,1,1}, /* inverse implication ( << ) */ 82 {1,1,0,0} /* not ( ! ) */ 83}; 84 85 86 /* Variables needed for the operators */ 87static int applyop; /* Current operator for apply */ 88static int appexop; /* Current operator for appex */ 89static int appexid; /* Current cache id for appex */ 90static int quantid; /* Current cache id for quantifications */ 91static int *quantvarset; /* Current variable set for quant. */ 92static int quantvarsetID; /* Current id used in quantvarset */ 93static int quantlast; /* Current last variable to be quant. */ 94static int replaceid; /* Current cache id for replace */ 95static int *replacepair; /* Current replace pair */ 96static int replacelast; /* Current last var. level to replace */ 97static int composelevel; /* Current variable used for compose */ 98static int miscid; /* Current cache id for other results */ 99static int *varprofile; /* Current variable profile */ 100static int supportID; /* Current ID (true value) for support */ 101static int supportMin; /* Min. used level in support calc. */ 102static int supportMax; /* Max. used level in support calc. */ 103static int* supportSet; /* The found support set */ 104static BddCache applycache; /* Cache for apply results */ 105static BddCache itecache; /* Cache for ITE results */ 106static BddCache quantcache; /* Cache for exist/forall results */ 107static BddCache appexcache; /* Cache for appex/appall results */ 108static BddCache replacecache; /* Cache for replace results */ 109static BddCache misccache; /* Cache for other results */ 110static int cacheratio; 111static BDD satPolarity; 112static int firstReorder; /* Used instead of local variable in order 113 to avoid compiler warning about 'first' 114 being clobbered by setjmp */ 115 116extern bddCacheStat bddcachestats; 117 118 /* Internal prototypes */ 119static BDD not_rec(BDD); 120static BDD apply_rec(BDD, BDD); 121static BDD ite_rec(BDD, BDD, BDD); 122static int simplify_rec(BDD, BDD); 123static int quant_rec(int); 124static int appquant_rec(int, int); 125static int restrict_rec(int); 126static BDD constrain_rec(BDD, BDD); 127static BDD replace_rec(BDD); 128static BDD bdd_correctify(int, BDD, BDD); 129static BDD compose_rec(BDD, BDD); 130static BDD veccompose_rec(BDD); 131static void support_rec(int, int*); 132static BDD satone_rec(BDD); 133static BDD satoneset_rec(BDD, BDD); 134static int fullsatone_rec(int); 135static double satcount_rec(int); 136static double satcountln_rec(int); 137static void varprofile_rec(int); 138static double bdd_pathcount_rec(BDD); 139static int varset2vartable(BDD); 140static int varset2svartable(BDD); 141 142 143 /* Hashvalues */ 144#define NOTHASH(r) (r) 145#define APPLYHASH(l,r,op) (TRIPLE(l,r,op)) 146#define ITEHASH(f,g,h) (TRIPLE(f,g,h)) 147#define RESTRHASH(r,var) (PAIR(r,var)) 148#define CONSTRAINHASH(f,c) (PAIR(f,c)) 149#define QUANTHASH(r) (r) 150#define REPLACEHASH(r) (r) 151#define VECCOMPOSEHASH(f) (f) 152#define COMPOSEHASH(f,g) (PAIR(f,g)) 153#define SATCOUHASH(r) (r) 154#define PATHCOUHASH(r) (r) 155#define APPEXHASH(l,r,op) (PAIR(l,r)) 156 157#ifndef M_LN2 158#define M_LN2 0.69314718055994530942 159#endif 160 161#define log1p(a) (log(1.0+a)) 162 163#define INVARSET(a) (quantvarset[a] == quantvarsetID) /* unsigned check */ 164#define INSVARSET(a) (abs(quantvarset[a]) == quantvarsetID) /* signed check */ 165 166/************************************************************************* 167 Setup and shutdown 168*************************************************************************/ 169 170int bdd_operator_init(int cachesize) 171{ 172 if (BddCache_init(&applycache,cachesize) < 0) 173 return bdd_error(BDD_MEMORY); 174 175 if (BddCache_init(&itecache,cachesize) < 0) 176 return bdd_error(BDD_MEMORY); 177 178 if (BddCache_init(&quantcache,cachesize) < 0) 179 return bdd_error(BDD_MEMORY); 180 181 if (BddCache_init(&appexcache,cachesize) < 0) 182 return bdd_error(BDD_MEMORY); 183 184 if (BddCache_init(&replacecache,cachesize) < 0) 185 return bdd_error(BDD_MEMORY); 186 187 if (BddCache_init(&misccache,cachesize) < 0) 188 return bdd_error(BDD_MEMORY); 189 190 quantvarsetID = 0; 191 quantvarset = NULL; 192 cacheratio = 0; 193 supportSet = NULL; 194 195 return 0; 196} 197 198 199void bdd_operator_done(void) 200{ 201 if (quantvarset != NULL) 202 free(quantvarset); 203 204 BddCache_done(&applycache); 205 BddCache_done(&itecache); 206 BddCache_done(&quantcache); 207 BddCache_done(&appexcache); 208 BddCache_done(&replacecache); 209 BddCache_done(&misccache); 210 211 if (supportSet != NULL) 212 free(supportSet); 213} 214 215 216void bdd_operator_reset(void) 217{ 218 BddCache_reset(&applycache); 219 BddCache_reset(&itecache); 220 BddCache_reset(&quantcache); 221 BddCache_reset(&appexcache); 222 BddCache_reset(&replacecache); 223 BddCache_reset(&misccache); 224} 225 226 227void bdd_operator_varresize(void) 228{ 229 if (quantvarset != NULL) 230 free(quantvarset); 231 232 if ((quantvarset=NEW(int,bddvarnum)) == NULL) 233 bdd_error(BDD_MEMORY); 234 235 memset(quantvarset, 0, sizeof(int)*bddvarnum); 236 quantvarsetID = 0; 237} 238 239 240static void bdd_operator_noderesize(void) 241{ 242 if (cacheratio > 0) 243 { 244 int newcachesize = bddnodesize / cacheratio; 245 246 BddCache_resize(&applycache, newcachesize); 247 BddCache_resize(&itecache, newcachesize); 248 BddCache_resize(&quantcache, newcachesize); 249 BddCache_resize(&appexcache, newcachesize); 250 BddCache_resize(&replacecache, newcachesize); 251 BddCache_resize(&misccache, newcachesize); 252 } 253} 254 255 256/************************************************************************* 257 Other 258*************************************************************************/ 259 260/* 261NAME {* bdd\_setcacheratio *} 262SECTION {* kernel *} 263SHORT {* Sets the cache ratio for the operator caches *} 264PROTO {* int bdd_setcacheratio(int r) *} 265DESCR {* The ratio between the number of nodes in the nodetable 266 and the number of entries in the operator cachetables is called 267 the cache ratio. So a cache ratio of say, four, allocates one cache 268 entry for each four unique node entries. This value can be set with 269 {\tt bdd\_setcacheratio} to any positive value. When this is done 270 the caches are resized instantly to fit the new ratio. 271 The default is a fixed cache size determined at 272 initialization time. *} 273RETURN {* The previous cache ratio or a negative number on error. *} 274ALSO {* bdd\_init *} 275*/ 276int bdd_setcacheratio(int r) 277{ 278 int old = cacheratio; 279 280 if (r <= 0) 281 return bdd_error(BDD_RANGE); 282 if (bddnodesize == 0) 283 return old; 284 285 cacheratio = r; 286 bdd_operator_noderesize(); 287 return old; 288} 289 290 291/************************************************************************* 292 Operators 293*************************************************************************/ 294 295static void checkresize(void) 296{ 297 if (bddresized) 298 bdd_operator_noderesize(); 299 bddresized = 0; 300} 301 302 303/*=== BUILD A CUBE =====================================================*/ 304 305/* 306NAME {* bdd\_buildcube *} 307EXTRA {* bdd\_ibuildcube *} 308SECTION {* operator *} 309SHORT {* build a cube from an array of variables *} 310PROTO {* BDD bdd_buildcube(int value, int width, BDD *var) 311BDD bdd_ibuildcube(int value, int width, int *var)*} 312DESCR {* This function builds a cube from the variables in {\tt 313 var}. It does so by interpreting the {\tt width} low order 314 bits of {\tt value} as a bit mask--a set bit indicates that the 315 variable should be added in it's positive form, and a cleared 316 bit the opposite. The most significant bits are encoded with 317 the first variables in {\tt var}. Consider as an example 318 the call {\tt bdd\_buildcube(0xB, 4, var)}. This corresponds 319 to the expression: $var[0] \conj \neg var[1] \conj var[2] 320 \conj var[3]$. The first version of the function takes an array 321 of BDDs, whereas the second takes an array of variable numbers 322 as used in {\tt bdd\_ithvar}. *} 323RETURN {* The resulting cube *} 324ALSO {* bdd\_ithvar, fdd\_ithvar *} 325*/ 326BDD bdd_buildcube(int value, int width, BDD *variables) 327{ 328 BDD result = BDDONE; 329 int z; 330 331 for (z=0 ; z<width ; z++, value>>=1) 332 { 333 BDD tmp; 334 BDD v; 335 336 if (value & 0x1) 337 v = bdd_addref( variables[width-z-1] ); 338 else 339 v = bdd_addref( bdd_not(variables[width-z-1]) ); 340 341 bdd_addref(result); 342 tmp = bdd_apply(result,v,bddop_and); 343 bdd_delref(result); 344 bdd_delref(v); 345 346 result = tmp; 347 } 348 349 return result; 350} 351 352 353BDD bdd_ibuildcube(int value, int width, int *variables) 354{ 355 BDD result = BDDONE; 356 int z; 357 358 for (z=0 ; z<width ; z++, value>>=1) 359 { 360 BDD tmp; 361 BDD v; 362 363 if (value & 0x1) 364 v = bdd_ithvar(variables[width-z-1]); 365 else 366 v = bdd_nithvar(variables[width-z-1]); 367 368 bdd_addref(result); 369 tmp = bdd_apply(result,v,bddop_and); 370 bdd_delref(result); 371 372 result = tmp; 373 } 374 375 return result; 376} 377 378 379/*=== NOT ==============================================================*/ 380 381/* 382NAME {* bdd\_not *} 383SECTION {* operator *} 384SHORT {* negates a bdd *} 385PROTO {* BDD bdd_not(BDD r) *} 386DESCR {* Negates the BDD {\tt r} by exchanging 387 all references to the zero-terminal with references to the 388 one-terminal and vice versa. *} 389RETURN {* The negated bdd. *} 390*/ 391BDD bdd_not(BDD r) 392{ 393 BDD res; 394 firstReorder = 1; 395 CHECKa(r, bddfalse); 396 397 again: 398 if (setjmp(bddexception) == 0) 399 { 400 bddrefstacktop = bddrefstack; 401 402 if (!firstReorder) 403 bdd_disable_reorder(); 404 res = not_rec(r); 405 if (!firstReorder) 406 bdd_enable_reorder(); 407 } 408 else 409 { 410 bdd_checkreorder(); 411 if (firstReorder-- == 1) 412 goto again; 413 res = BDDZERO; /* avoid warning about res being uninitialized */ 414 } 415 416 checkresize(); 417 return res; 418} 419 420 421static BDD not_rec(BDD r) 422{ 423 BddCacheData *entry; 424 BDD res; 425 426 if (ISZERO(r)) 427 return BDDONE; 428 if (ISONE(r)) 429 return BDDZERO; 430 431 entry = BddCache_lookup(&applycache, NOTHASH(r)); 432 433 if (entry->a == r && entry->c == bddop_not) 434 { 435#ifdef CACHESTATS 436 bddcachestats.opHit++; 437#endif 438 return entry->r.res; 439 } 440#ifdef CACHESTATS 441 bddcachestats.opMiss++; 442#endif 443 444 PUSHREF( not_rec(LOW(r)) ); 445 PUSHREF( not_rec(HIGH(r)) ); 446 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); 447 POPREF(2); 448 449 entry->a = r; 450 entry->c = bddop_not; 451 entry->r.res = res; 452 453 return res; 454} 455 456 457/*=== APPLY ============================================================*/ 458 459/* 460NAME {* bdd\_apply *} 461SECTION {* operator *} 462SHORT {* basic bdd operations *} 463PROTO {* BDD bdd_apply(BDD left, BDD right, int opr) *} 464DESCR {* The {\tt bdd\_apply} function performs all of the basic 465 bdd operations with two operands, such as AND, OR etc. 466 The {\tt left} argument is the left bdd operand and {\tt right} 467 is the right operand. The {\tt opr} argument is the requested 468 operation and must be one of the following\\ 469 470 \begin{tabular}{lllc} 471 {\bf Identifier} & {\bf Description} & {\bf Truth table} 472 & {\bf C++ opr.} \\ 473 {\tt bddop\_and} & logical and ($A \wedge B$) & [0,0,0,1] 474 & \verb%&% \\ 475 {\tt bddop\_xor} & logical xor ($A \oplus B$) & [0,1,1,0] 476 & \verb%^% \\ 477 {\tt bddop\_or} & logical or ($A \vee B$) & [0,1,1,1] 478 & \verb%|% \\ 479 {\tt bddop\_nand} & logical not-and & [1,1,1,0] \\ 480 {\tt bddop\_nor} & logical not-or & [1,0,0,0] \\ 481 {\tt bddop\_imp} & implication ($A \Rightarrow B$) & [1,1,0,1] 482 & \verb%>>% \\ 483 {\tt bddop\_biimp} & bi-implication ($A \Leftrightarrow B$)& [1,0,0,1] \\ 484 {\tt bddop\_diff} & set difference ($A \setminus B$) & [0,0,1,0] 485 & \verb%-% \\ 486 {\tt bddop\_less} & less than ($A < B$) & [0,1,0,0] 487 & \verb%<% \\ 488 {\tt bddop\_invimp} & reverse implication ($A \Leftarrow B$)& [1,0,1,1] 489 & \verb%<<% \\ 490 \end{tabular} 491 *} 492 RETURN {* The result of the operation. *} 493 ALSO {* bdd\_ite *} 494*/ 495BDD bdd_apply(BDD l, BDD r, int op) 496{ 497 BDD res; 498 firstReorder = 1; 499 500 CHECKa(l, bddfalse); 501 CHECKa(r, bddfalse); 502 503 if (op<0 || op>bddop_invimp) 504 { 505 bdd_error(BDD_OP); 506 return bddfalse; 507 } 508 509 again: 510 if (setjmp(bddexception) == 0) 511 { 512 bddrefstacktop = bddrefstack; 513 applyop = op; 514 515 if (!firstReorder) 516 bdd_disable_reorder(); 517 res = apply_rec(l, r); 518 if (!firstReorder) 519 bdd_enable_reorder(); 520 } 521 else 522 { 523 bdd_checkreorder(); 524 525 if (firstReorder-- == 1) 526 goto again; 527 res = BDDZERO; /* avoid warning about res being uninitialized */ 528 } 529 530 checkresize(); 531 return res; 532} 533 534 535static BDD apply_rec(BDD l, BDD r) 536{ 537 BddCacheData *entry; 538 BDD res; 539 540 switch (applyop) 541 { 542 case bddop_and: 543 if (l == r) 544 return l; 545 if (ISZERO(l) || ISZERO(r)) 546 return 0; 547 if (ISONE(l)) 548 return r; 549 if (ISONE(r)) 550 return l; 551 break; 552 case bddop_or: 553 if (l == r) 554 return l; 555 if (ISONE(l) || ISONE(r)) 556 return 1; 557 if (ISZERO(l)) 558 return r; 559 if (ISZERO(r)) 560 return l; 561 break; 562 case bddop_xor: 563 if (l == r) 564 return 0; 565 if (ISZERO(l)) 566 return r; 567 if (ISZERO(r)) 568 return l; 569 break; 570 case bddop_nand: 571 if (ISZERO(l) || ISZERO(r)) 572 return 1; 573 break; 574 case bddop_nor: 575 if (ISONE(l) || ISONE(r)) 576 return 0; 577 break; 578 case bddop_imp: 579 if (ISZERO(l)) 580 return 1; 581 if (ISONE(l)) 582 return r; 583 if (ISONE(r)) 584 return 1; 585 break; 586 } 587 588 if (ISCONST(l) && ISCONST(r)) 589 res = oprres[applyop][l<<1 | r]; 590 else 591 { 592 entry = BddCache_lookup(&applycache, APPLYHASH(l,r,applyop)); 593 594 if (entry->a == l && entry->b == r && entry->c == applyop) 595 { 596#ifdef CACHESTATS 597 bddcachestats.opHit++; 598#endif 599 return entry->r.res; 600 } 601#ifdef CACHESTATS 602 bddcachestats.opMiss++; 603#endif 604 605 if (LEVEL(l) == LEVEL(r)) 606 { 607 PUSHREF( apply_rec(LOW(l), LOW(r)) ); 608 PUSHREF( apply_rec(HIGH(l), HIGH(r)) ); 609 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); 610 } 611 else 612 if (LEVEL(l) < LEVEL(r)) 613 { 614 PUSHREF( apply_rec(LOW(l), r) ); 615 PUSHREF( apply_rec(HIGH(l), r) ); 616 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); 617 } 618 else 619 { 620 PUSHREF( apply_rec(l, LOW(r)) ); 621 PUSHREF( apply_rec(l, HIGH(r)) ); 622 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); 623 } 624 625 POPREF(2); 626 627 entry->a = l; 628 entry->b = r; 629 entry->c = applyop; 630 entry->r.res = res; 631 } 632 633 return res; 634} 635 636 637/* 638NAME {* bdd\_and *} 639SECTION {* operator *} 640SHORT {* The logical 'and' of two BDDs *} 641PROTO {* BDD bdd_and(BDD l, BDD r) *} 642DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_and)}. *} 643RETURN {* The logical 'and' of {\tt l} and {\tt r}. *} 644ALSO {* bdd\_apply, bdd\_or, bdd\_xor *} 645*/ 646BDD bdd_and(BDD l, BDD r) 647{ 648 return bdd_apply(l,r,bddop_and); 649} 650 651 652/* 653NAME {* bdd\_or *} 654SECTION {* operator *} 655SHORT {* The logical 'or' of two BDDs *} 656PROTO {* BDD bdd_or(BDD l, BDD r) *} 657DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_or)}. *} 658RETURN {* The logical 'or' of {\tt l} and {\tt r}. *} 659ALSO {* bdd\_apply, bdd\_xor, bdd\_and *} 660*/ 661BDD bdd_or(BDD l, BDD r) 662{ 663 return bdd_apply(l,r,bddop_or); 664} 665 666 667/* 668NAME {* bdd\_xor *} 669SECTION {* operator *} 670SHORT {* The logical 'xor' of two BDDs *} 671PROTO {* BDD bdd_xor(BDD l, BDD r) *} 672DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_xor)}. *} 673RETURN {* The logical 'xor' of {\tt l} and {\tt r}. *} 674ALSO {* bdd\_apply, bdd\_or, bdd\_and *} 675*/ 676BDD bdd_xor(BDD l, BDD r) 677{ 678 return bdd_apply(l,r,bddop_xor); 679} 680 681 682/* 683NAME {* bdd\_imp *} 684SECTION {* operator *} 685SHORT {* The logical 'implication' between two BDDs *} 686PROTO {* BDD bdd_imp(BDD l, BDD r) *} 687DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_imp)}. *} 688RETURN {* The logical 'implication' of {\tt l} and {\tt r} ($l \Rightarrow r$). *} 689ALSO {* bdd\_apply, bdd\_biimp *} 690*/ 691BDD bdd_imp(BDD l, BDD r) 692{ 693 return bdd_apply(l,r,bddop_imp); 694} 695 696 697/* 698NAME {* bdd\_biimp *} 699SECTION {* operator *} 700SHORT {* The logical 'bi-implication' between two BDDs *} 701PROTO {* BDD bdd_biimp(BDD l, BDD r) *} 702DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_biimp)}. *} 703RETURN {* The logical 'bi-implication' of {\tt l} and {\tt r} ($l \Leftrightarrow r$). *} 704ALSO {* bdd\_apply, bdd\_imp *} 705*/ 706BDD bdd_biimp(BDD l, BDD r) 707{ 708 return bdd_apply(l,r,bddop_biimp); 709} 710 711 712/*=== ITE ==============================================================*/ 713 714/* 715NAME {* bdd\_ite *} 716SECTION {* operator *} 717SHORT {* if-then-else operator *} 718PROTO {* BDD bdd_ite(BDD f, BDD g, BDD h) *} 719DESCR {* Calculates the BDD for the expression 720 $(f \conj g) \disj (\neg f \conj h)$ more efficiently than doing 721 the three operations separately. {\tt bdd\_ite} can also be used 722 for conjunction, disjunction and any other boolean operator, but 723 is not as efficient for the binary and unary operations. *} 724RETURN {* The BDD for $(f \conj g) \disj (\neg f \conj h)$ *} 725ALSO {* bdd\_apply *} 726*/ 727BDD bdd_ite(BDD f, BDD g, BDD h) 728{ 729 BDD res; 730 firstReorder = 1; 731 732 CHECKa(f, bddfalse); 733 CHECKa(g, bddfalse); 734 CHECKa(h, bddfalse); 735 736 again: 737 if (setjmp(bddexception) == 0) 738 { 739 bddrefstacktop = bddrefstack; 740 741 if (!firstReorder) 742 bdd_disable_reorder(); 743 res = ite_rec(f,g,h); 744 if (!firstReorder) 745 bdd_enable_reorder(); 746 } 747 else 748 { 749 bdd_checkreorder(); 750 751 if (firstReorder-- == 1) 752 goto again; 753 res = BDDZERO; /* avoid warning about res being uninitialized */ 754 } 755 756 checkresize(); 757 return res; 758} 759 760 761static BDD ite_rec(BDD f, BDD g, BDD h) 762{ 763 BddCacheData *entry; 764 BDD res; 765 766 if (ISONE(f)) 767 return g; 768 if (ISZERO(f)) 769 return h; 770 if (g == h) 771 return g; 772 if (ISONE(g) && ISZERO(h)) 773 return f; 774 if (ISZERO(g) && ISONE(h)) 775 return not_rec(f); 776 777 entry = BddCache_lookup(&itecache, ITEHASH(f,g,h)); 778 if (entry->a == f && entry->b == g && entry->c == h) 779 { 780#ifdef CACHESTATS 781 bddcachestats.opHit++; 782#endif 783 return entry->r.res; 784 } 785#ifdef CACHESTATS 786 bddcachestats.opMiss++; 787#endif 788 789 if (LEVEL(f) == LEVEL(g)) 790 { 791 if (LEVEL(f) == LEVEL(h)) 792 { 793 PUSHREF( ite_rec(LOW(f), LOW(g), LOW(h)) ); 794 PUSHREF( ite_rec(HIGH(f), HIGH(g), HIGH(h)) ); 795 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 796 } 797 else 798 if (LEVEL(f) < LEVEL(h)) 799 { 800 PUSHREF( ite_rec(LOW(f), LOW(g), h) ); 801 PUSHREF( ite_rec(HIGH(f), HIGH(g), h) ); 802 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 803 } 804 else /* f > h */ 805 { 806 PUSHREF( ite_rec(f, g, LOW(h)) ); 807 PUSHREF( ite_rec(f, g, HIGH(h)) ); 808 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1)); 809 } 810 } 811 else 812 if (LEVEL(f) < LEVEL(g)) 813 { 814 if (LEVEL(f) == LEVEL(h)) 815 { 816 PUSHREF( ite_rec(LOW(f), g, LOW(h)) ); 817 PUSHREF( ite_rec(HIGH(f), g, HIGH(h)) ); 818 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 819 } 820 else 821 if (LEVEL(f) < LEVEL(h)) 822 { 823 PUSHREF( ite_rec(LOW(f), g, h) ); 824 PUSHREF( ite_rec(HIGH(f), g, h) ); 825 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 826 } 827 else /* f > h */ 828 { 829 PUSHREF( ite_rec(f, g, LOW(h)) ); 830 PUSHREF( ite_rec(f, g, HIGH(h)) ); 831 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1)); 832 } 833 } 834 else /* f > g */ 835 { 836 if (LEVEL(g) == LEVEL(h)) 837 { 838 PUSHREF( ite_rec(f, LOW(g), LOW(h)) ); 839 PUSHREF( ite_rec(f, HIGH(g), HIGH(h)) ); 840 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1)); 841 } 842 else 843 if (LEVEL(g) < LEVEL(h)) 844 { 845 PUSHREF( ite_rec(f, LOW(g), h) ); 846 PUSHREF( ite_rec(f, HIGH(g), h) ); 847 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1)); 848 } 849 else /* g > h */ 850 { 851 PUSHREF( ite_rec(f, g, LOW(h)) ); 852 PUSHREF( ite_rec(f, g, HIGH(h)) ); 853 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1)); 854 } 855 } 856 857 POPREF(2); 858 859 entry->a = f; 860 entry->b = g; 861 entry->c = h; 862 entry->r.res = res; 863 864 return res; 865} 866 867 868/*=== RESTRICT =========================================================*/ 869 870/* 871NAME {* bdd\_restrict *} 872SECTION {* operator *} 873SHORT {* restric a set of variables to constant values *} 874PROTO {* BDD bdd_restrict(BDD r, BDD var) *} 875DESCR {* This function restricts the variables in {\tt r} to constant 876 true or false. How this is done 877 depends on how the variables are included in the variable set 878 {\tt var}. If they 879 are included in their positive form then they are restricted to 880 true and vice versa. Unfortunately it is not possible to 881 insert variables in their negated form using {\tt bdd\_makeset}, 882 so the variable set has to be build manually as a 883 conjunction of the variables. Example: Assume variable 1 should be 884 restricted to true and variable 3 to false. 885 \begin{verbatim} 886 bdd X = make_user_bdd(); 887 bdd R1 = bdd_ithvar(1); 888 bdd R2 = bdd_nithvar(3); 889 bdd R = bdd_addref( bdd_apply(R1,R2, bddop_and) ); 890 bdd RES = bdd_addref( bdd_restrict(X,R) ); 891\end{verbatim} 892 *} 893RETURN {* The restricted bdd. *} 894ALSO {* bdd\_makeset, bdd\_exist, bdd\_forall *} 895*/ 896BDD bdd_restrict(BDD r, BDD var) 897{ 898 BDD res; 899 firstReorder = 1; 900 901 CHECKa(r,bddfalse); 902 CHECKa(var,bddfalse); 903 904 if (var < 2) /* Empty set */ 905 return r; 906 907 again: 908 if (setjmp(bddexception) == 0) 909 { 910 if (varset2svartable(var) < 0) 911 return bddfalse; 912 913 bddrefstacktop = bddrefstack; 914 miscid = (var << 3) | CACHEID_RESTRICT; 915 916 if (!firstReorder) 917 bdd_disable_reorder(); 918 res = restrict_rec(r); 919 if (!firstReorder) 920 bdd_enable_reorder(); 921 } 922 else 923 { 924 bdd_checkreorder(); 925 926 if (firstReorder-- == 1) 927 goto again; 928 res = BDDZERO; /* avoid warning about res being uninitialized */ 929 } 930 931 checkresize(); 932 return res; 933} 934 935 936static int restrict_rec(int r) 937{ 938 BddCacheData *entry; 939 int res; 940 941 if (ISCONST(r) || LEVEL(r) > quantlast) 942 return r; 943 944 entry = BddCache_lookup(&misccache, RESTRHASH(r,miscid)); 945 if (entry->a == r && entry->c == miscid) 946 { 947#ifdef CACHESTATS 948 bddcachestats.opHit++; 949#endif 950 return entry->r.res; 951 } 952#ifdef CACHESTATS 953 bddcachestats.opMiss++; 954#endif 955 956 if (INSVARSET(LEVEL(r))) 957 { 958 if (quantvarset[LEVEL(r)] > 0) 959 res = restrict_rec(HIGH(r)); 960 else 961 res = restrict_rec(LOW(r)); 962 } 963 else 964 { 965 PUSHREF( restrict_rec(LOW(r)) ); 966 PUSHREF( restrict_rec(HIGH(r)) ); 967 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); 968 POPREF(2); 969 } 970 971 entry->a = r; 972 entry->c = miscid; 973 entry->r.res = res; 974 975 return res; 976} 977 978 979/*=== GENERALIZED COFACTOR =============================================*/ 980 981/* 982NAME {* bdd\_constrain *} 983SECTION {* operator *} 984SHORT {* generalized cofactor *} 985PROTO {* BDD bdd_constrain(BDD f, BDD c) *} 986DESCR {* Computes the generalized cofactor of {\tt f} with respect to 987 {\tt c}. *} 988RETURN {* The constrained BDD *} 989ALSO {* bdd\_restrict, bdd\_simplify *} 990*/ 991BDD bdd_constrain(BDD f, BDD c) 992{ 993 BDD res; 994 firstReorder = 1; 995 996 CHECKa(f,bddfalse); 997 CHECKa(c,bddfalse); 998 999 again: 1000 if (setjmp(bddexception) == 0) 1001 { 1002 bddrefstacktop = bddrefstack; 1003 miscid = CACHEID_CONSTRAIN; 1004 1005 if (!firstReorder) 1006 bdd_disable_reorder(); 1007 res = constrain_rec(f, c); 1008 if (!firstReorder) 1009 bdd_enable_reorder(); 1010 } 1011 else 1012 { 1013 bdd_checkreorder(); 1014 1015 if (firstReorder-- == 1) 1016 goto again; 1017 res = BDDZERO; /* avoid warning about res being uninitialized */ 1018 } 1019 1020 checkresize(); 1021 return res; 1022} 1023 1024 1025static BDD constrain_rec(BDD f, BDD c) 1026{ 1027 BddCacheData *entry; 1028 BDD res; 1029 1030 if (ISONE(c)) 1031 return f; 1032 if (ISCONST(f)) 1033 return f; 1034 if (c == f) 1035 return BDDONE; 1036 if (ISZERO(c)) 1037 return BDDZERO; 1038 1039 entry = BddCache_lookup(&misccache, CONSTRAINHASH(f,c)); 1040 if (entry->a == f && entry->b == c && entry->c == miscid) 1041 { 1042#ifdef CACHESTATS 1043 bddcachestats.opHit++; 1044#endif 1045 return entry->r.res; 1046 } 1047#ifdef CACHESTATS 1048 bddcachestats.opMiss++; 1049#endif 1050 1051 if (LEVEL(f) == LEVEL(c)) 1052 { 1053 if (ISZERO(LOW(c))) 1054 res = constrain_rec(HIGH(f), HIGH(c)); 1055 else if (ISZERO(HIGH(c))) 1056 res = constrain_rec(LOW(f), LOW(c)); 1057 else 1058 { 1059 PUSHREF( constrain_rec(LOW(f), LOW(c)) ); 1060 PUSHREF( constrain_rec(HIGH(f), HIGH(c)) ); 1061 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 1062 POPREF(2); 1063 } 1064 } 1065 else 1066 if (LEVEL(f) < LEVEL(c)) 1067 { 1068 PUSHREF( constrain_rec(LOW(f), c) ); 1069 PUSHREF( constrain_rec(HIGH(f), c) ); 1070 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 1071 POPREF(2); 1072 } 1073 else 1074 { 1075 if (ISZERO(LOW(c))) 1076 res = constrain_rec(f, HIGH(c)); 1077 else if (ISZERO(HIGH(c))) 1078 res = constrain_rec(f, LOW(c)); 1079 else 1080 { 1081 PUSHREF( constrain_rec(f, LOW(c)) ); 1082 PUSHREF( constrain_rec(f, HIGH(c)) ); 1083 res = bdd_makenode(LEVEL(c), READREF(2), READREF(1)); 1084 POPREF(2); 1085 } 1086 } 1087 1088 entry->a = f; 1089 entry->b = c; 1090 entry->c = miscid; 1091 entry->r.res = res; 1092 1093 return res; 1094} 1095 1096 1097/*=== REPLACE ==========================================================*/ 1098 1099/* 1100NAME {* bdd\_replace *} 1101SECTION {* operator *} 1102SHORT {* replaces variables with other variables *} 1103PROTO {* BDD bdd_replace(BDD r, bddPair *pair) *} 1104DESCR {* Replaces all variables in the BDD {\tt r} with the variables 1105 defined by {\tt pair}. Each entry in {\tt pair} consists of a 1106 old and a new variable. Whenever the old variable is found in 1107 {\tt r} then a new node with the new variable is inserted instead. 1108 *} 1109ALSO {* bdd\_newpair, bdd\_setpair, bdd\_setpairs *} 1110RETURN {* The result of the operation. *} 1111*/ 1112BDD bdd_replace(BDD r, bddPair *pair) 1113{ 1114 BDD res; 1115 firstReorder = 1; 1116 1117 CHECKa(r, bddfalse); 1118 1119 again: 1120 if (setjmp(bddexception) == 0) 1121 { 1122 bddrefstacktop = bddrefstack; 1123 replacepair = pair->result; 1124 replacelast = pair->last; 1125 replaceid = (pair->id << 2) | CACHEID_REPLACE; 1126 1127 if (!firstReorder) 1128 bdd_disable_reorder(); 1129 res = replace_rec(r); 1130 if (!firstReorder) 1131 bdd_enable_reorder(); 1132 } 1133 else 1134 { 1135 bdd_checkreorder(); 1136 1137 if (firstReorder-- == 1) 1138 goto again; 1139 res = BDDZERO; /* avoid warning about res being uninitialized */ 1140 } 1141 1142 checkresize(); 1143 return res; 1144} 1145 1146 1147static BDD replace_rec(BDD r) 1148{ 1149 BddCacheData *entry; 1150 BDD res; 1151 1152 if (ISCONST(r) || LEVEL(r) > replacelast) 1153 return r; 1154 1155 entry = BddCache_lookup(&replacecache, REPLACEHASH(r)); 1156 if (entry->a == r && entry->c == replaceid) 1157 { 1158#ifdef CACHESTATS 1159 bddcachestats.opHit++; 1160#endif 1161 return entry->r.res; 1162 } 1163#ifdef CACHESTATS 1164 bddcachestats.opMiss++; 1165#endif 1166 1167 PUSHREF( replace_rec(LOW(r)) ); 1168 PUSHREF( replace_rec(HIGH(r)) ); 1169 1170 res = bdd_correctify(LEVEL(replacepair[LEVEL(r)]), READREF(2), READREF(1)); 1171 POPREF(2); 1172 1173 entry->a = r; 1174 entry->c = replaceid; 1175 entry->r.res = res; 1176 1177 return res; 1178} 1179 1180 1181static BDD bdd_correctify(int level, BDD l, BDD r) 1182{ 1183 BDD res; 1184 1185 if (level < LEVEL(l) && level < LEVEL(r)) 1186 return bdd_makenode(level, l, r); 1187 1188 if (level == LEVEL(l) || level == LEVEL(r)) 1189 { 1190 bdd_error(BDD_REPLACE); 1191 return 0; 1192 } 1193 1194 if (LEVEL(l) == LEVEL(r)) 1195 { 1196 PUSHREF( bdd_correctify(level, LOW(l), LOW(r)) ); 1197 PUSHREF( bdd_correctify(level, HIGH(l), HIGH(r)) ); 1198 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); 1199 } 1200 else 1201 if (LEVEL(l) < LEVEL(r)) 1202 { 1203 PUSHREF( bdd_correctify(level, LOW(l), r) ); 1204 PUSHREF( bdd_correctify(level, HIGH(l), r) ); 1205 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); 1206 } 1207 else 1208 { 1209 PUSHREF( bdd_correctify(level, l, LOW(r)) ); 1210 PUSHREF( bdd_correctify(level, l, HIGH(r)) ); 1211 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); 1212 } 1213 POPREF(2); 1214 1215 return res; /* FIXME: cache ? */ 1216} 1217 1218 1219/*=== COMPOSE ==========================================================*/ 1220 1221/* 1222NAME {* bdd\_compose *} 1223SECTION {* operator *} 1224SHORT {* functional composition *} 1225PROTO {* BDD bdd_compose(BDD f, BDD g, int var) *} 1226DESCR {* Substitutes the variable {\tt var} with the BDD {\tt g} in 1227 the BDD {\tt f}: result $= f[g/var]$. *} 1228RETURN {* The composed BDD *} 1229ALSO {* bdd\_veccompose, bdd\_replace, bdd\_restrict *} 1230*/ 1231BDD bdd_compose(BDD f, BDD g, int var) 1232{ 1233 BDD res; 1234 firstReorder = 1; 1235 1236 CHECKa(f, bddfalse); 1237 CHECKa(g, bddfalse); 1238 if (var < 0 || var >= bddvarnum) 1239 { 1240 bdd_error(BDD_VAR); 1241 return bddfalse; 1242 } 1243 1244 again: 1245 if (setjmp(bddexception) == 0) 1246 { 1247 bddrefstacktop = bddrefstack; 1248 composelevel = bddvar2level[var]; 1249 replaceid = (composelevel << 2) | CACHEID_COMPOSE; 1250 1251 if (!firstReorder) 1252 bdd_disable_reorder(); 1253 res = compose_rec(f, g); 1254 if (!firstReorder) 1255 bdd_enable_reorder(); 1256 } 1257 else 1258 { 1259 bdd_checkreorder(); 1260 1261 if (firstReorder-- == 1) 1262 goto again; 1263 res = BDDZERO; /* avoid warning about res being uninitialized */ 1264 } 1265 1266 checkresize(); 1267 return res; 1268} 1269 1270 1271static BDD compose_rec(BDD f, BDD g) 1272{ 1273 BddCacheData *entry; 1274 BDD res; 1275 1276 if (LEVEL(f) > composelevel) 1277 return f; 1278 1279 entry = BddCache_lookup(&replacecache, COMPOSEHASH(f,g)); 1280 if (entry->a == f && entry->b == g && entry->c == replaceid) 1281 { 1282#ifdef CACHESTATS 1283 bddcachestats.opHit++; 1284#endif 1285 return entry->r.res; 1286 } 1287#ifdef CACHESTATS 1288 bddcachestats.opMiss++; 1289#endif 1290 1291 if (LEVEL(f) < composelevel) 1292 { 1293 if (LEVEL(f) == LEVEL(g)) 1294 { 1295 PUSHREF( compose_rec(LOW(f), LOW(g)) ); 1296 PUSHREF( compose_rec(HIGH(f), HIGH(g)) ); 1297 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 1298 } 1299 else 1300 if (LEVEL(f) < LEVEL(g)) 1301 { 1302 PUSHREF( compose_rec(LOW(f), g) ); 1303 PUSHREF( compose_rec(HIGH(f), g) ); 1304 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 1305 } 1306 else 1307 { 1308 PUSHREF( compose_rec(f, LOW(g)) ); 1309 PUSHREF( compose_rec(f, HIGH(g)) ); 1310 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1)); 1311 } 1312 POPREF(2); 1313 } 1314 else 1315 /*if (LEVEL(f) == composelevel) changed 2-nov-98 */ 1316 { 1317 res = ite_rec(g, HIGH(f), LOW(f)); 1318 } 1319 1320 entry->a = f; 1321 entry->b = g; 1322 entry->c = replaceid; 1323 entry->r.res = res; 1324 1325 return res; 1326} 1327 1328 1329/* 1330NAME {* bdd\_veccompose *} 1331SECTION {* operator *} 1332SHORT {* simultaneous functional composition *} 1333PROTO {* BDD bdd_veccompose(BDD f, bddPair *pair) *} 1334DESCR {* Uses the pairs of variables and BDDs in {\tt pair} to make 1335 the simultaneous substitution: $f[g_1/V_1, \ldots, g_n/V_n]$. 1336 In this way one or more BDDs 1337 may be substituted in one step. The BDDs in 1338 {\tt pair} may depend on the variables they are substituting. 1339 {\tt bdd\_compose} may be used instead of 1340 {\tt bdd\_replace} but is not as efficient when $g_i$ is a 1341 single variable, the same applies to {\tt bdd\_restrict}. 1342 Note that simultaneous substitution is not necessarily the same 1343 as repeated substitution. Example: 1344 $(x_1 \disj x_2)[x_3/x_1,x_4/x_3] = (x_3 \disj x_2) \neq 1345 ((x_1 \disj x_2)[x_3/x_1])[x_4/x_3] = (x_4 \disj x_2)$. *} 1346RETURN {* The composed BDD *} 1347ALSO {* bdd\_compose, bdd\_replace, bdd\_restrict *} 1348*/ 1349BDD bdd_veccompose(BDD f, bddPair *pair) 1350{ 1351 BDD res; 1352 firstReorder = 1; 1353 1354 CHECKa(f, bddfalse); 1355 1356 again: 1357 if (setjmp(bddexception) == 0) 1358 { 1359 bddrefstacktop = bddrefstack; 1360 replacepair = pair->result; 1361 replaceid = (pair->id << 2) | CACHEID_VECCOMPOSE; 1362 replacelast = pair->last; 1363 1364 if (!firstReorder) 1365 bdd_disable_reorder(); 1366 res = veccompose_rec(f); 1367 if (!firstReorder) 1368 bdd_enable_reorder(); 1369 } 1370 else 1371 { 1372 bdd_checkreorder(); 1373 1374 if (firstReorder-- == 1) 1375 goto again; 1376 res = BDDZERO; /* avoid warning about res being uninitialized */ 1377 } 1378 1379 checkresize(); 1380 return res; 1381} 1382 1383 1384static BDD veccompose_rec(BDD f) 1385{ 1386 BddCacheData *entry; 1387 register BDD res; 1388 1389 if (LEVEL(f) > replacelast) 1390 return f; 1391 1392 entry = BddCache_lookup(&replacecache, VECCOMPOSEHASH(f)); 1393 if (entry->a == f && entry->c == replaceid) 1394 { 1395#ifdef CACHESTATS 1396 bddcachestats.opHit++; 1397#endif 1398 return entry->r.res; 1399 } 1400#ifdef CACHESTATS 1401 bddcachestats.opMiss++; 1402#endif 1403 1404 PUSHREF( veccompose_rec(LOW(f)) ); 1405 PUSHREF( veccompose_rec(HIGH(f)) ); 1406 res = ite_rec(replacepair[LEVEL(f)], READREF(1), READREF(2)); 1407 POPREF(2); 1408 1409 entry->a = f; 1410 entry->c = replaceid; 1411 entry->r.res = res; 1412 1413 return res; 1414} 1415 1416 1417/*=== SIMPLIFY =========================================================*/ 1418 1419/* 1420NAME {* bdd\_simplify *} 1421SECTION {* operator *} 1422SHORT {* coudert and Madre's restrict function *} 1423PROTO {* BDD bdd_simplify(BDD f, BDD d) *} 1424DESCR {* Tries to simplify the BDD {\tt f} by restricting it to the 1425 domaine covered by {\tt d}. No checks are done to see if the 1426 result is actually smaller than the input. This can be done 1427 by the user with a call to {\tt bdd\_nodecount}. *} 1428ALSO {* bdd\_restrict *} 1429RETURN {* The simplified BDD *} 1430*/ 1431BDD bdd_simplify(BDD f, BDD d) 1432{ 1433 BDD res; 1434 firstReorder = 1; 1435 1436 CHECKa(f, bddfalse); 1437 CHECKa(d, bddfalse); 1438 1439 again: 1440 if (setjmp(bddexception) == 0) 1441 { 1442 bddrefstacktop = bddrefstack; 1443 applyop = bddop_or; 1444 1445 if (!firstReorder) 1446 bdd_disable_reorder(); 1447 res = simplify_rec(f, d); 1448 if (!firstReorder) 1449 bdd_enable_reorder(); 1450 } 1451 else 1452 { 1453 bdd_checkreorder(); 1454 1455 if (firstReorder-- == 1) 1456 goto again; 1457 res = BDDZERO; /* avoid warning about res being uninitialized */ 1458 } 1459 1460 checkresize(); 1461 return res; 1462} 1463 1464 1465static BDD simplify_rec(BDD f, BDD d) 1466{ 1467 BddCacheData *entry; 1468 BDD res; 1469 1470 if (ISONE(d) || ISCONST(f)) 1471 return f; 1472 if (d == f) 1473 return BDDONE; 1474 if (ISZERO(d)) 1475 return BDDZERO; 1476 1477 entry = BddCache_lookup(&applycache, APPLYHASH(f,d,bddop_simplify)); 1478 1479 if (entry->a == f && entry->b == d && entry->c == bddop_simplify) 1480 { 1481#ifdef CACHESTATS 1482 bddcachestats.opHit++; 1483#endif 1484 return entry->r.res; 1485 } 1486#ifdef CACHESTATS 1487 bddcachestats.opMiss++; 1488#endif 1489 1490 if (LEVEL(f) == LEVEL(d)) 1491 { 1492 if (ISZERO(LOW(d))) 1493 res = simplify_rec(HIGH(f), HIGH(d)); 1494 else 1495 if (ISZERO(HIGH(d))) 1496 res = simplify_rec(LOW(f), LOW(d)); 1497 else 1498 { 1499 PUSHREF( simplify_rec(LOW(f), LOW(d)) ); 1500 PUSHREF( simplify_rec(HIGH(f), HIGH(d)) ); 1501 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 1502 POPREF(2); 1503 } 1504 } 1505 else 1506 if (LEVEL(f) < LEVEL(d)) 1507 { 1508 PUSHREF( simplify_rec(LOW(f), d) ); 1509 PUSHREF( simplify_rec(HIGH(f), d) ); 1510 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); 1511 POPREF(2); 1512 } 1513 else /* LEVEL(d) < LEVEL(f) */ 1514 { 1515 PUSHREF( apply_rec(LOW(d), HIGH(d)) ); /* Exist quant */ 1516 res = simplify_rec(f, READREF(1)); 1517 POPREF(1); 1518 } 1519 1520 entry->a = f; 1521 entry->b = d; 1522 entry->c = bddop_simplify; 1523 entry->r.res = res; 1524 1525 return res; 1526} 1527 1528 1529/*=== QUANTIFICATION ===================================================*/ 1530 1531/* 1532NAME {* bdd\_exist *} 1533SECTION {* operator *} 1534SHORT {* existential quantification of variables *} 1535PROTO {* BDD bdd_exist(BDD r, BDD var) *} 1536DESCR {* Removes all occurences in {\tt r} of variables in the set 1537 {\tt var} by existential quantification. *} 1538ALSO {* bdd\_forall, bdd\_unique, bdd\_makeset *} 1539RETURN {* The quantified BDD. *} 1540*/ 1541BDD bdd_exist(BDD r, BDD var) 1542{ 1543 BDD res; 1544 firstReorder = 1; 1545 1546 CHECKa(r, bddfalse); 1547 CHECKa(var, bddfalse); 1548 1549 if (var < 2) /* Empty set */ 1550 return r; 1551 1552 again: 1553 if (setjmp(bddexception) == 0) 1554 { 1555 if (varset2vartable(var) < 0) 1556 return bddfalse; 1557 1558 bddrefstacktop = bddrefstack; 1559 quantid = (var << 3) | CACHEID_EXIST; /* FIXME: range */ 1560 applyop = bddop_or; 1561 1562 if (!firstReorder) 1563 bdd_disable_reorder(); 1564 res = quant_rec(r); 1565 if (!firstReorder) 1566 bdd_enable_reorder(); 1567 } 1568 else 1569 { 1570 bdd_checkreorder(); 1571 1572 if (firstReorder-- == 1) 1573 goto again; 1574 res = BDDZERO; /* avoid warning about res being uninitialized */ 1575 } 1576 1577 checkresize(); 1578 return res; 1579} 1580 1581 1582/* 1583NAME {* bdd\_forall *} 1584SECTION {* operator *} 1585SHORT {* universal quantification of variables *} 1586PROTO {* BDD bdd_forall(BDD r, BDD var) *} 1587DESCR {* Removes all occurences in {\tt r} of variables in the set 1588 {\tt var} by universal quantification. *} 1589ALSO {* bdd\_exist, bdd\_unique, bdd\_makeset *} 1590RETURN {* The quantified BDD. *} 1591*/ 1592BDD bdd_forall(BDD r, BDD var) 1593{ 1594 BDD res; 1595 firstReorder = 1; 1596 1597 CHECKa(r, bddfalse); 1598 CHECKa(var, bddfalse); 1599 1600 if (var < 2) /* Empty set */ 1601 return r; 1602 1603 again: 1604 if (setjmp(bddexception) == 0) 1605 { 1606 if (varset2vartable(var) < 0) 1607 return bddfalse; 1608 1609 bddrefstacktop = bddrefstack; 1610 quantid = (var << 3) | CACHEID_FORALL; 1611 applyop = bddop_and; 1612 1613 if (!firstReorder) 1614 bdd_disable_reorder(); 1615 res = quant_rec(r); 1616 if (!firstReorder) 1617 bdd_enable_reorder(); 1618 } 1619 else 1620 { 1621 bdd_checkreorder(); 1622 1623 if (firstReorder-- == 1) 1624 goto again; 1625 res = BDDZERO; /* avoid warning about res being uninitialized */ 1626 } 1627 1628 checkresize(); 1629 return res; 1630} 1631 1632 1633/* 1634NAME {* bdd\_unique *} 1635SECTION {* operator *} 1636SHORT {* unique quantification of variables *} 1637PROTO {* BDD bdd_unique(BDD r, BDD var) *} 1638DESCR {* Removes all occurences in {\tt r} of variables in the set 1639 {\tt var} by unique quantification. This type of quantification 1640 uses a XOR operator instead of an OR operator as in the 1641 existential quantification, and an AND operator as in the 1642 universal quantification. *} 1643ALSO {* bdd\_exist, bdd\_forall, bdd\_makeset *} 1644RETURN {* The quantified BDD. *} 1645*/ 1646BDD bdd_unique(BDD r, BDD var) 1647{ 1648 BDD res; 1649 firstReorder = 1; 1650 1651 CHECKa(r, bddfalse); 1652 CHECKa(var, bddfalse); 1653 1654 if (var < 2) /* Empty set */ 1655 return r; 1656 1657 again: 1658 if (setjmp(bddexception) == 0) 1659 { 1660 if (varset2vartable(var) < 0) 1661 return bddfalse; 1662 1663 bddrefstacktop = bddrefstack; 1664 quantid = (var << 3) | CACHEID_UNIQUE; 1665 applyop = bddop_xor; 1666 1667 if (!firstReorder) 1668 bdd_disable_reorder(); 1669 res = quant_rec(r); 1670 if (!firstReorder) 1671 bdd_enable_reorder(); 1672 } 1673 else 1674 { 1675 bdd_checkreorder(); 1676 1677 if (firstReorder-- == 1) 1678 goto again; 1679 res = BDDZERO; /* avoid warning about res being uninitialized */ 1680 } 1681 1682 checkresize(); 1683 return res; 1684} 1685 1686 1687static int quant_rec(int r) 1688{ 1689 BddCacheData *entry; 1690 int res; 1691 1692 if (r < 2 || LEVEL(r) > quantlast) 1693 return r; 1694 1695 entry = BddCache_lookup(&quantcache, QUANTHASH(r)); 1696 if (entry->a == r && entry->c == quantid) 1697 { 1698#ifdef CACHESTATS 1699 bddcachestats.opHit++; 1700#endif 1701 return entry->r.res; 1702 } 1703#ifdef CACHESTATS 1704 bddcachestats.opMiss++; 1705#endif 1706 1707 PUSHREF( quant_rec(LOW(r)) ); 1708 PUSHREF( quant_rec(HIGH(r)) ); 1709 1710 if (INVARSET(LEVEL(r))) 1711 res = apply_rec(READREF(2), READREF(1)); 1712 else 1713 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); 1714 1715 POPREF(2); 1716 1717 entry->a = r; 1718 entry->c = quantid; 1719 entry->r.res = res; 1720 1721 return res; 1722} 1723 1724 1725/*=== APPLY & QUANTIFY =================================================*/ 1726 1727/* 1728NAME {* bdd\_appex *} 1729SECTION {* operator *} 1730SHORT {* apply operation and existential quantification *} 1731PROTO {* BDD bdd_appex(BDD left, BDD right, int opr, BDD var) *} 1732DESCR {* Applies the binary operator {\tt opr} to the arguments 1733 {\tt left} and {\tt right} and then performs an existential 1734 quantification of the variables from the variable set 1735 {\tt var}. This is done in a bottom up manner such that both the 1736 apply and quantification is done on the lower nodes before 1737 stepping up to the higher nodes. This makes the {\tt bdd\_appex} 1738 function much more efficient than an apply operation followed 1739 by a quantification. If the operator is a conjunction then this 1740 is similar to the relational product of the two BDDs. 1741 \index{relational product} *} 1742ALSO {* bdd\_appall, bdd\_appuni, bdd\_apply, bdd\_exist, bdd\_forall, bdd\_unique, bdd\_makeset *} 1743RETURN {* The result of the operation. *} 1744*/ 1745BDD bdd_appex(BDD l, BDD r, int opr, BDD var) 1746{ 1747 BDD res; 1748 firstReorder = 1; 1749 1750 CHECKa(l, bddfalse); 1751 CHECKa(r, bddfalse); 1752 CHECKa(var, bddfalse); 1753 1754 if (opr<0 || opr>bddop_invimp) 1755 { 1756 bdd_error(BDD_OP); 1757 return bddfalse; 1758 } 1759 1760 if (var < 2) /* Empty set */ 1761 return bdd_apply(l,r,opr); 1762 1763 again: 1764 if (setjmp(bddexception) == 0) 1765 { 1766 if (varset2vartable(var) < 0) 1767 return bddfalse; 1768 1769 bddrefstacktop = bddrefstack; 1770 applyop = bddop_or; 1771 appexop = opr; 1772 appexid = (var << 5) | (appexop << 1); /* FIXME: range! */ 1773 quantid = (appexid << 3) | CACHEID_APPEX; 1774 1775 if (!firstReorder) 1776 bdd_disable_reorder(); 1777 res = appquant_rec(l, r); 1778 if (!firstReorder) 1779 bdd_enable_reorder(); 1780 } 1781 else 1782 { 1783 bdd_checkreorder(); 1784 1785 if (firstReorder-- == 1) 1786 goto again; 1787 res = BDDZERO; /* avoid warning about res being uninitialized */ 1788 } 1789 1790 checkresize(); 1791 return res; 1792} 1793 1794 1795/* 1796NAME {* bdd\_appall *} 1797SECTION {* operator *} 1798SHORT {* apply operation and universal quantification *} 1799PROTO {* BDD bdd_appall(BDD left, BDD right, int opr, BDD var) *} 1800DESCR {* Applies the binary operator {\tt opr} to the arguments 1801 {\tt left} and {\tt right} and then performs an universal 1802 quantification of the variables from the variable set 1803 {\tt var}. This is done in a bottom up manner such that both the 1804 apply and quantification is done on the lower nodes before 1805 stepping up to the higher nodes. This makes the {\tt bdd\_appall} 1806 function much more efficient than an apply operation followed 1807 by a quantification. *} 1808ALSO {* bdd\_appex, bdd\_appuni, bdd\_apply, bdd\_exist, bdd\_forall, bdd\_unique, bdd\_makeset *} 1809RETURN {* The result of the operation. *} 1810*/ 1811BDD bdd_appall(BDD l, BDD r, int opr, BDD var) 1812{ 1813 BDD res; 1814 firstReorder = 1; 1815 1816 CHECKa(l, bddfalse); 1817 CHECKa(r, bddfalse); 1818 CHECKa(var, bddfalse); 1819 1820 if (opr<0 || opr>bddop_invimp) 1821 { 1822 bdd_error(BDD_OP); 1823 return bddfalse; 1824 } 1825 1826 if (var < 2) /* Empty set */ 1827 return bdd_apply(l,r,opr); 1828 1829 again: 1830 if (setjmp(bddexception) == 0) 1831 { 1832 if (varset2vartable(var) < 0) 1833 return bddfalse; 1834 1835 bddrefstacktop = bddrefstack; 1836 applyop = bddop_and; 1837 appexop = opr; 1838 appexid = (var << 5) | (appexop << 1) | 1; /* FIXME: range! */ 1839 quantid = (appexid << 3) | CACHEID_APPAL; 1840 1841 if (!firstReorder) 1842 bdd_disable_reorder(); 1843 res = appquant_rec(l, r); 1844 if (!firstReorder) 1845 bdd_enable_reorder(); 1846 } 1847 else 1848 { 1849 bdd_checkreorder(); 1850 1851 if (firstReorder-- == 1) 1852 goto again; 1853 res = BDDZERO; /* avoid warning about res being uninitialized */ 1854 } 1855 1856 checkresize(); 1857 return res; 1858} 1859 1860 1861/* 1862NAME {* bdd\_appuni *} 1863SECTION {* operator *} 1864SHORT {* apply operation and unique quantification *} 1865PROTO {* BDD bdd_appuni(BDD left, BDD right, int opr, BDD var) *} 1866DESCR {* Applies the binary operator {\tt opr} to the arguments 1867 {\tt left} and {\tt right} and then performs a unique 1868 quantification of the variables from the variable set 1869 {\tt var}. This is done in a bottom up manner such that both the 1870 apply and quantification is done on the lower nodes before 1871 stepping up to the higher nodes. This makes the {\tt bdd\_appuni} 1872 function much more efficient than an apply operation followed 1873 by a quantification. *} 1874ALSO {* bdd\_appex, bdd\_appall, bdd\_apply, bdd\_exist, bdd\_unique, bdd\_forall, bdd\_makeset *} 1875RETURN {* The result of the operation. *} 1876*/ 1877BDD bdd_appuni(BDD l, BDD r, int opr, BDD var) 1878{ 1879 BDD res; 1880 firstReorder = 1; 1881 1882 CHECKa(l, bddfalse); 1883 CHECKa(r, bddfalse); 1884 CHECKa(var, bddfalse); 1885 1886 if (opr<0 || opr>bddop_invimp) 1887 { 1888 bdd_error(BDD_OP); 1889 return bddfalse; 1890 } 1891 1892 if (var < 2) /* Empty set */ 1893 return bdd_apply(l,r,opr); 1894 1895 again: 1896 if (setjmp(bddexception) == 0) 1897 { 1898 if (varset2vartable(var) < 0) 1899 return bddfalse; 1900 1901 bddrefstacktop = bddrefstack; 1902 applyop = bddop_xor; 1903 appexop = opr; 1904 appexid = (var << 5) | (appexop << 1) | 1; /* FIXME: range! */ 1905 quantid = (appexid << 3) | CACHEID_APPUN; 1906 1907 if (!firstReorder) 1908 bdd_disable_reorder(); 1909 res = appquant_rec(l, r); 1910 if (!firstReorder) 1911 bdd_enable_reorder(); 1912 } 1913 else 1914 { 1915 bdd_checkreorder(); 1916 1917 if (firstReorder-- == 1) 1918 goto again; 1919 res = BDDZERO; /* avoid warning about res being uninitialized */ 1920 } 1921 1922 checkresize(); 1923 return res; 1924} 1925 1926 1927static int appquant_rec(int l, int r) 1928{ 1929 BddCacheData *entry; 1930 int res; 1931 1932 switch (appexop) 1933 { 1934 case bddop_and: 1935 if (l == 0 || r == 0) 1936 return 0; 1937 if (l == r) 1938 return quant_rec(l); 1939 if (l == 1) 1940 return quant_rec(r); 1941 if (r == 1) 1942 return quant_rec(l); 1943 break; 1944 case bddop_or: 1945 if (l == 1 || r == 1) 1946 return 1; 1947 if (l == r) 1948 return quant_rec(l); 1949 if (l == 0) 1950 return quant_rec(r); 1951 if (r == 0) 1952 return quant_rec(l); 1953 break; 1954 case bddop_xor: 1955 if (l == r) 1956 return 0; 1957 if (l == 0) 1958 return quant_rec(r); 1959 if (r == 0) 1960 return quant_rec(l); 1961 break; 1962 case bddop_nand: 1963 if (l == 0 || r == 0) 1964 return 1; 1965 break; 1966 case bddop_nor: 1967 if (l == 1 || r == 1) 1968 return 0; 1969 break; 1970 } 1971 1972 if (ISCONST(l) && ISCONST(r)) 1973 res = oprres[appexop][(l<<1) | r]; 1974 else 1975 if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) 1976 { 1977 int oldop = applyop; 1978 applyop = appexop; 1979 res = apply_rec(l,r); 1980 applyop = oldop; 1981 } 1982 else 1983 { 1984 entry = BddCache_lookup(&appexcache, APPEXHASH(l,r,appexop)); 1985 if (entry->a == l && entry->b == r && entry->c == appexid) 1986 { 1987#ifdef CACHESTATS 1988 bddcachestats.opHit++; 1989#endif 1990 return entry->r.res; 1991 } 1992#ifdef CACHESTATS 1993 bddcachestats.opMiss++; 1994#endif 1995 1996 if (LEVEL(l) == LEVEL(r)) 1997 { 1998 PUSHREF( appquant_rec(LOW(l), LOW(r)) ); 1999 PUSHREF( appquant_rec(HIGH(l), HIGH(r)) ); 2000 if (INVARSET(LEVEL(l))) 2001 res = apply_rec(READREF(2), READREF(1)); 2002 else 2003 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); 2004 } 2005 else 2006 if (LEVEL(l) < LEVEL(r)) 2007 { 2008 PUSHREF( appquant_rec(LOW(l), r) ); 2009 PUSHREF( appquant_rec(HIGH(l), r) ); 2010 if (INVARSET(LEVEL(l))) 2011 res = apply_rec(READREF(2), READREF(1)); 2012 else 2013 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); 2014 } 2015 else 2016 { 2017 PUSHREF( appquant_rec(l, LOW(r)) ); 2018 PUSHREF( appquant_rec(l, HIGH(r)) ); 2019 if (INVARSET(LEVEL(r))) 2020 res = apply_rec(READREF(2), READREF(1)); 2021 else 2022 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); 2023 } 2024 2025 POPREF(2); 2026 2027 entry->a = l; 2028 entry->b = r; 2029 entry->c = appexid; 2030 entry->r.res = res; 2031 } 2032 2033 return res; 2034} 2035 2036 2037/************************************************************************* 2038 Informational functions 2039*************************************************************************/ 2040 2041/*=== SUPPORT ==========================================================*/ 2042 2043/* 2044NAME {* bdd\_support *} 2045SECTION {* info *} 2046SHORT {* returns the variable support of a BDD *} 2047PROTO {* BDD bdd_support(BDD r) *} 2048DESCR {* Finds all the variables that {\tt r} depends on. That is 2049 the support of {\tt r}. *} 2050ALSO {* bdd\_makeset *} 2051RETURN {* A BDD variable set. *} 2052*/ 2053BDD bdd_support(BDD r) 2054{ 2055 static int supportSize = 0; 2056 int n; 2057 int res=1; 2058 2059 CHECKa(r, bddfalse); 2060 2061 if (r < 2) 2062 return bddfalse; 2063 2064 /* On-demand allocation of support set */ 2065 if (supportSize < bddvarnum) 2066 { 2067 if ((supportSet=(int*)malloc(bddvarnum*sizeof(int))) == NULL) 2068 { 2069 bdd_error(BDD_MEMORY); 2070 return bddfalse; 2071 } 2072 memset(supportSet, 0, bddvarnum*sizeof(int)); 2073 supportSize = bddvarnum; 2074 supportID = 0; 2075 } 2076 2077 /* Update global variables used to speed up bdd_support() 2078 * - instead of always memsetting support to zero, we use 2079 * a change counter. 2080 * - and instead of reading the whole array afterwards, we just 2081 * look from 'min' to 'max' used BDD variables. 2082 */ 2083 if (supportID == 0x0FFFFFFF) 2084 { 2085 /* We probably don't get here -- but let's just be sure */ 2086 memset(supportSet, 0, bddvarnum*sizeof(int)); 2087 supportID = 0; 2088 } 2089 ++supportID; 2090 supportMin = LEVEL(r); 2091 supportMax = supportMin; 2092 2093 support_rec(r, supportSet); 2094 bdd_unmark(r); 2095 2096 bdd_disable_reorder(); 2097 2098 for (n=supportMax ; n>=supportMin ; --n) 2099 if (supportSet[n] == supportID) 2100 { 2101 register BDD tmp; 2102 bdd_addref(res); 2103 tmp = bdd_makenode(n, 0, res); 2104 bdd_delref(res); 2105 res = tmp; 2106 } 2107 2108 bdd_enable_reorder(); 2109 2110 return res; 2111} 2112 2113 2114static void support_rec(int r, int* support) 2115{ 2116 BddNode *node; 2117 2118 if (r < 2) 2119 return; 2120 2121 node = &bddnodes[r]; 2122 if (LEVELp(node) & MARKON || LOWp(node) == -1) 2123 return; 2124 2125 support[LEVELp(node)] = supportID; 2126 2127 if (LEVELp(node) > supportMax) 2128 supportMax = LEVELp(node); 2129 2130 LEVELp(node) |= MARKON; 2131 2132 support_rec(LOWp(node), support); 2133 support_rec(HIGHp(node), support); 2134} 2135 2136 2137/*=== ONE SATISFYING VARIABLE ASSIGNMENT ===============================*/ 2138 2139/* 2140NAME {* bdd\_satone *} 2141SECTION {* operator *} 2142SHORT {* finds one satisfying variable assignment *} 2143PROTO {* BDD bdd_satone(BDD r) *} 2144DESCR {* Finds a BDD with at most one variable at each level. This BDD 2145 implies {\tt r} and is not false unless {\tt r} is 2146 false. *} 2147ALSO {* bdd\_satoneset, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} 2148RETURN {* The result of the operation. *} 2149*/ 2150BDD bdd_satone(BDD r) 2151{ 2152 BDD res; 2153 2154 CHECKa(r, bddfalse); 2155 if (r < 2) 2156 return r; 2157 2158 bdd_disable_reorder(); 2159 2160 bddrefstacktop = bddrefstack; 2161 res = satone_rec(r); 2162 2163 bdd_enable_reorder(); 2164 2165 checkresize(); 2166 return res; 2167} 2168 2169 2170static BDD satone_rec(BDD r) 2171{ 2172 if (ISCONST(r)) 2173 return r; 2174 2175 if (ISZERO(LOW(r))) 2176 { 2177 BDD res = satone_rec(HIGH(r)); 2178 return PUSHREF( bdd_makenode(LEVEL(r), BDDZERO, res) ); 2179 } 2180 else 2181 { 2182 BDD res = satone_rec(LOW(r)); 2183 return PUSHREF( bdd_makenode(LEVEL(r), res, BDDZERO) ); 2184 } 2185} 2186 2187 2188/* 2189NAME {* bdd\_satoneset *} 2190SECTION {* operator *} 2191SHORT {* finds one satisfying variable assignment *} 2192PROTO {* BDD bdd_satoneset(BDD r, BDD var, BDD pol) *} 2193DESCR {* Finds a minterm in {\tt r}. The {\tt var} argument is a 2194 variable set that defines a set of variables that {\em must} be 2195 mentioned in the result. The polarity of these variables in 2196 result---in case they are undefined in {\tt r}---are defined 2197 by the {\tt pol} parameter. If {\tt pol} is the false BDD then 2198 the variables will be in negative form, and otherwise they will 2199 be in positive form. *} 2200ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} 2201RETURN {* The result of the operation. *} 2202*/ 2203BDD bdd_satoneset(BDD r, BDD var, BDD pol) 2204{ 2205 BDD res; 2206 2207 CHECKa(r, bddfalse); 2208 if (ISZERO(r)) 2209 return r; 2210 if (!ISCONST(pol)) 2211 { 2212 bdd_error(BDD_ILLBDD); 2213 return bddfalse; 2214 } 2215 2216 bdd_disable_reorder(); 2217 2218 bddrefstacktop = bddrefstack; 2219 satPolarity = pol; 2220 res = satoneset_rec(r, var); 2221 2222 bdd_enable_reorder(); 2223 2224 checkresize(); 2225 return res; 2226} 2227 2228 2229static BDD satoneset_rec(BDD r, BDD var) 2230{ 2231 if (ISCONST(r) && ISCONST(var)) 2232 return r; 2233 2234 if (LEVEL(r) < LEVEL(var)) 2235 { 2236 if (ISZERO(LOW(r))) 2237 { 2238 BDD res = satoneset_rec(HIGH(r), var); 2239 return PUSHREF( bdd_makenode(LEVEL(r), BDDZERO, res) ); 2240 } 2241 else 2242 { 2243 BDD res = satoneset_rec(LOW(r), var); 2244 return PUSHREF( bdd_makenode(LEVEL(r), res, BDDZERO) ); 2245 } 2246 } 2247 else if (LEVEL(var) < LEVEL(r)) 2248 { 2249 BDD res = satoneset_rec(r, HIGH(var)); 2250 if (satPolarity == BDDONE) 2251 return PUSHREF( bdd_makenode(LEVEL(var), BDDZERO, res) ); 2252 else 2253 return PUSHREF( bdd_makenode(LEVEL(var), res, BDDZERO) ); 2254 } 2255 else /* LEVEL(r) == LEVEL(var) */ 2256 { 2257 if (ISZERO(LOW(r))) 2258 { 2259 BDD res = satoneset_rec(HIGH(r), HIGH(var)); 2260 return PUSHREF( bdd_makenode(LEVEL(r), BDDZERO, res) ); 2261 } 2262 else 2263 { 2264 BDD res = satoneset_rec(LOW(r), HIGH(var)); 2265 return PUSHREF( bdd_makenode(LEVEL(r), res, BDDZERO) ); 2266 } 2267 } 2268 2269} 2270 2271 2272/*=== EXACTLY ONE SATISFYING VARIABLE ASSIGNMENT =======================*/ 2273 2274/* 2275NAME {* bdd\_fullsatone *} 2276SECTION {* operator *} 2277SHORT {* finds one satisfying variable assignment *} 2278PROTO {* BDD bdd_fullsatone(BDD r) *} 2279DESCR {* Finds a BDD with exactly one variable at all levels. This BDD 2280 implies {\tt r} and is not false unless {\tt r} is 2281 false. *} 2282ALSO {* bdd\_satone, bdd\_satoneset, bdd\_satcount, bdd\_satcountln *} 2283RETURN {* The result of the operation. *} 2284*/ 2285BDD bdd_fullsatone(BDD r) 2286{ 2287 BDD res; 2288 int v; 2289 2290 CHECKa(r, bddfalse); 2291 if (r == 0) 2292 return 0; 2293 2294 bdd_disable_reorder(); 2295 2296 bddrefstacktop = bddrefstack; 2297 res = fullsatone_rec(r); 2298 2299 for (v=LEVEL(r)-1 ; v>=0 ; v--) 2300 { 2301 res = PUSHREF( bdd_makenode(v, res, 0) ); 2302 } 2303 2304 bdd_enable_reorder(); 2305 2306 checkresize(); 2307 return res; 2308} 2309 2310 2311static int fullsatone_rec(int r) 2312{ 2313 if (r < 2) 2314 return r; 2315 2316 if (LOW(r) != 0) 2317 { 2318 int res = fullsatone_rec(LOW(r)); 2319 int v; 2320 2321 for (v=LEVEL(LOW(r))-1 ; v>LEVEL(r) ; v--) 2322 { 2323 res = PUSHREF( bdd_makenode(v, res, 0) ); 2324 } 2325 2326 return PUSHREF( bdd_makenode(LEVEL(r), res, 0) ); 2327 } 2328 else 2329 { 2330 int res = fullsatone_rec(HIGH(r)); 2331 int v; 2332 2333 for (v=LEVEL(HIGH(r))-1 ; v>LEVEL(r) ; v--) 2334 { 2335 res = PUSHREF( bdd_makenode(v, res, 0) ); 2336 } 2337 2338 return PUSHREF( bdd_makenode(LEVEL(r), 0, res) ); 2339 } 2340} 2341 2342 2343/*=== COUNT NUMBER OF SATISFYING ASSIGNMENT ============================*/ 2344 2345/* 2346NAME {* bdd\_satcount *} 2347EXTRA {* bdd\_setcountset *} 2348SECTION {* info *} 2349SHORT {* calculates the number of satisfying variable assignments *} 2350PROTO {* double bdd_satcount(BDD r) 2351double bdd_satcountset(BDD r, BDD varset) *} 2352DESCR {* Calculates how many possible variable assignments there exists 2353 such that {\tt r} is satisfied (true). All defined 2354 variables are considered in the first version. In the 2355 second version, only the variables in the variable 2356 set {\tt varset} are considered. This makes the function a 2357 {\em lot} slower. *} 2358ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcountln *} 2359RETURN {* The number of possible assignments. *} 2360*/ 2361double bdd_satcount(BDD r) 2362{ 2363 double size=1; 2364 2365 CHECKa(r, 0.0); 2366 2367 miscid = CACHEID_SATCOU; 2368 size = pow(2.0, (double)LEVEL(r)); 2369 2370 return size * satcount_rec(r); 2371} 2372 2373 2374double bdd_satcountset(BDD r, BDD varset) 2375{ 2376 double unused = bddvarnum; 2377 BDD n; 2378 2379 if (ISCONST(varset) || ISZERO(r)) /* empty set */ 2380 return 0.0; 2381 2382 for (n=varset ; !ISCONST(n) ; n=HIGH(n)) 2383 unused--; 2384 2385 unused = bdd_satcount(r) / pow(2.0,unused); 2386 2387 return unused >= 1.0 ? unused : 1.0; 2388} 2389 2390 2391static double satcount_rec(int root) 2392{ 2393 BddCacheData *entry; 2394 BddNode *node; 2395 double size, s; 2396 2397 if (root < 2) 2398 return root; 2399 2400 entry = BddCache_lookup(&misccache, SATCOUHASH(root)); 2401 if (entry->a == root && entry->c == miscid) 2402 return entry->r.dres; 2403 2404 node = &bddnodes[root]; 2405 size = 0; 2406 s = 1; 2407 2408 s *= pow(2.0, (float)(LEVEL(LOWp(node)) - LEVELp(node) - 1)); 2409 size += s * satcount_rec(LOWp(node)); 2410 2411 s = 1; 2412 s *= pow(2.0, (float)(LEVEL(HIGHp(node)) - LEVELp(node) - 1)); 2413 size += s * satcount_rec(HIGHp(node)); 2414 2415 entry->a = root; 2416 entry->c = miscid; 2417 entry->r.dres = size; 2418 2419 return size; 2420} 2421 2422 2423/* 2424NAME {* bdd\_satcountln *} 2425EXTRA {* bdd\_setcountlnset *} 2426SECTION {* info *} 2427SHORT {* calculates the log. number of satisfying variable assignments *} 2428PROTO {* double bdd_satcountln(BDD r) 2429double bdd_satcountlnset(BDD r, BDD varset)*} 2430DESCR {* Calculates how many possible variable assignments there 2431 exists such that {\tt r} is satisfied (true) and returns 2432 the logarithm of this. The result is calculated in such a 2433 manner that it is practically impossible to get an 2434 overflow, which is very possible for {\tt bdd\_satcount} if 2435 the number of defined variables is too large. All defined 2436 variables are considered in the first version. In the 2437 second version, only the variables in the variable 2438 set {\tt varset} are considered. This makes the function 2439 a {\em lot} slower! *} 2440ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcount *} 2441RETURN {* The logarithm of the number of possible assignments. *} */ 2442double bdd_satcountln(BDD r) 2443{ 2444 double size; 2445 2446 CHECKa(r, 0.0); 2447 2448 miscid = CACHEID_SATCOULN; 2449 size = satcountln_rec(r); 2450 2451 if (size >= 0.0) 2452 size += LEVEL(r); 2453 2454 return size; 2455} 2456 2457 2458double bdd_satcountlnset(BDD r, BDD varset) 2459{ 2460 double unused = bddvarnum; 2461 BDD n; 2462 2463 if (ISCONST(varset)) /* empty set */ 2464 return 0.0; 2465 2466 for (n=varset ; !ISCONST(n) ; n=HIGH(n)) 2467 unused--; 2468 2469 unused = bdd_satcountln(r) - unused; 2470 2471 return unused >= 0.0 ? unused : 0.0; 2472} 2473 2474 2475static double satcountln_rec(int root) 2476{ 2477 BddCacheData *entry; 2478 BddNode *node; 2479 double size, s1,s2; 2480 2481 if (root == 0) 2482 return -1.0; 2483 if (root == 1) 2484 return 0.0; 2485 2486 entry = BddCache_lookup(&misccache, SATCOUHASH(root)); 2487 if (entry->a == root && entry->c == miscid) 2488 return entry->r.dres; 2489 2490 node = &bddnodes[root]; 2491 2492 s1 = satcountln_rec(LOWp(node)); 2493 if (s1 >= 0.0) 2494 s1 += LEVEL(LOWp(node)) - LEVELp(node) - 1; 2495 2496 s2 = satcountln_rec(HIGHp(node)); 2497 if (s2 >= 0.0) 2498 s2 += LEVEL(HIGHp(node)) - LEVELp(node) - 1; 2499 2500 if (s1 < 0.0) 2501 size = s2; 2502 else if (s2 < 0.0) 2503 size = s1; 2504 else if (s1 < s2) 2505 size = s2 + log1p(pow(2.0,s1-s2)) / M_LN2; 2506 else 2507 size = s1 + log1p(pow(2.0,s2-s1)) / M_LN2; 2508 2509 entry->a = root; 2510 entry->c = miscid; 2511 entry->r.dres = size; 2512 2513 return size; 2514} 2515 2516 2517/*=== COUNT NUMBER OF ALLOCATED NODES ==================================*/ 2518 2519/* 2520NAME {* bdd\_nodecount *} 2521SECTION {* info *} 2522SHORT {* counts the number of nodes used for a BDD *} 2523PROTO {* int bdd_nodecount(BDD r) *} 2524DESCR {* Traverses the BDD and counts all distinct nodes that are used 2525 for the BDD. *} 2526RETURN {* The number of nodes. *} 2527ALSO {* bdd\_pathcount, bdd\_satcount, bdd\_anodecount *} 2528*/ 2529int bdd_nodecount(BDD r) 2530{ 2531 int num=0; 2532 2533 CHECK(r); 2534 2535 bdd_markcount(r, &num); 2536 bdd_unmark(r); 2537 2538 return num; 2539} 2540 2541 2542/* 2543NAME {* bdd\_anodecount *} 2544SECTION {* info *} 2545SHORT {* counts the number of shared nodes in an array of BDDs *} 2546PROTO {* int bdd_anodecount(BDD *r, int num) *} 2547DESCR {* Traverses all of the BDDs in {\tt r} and counts all distinct nodes 2548 that are used in the BDDs--if a node is used in more than one 2549 BDD then it only counts once. The {\tt num} parameter holds the 2550 size of the array. *} 2551RETURN {* The number of nodes *} 2552ALSO {* bdd\_nodecount *} 2553*/ 2554int bdd_anodecount(BDD *r, int num) 2555{ 2556 int n; 2557 int cou=0; 2558 2559 for (n=0 ; n<num ; n++) 2560 bdd_markcount(r[n], &cou); 2561 2562 for (n=0 ; n<num ; n++) 2563 bdd_unmark(r[n]); 2564 2565 return cou; 2566} 2567 2568 2569/*=== NODE PROFILE =====================================================*/ 2570 2571/* 2572NAME {* bdd\_varprofile *} 2573SECTION {* info *} 2574SHORT {* returns a variable profile *} 2575PROTO {* int *bdd_varprofile(BDD r) *} 2576DESCR {* Counts the number of times each variable occurs in the 2577 bdd {\tt r}. The result is stored and returned in an integer array 2578 where the i'th position stores the number of times the i'th 2579 variable occured in the BDD. It is the users responsibility to 2580 free the array again using a call to {\tt free}. *} 2581RETURN {* A pointer to an integer array with the profile or NULL if an 2582 error occured. *} 2583*/ 2584int *bdd_varprofile(BDD r) 2585{ 2586 CHECKa(r, NULL); 2587 2588 if ((varprofile=(int*)malloc(sizeof(int)*bddvarnum)) == NULL) 2589 { 2590 bdd_error(BDD_MEMORY); 2591 return NULL; 2592 } 2593 2594 memset(varprofile, 0, sizeof(int)*bddvarnum); 2595 varprofile_rec(r); 2596 bdd_unmark(r); 2597 return varprofile; 2598} 2599 2600 2601static void varprofile_rec(int r) 2602{ 2603 BddNode *node; 2604 2605 if (r < 2) 2606 return; 2607 2608 node = &bddnodes[r]; 2609 if (LEVELp(node) & MARKON) 2610 return; 2611 2612 varprofile[bddlevel2var[LEVELp(node)]]++; 2613 LEVELp(node) |= MARKON; 2614 2615 varprofile_rec(LOWp(node)); 2616 varprofile_rec(HIGHp(node)); 2617} 2618 2619 2620/*=== COUNT NUMBER OF PATHS ============================================*/ 2621 2622/* 2623NAME {* bdd\_pathcount *} 2624SECTION {* info *} 2625SHORT {* count the number of paths leading to the true terminal *} 2626PROTO {* double bdd_pathcount(BDD r) *} 2627DESCR {* Counts the number of paths from the root node {\tt r} 2628 leading to the terminal true node. *} 2629RETURN {* The number of paths *} 2630ALSO {* bdd\_nodecount, bdd\_satcount *} 2631*/ 2632double bdd_pathcount(BDD r) 2633{ 2634 CHECKa(r, 0.0); 2635 2636 miscid = CACHEID_PATHCOU; 2637 2638 return bdd_pathcount_rec(r); 2639} 2640 2641 2642static double bdd_pathcount_rec(BDD r) 2643{ 2644 BddCacheData *entry; 2645 double size; 2646 2647 if (ISZERO(r)) 2648 return 0.0; 2649 if (ISONE(r)) 2650 return 1.0; 2651 2652 entry = BddCache_lookup(&misccache, PATHCOUHASH(r)); 2653 if (entry->a == r && entry->c == miscid) 2654 return entry->r.dres; 2655 2656 size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r)); 2657 2658 entry->a = r; 2659 entry->c = miscid; 2660 entry->r.dres = size; 2661 2662 return size; 2663} 2664 2665 2666/************************************************************************* 2667 Other internal functions 2668*************************************************************************/ 2669 2670static int varset2vartable(BDD r) 2671{ 2672 BDD n; 2673 2674 if (r < 2) 2675 return bdd_error(BDD_VARSET); 2676 2677 quantvarsetID++; 2678 2679 if (quantvarsetID == INT_MAX) 2680 { 2681 memset(quantvarset, 0, sizeof(int)*bddvarnum); 2682 quantvarsetID = 1; 2683 } 2684 2685 for (n=r ; n > 1 ; n=HIGH(n)) 2686 { 2687 quantvarset[LEVEL(n)] = quantvarsetID; 2688 quantlast = LEVEL(n); 2689 } 2690 2691 return 0; 2692} 2693 2694 2695static int varset2svartable(BDD r) 2696{ 2697 BDD n; 2698 2699 if (r < 2) 2700 return bdd_error(BDD_VARSET); 2701 2702 quantvarsetID++; 2703 2704 if (quantvarsetID == INT_MAX/2) 2705 { 2706 memset(quantvarset, 0, sizeof(int)*bddvarnum); 2707 quantvarsetID = 1; 2708 } 2709 2710 for (n=r ; !ISCONST(n) ; ) 2711 { 2712 if (ISZERO(LOW(n))) 2713 { 2714 quantvarset[LEVEL(n)] = quantvarsetID; 2715 n = HIGH(n); 2716 } 2717 else 2718 { 2719 quantvarset[LEVEL(n)] = -quantvarsetID; 2720 n = LOW(n); 2721 } 2722 quantlast = LEVEL(n); 2723 } 2724 2725 return 0; 2726} 2727 2728 2729/* EOF */ 2730