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: kernel.c 33 DESCR: implements the bdd kernel functions. 34 AUTH: Jorn Lind 35 DATE: (C) june 1997 36 37 WARNING: Do not use pointers to nodes across makenode calls, 38 as makenode may resize/move the nodetable. 39 40*************************************************************************/ 41#include <stdlib.h> 42#include <string.h> 43#include <math.h> 44#include <time.h> 45#include <assert.h> 46 47#include "kernel.h" 48#include "cache.h" 49#include "prime.h" 50 51/************************************************************************* 52 Various definitions and global variables 53*************************************************************************/ 54 55/*=== EXTERNAL VARIABLES FOR PACKAGE USERS =============================*/ 56 57/* 58NAME {* bddtrue *} 59SECTION {* kernel *} 60SHORT {* the constant true bdd *} 61PROTO {* extern const BDD bddtrue; *} 62DESCR {* This bdd holds the constant true value *} 63ALSO {* bddfalse, bdd\_true, bdd\_false *} 64*/ 65const BDD bddtrue=1; /* The constant true bdd */ 66 67/* 68NAME {* bddfalse*} 69SECTION {* kernel *} 70SHORT {* the constant false bdd *} 71PROTO {* extern const BDD bddfalse; *} 72DESCR {* This bdd holds the constant false value *} 73ALSO {* bddtrue, bdd\_true, bdd\_false *} 74*/ 75const BDD bddfalse=0; /* The constant false bdd */ 76 77 78/*=== INTERNAL DEFINITIONS =============================================*/ 79 80/* Min. number of nodes (%) that has to be left after a garbage collect 81 unless a resize should be done. */ 82static int minfreenodes=20; 83 84 85/*=== GLOBAL KERNEL VARIABLES ==========================================*/ 86 87int bddrunning; /* Flag - package initialized */ 88int bdderrorcond; /* Some error condition */ 89int bddnodesize; /* Number of allocated nodes */ 90int bddmaxnodesize; /* Maximum allowed number of nodes */ 91int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ 92BddNode* bddnodes; /* All of the bdd nodes */ 93int bddfreepos; /* First free node */ 94int bddfreenum; /* Number of free nodes */ 95long int bddproduced; /* Number of new nodes ever produced */ 96int bddvarnum; /* Number of defined BDD variables */ 97int* bddrefstack; /* Internal node reference stack */ 98int* bddrefstacktop; /* Internal node reference stack top */ 99int* bddvar2level; /* Variable -> level table */ 100int* bddlevel2var; /* Level -> variable table */ 101jmp_buf bddexception; /* Long-jump point for interrupting calc. */ 102int bddresized; /* Flag indicating a resize of the nodetable */ 103 104bddCacheStat bddcachestats; 105 106 107/*=== PRIVATE KERNEL VARIABLES =========================================*/ 108 109static BDD* bddvarset; /* Set of defined BDD variables */ 110static int gbcollectnum; /* Number of garbage collections */ 111static int cachesize; /* Size of the operator caches */ 112static long int gbcclock; /* Clock ticks used in GBC */ 113static int usednodes_nextreorder; /* When to do reorder next time */ 114static bddinthandler err_handler; /* Error handler */ 115static bddgbchandler gbc_handler; /* Garbage collection handler */ 116static bdd2inthandler resize_handler; /* Node-table-resize handler */ 117 118 119 /* Strings for all error mesages */ 120static char *errorstrings[BDD_ERRNUM] = 121{ "Out of memory", "Unknown variable", "Value out of range", 122 "Unknown BDD root dereferenced", "bdd_init() called twice", 123 "File operation failed", "Incorrect file format", 124 "Variables not in ascending order", "User called break", 125 "Mismatch in size of variable sets", 126 "Cannot allocate fewer nodes than already in use", 127 "Unknown operator", "Illegal variable set", 128 "Bad variable block operation", 129 "Trying to decrease the number of variables", 130 "Trying to replace with variables already in the bdd", 131 "Number of nodes reached user defined maximum", 132 "Unknown BDD - was not in node table", 133 "Bad size argument", 134 "Mismatch in bitvector size", 135 "Illegal shift-left/right parameter", 136 "Division by zero" }; 137 138 139/*=== OTHER INTERNAL DEFINITIONS =======================================*/ 140 141#define NODEHASH(lvl,l,h) (TRIPLE(lvl,l,h) % bddnodesize) 142 143 144/************************************************************************* 145 BDD misc. user operations 146*************************************************************************/ 147 148/* 149NAME {* bdd\_init *} 150SECTION {* kernel *} 151SHORT {* initializes the BDD package *} 152PROTO {* int bdd_init(int nodesize, int cachesize) *} 153DESCR {* This function initiates the bdd package and {\em must} be called 154 before any bdd operations are done. The argument {\tt nodesize} 155 is the initial number of nodes in the nodetable and {\tt cachesize} 156 is the fixed size of the internal caches. Typical values for 157 {\tt nodesize} are 10000 nodes for small test examples and up to 158 1000000 nodes for large examples. A cache size of 10000 seems to 159 work good even for large examples, but lesser values should do it 160 for smaller examples. 161 162 The number of cache entries can also be set to depend on the size 163 of the nodetable using a call to {\tt bdd\_setcacheratio}. 164 165 The initial number of nodes is not critical for any bdd operation 166 as the table will be resized whenever there are to few nodes left 167 after a garbage collection. But it does have some impact on the 168 efficency of the operations. *} 169RETURN {* If no errors occur then 0 is returned, otherwise 170 a negative error code. *} 171ALSO {* bdd\_done, bdd\_resize\_hook *} 172*/ 173int bdd_init(int initnodesize, int cs) 174{ 175 int n, err; 176 177 if (bddrunning) 178 return bdd_error(BDD_RUNNING); 179 180 bddnodesize = bdd_prime_gte(initnodesize); 181 182 if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) 183 return bdd_error(BDD_MEMORY); 184 185 bddresized = 0; 186 187 for (n=0 ; n<bddnodesize ; n++) 188 { 189 bddnodes[n].refcou = 0; 190 LOW(n) = -1; 191 bddnodes[n].hash = 0; 192 LEVEL(n) = 0; 193 bddnodes[n].next = n+1; 194 } 195 bddnodes[bddnodesize-1].next = 0; 196 197 bddnodes[0].refcou = bddnodes[1].refcou = MAXREF; 198 LOW(0) = HIGH(0) = 0; 199 LOW(1) = HIGH(1) = 1; 200 201 if ((err=bdd_operator_init(cs)) < 0) 202 { 203 bdd_done(); 204 return err; 205 } 206 207 bddfreepos = 2; 208 bddfreenum = bddnodesize-2; 209 bddrunning = 1; 210 bddvarnum = 0; 211 gbcollectnum = 0; 212 gbcclock = 0; 213 cachesize = cs; 214 usednodes_nextreorder = bddnodesize; 215 bddmaxnodeincrease = DEFAULTMAXNODEINC; 216 217 bdderrorcond = 0; 218 219 bddcachestats.uniqueAccess = 0; 220 bddcachestats.uniqueChain = 0; 221 bddcachestats.uniqueHit = 0; 222 bddcachestats.uniqueMiss = 0; 223 bddcachestats.opHit = 0; 224 bddcachestats.opMiss = 0; 225 bddcachestats.swapCount = 0; 226 227 bdd_gbc_hook(bdd_default_gbchandler); 228 bdd_error_hook(bdd_default_errhandler); 229 bdd_resize_hook(NULL); 230 bdd_pairs_init(); 231 bdd_reorder_init(); 232 bdd_fdd_init(); 233 234 if (setjmp(bddexception) != 0) 235 assert(0); 236 237 return 0; 238} 239 240 241/* 242NAME {* bdd\_done*} 243SECTION {* kernel *} 244SHORT {* resets the bdd package *} 245PROTO {* void bdd_done(void) *} 246DESCR {* This function frees all memory used by the bdd package and resets 247 the package to it's initial state.*} 248ALSO {* bdd\_init *} 249*/ 250void bdd_done(void) 251{ 252 /*sanitycheck(); FIXME */ 253 bdd_fdd_done(); 254 bdd_reorder_done(); 255 bdd_pairs_done(); 256 257 free(bddnodes); 258 free(bddrefstack); 259 free(bddvarset); 260 free(bddvar2level); 261 free(bddlevel2var); 262 263 bddnodes = NULL; 264 bddrefstack = NULL; 265 bddvarset = NULL; 266 267 bdd_operator_done(); 268 269 bddrunning = 0; 270 bddnodesize = 0; 271 bddmaxnodesize = 0; 272 bddvarnum = 0; 273 bddproduced = 0; 274 275 err_handler = NULL; 276 gbc_handler = NULL; 277 resize_handler = NULL; 278} 279 280 281/* 282NAME {* bdd\_setvarnum *} 283SECTION {* kernel *} 284SHORT {* set the number of used bdd variables *} 285PROTO {* int bdd_setvarnum(int num) *} 286DESCR {* This function is used to define the number of variables used in 287 the bdd package. It may be called more than one time, but only 288 to increase the number of variables. The argument 289 {\tt num} is the number of variables to use. *} 290RETURN {* Zero on succes, otherwise a negative error code. *} 291ALSO {* bdd\_ithvar, bdd\_varnum, bdd\_extvarnum *} 292*/ 293int bdd_setvarnum(int num) 294{ 295 int bdv; 296 int oldbddvarnum = bddvarnum; 297 298 bdd_disable_reorder(); 299 300 if (num < 1 || num > MAXVAR) 301 { 302 bdd_error(BDD_RANGE); 303 return bddfalse; 304 } 305 306 if (num < bddvarnum) 307 return bdd_error(BDD_DECVNUM); 308 if (num == bddvarnum) 309 return 0; 310 311 if (bddvarset == NULL) 312 { 313 if ((bddvarset=(BDD*)malloc(sizeof(BDD)*num*2)) == NULL) 314 return bdd_error(BDD_MEMORY); 315 if ((bddlevel2var=(int*)malloc(sizeof(int)*(num+1))) == NULL) 316 { 317 free(bddvarset); 318 return bdd_error(BDD_MEMORY); 319 } 320 if ((bddvar2level=(int*)malloc(sizeof(int)*(num+1))) == NULL) 321 { 322 free(bddvarset); 323 free(bddlevel2var); 324 return bdd_error(BDD_MEMORY); 325 } 326 } 327 else 328 { 329 if ((bddvarset=(BDD*)realloc(bddvarset,sizeof(BDD)*num*2)) == NULL) 330 return bdd_error(BDD_MEMORY); 331 if ((bddlevel2var=(int*)realloc(bddlevel2var,sizeof(int)*(num+1))) == NULL) 332 { 333 free(bddvarset); 334 return bdd_error(BDD_MEMORY); 335 } 336 if ((bddvar2level=(int*)realloc(bddvar2level,sizeof(int)*(num+1))) == NULL) 337 { 338 free(bddvarset); 339 free(bddlevel2var); 340 return bdd_error(BDD_MEMORY); 341 } 342 } 343 344 if (bddrefstack != NULL) 345 free(bddrefstack); 346 bddrefstack = bddrefstacktop = (int*)malloc(sizeof(int)*(num*2+4)); 347 348 for(bdv=bddvarnum ; bddvarnum < num; bddvarnum++) 349 { 350 bddvarset[bddvarnum*2] = PUSHREF( bdd_makenode(bddvarnum, 0, 1) ); 351 bddvarset[bddvarnum*2+1] = bdd_makenode(bddvarnum, 1, 0); 352 POPREF(1); 353 354 if (bdderrorcond) 355 { 356 bddvarnum = bdv; 357 return -bdderrorcond; 358 } 359 360 bddnodes[bddvarset[bddvarnum*2]].refcou = MAXREF; 361 bddnodes[bddvarset[bddvarnum*2+1]].refcou = MAXREF; 362 bddlevel2var[bddvarnum] = bddvarnum; 363 bddvar2level[bddvarnum] = bddvarnum; 364 } 365 366 LEVEL(0) = num; 367 LEVEL(1) = num; 368 bddvar2level[num] = num; 369 bddlevel2var[num] = num; 370 371 bdd_pairs_resize(oldbddvarnum, bddvarnum); 372 bdd_operator_varresize(); 373 374 bdd_enable_reorder(); 375 376 return 0; 377} 378 379 380/* 381NAME {* bdd\_extvarnum *} 382SECTION {* kernel *} 383SHORT {* add extra BDD variables *} 384PROTO {* int bdd_extvarnum(int num) *} 385DESCR {* Extends the current number of allocated BDD variables with 386 {\tt num} extra variables. *} 387RETURN {* The old number of allocated variables or a negative error code. *} 388ALSO {* bdd\_setvarnum, bdd\_ithvar, bdd\_nithvar *} 389*/ 390int bdd_extvarnum(int num) 391{ 392 int start = bddvarnum; 393 394 if (num < 0 || num > 0x3FFFFFFF) 395 return bdd_error(BDD_RANGE); 396 397 bdd_setvarnum(bddvarnum+num); 398 return start; 399} 400 401 402/* 403NAME {* bdd\_error\_hook *} 404SECTION {* kernel *} 405SHORT {* set a handler for error conditions *} 406PROTO {* bddinthandler bdd_error_hook(bddinthandler handler) *} 407DESCR {* Whenever an error occurs in the bdd package a test is done to 408 see if an error handler is supplied by the user and if such exists 409 then it will be called 410 with an error code in the variable {\tt errcode}. The handler may 411 then print any usefull information and return or exit afterwards. 412 413 This function sets the handler to be {\tt handler}. If a {\tt NULL} 414 argument is supplied then no calls are made when an error occurs. 415 Possible error codes are found in {\tt bdd.h}. The default handler 416 is {\tt bdd\_default\_errhandler} which will use {\tt exit()} to 417 terminate the program. 418 419 Any handler should be defined like this: 420 \begin{verbatim} 421void my_error_handler(int errcode) 422{ 423 ... 424} 425\end{verbatim} *} 426RETURN {* The previous handler *} 427ALSO {* bdd\_errstring *} 428*/ 429bddinthandler bdd_error_hook(bddinthandler handler) 430{ 431 bddinthandler tmp = err_handler; 432 err_handler = handler; 433 return tmp; 434} 435 436 437/* 438NAME {* bdd\_clear\_error *} 439SECTION {* kernel *} 440SHORT {* clears an error condition in the kernel *} 441PROTO {* void bdd_clear_error(void) *} 442DESCR {* The BuDDy kernel may at some point run out of new ROBDD nodes if 443 a maximum limit is set with {\tt bdd\_setmaxnodenum}. In this case 444 the current error handler is called and an internal error flag 445 is set. Further calls to BuDDy will always return {\tt bddfalse}. 446 From here BuDDy must either be restarted or {\tt bdd\_clear\_error} 447 may be called after action is taken to let BuDDy continue. This may 448 not be especially usefull since the default error handler exits 449 the program - other needs may of course exist.*} 450ALSO {* bdd\_error\_hook, bdd\_setmaxnodenum *} 451*/ 452void bdd_clear_error(void) 453{ 454 bdderrorcond = 0; 455 bdd_operator_reset(); 456} 457 458 459/* 460NAME {* bdd\_gbc\_hook *} 461SECTION {* kernel *} 462SHORT {* set a handler for garbage collections *} 463PROTO {* bddgbchandler bdd_gbc_hook(bddgbchandler handler) *} 464DESCR {* Whenever a garbage collection is required, a test is done to 465 see if a handler for this event is supplied by the user and if such 466 exists then it is called, both before and after the garbage collection 467 takes places. This is indicated by an integer flag {\tt pre} passed to 468 the handler, which will be one before garbage collection and zero 469 after garbage collection. 470 471 This function sets the handler to be {\tt handler}. If a {\tt 472 NULL} argument is supplied then no calls are made when a 473 garbage collection takes place. The argument {\tt pre} 474 indicates pre vs. post garbage collection and the argument 475 {\tt stat} contains information about the garbage 476 collection. The default handler is {\tt bdd\_default\_gbchandler}. 477 478 Any handler should be defined like this: 479 \begin{verbatim} 480void my_gbc_handler(int pre, bddGbcStat *stat) 481{ 482 ... 483} 484\end{verbatim} *} 485RETURN {* The previous handler *} 486ALSO {* bdd\_resize\_hook, bdd\_reorder\_hook *} */ 487bddgbchandler bdd_gbc_hook(bddgbchandler handler) 488{ 489 bddgbchandler tmp = gbc_handler; 490 gbc_handler = handler; 491 return tmp; 492} 493 494 495/* 496NAME {* bdd\_resize\_hook *} 497SECTION {* kernel *} 498SHORT {* set a handler for nodetable resizes *} 499PROTO {* bdd2inthandler bdd_resize_hook(bdd2inthandler handler) *} 500DESCR {* Whenever it is impossible to get enough free nodes by a garbage 501 collection then the node table is resized and a test is done to see 502 if a handler is supllied by the user for this event. If so then 503 it is called with {\tt oldsize} being the old nodetable size and 504 {\tt newsize} being the new nodetable size. 505 506 This function sets the handler to be {\tt handler}. If a {\tt NULL} 507 argument is supplied then no calls are made when a table resize 508 is done. No default handler is supplied. 509 510 Any handler should be defined like this: 511 \begin{verbatim} 512void my_resize_handler(int oldsize, int newsize) 513{ 514 ... 515} 516\end{verbatim} *} 517RETURN {* The previous handler *} 518ALSO {* bdd\_gbc\_hook, bdd\_reorder\_hook, bdd\_setminfreenodes *} 519*/ 520bdd2inthandler bdd_resize_hook(bdd2inthandler handler) 521{ 522 bdd2inthandler tmp = handler; 523 resize_handler = handler; 524 return tmp; 525} 526 527 528/* 529NAME {* bdd\_setmaxincrease *} 530SECTION {* kernel *} 531SHORT {* set max. number of nodes used to increase node table *} 532PROTO {* int bdd_setmaxincrease(int size) *} 533DESCR {* The node table is expanded by doubling the size of the table 534 when no more free nodes can be found, but a maximum for the 535 number of new nodes added can be set with {\tt bdd\_maxincrease} 536 to {\tt size} nodes. The default is 50000 nodes (1 Mb). *} 537RETURN {* The old threshold on succes, otherwise a negative error code. *} 538ALSO {* bdd\_setmaxnodenum, bdd\_setminfreenodes *} 539*/ 540int bdd_setmaxincrease(int size) 541{ 542 int old = bddmaxnodeincrease; 543 544 if (size < 0) 545 return bdd_error(BDD_SIZE); 546 547 bddmaxnodeincrease = size; 548 return old; 549} 550 551/* 552NAME {* bdd\_setmaxnodenum *} 553SECTION {* kernel *} 554SHORT {* set the maximum available number of bdd nodes *} 555PROTO {* int bdd_setmaxnodenum(int size) *} 556DESCR {* This function sets the maximal number of bdd nodes the package may 557 allocate before it gives up a bdd operation. The 558 argument {\tt size} is the absolute maximal number of nodes there 559 may be allocated for the nodetable. Any attempt to allocate more 560 nodes results in the constant false being returned and the error 561 handler being called until some nodes are deallocated. 562 A value of 0 is interpreted as an unlimited amount. 563 It is {\em not} possible to specify 564 fewer nodes than there has already been allocated. *} 565RETURN {* The old threshold on succes, otherwise a negative error code. *} 566ALSO {* bdd\_setmaxincrease, bdd\_setminfreenodes *} 567*/ 568int bdd_setmaxnodenum(int size) 569{ 570 if (size > bddnodesize || size == 0) 571 { 572 int old = bddmaxnodesize; 573 bddmaxnodesize = size; 574 return old; 575 } 576 577 return bdd_error(BDD_NODES); 578} 579 580 581/* 582NAME {* bdd\_setminfreenodes *} 583SECTION {* kernel *} 584SHORT {* set min. no. of nodes to be reclaimed after GBC. *} 585PROTO {* int bdd_setminfreenodes(int n) *} 586DESCR {* Whenever a garbage collection is executed the number of free 587 nodes left are checked to see if a resize of the node table is 588 required. If $X = (\mathit{bddfreenum}*100)/\mathit{maxnum}$ 589 is less than or 590 equal to {\tt n} then a resize is initiated. The range of 591 {\tt X} is of course $0\ldots 100$ and has some influence 592 on how fast the package is. A low number means harder attempts 593 to avoid resizing and saves space, and a high number reduces 594 the time used in garbage collections. The default value is 595 20. *} 596RETURN {* The old threshold on succes, otherwise a negative error code. *} 597ALSO {* bdd\_setmaxnodenum, bdd\_setmaxincrease *} 598*/ 599int bdd_setminfreenodes(int mf) 600{ 601 int old = minfreenodes; 602 603 if (mf<0 || mf>100) 604 return bdd_error(BDD_RANGE); 605 606 minfreenodes = mf; 607 return old; 608} 609 610 611/* 612NAME {* bdd\_getnodenum *} 613SECTION {* kernel *} 614SHORT {* get the number of active nodes in use *} 615PROTO {* int bdd_getnodenum(void) *} 616DESCR {* Returns the number of nodes in the nodetable that are 617 currently in use. Note that dead nodes that have not been 618 reclaimed yet 619 by a garbage collection are counted as active. *} 620RETURN {* The number of nodes. *} 621ALSO {* bdd\_getallocnum, bdd\_setmaxnodenum *} 622*/ 623int bdd_getnodenum(void) 624{ 625 return bddnodesize - bddfreenum; 626} 627 628 629/* 630NAME {* bdd\_getallocnum *} 631SECTION {* kernel *} 632SHORT {* get the number of allocated nodes *} 633PROTO {* int bdd_getallocnum(void) *} 634DESCR {* Returns the number of nodes currently allocated. This includes 635 both dead and active nodes. *} 636RETURN {* The number of nodes. *} 637ALSO {* bdd\_getnodenum, bdd\_setmaxnodenum *} 638*/ 639int bdd_getallocnum(void) 640{ 641 return bddnodesize; 642} 643 644 645/* 646NAME {* bdd\_isrunning *} 647SECTION {* kernel *} 648SHORT {* test whether the package is started or not *} 649PROTO {* void bdd_isrunning(void) *} 650DESCR {* This function tests the internal state of the package and returns 651 a status. *} 652RETURN {* 1 (true) if the package has been started, otherwise 0. *} 653ALSO {* bdd\_init, bdd\_done *} 654*/ 655int bdd_isrunning(void) 656{ 657 return bddrunning; 658} 659 660 661/* 662NAME {* bdd\_versionstr *} 663SECTION {* kernel *} 664SHORT {* returns a text string with version information *} 665PROTO {* char* bdd_versionstr(void) *} 666DESCR {* This function returns a text string with information about the 667 version of the bdd package. *} 668ALSO {* bdd\_versionnum *} 669*/ 670char *bdd_versionstr(void) 671{ 672 static char str[100]; 673 sprintf(str, "BuDDy - release %d.%d", VERSION/10, VERSION%10); 674 return str; 675} 676 677 678/* 679NAME {* bdd\_versionnum *} 680SECTION {* kernel *} 681SHORT {* returns the version number of the bdd package *} 682PROTO {* int bdd_versionnum(void) *} 683DESCR {* This function returns the version number of the bdd package. The 684 number is in the range 10-99 for version 1.0 to 9.9. *} 685ALSO {* bdd\_versionstr *} 686*/ 687int bdd_versionnum(void) 688{ 689 return VERSION; 690} 691 692 693/* 694NAME {* bdd\_stats *} 695SECTION {* kernel *} 696SHORT {* returns some status information about the bdd package *} 697PROTO {* void bdd_stats(bddStat* stat) *} 698DESCR {* This function acquires information about the internal state of 699 the bdd package. The status information is written into the 700 {\tt stat} argument. *} 701ALSO {* bddStat *} 702*/ 703void bdd_stats(bddStat *s) 704{ 705 s->produced = bddproduced; 706 s->nodenum = bddnodesize; 707 s->maxnodenum = bddmaxnodesize; 708 s->freenodes = bddfreenum; 709 s->minfreenodes = minfreenodes; 710 s->varnum = bddvarnum; 711 s->cachesize = cachesize; 712 s->gbcnum = gbcollectnum; 713} 714 715 716 717/* 718NAME {* bdd\_cachestats *} 719SECTION {* kernel *} 720SHORT {* Fetch cache access usage *} 721PROTO {* void bdd_cachestats(bddCacheStat *s) *} 722DESCR {* Fetches cache usage information and stores it in {\tt s}. The 723 fields of {\tt s} can be found in the documentaion for 724 {\tt bddCacheStat}. This function may or may not be compiled 725 into the BuDDy package - depending on the setup at compile 726 time of BuDDy. *} 727ALSO {* bddCacheStat, bdd\_printstat *} 728*/ 729void bdd_cachestats(bddCacheStat *s) 730{ 731 *s = bddcachestats; 732} 733 734 735/* 736NAME {* bdd\_printstat *} 737EXTRA {* bdd\_fprintstat *} 738SECTION {* kernel *} 739SHORT {* print cache statistics *} 740PROTO {* void bdd_printstat(void) 741void bdd_fprintstat(FILE *ofile) *} 742DESCR {* Prints information about the cache performance on standard output 743 (or the supplied file). The information contains the number of 744 accesses to the unique node table, the number of times a node 745 was (not) found there and how many times a hash chain had to 746 traversed. Hit and miss count is also given for the operator 747 caches. *} 748ALSO {* bddCacheStat, bdd\_cachestats *} 749*/ 750void bdd_fprintstat(FILE *ofile) 751{ 752 bddCacheStat s; 753 bdd_cachestats(&s); 754 755 fprintf(ofile, "\nCache statistics\n"); 756 fprintf(ofile, "----------------\n"); 757 758 fprintf(ofile, "Unique Access: %ld\n", s.uniqueAccess); 759 fprintf(ofile, "Unique Chain: %ld\n", s.uniqueChain); 760 fprintf(ofile, "Unique Hit: %ld\n", s.uniqueHit); 761 fprintf(ofile, "Unique Miss: %ld\n", s.uniqueMiss); 762 fprintf(ofile, "=> Hit rate = %.2f\n", 763 (s.uniqueHit+s.uniqueMiss > 0) ? 764 ((float)s.uniqueHit)/((float)s.uniqueHit+s.uniqueMiss) : 0); 765 fprintf(ofile, "Operator Hits: %ld\n", s.opHit); 766 fprintf(ofile, "Operator Miss: %ld\n", s.opMiss); 767 fprintf(ofile, "=> Hit rate = %.2f\n", 768 (s.opHit+s.opMiss > 0) ? 769 ((float)s.opHit)/((float)s.opHit+s.opMiss) : 0); 770 fprintf(ofile, "Swap count = %ld\n", s.swapCount); 771} 772 773 774void bdd_printstat(void) 775{ 776 bdd_fprintstat(stdout); 777} 778 779 780/************************************************************************* 781 Error handler 782*************************************************************************/ 783 784/* 785NAME {* bdd\_errstring *} 786SECTION {* kernel *} 787SHORT {* converts an error code to a string*} 788PROTO {* const char *bdd_errstring(int errorcode) *} 789DESCR {* Converts a negative error code {\tt errorcode} to a descriptive 790 string that can be used for error handling. *} 791RETURN {* An error description string if {\tt e} is known, otherwise {\tt NULL}. *} 792ALSO {* bdd\_err\_hook *} 793*/ 794const char *bdd_errstring(int e) 795{ 796 e = abs(e); 797 if (e<1 || e>BDD_ERRNUM) 798 return NULL; 799 return errorstrings[e-1]; 800} 801 802 803void bdd_default_errhandler(int e) 804{ 805 fprintf(stderr, "BDD error: %s\n", bdd_errstring(e)); 806 exit(1); 807} 808 809 810int bdd_error(int e) 811{ 812 if (err_handler != NULL) 813 err_handler(e); 814 815 return e; 816} 817 818 819/************************************************************************* 820 BDD primitives 821*************************************************************************/ 822 823/* 824NAME {* bdd\_true *} 825SECTION {* kernel *} 826SHORT {* returns the constant true bdd *} 827PROTO {* BDD bdd_true(void) *} 828DESCR {* This function returns the constant true bdd and can freely be 829 used together with the {\tt bddtrue} and {\tt bddfalse} 830 constants. *} 831RETURN {* The constant true bdd *} 832ALSO {* bdd\_false, bddtrue, bddfalse *} 833*/ 834BDD bdd_true(void) 835{ 836 return 1; 837} 838 839 840/* 841NAME {* bdd\_false *} 842SECTION {* kernel *} 843SHORT {* returns the constant false bdd *} 844PROTO {* BDD bdd_false(void) *} 845DESCR {* This function returns the constant false bdd and can freely be 846 used together with the {\tt bddtrue} and {\tt bddfalse} 847 constants. *} 848RETURN {* The constant false bdd *} 849ALSO {* bdd\_true, bddtrue, bddfalse *} 850*/ 851BDD bdd_false(void) 852{ 853 return 0; 854} 855 856 857/* 858NAME {* bdd\_ithvar *} 859SECTION {* kernel *} 860SHORT {* returns a bdd representing the I'th variable *} 861PROTO {* BDD bdd_ithvar(int var) *} 862DESCR {* This function is used to get a bdd representing the I'th 863 variable (one node with the childs true and false). The requested 864 variable must be in the range define by {\tt 865 bdd\_setvarnum} starting with 0 being the first. For ease 866 of use then the bdd returned from {\tt bdd\_ithvar} does 867 not have to be referenced counted with a call to {\tt 868 bdd\_addref}. The initial variable order is defined by the 869 the index {\tt var} that also defines the position in the 870 variable order -- variables with lower indecies are before 871 those with higher indecies. *} 872RETURN {* The I'th variable on succes, otherwise the constant false bdd *} 873ALSO {* bdd\_setvarnum, bdd\_nithvar, bddtrue, bddfalse *} */ 874BDD bdd_ithvar(int var) 875{ 876 if (var < 0 || var >= bddvarnum) 877 { 878 bdd_error(BDD_VAR); 879 return bddfalse; 880 } 881 882 return bddvarset[var*2]; 883} 884 885 886/* 887NAME {* bdd\_nithvar *} 888SECTION {* kernel *} 889SHORT {* returns a bdd representing the negation of the I'th variable *} 890PROTO {* BDD bdd_nithvar(int var) *} 891DESCR {* This function is used to get a bdd representing the negation of 892 the I'th variable (one node with the childs false and true). 893 The requested variable must be in the range define by 894 {\tt bdd\_setvarnum} starting with 0 being the first. For ease of 895 use then the bdd returned from {\tt bdd\_nithvar} does not have 896 to be referenced counted with a call to {\tt bdd\_addref}. *} 897RETURN {* The negated I'th variable on succes, otherwise the constant false bdd *} 898ALSO {* bdd\_setvarnum, bdd\_ithvar, bddtrue, bddfalse *} 899*/ 900BDD bdd_nithvar(int var) 901{ 902 if (var < 0 || var >= bddvarnum) 903 { 904 bdd_error(BDD_VAR); 905 return bddfalse; 906 } 907 908 return bddvarset[var*2+1]; 909} 910 911 912/* 913NAME {* bdd\_varnum *} 914SECTION {* kernel *} 915SHORT {* returns the number of defined variables *} 916PROTO {* int bdd_varnum(void) *} 917DESCR {* This function returns the number of variables defined by 918 a call to {\tt bdd\_setvarnum}.*} 919RETURN {* The number of defined variables *} 920ALSO {* bdd\_setvarnum, bdd\_ithvar *} 921*/ 922int bdd_varnum(void) 923{ 924 return bddvarnum; 925} 926 927 928/* 929NAME {* bdd\_var *} 930SECTION {* info *} 931SHORT {* gets the variable labeling the bdd *} 932PROTO {* int bdd_var(BDD r) *} 933DESCR {* Gets the variable labeling the bdd {\tt r}. *} 934RETURN {* The variable number. *} 935*/ 936int bdd_var(BDD root) 937{ 938 CHECK(root); 939 if (root < 2) 940 return bdd_error(BDD_ILLBDD); 941 942 return (bddlevel2var[LEVEL(root)]); 943} 944 945 946/* 947NAME {* bdd\_low *} 948SECTION {* info *} 949SHORT {* gets the false branch of a bdd *} 950PROTO {* BDD bdd_low(BDD r) *} 951DESCR {* Gets the false branch of the bdd {\tt r}. *} 952RETURN {* The bdd of the false branch *} 953ALSO {* bdd\_high *} 954*/ 955BDD bdd_low(BDD root) 956{ 957 CHECK(root); 958 if (root < 2) 959 return bdd_error(BDD_ILLBDD); 960 961 return (LOW(root)); 962} 963 964 965/* 966NAME {* bdd\_high *} 967SECTION {* info *} 968SHORT {* gets the true branch of a bdd *} 969PROTO {* BDD bdd_high(BDD r) *} 970DESCR {* Gets the true branch of the bdd {\tt r}. *} 971RETURN {* The bdd of the true branch *} 972ALSO {* bdd\_low *} 973*/ 974BDD bdd_high(BDD root) 975{ 976 CHECK(root); 977 if (root < 2) 978 return bdd_error(BDD_ILLBDD); 979 980 return (HIGH(root)); 981} 982 983 984 985/************************************************************************* 986 Garbage collection and node referencing 987*************************************************************************/ 988 989void bdd_default_gbchandler(int pre, bddGbcStat *s) 990{ 991 if (!pre) 992 { 993 printf("Garbage collection #%d: %d nodes / %d free", 994 s->num, s->nodes, s->freenodes); 995 printf(" / %.1fs / %.1fs total\n", 996 (float)s->time/(float)(CLOCKS_PER_SEC), 997 (float)s->sumtime/(float)CLOCKS_PER_SEC); 998 } 999} 1000 1001 1002static void bdd_gbc_rehash(void) 1003{ 1004 int n; 1005 1006 bddfreepos = 0; 1007 bddfreenum = 0; 1008 1009 for (n=bddnodesize-1 ; n>=2 ; n--) 1010 { 1011 register BddNode *node = &bddnodes[n]; 1012 1013 if (LOWp(node) != -1) 1014 { 1015 register unsigned int hash; 1016 1017 hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); 1018 node->next = bddnodes[hash].hash; 1019 bddnodes[hash].hash = n; 1020 } 1021 else 1022 { 1023 node->next = bddfreepos; 1024 bddfreepos = n; 1025 bddfreenum++; 1026 } 1027 } 1028} 1029 1030 1031void bdd_gbc(void) 1032{ 1033 int *r; 1034 int n; 1035 long int c2, c1 = clock(); 1036 1037 if (gbc_handler != NULL) 1038 { 1039 bddGbcStat s; 1040 s.nodes = bddnodesize; 1041 s.freenodes = bddfreenum; 1042 s.time = 0; 1043 s.sumtime = gbcclock; 1044 s.num = gbcollectnum; 1045 gbc_handler(1, &s); 1046 } 1047 1048 for (r=bddrefstack ; r<bddrefstacktop ; r++) 1049 bdd_mark(*r); 1050 1051 for (n=0 ; n<bddnodesize ; n++) 1052 { 1053 if (bddnodes[n].refcou > 0) 1054 bdd_mark(n); 1055 bddnodes[n].hash = 0; 1056 } 1057 1058 bddfreepos = 0; 1059 bddfreenum = 0; 1060 1061 for (n=bddnodesize-1 ; n>=2 ; n--) 1062 { 1063 register BddNode *node = &bddnodes[n]; 1064 1065 if ((LEVELp(node) & MARKON) && LOWp(node) != -1) 1066 { 1067 register unsigned int hash; 1068 1069 LEVELp(node) &= MARKOFF; 1070 hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); 1071 node->next = bddnodes[hash].hash; 1072 bddnodes[hash].hash = n; 1073 } 1074 else 1075 { 1076 LOWp(node) = -1; 1077 node->next = bddfreepos; 1078 bddfreepos = n; 1079 bddfreenum++; 1080 } 1081 } 1082 1083 bdd_operator_reset(); 1084 1085 c2 = clock(); 1086 gbcclock += c2-c1; 1087 gbcollectnum++; 1088 1089 if (gbc_handler != NULL) 1090 { 1091 bddGbcStat s; 1092 s.nodes = bddnodesize; 1093 s.freenodes = bddfreenum; 1094 s.time = c2-c1; 1095 s.sumtime = gbcclock; 1096 s.num = gbcollectnum; 1097 gbc_handler(0, &s); 1098 } 1099} 1100 1101 1102/* 1103NAME {* bdd\_addref *} 1104SECTION {* kernel *} 1105SHORT {* increases the reference count on a node *} 1106PROTO {* BDD bdd_addref(BDD r) *} 1107DESCR {* Reference counting is done on externaly referenced nodes only 1108 and the count for a specific node {\tt r} can and must be 1109 increased using this function to avoid loosing the node in the next 1110 garbage collection. *} 1111ALSO {* bdd\_delref *} 1112RETURN {* The BDD node {\tt r}. *} 1113*/ 1114BDD bdd_addref(BDD root) 1115{ 1116 if (root < 2 || !bddrunning) 1117 return root; 1118 if (root >= bddnodesize) 1119 return bdd_error(BDD_ILLBDD); 1120 if (LOW(root) == -1) 1121 return bdd_error(BDD_ILLBDD); 1122 1123 INCREF(root); 1124 return root; 1125} 1126 1127 1128/* 1129NAME {* bdd\_delref *} 1130SECTION {* kernel *} 1131SHORT {* decreases the reference count on a node *} 1132PROTO {* BDD bdd_delref(BDD r) *} 1133DESCR {* Reference counting is done on externaly referenced nodes only 1134 and the count for a specific node {\tt r} can and must be 1135 decreased using this function to make it possible to reclaim the 1136 node in the next garbage collection. *} 1137ALSO {* bdd\_addref *} 1138RETURN {* The BDD node {\tt r}. *} 1139*/ 1140BDD bdd_delref(BDD root) 1141{ 1142 if (root < 2 || !bddrunning) 1143 return root; 1144 if (root >= bddnodesize) 1145 return bdd_error(BDD_ILLBDD); 1146 if (LOW(root) == -1) 1147 return bdd_error(BDD_ILLBDD); 1148 1149 DECREF(root); 1150 return root; 1151} 1152 1153 1154/*=== RECURSIVE MARK / UNMARK ==========================================*/ 1155 1156void bdd_mark(int i) 1157{ 1158 BddNode *node; 1159 1160 if (i < 2) 1161 return; 1162 1163 node = &bddnodes[i]; 1164 if (LEVELp(node) & MARKON || LOWp(node) == -1) 1165 return; 1166 1167 LEVELp(node) |= MARKON; 1168 1169 bdd_mark(LOWp(node)); 1170 bdd_mark(HIGHp(node)); 1171} 1172 1173 1174void bdd_mark_upto(int i, int level) 1175{ 1176 BddNode *node = &bddnodes[i]; 1177 1178 if (i < 2) 1179 return; 1180 1181 if (LEVELp(node) & MARKON || LOWp(node) == -1) 1182 return; 1183 1184 if (LEVELp(node) > level) 1185 return; 1186 1187 LEVELp(node) |= MARKON; 1188 1189 bdd_mark_upto(LOWp(node), level); 1190 bdd_mark_upto(HIGHp(node), level); 1191} 1192 1193 1194void bdd_markcount(int i, int *cou) 1195{ 1196 BddNode *node; 1197 1198 if (i < 2) 1199 return; 1200 1201 node = &bddnodes[i]; 1202 if (MARKEDp(node) || LOWp(node) == -1) 1203 return; 1204 1205 SETMARKp(node); 1206 *cou += 1; 1207 1208 bdd_markcount(LOWp(node), cou); 1209 bdd_markcount(HIGHp(node), cou); 1210} 1211 1212 1213void bdd_unmark(int i) 1214{ 1215 BddNode *node; 1216 1217 if (i < 2) 1218 return; 1219 1220 node = &bddnodes[i]; 1221 1222 if (!MARKEDp(node) || LOWp(node) == -1) 1223 return; 1224 UNMARKp(node); 1225 1226 bdd_unmark(LOWp(node)); 1227 bdd_unmark(HIGHp(node)); 1228} 1229 1230 1231void bdd_unmark_upto(int i, int level) 1232{ 1233 BddNode *node = &bddnodes[i]; 1234 1235 if (i < 2) 1236 return; 1237 1238 if (!(LEVELp(node) & MARKON)) 1239 return; 1240 1241 LEVELp(node) &= MARKOFF; 1242 1243 if (LEVELp(node) > level) 1244 return; 1245 1246 bdd_unmark_upto(LOWp(node), level); 1247 bdd_unmark_upto(HIGHp(node), level); 1248} 1249 1250 1251/************************************************************************* 1252 Unique node table functions 1253*************************************************************************/ 1254 1255int bdd_makenode(unsigned int level, int low, int high) 1256{ 1257 register BddNode *node; 1258 register unsigned int hash; 1259 register int res; 1260 1261#ifdef CACHESTATS 1262 bddcachestats.uniqueAccess++; 1263#endif 1264 1265 /* check whether childs are equal */ 1266 if (low == high) 1267 return low; 1268 1269 /* Try to find an existing node of this kind */ 1270 hash = NODEHASH(level, low, high); 1271 res = bddnodes[hash].hash; 1272 1273 while(res != 0) 1274 { 1275 if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) 1276 { 1277#ifdef CACHESTATS 1278 bddcachestats.uniqueHit++; 1279#endif 1280 return res; 1281 } 1282 1283 res = bddnodes[res].next; 1284#ifdef CACHESTATS 1285 bddcachestats.uniqueChain++; 1286#endif 1287 } 1288 1289 /* No existing node -> build one */ 1290#ifdef CACHESTATS 1291 bddcachestats.uniqueMiss++; 1292#endif 1293 1294 /* Any free nodes to use ? */ 1295 if (bddfreepos == 0) 1296 { 1297 if (bdderrorcond) 1298 return 0; 1299 1300 /* Try to allocate more nodes */ 1301 bdd_gbc(); 1302 1303 if ((bddnodesize-bddfreenum) >= usednodes_nextreorder && 1304 bdd_reorder_ready()) 1305 { 1306 longjmp(bddexception,1); 1307 } 1308 1309 if ((bddfreenum*100) / bddnodesize <= minfreenodes) 1310 { 1311 bdd_noderesize(1); 1312 hash = NODEHASH(level, low, high); 1313 } 1314 1315 /* Panic if that is not possible */ 1316 if (bddfreepos == 0) 1317 { 1318 bdd_error(BDD_NODENUM); 1319 bdderrorcond = abs(BDD_NODENUM); 1320 return 0; 1321 } 1322 } 1323 1324 /* Build new node */ 1325 res = bddfreepos; 1326 bddfreepos = bddnodes[bddfreepos].next; 1327 bddfreenum--; 1328 bddproduced++; 1329 1330 node = &bddnodes[res]; 1331 LEVELp(node) = level; 1332 LOWp(node) = low; 1333 HIGHp(node) = high; 1334 1335 /* Insert node */ 1336 node->next = bddnodes[hash].hash; 1337 bddnodes[hash].hash = res; 1338 1339 return res; 1340} 1341 1342 1343int bdd_noderesize(int doRehash) 1344{ 1345 BddNode *newnodes; 1346 int oldsize = bddnodesize; 1347 int n; 1348 1349 if (bddnodesize >= bddmaxnodesize && bddmaxnodesize > 0) 1350 return -1; 1351 1352 bddnodesize = bddnodesize << 1; 1353 1354 if (bddnodesize > oldsize + bddmaxnodeincrease) 1355 bddnodesize = oldsize + bddmaxnodeincrease; 1356 1357 if (bddnodesize > bddmaxnodesize && bddmaxnodesize > 0) 1358 bddnodesize = bddmaxnodesize; 1359 1360 bddnodesize = bdd_prime_lte(bddnodesize); 1361 1362 if (resize_handler != NULL) 1363 resize_handler(oldsize, bddnodesize); 1364 1365 newnodes = (BddNode*)realloc(bddnodes, sizeof(BddNode)*bddnodesize); 1366 if (newnodes == NULL) 1367 return bdd_error(BDD_MEMORY); 1368 bddnodes = newnodes; 1369 1370 if (doRehash) 1371 for (n=0 ; n<oldsize ; n++) 1372 bddnodes[n].hash = 0; 1373 1374 for (n=oldsize ; n<bddnodesize ; n++) 1375 { 1376 bddnodes[n].refcou = 0; 1377 bddnodes[n].hash = 0; 1378 LEVEL(n) = 0; 1379 LOW(n) = -1; 1380 bddnodes[n].next = n+1; 1381 } 1382 bddnodes[bddnodesize-1].next = bddfreepos; 1383 bddfreepos = oldsize; 1384 bddfreenum += bddnodesize - oldsize; 1385 1386 if (doRehash) 1387 bdd_gbc_rehash(); 1388 1389 bddresized = 1; 1390 1391 return 0; 1392} 1393 1394 1395void bdd_checkreorder(void) 1396{ 1397 bdd_reorder_auto(); 1398 1399 /* Do not reorder before twice as many nodes have been used */ 1400 usednodes_nextreorder = 2 * (bddnodesize - bddfreenum); 1401 1402 /* And if very little was gained this time (< 20%) then wait until 1403 * even more nodes (upto twice as many again) have been used */ 1404 if (bdd_reorder_gain() < 20) 1405 usednodes_nextreorder += 1406 (usednodes_nextreorder * (20-bdd_reorder_gain())) / 20; 1407} 1408 1409 1410/************************************************************************* 1411 Variable sets 1412*************************************************************************/ 1413 1414/* 1415NAME {* bdd\_scanset *} 1416SECTION {* kernel *} 1417SHORT {* returns an integer representation of a variable set *} 1418PROTO {* int bdd_scanset(BDD r, int **v, int *n) *} 1419DESCR {* Scans a variable set {\tt r} and copies the stored variables into 1420 an integer array of variable numbers. The argument {\tt v} is 1421 the address of an integer pointer where the array is stored and 1422 {\tt n} is a pointer to an integer where the number of elements 1423 are stored. It is the users responsibility to make sure the 1424 array is deallocated by a call to {\tt free(v)}. The numbers 1425 returned are guaranteed to be in ascending order. *} 1426ALSO {* bdd\_makeset *} 1427RETURN {* Zero on success, otherwise a negative error code. *} 1428*/ 1429int bdd_scanset(BDD r, int **varset, int *varnum) 1430{ 1431 int n, num; 1432 1433 CHECK(r); 1434 if (r < 2) 1435 { 1436 *varnum = 0; 1437 *varset = NULL; 1438 return 0; 1439 } 1440 1441 for (n=r, num=0 ; n > 1 ; n=HIGH(n)) 1442 num++; 1443 1444 if (((*varset) = (int *)malloc(sizeof(int)*num)) == NULL) 1445 return bdd_error(BDD_MEMORY); 1446 1447 for (n=r, num=0 ; n > 1 ; n=HIGH(n)) 1448 (*varset)[num++] = bddlevel2var[LEVEL(n)]; 1449 1450 *varnum = num; 1451 1452 return 0; 1453} 1454 1455 1456/* 1457NAME {* bdd\_makeset *} 1458SECTION {* kernel *} 1459SHORT {* builds a BDD variable set from an integer array *} 1460PROTO {* BDD bdd_makeset(int *v, int n) *} 1461DESCR {* Reads a set of variable numbers from the integer array {\tt v} 1462 which must hold exactly {\tt n} integers and then builds a BDD 1463 representing the variable set. 1464 1465 The BDD variable set is represented as the conjunction of 1466 all the variables in their positive form and may just as 1467 well be made that way by the user. The user should keep a 1468 reference to the returned BDD instead of building it every 1469 time the set is needed. *} 1470ALSO {* bdd\_scanset *} 1471RETURN {* A BDD variable set. *} */ 1472BDD bdd_makeset(int *varset, int varnum) 1473{ 1474 int v, res=1; 1475 1476 for (v=varnum-1 ; v>=0 ; v--) 1477 { 1478 BDD tmp; 1479 bdd_addref(res); 1480 tmp = bdd_apply(res, bdd_ithvar(varset[v]), bddop_and); 1481 bdd_delref(res); 1482 res = tmp; 1483 } 1484 1485 return res; 1486} 1487 1488 1489/* EOF */ 1490