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