1 /*========================================================================
2 Copyright (C) 1996-2004, 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/bddop.c,v 1.9 2004/01/07 16:05:21 adl Exp $
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
42 #include "kernel.h"
43 #include "cache.h"
44
45 #ifdef __has_attribute
46 # if __has_attribute(fallthrough)
47 # define BUDDY_FALLTHROUGH __attribute__ ((fallthrough))
48 # endif
49 #endif
50 #ifndef BUDDY_FALLTHROUGH
51 # define BUDDY_FALLTHROUGH while (0);
52 #endif
53
54 /* Hash value modifiers to distinguish between entries in misccache */
55 #define CACHEID_CONSTRAIN 0x0
56 #define CACHEID_RESTRICT 0x1
57 #define CACHEID_SATCOU 0x2
58 #define CACHEID_SATCOULN 0x3
59 #define CACHEID_PATHCOU 0x4
60 #define CACHEID_SETXOR 0x5
61 #define CACHEID_SUPPORT 0x6
62 #define CACHEID_IMPLIES 0x7
63 #define CACHEID_COMMON 0x8
64 #define CACHEID_SHORTDIST 0x9
65 #define CACHEID_SHORTBDD 0xA
66
67 /* Hash value modifiers for replace/compose */
68 #define CACHEID_REPLACE 0x0
69 #define CACHEID_COMPOSE 0x1
70 #define CACHEID_VECCOMPOSE 0x2
71
72 /* Hash value modifiers for quantification */
73 #define CACHEID_EXIST 0x0
74 #define CACHEID_FORALL 0x1
75 #define CACHEID_UNIQUE 0x2
76 #define CACHEID_APPEX 0x3
77 #define CACHEID_APPAL 0x4
78 #define CACHEID_APPUN 0x5
79 #define CACHEID_EXISTC 0x6
80 #define CACHEID_FORALLC 0x7
81 #define CACHEID_UNIQUEC 0x8
82 #define CACHEID_APPEXC 0x9
83 #define CACHEID_APPALC 0xA
84 #define CACHEID_APPUNC 0xB
85
86
87 /* Number of boolean operators */
88 #define OPERATOR_NUM 11
89
90 /* Operator results - entry = left<<1 | right (left,right in {0,1}) */
91 static int oprres[OPERATOR_NUM][4] =
92 { {0,0,0,1}, /* and ( & ) */
93 {0,1,1,0}, /* xor ( ^ ) */
94 {0,1,1,1}, /* or ( | ) */
95 {1,1,1,0}, /* nand */
96 {1,0,0,0}, /* nor */
97 {1,1,0,1}, /* implication ( >> ) */
98 {1,0,0,1}, /* bi-implication */
99 {0,0,1,0}, /* difference /greater than ( - ) ( > ) */
100 {0,1,0,0}, /* less than ( < ) */
101 {1,0,1,1}, /* inverse implication ( << ) */
102 {1,1,0,0} /* not ( ! ) */
103 };
104
105
106 /* Variables needed for the operators */
107 static int applyop; /* Current operator for apply */
108 static int appexop; /* Current operator for appex */
109 static int appexid; /* Current cache id for appex */
110 static int quantid; /* Current cache id for quantifications */
111 static int *quantvarset; /* Current variable set for quant. */
112 static int quantvarsetcomp; /* Should quantvarset be complemented? */
113 static int quantvarsetID; /* Current id used in quantvarset */
114 static int quantlast; /* Current last variable to be quant. */
115 static int replaceid; /* Current cache id for replace */
116 static int *replacepair; /* Current replace pair */
117 static int replacelast; /* Current last var. level to replace */
118 static int composelevel; /* Current variable used for compose */
119 static int miscid; /* Current cache id for other results */
120 static int *varprofile; /* Current variable profile */
121 static int supportID; /* Current ID (true value) for support */
122 static int supportMin; /* Min. used level in support calc. */
123 static int supportMax; /* Max. used level in support calc. */
124 static int* supportSet; /* The found support set */
125 static BddCache applycache; /* Cache for apply results */
126 static BddCache itecache; /* Cache for ITE results */
127 static BddCache quantcache; /* Cache for exist/forall results */
128 static BddCache appexcache; /* Cache for appex/appall results */
129 static BddCache replacecache; /* Cache for replace results */
130 static BddCache misccache; /* Cache for other results */
131 static int misccache_varnum; /* if this changes, invalidate misccache */
132 static int cacheratio;
133 static BDD satPolarity;
134 static int firstReorder; /* Used instead of local variable in order
135 to avoid compiler warning about 'first'
136 being clobbered by setjmp */
137
138 static signed char* allsatProfile; /* Variable profile for bdd_allsat() */
139 static bddallsathandler allsatHandler; /* Callback handler for bdd_allsat() */
140
141 extern bddCacheStat bddcachestats;
142
143 /* Internal prototypes */
144 static BDD not_rec(BDD); /* non-recursive implementation */
145 static BDD apply_rec(BDD, BDD); /* non-recursive implementation */
146 static BDD ite_rec(BDD, BDD, BDD); /* non-recursive implementation */
147 static int simplify_rec(BDD, BDD);
148 static BDD quant_rec(BDD); /* non-recursive implementation */
149 static BDD appquant_rec(BDD, BDD); /* non-recursive implementation */
150 static BDD restrict_rec(BDD); /* non-recursive implementation */
151 static BDD constrain_rec(BDD, BDD);
152 static BDD replace_rec(BDD);
153 static BDD bdd_correctify(int, BDD, BDD);
154 static BDD compose_rec(BDD, BDD); /* non-recursive implementation */
155 static BDD veccompose_rec(BDD);
156 static void support_rec(int, int*); /* non-recursive implementation */
157 static BDD satone_rec(BDD); /* non-recursive implementation */
158 static BDD satoneset_rec(BDD, BDD); /* non-recursive implementation */
159 static int fullsatone_rec(int);
160 static BDD satprefix_rec(BDD*);
161 static void allsat_rec(BDD r);
162 static double satcount_rec(int);
163 static double satcountln_rec(int);
164 static void varprofile_rec(int);
165 static double bdd_pathcount_rec(BDD);
166 static int varset2vartable(BDD, int);
167 static int varset2svartable(BDD);
168
169
170 /* Hashvalues */
171 #define NOTHASH(r) (r)
172 #define APPLYHASH(l,r,op) (TRIPLE(l,r,op))
173 #define ITEHASH(f,g,h) (TRIPLE(f,g,h))
174 #define SETXORHASH(l,r) (TRIPLE(l,r,CACHEID_SETXOR))
175 #define IMPLIESHASH(l,r) (TRIPLE(l,r,CACHEID_IMPLIES))
176 #define COMMONHASH(l,r) (TRIPLE(l,r,CACHEID_COMMON))
177 #define RESTRHASH(r,var) (PAIR(r,var))
178 #define CONSTRAINHASH(f,c) (PAIR(f,c))
179 #define QUANTHASH(r) (r)
180 #define REPLACEHASH(r) (r)
181 #define VECCOMPOSEHASH(f) (f)
182 #define COMPOSEHASH(f,g) (PAIR(f,g))
183 #define SATCOUHASH(r) (r)
184 #define PATHCOUHASH(r) (r)
185 #define SUPPORTHASH(r) (PAIR(r,CACHEID_SUPPORT))
186 #define APPEXHASH(l,r,op) (PAIR(l,r))
187 #define SHORTDISTHASH(l,rev) (TRIPLE(l,rev,CACHEID_SHORTDIST))
188 #define SHORTBDDHASH(l,rev) (TRIPLE(l,rev,CACHEID_SHORTBDD))
189
190 #ifndef M_LN2
191 #define M_LN2 0.69314718055994530942
192 #endif
193
194 #define log1p(a) (log(1.0+a))
195
196 /* unsigned check */
197 #define INVARSET(a) ((quantvarset[a] == quantvarsetID) ^ quantvarsetcomp)
198 /* signed check */
199 #define INSVARSET(a) (abs(quantvarset[a]) == quantvarsetID)
200
201 /*************************************************************************
202 Setup and shutdown
203 *************************************************************************/
204
bdd_operator_init(int cachesize)205 int bdd_operator_init(int cachesize)
206 {
207 if (BddCache_init(&applycache,cachesize) < 0)
208 return bdd_error(BDD_MEMORY);
209
210 if (BddCache_init(&itecache,cachesize) < 0)
211 return bdd_error(BDD_MEMORY);
212
213 if (BddCache_init(&quantcache,cachesize) < 0)
214 return bdd_error(BDD_MEMORY);
215
216 if (BddCache_init(&appexcache,cachesize) < 0)
217 return bdd_error(BDD_MEMORY);
218
219 if (BddCache_init(&replacecache,cachesize) < 0)
220 return bdd_error(BDD_MEMORY);
221
222 if (BddCache_init(&misccache,cachesize) < 0)
223 return bdd_error(BDD_MEMORY);
224 misccache_varnum = bddvarnum;
225
226 quantvarsetID = 0;
227 quantvarset = NULL;
228 cacheratio = 0;
229 supportSet = NULL;
230
231 return 0;
232 }
233
234
bdd_operator_done(void)235 void bdd_operator_done(void)
236 {
237 if (quantvarset != NULL)
238 free(quantvarset);
239
240 BddCache_done(&applycache);
241 BddCache_done(&itecache);
242 BddCache_done(&quantcache);
243 BddCache_done(&appexcache);
244 BddCache_done(&replacecache);
245 BddCache_done(&misccache);
246
247 if (supportSet != NULL)
248 free(supportSet);
249 }
250
251
bdd_operator_reset(void)252 void bdd_operator_reset(void)
253 {
254 BddCache_reset(&applycache);
255 BddCache_reset(&itecache);
256 BddCache_reset(&quantcache);
257 BddCache_reset(&appexcache);
258 BddCache_reset(&replacecache);
259 BddCache_reset(&misccache);
260 misccache_varnum = bddvarnum;
261 }
262
263
bdd_operator_varresize(void)264 void bdd_operator_varresize(void)
265 {
266 if (quantvarset != NULL)
267 free(quantvarset);
268
269 if ((quantvarset=NEW(int,bddvarnum)) == NULL)
270 bdd_error(BDD_MEMORY);
271 else
272 memset(quantvarset, 0, sizeof(int)*bddvarnum);
273 quantvarsetID = 0;
274 }
275
276
bdd_operator_noderesize(void)277 static void bdd_operator_noderesize(void)
278 {
279 if (cacheratio > 0)
280 {
281 int newcachesize = bddnodesize / cacheratio;
282 BddCache_resize(&applycache, newcachesize);
283 BddCache_resize(&itecache, newcachesize);
284 BddCache_resize(&quantcache, newcachesize);
285 BddCache_resize(&appexcache, newcachesize);
286 BddCache_resize(&replacecache, newcachesize);
287 BddCache_resize(&misccache, newcachesize);
288 bddcachesize = misccache.tablesize;
289 }
290 }
291
292
293 /*************************************************************************
294 Other
295 *************************************************************************/
296
297 /*
298 NAME {* bdd\_setcacheratio *}
299 SECTION {* kernel *}
300 SHORT {* Sets the cache ratio for the operator caches *}
301 PROTO {* int bdd_setcacheratio(int r) *}
302 DESCR {* The ratio between the number of nodes in the nodetable
303 and the number of entries in the operator cachetables is called
304 the cache ratio. So a cache ratio of say, four, allocates one cache
305 entry for each four unique node entries. This value can be set with
306 {\tt bdd\_setcacheratio} to any positive value. When this is done
307 the caches are resized instantly to fit the new ratio.
308 The default is a fixed cache size determined at
309 initialization time. *}
310 RETURN {* The previous cache ratio or a negative number on error. *}
311 ALSO {* bdd\_init *}
312 */
bdd_setcacheratio(int r)313 int bdd_setcacheratio(int r)
314 {
315 int old = cacheratio;
316
317 if (r <= 0)
318 return bdd_error(BDD_RANGE);
319 if (bddnodesize == 0)
320 return old;
321
322 cacheratio = r;
323 bdd_operator_noderesize();
324 return old;
325 }
326
327
328 /*************************************************************************
329 Operators
330 *************************************************************************/
331
checkresize(void)332 static void checkresize(void)
333 {
334 if (bddresized)
335 bdd_operator_noderesize();
336 bddresized = 0;
337 }
338
339
340 /*=== BUILD A CUBE =====================================================*/
341
342 /*
343 NAME {* bdd\_buildcube *}
344 EXTRA {* bdd\_ibuildcube *}
345 SECTION {* operator *}
346 SHORT {* build a cube from an array of variables *}
347 PROTO {* BDD bdd_buildcube(int value, int width, BDD *var)
348 BDD bdd_ibuildcube(int value, int width, int *var)*}
349 DESCR {* This function builds a cube from the variables in {\tt
350 var}. It does so by interpreting the {\tt width} low order
351 bits of {\tt value} as a bit mask--a set bit indicates that the
352 variable should be added in it's positive form, and a cleared
353 bit the opposite. The most significant bits are encoded with
354 the first variables in {\tt var}. Consider as an example
355 the call {\tt bdd\_buildcube(0xB, 4, var)}. This corresponds
356 to the expression: $var[0] \conj \neg var[1] \conj var[2]
357 \conj var[3]$. The first version of the function takes an array
358 of BDDs, whereas the second takes an array of variable numbers
359 as used in {\tt bdd\_ithvar}. *}
360 RETURN {* The resulting cube *}
361 ALSO {* bdd\_ithvar, fdd\_ithvar *}
362 */
bdd_buildcube(int value,int width,BDD * variables)363 BDD bdd_buildcube(int value, int width, BDD *variables)
364 {
365 BDD result = BDDONE;
366 int z;
367
368 for (z=0 ; z<width ; z++, value>>=1)
369 {
370 BDD tmp;
371 BDD v;
372
373 if (value & 0x1)
374 v = bdd_addref( variables[width-z-1] );
375 else
376 v = bdd_addref( bdd_not(variables[width-z-1]) );
377
378 bdd_addref(result);
379 tmp = bdd_apply(result,v,bddop_and);
380 bdd_delref(result);
381 bdd_delref(v);
382
383 result = tmp;
384 }
385
386 return result;
387 }
388
389
bdd_ibuildcube(int value,int width,int * variables)390 BDD bdd_ibuildcube(int value, int width, int *variables)
391 {
392 BDD result = BDDONE;
393 int z;
394
395 for (z=0 ; z<width ; z++, value>>=1)
396 {
397 BDD tmp;
398 BDD v;
399
400 if (value & 0x1)
401 v = bdd_ithvar(variables[width-z-1]);
402 else
403 v = bdd_nithvar(variables[width-z-1]);
404
405 bdd_addref(result);
406 tmp = bdd_apply(result,v,bddop_and);
407 bdd_delref(result);
408
409 result = tmp;
410 }
411
412 return result;
413 }
414
bdd_ibuildcube2(int width,const int * variables)415 BDD bdd_ibuildcube2(int width, const int *variables)
416 {
417 if (width == 0)
418 return BDDONE;
419
420 BDD result;
421 {
422 int vn = variables[width - 1];
423 if (vn >= 0)
424 result = bdd_ithvar(vn);
425 else
426 result = bdd_nithvar(~vn);
427 }
428
429 for (int z = width - 2 ; z >= 0 ; --z)
430 {
431 BDD v;
432 int vn = variables[z];
433 if (vn >= 0)
434 v = bdd_ithvar(vn);
435 else
436 v = bdd_nithvar(~vn);
437 int lv = LEVEL(v);
438 if (__likely(LEVEL(result) > lv))
439 {
440 PUSHREF(result);
441 if (vn >= 0)
442 result = bdd_makenode(lv, BDDZERO, result);
443 else
444 result = bdd_makenode(lv, result, BDDZERO);
445 POPREF(1);
446 }
447 else
448 {
449 bdd_addref(result);
450 BDD tmp = bdd_apply(result, v, bddop_and);
451 bdd_delref(result);
452 result = tmp;
453 }
454 }
455
456 return result;
457 }
458
bdd_init_minterm(BDD fun,BDD vars)459 mintermEnumerator* bdd_init_minterm(BDD fun, BDD vars)
460 {
461 mintermEnumerator* me = malloc(sizeof(mintermEnumerator));
462 if (__unlikely(me == NULL))
463 {
464 bdd_error(BDD_MEMORY);
465 return NULL;
466 }
467 int* varsptr = malloc(sizeof(int)*bddvarnum);
468 if (__unlikely(varsptr == NULL))
469 {
470 free(me);
471 bdd_error(BDD_MEMORY);
472 return NULL;
473 }
474 int i = 0;
475 while (!ISCONST(vars))
476 {
477 varsptr[i++] = bddlevel2var[LEVEL(vars)];
478 vars = HIGH(vars);
479 }
480 int* stack = malloc(sizeof(int)*i*2);
481 if (__unlikely(stack == NULL))
482 {
483 free(varsptr);
484 free(me);
485 bdd_error(BDD_MEMORY);
486 return NULL;
487 }
488 bdd_addref(fun);
489 me->vars = varsptr;
490 me->stacktop = stack;
491 me->stack = stack;
492 me->fun = fun;
493 me->nvars = i;
494 return me;
495 }
496
bdd_free_minterm(mintermEnumerator * me)497 void bdd_free_minterm(mintermEnumerator* me)
498 {
499 bdd_delref(me->fun);
500 free(me->stack);
501 free(me->vars);
502 free(me);
503 }
504
reset_minterm(mintermEnumerator * me,BDD sub,int var)505 static int reset_minterm(mintermEnumerator*me,
506 BDD sub, int var)
507 {
508 int nvars = me->nvars;
509 int* vars = me->vars;
510 int ls = LEVEL(sub);
511 for (int i = var; i < nvars; ++i)
512 {
513 int v = vars[i];
514 int neg = v < 0;
515 if (neg)
516 v = ~v;
517 int lv = bddvar2level[v];
518 if (ls == lv) /* variable used in fun */
519 {
520 BDD low = LOW(sub);
521 if (low == BDDZERO)
522 {
523 sub = HIGH(sub);
524 }
525 else
526 {
527 if (HIGH(sub) != BDDZERO)
528 {
529 *me->stacktop++ = sub;
530 *me->stacktop++ = i;
531 }
532 v = ~v;
533 sub = low;
534 }
535 ls = LEVEL(sub);
536 }
537 else
538 {
539 *me->stacktop++ = sub;
540 *me->stacktop++ = i;
541 v = ~v;
542 }
543 vars[i] = v;
544 }
545 return 1;
546 }
547
548
bdd_first_minterm(mintermEnumerator * me)549 int bdd_first_minterm(mintermEnumerator* me)
550 {
551 if (__unlikely(me->fun == BDDZERO))
552 return 0;
553 me->stacktop = me->stack;
554 return reset_minterm(me, me->fun, 0);
555 }
556
bdd_next_minterm(mintermEnumerator * me)557 bdd bdd_next_minterm(mintermEnumerator* me)
558 {
559 if (me->stacktop == me->stack) // end of iteration
560 return 0;
561 int *vars = me->vars;
562 // switch polarity of variable of last possible branching
563 int lastbranch = *--me->stacktop;
564 BDD lastsub = *--me->stacktop;
565 int v = ~vars[lastbranch];
566 if (LEVEL(lastsub) == bddvar2level[v])
567 lastsub = HIGH(lastsub);
568 vars[lastbranch] = v;
569 // reset everything below to negative polarity
570 return reset_minterm(me, lastsub, lastbranch + 1);
571 }
572
573
574 /*=== NOT ==============================================================*/
575
576 /*
577 NAME {* bdd\_not *}
578 SECTION {* operator *}
579 SHORT {* negates a bdd *}
580 PROTO {* BDD bdd_not(BDD r) *}
581 DESCR {* Negates the BDD {\tt r} by exchanging
582 all references to the zero-terminal with references to the
583 one-terminal and vice versa. *}
584 RETURN {* The negated bdd. *}
585 */
bdd_not(BDD r)586 BDD bdd_not(BDD r)
587 {
588 BDD res;
589 firstReorder = 1;
590 CHECKa(r, bddfalse);
591
592 again:
593 if (__likely(bddreordermethod == BDD_REORDER_NONE)
594 || setjmp(bddexception) == 0)
595 {
596 INITREF;
597
598 if (__likely(firstReorder))
599 {
600 res = not_rec(r);
601 }
602 else
603 {
604 bdd_disable_reorder();
605 res = not_rec(r);
606 bdd_enable_reorder();
607 }
608 }
609 else
610 {
611 bdd_checkreorder();
612 if (firstReorder-- == 1)
613 goto again;
614 res = BDDZERO; /* avoid warning about res being uninitialized */
615 }
616
617 checkresize();
618 return res;
619 }
620
621
not_rec(BDD r)622 static BDD not_rec(BDD r)
623 {
624 LOCAL_REC_STACKS;
625 int index;
626
627 goto work;
628 do
629 {
630 index = POPINT_();
631 if (index < 0)
632 {
633 r = POPINT_();
634 work:;
635 /* C: NULL --- */
636 /* I: r --- */
637 /* R: --- r */
638 if (ISCONST(r))
639 {
640 PUSHREF_(ISZERO(r) ? BDDONE : BDDZERO);
641 }
642 else
643 {
644 BddCacheData *entry2 =
645 BddCache_index(&applycache, NOTHASH(r), index);
646 if (entry2->i.a == r && entry2->i.c == bddop_not)
647 {
648 #ifdef CACHESTATS
649 bddcachestats.opHit++;
650 #endif
651 PUSHREF_(entry2->i.res);
652 }
653 else
654 {
655 #ifdef CACHESTATS
656 bddcachestats.opMiss++;
657 #endif
658 /* C: -1 r --- (-1 lr) -1 rr index r */
659 PUSH4INT_(r, index, HIGH(r), -1);
660 r = LOW(r);
661 goto work;
662 }
663 }
664 }
665 else
666 {
667 /* C: -1 r --- */
668 /* R: rres lres --- res */
669 BDD rres = READREF_(1);
670 BDD lres = READREF_(2);
671 BDD r = POPINT_();
672 SYNC_REC_STACKS;
673 BDD res = bdd_makenode(LEVEL(r), lres, rres);
674 POPREF_(2);
675 PUSHREF_(res);
676 BddCacheData* entry = applycache.table + index;
677 entry->i.a = r;
678 entry->i.c = bddop_not;
679 entry->i.res = res;
680 }
681 }
682 while (NONEMPTY_REC_STACK);
683
684 BDD res = READREF_(1);
685 POPREF_(1);
686 SYNC_REC_STACKS;
687 return res;
688 }
689
690
691 /*=== APPLY ============================================================*/
692
693 /*
694 NAME {* bdd\_apply *}
695 SECTION {* operator *}
696 SHORT {* basic bdd operations *}
697 PROTO {* BDD bdd_apply(BDD left, BDD right, int opr) *}
698 DESCR {* The {\tt bdd\_apply} function performs all of the basic
699 bdd operations with two operands, such as AND, OR etc.
700 The {\tt left} argument is the left bdd operand and {\tt right}
701 is the right operand. The {\tt opr} argument is the requested
702 operation and must be one of the following\\
703
704 \begin{tabular}{lllc}
705 {\bf Identifier} & {\bf Description} & {\bf Truth table}
706 & {\bf C++ opr.} \\
707 {\tt bddop\_and} & logical and ($A \wedge B$) & [0,0,0,1]
708 & \verb%&% \\
709 {\tt bddop\_xor} & logical xor ($A \oplus B$) & [0,1,1,0]
710 & \verb%^% \\
711 {\tt bddop\_or} & logical or ($A \vee B$) & [0,1,1,1]
712 & \verb%|% \\
713 {\tt bddop\_nand} & logical not-and & [1,1,1,0] \\
714 {\tt bddop\_nor} & logical not-or & [1,0,0,0] \\
715 {\tt bddop\_imp} & implication ($A \Rightarrow B$) & [1,1,0,1]
716 & \verb%>>% \\
717 {\tt bddop\_biimp} & bi-implication ($A \Leftrightarrow B$)& [1,0,0,1] \\
718 {\tt bddop\_diff} & set difference ($A \setminus B$) & [0,0,1,0]
719 & \verb%-% \\
720 {\tt bddop\_less} & less than ($A < B$) & [0,1,0,0]
721 & \verb%<% \\
722 {\tt bddop\_invimp} & reverse implication ($A \Leftarrow B$)& [1,0,1,1]
723 & \verb%<<% \\
724 \end{tabular}
725 *}
726 RETURN {* The result of the operation. *}
727 ALSO {* bdd\_ite *}
728 */
bdd_apply(BDD l,BDD r,int op)729 BDD bdd_apply(BDD l, BDD r, int op)
730 {
731 BDD res;
732 firstReorder = 1;
733
734 CHECKa(l, bddfalse);
735 CHECKa(r, bddfalse);
736
737 #ifndef NDEBUG
738 if (op<0 || op>bddop_invimp)
739 {
740 bdd_error(BDD_OP);
741 return bddfalse;
742 }
743 #endif
744
745 again:
746 if (__likely(bddreordermethod == BDD_REORDER_NONE)
747 || setjmp(bddexception) == 0)
748 {
749 INITREF;
750 applyop = op;
751
752 if (__likely(firstReorder))
753 {
754 res = apply_rec(l, r);
755 }
756 else
757 {
758 bdd_disable_reorder();
759 res = apply_rec(l, r);
760 bdd_enable_reorder();
761 }
762 }
763 else
764 {
765 bdd_checkreorder();
766
767 if (firstReorder-- == 1)
768 goto again;
769 res = BDDZERO; /* avoid warning about res being uninitialized */
770 }
771
772 checkresize();
773 return res;
774 }
775
776 #define RETURN(val) { PUSHREF_(val); continue; }
777 #define APPLY_SHORTCUTS(op, rec) \
778 switch (op) \
779 { \
780 case bddop_and: \
781 if (l == r) \
782 RETURN(rec(l)); \
783 if (l > r) \
784 { \
785 BDD tmp = l; \
786 l = r; \
787 r = tmp; \
788 } \
789 if (ISCONST(l)) \
790 RETURN(ISONE(l) ? rec(r) : 0); \
791 break; \
792 case bddop_or: \
793 if (l == r) \
794 RETURN(rec(l)); \
795 if (l > r) \
796 { \
797 BDD tmp = l; \
798 l = r; \
799 r = tmp; \
800 } \
801 if (ISCONST(l)) \
802 RETURN(ISZERO(l) ? rec(r) : 1); \
803 break; \
804 case bddop_xor: \
805 if (l == r) \
806 RETURN(0); \
807 if (l > r) \
808 { \
809 BDD tmp = l; \
810 l = r; \
811 r = tmp; \
812 } \
813 if (ISZERO(l)) \
814 RETURN(rec(r)); \
815 break; \
816 case bddop_nand: \
817 if (l > r) \
818 { \
819 BDD tmp = l; \
820 l = r; \
821 r = tmp; \
822 } \
823 if (ISZERO(l)) \
824 RETURN(1); \
825 break; \
826 case bddop_nor: \
827 if (l > r) \
828 { \
829 BDD tmp = l; \
830 l = r; \
831 r = tmp; \
832 } \
833 if (ISONE(l) || ISONE(r)) \
834 RETURN(0); \
835 break; \
836 case bddop_invimp: /* l << r = r >> l */ \
837 { \
838 BDD tmp = l; \
839 l = r; \
840 r = tmp; \
841 op = bddop_imp; \
842 } \
843 BUDDY_FALLTHROUGH; \
844 case bddop_imp: \
845 if (ISONE(r) || ISZERO(l) || l == r) \
846 RETURN(1); \
847 if (ISONE(l)) \
848 RETURN(rec(r)); \
849 break; \
850 case bddop_biimp: \
851 if (l == r) \
852 RETURN(1); \
853 if (l > r) \
854 { \
855 BDD tmp = l; \
856 l = r; \
857 r = tmp; \
858 } \
859 if (ISONE(l)) \
860 RETURN(rec(r)); \
861 break; \
862 case bddop_less: /* l < r = r - l */ \
863 { \
864 BDD tmp = l; \
865 l = r; \
866 r = tmp; \
867 op = bddop_diff; \
868 } \
869 BUDDY_FALLTHROUGH; \
870 case bddop_diff: /* l - r = l &! r */ \
871 if (l == r || ISONE(r)) \
872 RETURN(0); \
873 if (ISZERO(r)) \
874 RETURN(rec(l)); \
875 break; \
876 }
877
878 //__attribute__((optimize("no-tree-vectorize")))
apply_rec(BDD l,BDD r)879 static BDD apply_rec(BDD l, BDD r)
880 {
881 LOCAL_REC_STACKS;
882 int index;
883
884 goto work;
885
886 do
887 {
888 index = POPINT_();
889 if (index < 0)
890 {
891 l = POPINT_();
892 r = POPINT_();
893 work:
894 /* empty macro arguments are undefined in ISO C90 and
895 ISO C++98, so use + when we do not want to call any
896 function.*/
897 APPLY_SHORTCUTS(applyop, +);
898
899 if (__unlikely(ISCONST(l) && ISCONST(r)))
900 /* C: -1 l r --- */
901 /* R: --- res */
902 RETURN(oprres[applyop][l<<1 | r]);
903
904 BddCacheData *entry2 =
905 BddCache_index(&applycache, APPLYHASH(l,r,applyop), index);
906 /* Check entry2->b last, because not_rec() does not
907 initialize it. */
908 if (entry2->i.a == l && entry2->i.c == applyop
909 && entry2->i.b == r)
910 {
911 #ifdef CACHESTATS
912 bddcachestats.opHit++;
913 #endif
914 /* C: -1 l r --- */
915 /* R: --- res */
916 RETURN(entry2->i.res);
917 }
918 #ifdef CACHESTATS
919 bddcachestats.opMiss++;
920 #endif
921 /* C: -1 l r --- (-1 ll rl) -1 lr rr index l r */
922 /* The element in parenthesis are not pushed, as they would
923 be popped right away. We jump to "work" instead.*/
924 int lvl_l = LEVEL(l);
925 int lvl_r = LEVEL(r);
926 if (lvl_l == lvl_r)
927 {
928 PUSH4INT_(r, l, lvl_l, index);
929 PUSH3INT_(HIGH(r), HIGH(l), -1);
930 r = LOW(r);
931 l = LOW(l);
932 }
933 else if (lvl_l < lvl_r)
934 {
935 PUSH4INT_(r, l, lvl_l, index);
936 PUSH3INT_(r, HIGH(l), -1);
937 l = LOW(l);
938 }
939 else /* (lvl_l > lvl_r) */
940 {
941 PUSH4INT_(r, l, lvl_r, index);
942 PUSH3INT_(HIGH(r), l, -1);
943 r = LOW(r);
944 }
945 goto work;
946 }
947 else
948 {
949 /* C: index lvl l r --- */
950 /* R: rres lres --- res */
951 /* res=(lvl, lres, rres) is the result of applyop(l,r) */
952 /* and it should be stored in *entry. */
953 BDD rres = READREF_(1);
954 BDD lres = READREF_(2);
955 int lvl = POPINT_();
956 BDD l = POPINT_();
957 BDD r = POPINT_();
958 SYNC_REC_STACKS;
959 BDD res = bdd_makenode(lvl, lres, rres);
960 POPREF_(2);
961 PUSHREF_(res);
962 BddCacheData* entry = applycache.table + index;
963 entry->i.a = l;
964 entry->i.c = applyop;
965 entry->i.b = r;
966 entry->i.res = res;
967 }
968 }
969 while (NONEMPTY_REC_STACK);
970 BDD res = READREF_(1);
971 POPREF_(1);
972 SYNC_REC_STACKS;
973 return res;
974 }
975
976
977 /*
978 NAME {* bdd\_and *}
979 SECTION {* operator *}
980 SHORT {* The logical 'and' of two BDDs *}
981 PROTO {* BDD bdd_and(BDD l, BDD r) *}
982 DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_and)}. *}
983 RETURN {* The logical 'and' of {\tt l} and {\tt r}. *}
984 ALSO {* bdd\_apply, bdd\_or, bdd\_xor *}
985 */
bdd_and(BDD l,BDD r)986 BDD bdd_and(BDD l, BDD r)
987 {
988 return bdd_apply(l,r,bddop_and);
989 }
990
991
992 /*
993 NAME {* bdd\_or *}
994 SECTION {* operator *}
995 SHORT {* The logical 'or' of two BDDs *}
996 PROTO {* BDD bdd_or(BDD l, BDD r) *}
997 DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_or)}. *}
998 RETURN {* The logical 'or' of {\tt l} and {\tt r}. *}
999 ALSO {* bdd\_apply, bdd\_xor, bdd\_and *}
1000 */
bdd_or(BDD l,BDD r)1001 BDD bdd_or(BDD l, BDD r)
1002 {
1003 return bdd_apply(l,r,bddop_or);
1004 }
1005
1006
1007 /*
1008 NAME {* bdd\_xor *}
1009 SECTION {* operator *}
1010 SHORT {* The logical 'xor' of two BDDs *}
1011 PROTO {* BDD bdd_xor(BDD l, BDD r) *}
1012 DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_xor)}. *}
1013 RETURN {* The logical 'xor' of {\tt l} and {\tt r}. *}
1014 ALSO {* bdd\_apply, bdd\_or, bdd\_and *}
1015 */
bdd_xor(BDD l,BDD r)1016 BDD bdd_xor(BDD l, BDD r)
1017 {
1018 return bdd_apply(l,r,bddop_xor);
1019 }
1020
1021
1022 /*
1023 NAME {* bdd\_imp *}
1024 SECTION {* operator *}
1025 SHORT {* The logical 'implication' between two BDDs *}
1026 PROTO {* BDD bdd_imp(BDD l, BDD r) *}
1027 DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_imp)}. *}
1028 RETURN {* The logical 'implication' of {\tt l} and {\tt r} ($l \Rightarrow r$). *}
1029 ALSO {* bdd\_apply, bdd\_biimp *}
1030 */
bdd_imp(BDD l,BDD r)1031 BDD bdd_imp(BDD l, BDD r)
1032 {
1033 return bdd_apply(l,r,bddop_imp);
1034 }
1035
1036
1037 /*
1038 NAME {* bdd\_biimp *}
1039 SECTION {* operator *}
1040 SHORT {* The logical 'bi-implication' between two BDDs *}
1041 PROTO {* BDD bdd_biimp(BDD l, BDD r) *}
1042 DESCR {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_biimp)}. *}
1043 RETURN {* The logical 'bi-implication' of {\tt l} and {\tt r} ($l \Leftrightarrow r$). *}
1044 ALSO {* bdd\_apply, bdd\_imp *}
1045 */
bdd_biimp(BDD l,BDD r)1046 BDD bdd_biimp(BDD l, BDD r)
1047 {
1048 return bdd_apply(l,r,bddop_biimp);
1049 }
1050
1051 /*=== bdd_setxor =========================================================*/
1052
1053 /*
1054 NAME {* bdd\_setxor *}
1055 SECTION {* operator *}
1056 SHORT {* xor operator for variable sets *}
1057 PROTO {* BDD bdd_setxor(BDD l, BDD r) *}
1058 DESCR {* Given to set $l$ and $r$ represented as conjuctions of variables.
1059 (positive variables are present in the set, negative or absent
1060 variables are not in the set), this computes
1061 $(l\setminus r)\cup(r\setminus l)$. The resulting set will be
1062 represented as a conjunction in which all variables occur
1063 (positive variables are present in the set, negative variables
1064 are not in the set) *}
1065 RETURN {* The BDD for $(l\setminus r)\cup(r\setminus l)$ *}
1066 */
bdd_setxor(BDD l,BDD r)1067 BDD bdd_setxor(BDD l, BDD r)
1068 {
1069 BddCacheData *entry;
1070 BDD res;
1071
1072 if (ISONE(l))
1073 return r;
1074 if (ISONE(r))
1075 return l;
1076
1077 entry = BddCache_lookup(&misccache, SETXORHASH(l,r));
1078 if (entry->i.a == l && entry->i.b == r && entry->i.c == CACHEID_SETXOR)
1079 {
1080 #ifdef CACHESTATS
1081 bddcachestats.opHit++;
1082 #endif
1083 return entry->i.res;
1084 }
1085 #ifdef CACHESTATS
1086 bddcachestats.opMiss++;
1087 #endif
1088
1089 if (LEVEL(l) == LEVEL(r))
1090 {
1091 if (ISZERO(LOW(l)))
1092 {
1093 if (ISZERO(LOW(r)))
1094 {
1095 PUSHREF(bdd_setxor(HIGH(l), HIGH(r)));
1096 res = bdd_makenode(LEVEL(l), READREF(1), 0);
1097 }
1098 else
1099 {
1100 PUSHREF(bdd_setxor(HIGH(l), LOW(r)));
1101 res = bdd_makenode(LEVEL(l), 0, READREF(1));
1102 }
1103 }
1104 else
1105 {
1106 if (ISZERO(LOW(r)))
1107 {
1108 PUSHREF(bdd_setxor(LOW(l), HIGH(r)));
1109 res = bdd_makenode(LEVEL(l), 0, READREF(1));
1110 }
1111 else
1112 {
1113 PUSHREF(bdd_setxor(LOW(l), LOW(r)));
1114 res = bdd_makenode(LEVEL(l), READREF(1), 0);
1115 }
1116 }
1117 }
1118 else if (LEVEL(l) < LEVEL(r))
1119 {
1120 if (ISZERO(LOW(l)))
1121 {
1122 PUSHREF(bdd_setxor(HIGH(l), r));
1123 res = bdd_makenode(LEVEL(l), 0, READREF(1));
1124 }
1125 else
1126 {
1127 PUSHREF(bdd_setxor(LOW(l), r));
1128 res = bdd_makenode(LEVEL(l), READREF(1), 0);
1129 }
1130 }
1131 else /* (LEVEL(l) > LEVEL(r)) */
1132 {
1133 if (ISZERO(LOW(r)))
1134 {
1135 PUSHREF(bdd_setxor(l, HIGH(r)));
1136 res = bdd_makenode(LEVEL(r), 0, READREF(1));
1137 }
1138 else
1139 {
1140 PUSHREF(bdd_setxor(l, LOW(r)));
1141 res = bdd_makenode(LEVEL(r), READREF(1), 0);
1142 }
1143 }
1144
1145 POPREF(1);
1146
1147 entry->i.a = l;
1148 entry->i.c = CACHEID_SETXOR;
1149 entry->i.b = r;
1150 entry->i.res = res;
1151
1152 return res;
1153 }
1154
1155
1156 /*=== bdd_implies =========================================================*/
1157
1158 /*
1159 NAME {* bdd\_implies *}
1160 SECTION {* operator *}
1161 SHORT {* check whether one BDD implies another *}
1162 PROTO {* int bdd_implies(BDD l, BDD r) *}
1163 DESCR {* Check whether $l$ implies $r$, or whether $r$ contains $l$. *}
1164 RETURN {* 1 if $l$ implies $r$, 0 otherwise *}
1165 */
bdd_implies(BDD l,BDD r)1166 int bdd_implies(BDD l, BDD r)
1167 {
1168 BddCacheData *entry;
1169 int res;
1170
1171 if ((l == r) || ISZERO(l) || ISONE(r))
1172 return 1;
1173 if (ISONE(l) || ISZERO(r))
1174 return 0;
1175
1176 entry = BddCache_lookup(&misccache, IMPLIESHASH(l,r));
1177 /* Check entry->b last, because not_rec() does not initialize it. */
1178 if (entry->i.a == l && entry->i.c == CACHEID_IMPLIES && entry->i.b == r)
1179 {
1180 #ifdef CACHESTATS
1181 bddcachestats.opHit++;
1182 #endif
1183 return entry->i.res;
1184 }
1185 #ifdef CACHESTATS
1186 bddcachestats.opMiss++;
1187 #endif
1188
1189 if (LEVEL(l) == LEVEL(r))
1190 {
1191 int hl = HIGH(l);
1192 int hr = HIGH(r);
1193 /* Avoid the recursion if the second implication will trivially
1194 fail. */
1195 if ((ISONE(hl) || ISZERO(hr)) && (hl != hr))
1196 res = 0;
1197 else
1198 res = bdd_implies(LOW(l), LOW(r)) && bdd_implies(hl, hr);
1199 }
1200 else if (LEVEL(l) < LEVEL(r))
1201 {
1202 int hl = HIGH(l);
1203 if (ISONE(hl) && (hl != r))
1204 res = 0;
1205 else
1206 res = bdd_implies(LOW(l), r) && bdd_implies(HIGH(l), r);
1207 }
1208 else /* LEVEL(l) > LEVEL(r) */
1209 {
1210 int hr = HIGH(r);
1211 if (ISZERO(hr) && (hr != r))
1212 res = 0;
1213 else
1214 res = bdd_implies(l, LOW(r)) && bdd_implies(l, HIGH(r));
1215 }
1216
1217 entry->i.a = l;
1218 entry->i.c = CACHEID_IMPLIES;
1219 entry->i.b = r;
1220 entry->i.res = res;
1221
1222 return res;
1223 }
1224
1225
1226
1227 /*=== ITE ==============================================================*/
1228
1229 /*
1230 NAME {* bdd\_ite *}
1231 SECTION {* operator *}
1232 SHORT {* if-then-else operator *}
1233 PROTO {* BDD bdd_ite(BDD f, BDD g, BDD h) *}
1234 DESCR {* Calculates the BDD for the expression
1235 $(f \conj g) \disj (\neg f \conj h)$ more efficiently than doing
1236 the three operations separately. {\tt bdd\_ite} can also be used
1237 for conjunction, disjunction and any other boolean operator, but
1238 is not as efficient for the binary and unary operations. *}
1239 RETURN {* The BDD for $(f \conj g) \disj (\neg f \conj h)$ *}
1240 ALSO {* bdd\_apply *}
1241 */
bdd_ite(BDD f,BDD g,BDD h)1242 BDD bdd_ite(BDD f, BDD g, BDD h)
1243 {
1244 BDD res;
1245 firstReorder = 1;
1246
1247 CHECKa(f, bddfalse);
1248 CHECKa(g, bddfalse);
1249 CHECKa(h, bddfalse);
1250
1251 again:
1252 if (__likely(bddreordermethod == BDD_REORDER_NONE)
1253 || setjmp(bddexception) == 0)
1254 {
1255 INITREF;
1256
1257 if (__likely(firstReorder))
1258 {
1259 res = ite_rec(f,g,h);
1260 }
1261 else
1262 {
1263 bdd_disable_reorder();
1264 res = ite_rec(f,g,h);
1265 bdd_enable_reorder();
1266 }
1267 }
1268 else
1269 {
1270 bdd_checkreorder();
1271
1272 if (firstReorder-- == 1)
1273 goto again;
1274 res = BDDZERO; /* avoid warning about res being uninitialized */
1275 }
1276
1277 checkresize();
1278 return res;
1279 }
1280
ite_rec(BDD f,BDD g,BDD h)1281 static BDD ite_rec(BDD f, BDD g, BDD h)
1282 {
1283 LOCAL_REC_STACKS;
1284 int index;
1285
1286 goto work;
1287 do
1288 {
1289 index = POPINT_();
1290 if (index < 0)
1291 {
1292 f = POPINT_();
1293 g = POPINT_();
1294 h = POPINT_();
1295 work:
1296 if (ISONE(f))
1297 RETURN(g);
1298 if (ISZERO(f))
1299 RETURN(h);
1300 if (g == h)
1301 RETURN(g);
1302 if (ISONE(g) && ISZERO(h))
1303 RETURN(f);
1304 if (ISZERO(g) && ISONE(h))
1305 {
1306 SYNC_REC_STACKS;
1307 int res = not_rec(f);
1308 RETURN(res);
1309 }
1310
1311 BddCacheData *entry2 =
1312 BddCache_index(&itecache, ITEHASH(f, g, h), index);
1313 if (entry2->i.a == f && entry2->i.c == h && entry2->i.b == g)
1314 {
1315 #ifdef CACHESTATS
1316 bddcachestats.opHit++;
1317 #endif
1318 /* C: -1 f g h --- */
1319 /* R: --- res */
1320 RETURN(entry2->i.res);
1321 }
1322 #ifdef CACHESTATS
1323 bddcachestats.opMiss++;
1324 #endif
1325 /* C: -1 f g h --- (-1 fl gl hl) -1 fr gr hr index lvl f g h */
1326 int lvl_f = LEVEL(f);
1327 int lvl_g = LEVEL(g);
1328 int lvl_h = LEVEL(h);
1329 if (lvl_f == lvl_g)
1330 {
1331 if (lvl_g == lvl_h)
1332 {
1333 PUSH4INT_(h, g, f, lvl_f);
1334 PUSHINT_(index);
1335 PUSH4INT_(HIGH(h), HIGH(g), HIGH(f), -1);
1336 h = LOW(h);
1337 g = LOW(g);
1338 f = LOW(f);
1339 }
1340 else if (lvl_f < lvl_h)
1341 {
1342 PUSH4INT_(h, g, f, lvl_f);
1343 PUSHINT_(index);
1344 PUSH4INT_(h, HIGH(g), HIGH(f), -1);
1345 g = LOW(g);
1346 f = LOW(f);
1347 }
1348 else /* lvl_f > lvl_h */
1349 {
1350 PUSH4INT_(h, g, f, lvl_h);
1351 PUSHINT_(index);
1352 PUSH4INT_(HIGH(h), g, f, -1);
1353 h = LOW(h);
1354 }
1355 }
1356 else if (lvl_f < lvl_g)
1357 {
1358 if (lvl_f == lvl_h)
1359 {
1360 PUSH4INT_(h, g, f, lvl_f);
1361 PUSHINT_(index);
1362 PUSH4INT_(HIGH(h), g, HIGH(f), -1);
1363 h = LOW(h);
1364 f = LOW(f);
1365 }
1366 else if (lvl_f < lvl_h)
1367 {
1368 PUSH4INT_(h, g, f, lvl_f);
1369 PUSHINT_(index);
1370 PUSH4INT_(h, g, HIGH(f), -1);
1371 f = LOW(f);
1372 }
1373 else /* lvl_f > lvl_h */
1374 {
1375 PUSH4INT_(h, g, f, lvl_h);
1376 PUSHINT_(index);
1377 PUSH4INT_(HIGH(h), g, f, -1);
1378 h = LOW(h);
1379 }
1380 }
1381 else /* lvl_f > lvl_g */
1382 {
1383 if (lvl_g == lvl_h)
1384 {
1385 PUSH4INT_(h, g, f, lvl_g);
1386 PUSHINT_(index);
1387 PUSH4INT_(HIGH(h), HIGH(g), f, -1);
1388 h = LOW(h);
1389 g = LOW(g);
1390 }
1391 else if (lvl_g < lvl_h)
1392 {
1393 PUSH4INT_(h, g, f, lvl_g);
1394 PUSHINT_(index);
1395 PUSH4INT_(h, HIGH(g), f, -1);
1396 g = LOW(g);
1397 }
1398 else /* lvl_g > lvl_h */
1399 {
1400 PUSH4INT_(h, g, f, lvl_h);
1401 PUSHINT_(index);
1402 PUSH4INT_(HIGH(h), g, f, -1);
1403 h = LOW(h);
1404 }
1405 }
1406 goto work;
1407 }
1408 else
1409 {
1410 /* C: index lvl f g h --- */
1411 /* R: rres lres --- res */
1412 /* res=(lvl, lres, rres) is the result of ite(f,g,h) */
1413 /* and it should be stored in *entry. */
1414 BDD rres = READREF_(1);
1415 BDD lres = READREF_(2);
1416 int lvl = POPINT_();
1417 SYNC_REC_STACKS;
1418 BDD res = bdd_makenode(lvl, lres, rres);
1419 POPREF_(2);
1420 PUSHREF_(res);
1421 BddCacheData* entry = itecache.table + index;
1422 entry->i.a = POPINT_(); // f
1423 entry->i.b = POPINT_(); // g
1424 entry->i.c = POPINT_(); // h
1425 entry->i.res = res;
1426 }
1427 }
1428 while (NONEMPTY_REC_STACK);
1429
1430 BDD res = READREF_(1);
1431 POPREF_(1);
1432 SYNC_REC_STACKS;
1433 return res;
1434 }
1435
1436 /*=== RESTRICT =========================================================*/
1437
1438 /*
1439 NAME {* bdd\_restrict *}
1440 SECTION {* operator *}
1441 SHORT {* restric a set of variables to constant values *}
1442 PROTO {* BDD bdd_restrict(BDD r, BDD var) *}
1443 DESCR {* This function restricts the variables in {\tt r} to constant
1444 true or false. How this is done
1445 depends on how the variables are included in the variable set
1446 {\tt var}. If they
1447 are included in their positive form then they are restricted to
1448 true and vice versa. Unfortunately it is not possible to
1449 insert variables in their negated form using {\tt bdd\_makeset},
1450 so the variable set has to be build manually as a
1451 conjunction of the variables. Example: Assume variable 1 should be
1452 restricted to true and variable 3 to false.
1453 \begin{verbatim}
1454 bdd X = make_user_bdd();
1455 bdd R1 = bdd_ithvar(1);
1456 bdd R2 = bdd_nithvar(3);
1457 bdd R = bdd_addref( bdd_apply(R1,R2, bddop_and) );
1458 bdd RES = bdd_addref( bdd_restrict(X,R) );
1459 \end{verbatim}
1460 *}
1461 RETURN {* The restricted bdd. *}
1462 ALSO {* bdd\_makeset, bdd\_exist, bdd\_forall *}
1463 */
bdd_restrict(BDD r,BDD var)1464 BDD bdd_restrict(BDD r, BDD var)
1465 {
1466 BDD res;
1467 firstReorder = 1;
1468
1469 CHECKa(r,bddfalse);
1470 CHECKa(var,bddfalse);
1471
1472 if (var < 2) /* Empty set */
1473 return r;
1474
1475 again:
1476 if (__likely(bddreordermethod == BDD_REORDER_NONE)
1477 || setjmp(bddexception) == 0)
1478 {
1479 if (varset2svartable(var) < 0)
1480 return bddfalse;
1481
1482 INITREF;
1483 miscid = (var << 3) | CACHEID_RESTRICT;
1484
1485 if (__likely(firstReorder))
1486 {
1487 res = restrict_rec(r);
1488 }
1489 else
1490 {
1491 bdd_disable_reorder();
1492 res = restrict_rec(r);
1493 bdd_enable_reorder();
1494 }
1495 }
1496 else
1497 {
1498 bdd_checkreorder();
1499
1500 if (firstReorder-- == 1)
1501 goto again;
1502 res = BDDZERO; /* avoid warning about res being uninitialized */
1503 }
1504
1505 checkresize();
1506 return res;
1507 }
1508
1509
restrict_rec(BDD r)1510 static BDD restrict_rec(BDD r)
1511 {
1512 LOCAL_REC_STACKS;
1513 int index;
1514
1515 goto work;
1516 do
1517 {
1518 index = POPINT_();
1519 if (index < 0)
1520 {
1521 r = POPINT_();
1522 work:
1523 /* C: -1 r --- */
1524 /* R: --- r */
1525 if (ISCONST(r) || LEVEL(r) > quantlast)
1526 RETURN(r);
1527
1528 BddCacheData *entry2 =
1529 BddCache_index(&misccache, RESTRHASH(r, miscid), index);
1530 if (entry2->i.a == r && entry2->i.c == miscid)
1531 {
1532 #ifdef CACHESTATS
1533 bddcachestats.opHit++;
1534 #endif
1535 /* C: -1 r --- */
1536 /* R: --- res */
1537 RETURN(entry2->i.res);
1538 }
1539 #ifdef CACHESTATS
1540 bddcachestats.opMiss++;
1541 #endif
1542 if (INSVARSET(LEVEL(r)))
1543 {
1544 /* C: -1 r --- (-1 r') */
1545 if (quantvarset[LEVEL(r)] > 0)
1546 r = HIGH(r);
1547 else
1548 r = LOW(r);
1549 goto work;
1550 }
1551 else
1552 {
1553 /* C: -1 r --- (-1 lr) -1 rr index r */
1554 PUSH4INT_(r, index, HIGH(r), -1);
1555 r = LOW(r);
1556 }
1557 goto work;
1558 }
1559 else
1560 {
1561 /* C: index r --- */
1562 /* R: rres lres --- res */
1563 BDD rres = READREF_(1);
1564 BDD lres = READREF_(2);
1565 BDD r = POPINT_();
1566 SYNC_REC_STACKS;
1567 BDD res = bdd_makenode(LEVEL(r), lres, rres);
1568 POPREF_(2);
1569 BddCacheData* entry = misccache.table + index;
1570 entry->i.a = r;
1571 entry->i.c = quantid;
1572 entry->i.res = res;
1573 PUSHREF_(res);
1574 }
1575 }
1576 while (NONEMPTY_REC_STACK);
1577
1578 BDD res = READREF_(1);
1579 POPREF_(1);
1580 SYNC_REC_STACKS;
1581 return res;
1582 }
1583
1584 /*=== GENERALIZED COFACTOR =============================================*/
1585
1586 /*
1587 NAME {* bdd\_constrain *}
1588 SECTION {* operator *}
1589 SHORT {* generalized cofactor *}
1590 PROTO {* BDD bdd_constrain(BDD f, BDD c) *}
1591 DESCR {* Computes the generalized cofactor of {\tt f} with respect to
1592 {\tt c}. *}
1593 RETURN {* The constrained BDD *}
1594 ALSO {* bdd\_restrict, bdd\_simplify *}
1595 */
bdd_constrain(BDD f,BDD c)1596 BDD bdd_constrain(BDD f, BDD c)
1597 {
1598 BDD res;
1599 firstReorder = 1;
1600
1601 CHECKa(f,bddfalse);
1602 CHECKa(c,bddfalse);
1603
1604 again:
1605 if (__likely(bddreordermethod == BDD_REORDER_NONE)
1606 || setjmp(bddexception) == 0)
1607 {
1608 INITREF;
1609 miscid = CACHEID_CONSTRAIN;
1610
1611 if (__likely(firstReorder))
1612 {
1613 res = constrain_rec(f, c);
1614 }
1615 else
1616 {
1617 bdd_disable_reorder();
1618 res = constrain_rec(f, c);
1619 bdd_enable_reorder();
1620 }
1621 }
1622 else
1623 {
1624 bdd_checkreorder();
1625
1626 if (firstReorder-- == 1)
1627 goto again;
1628 res = BDDZERO; /* avoid warning about res being uninitialized */
1629 }
1630
1631 checkresize();
1632 return res;
1633 }
1634
1635
constrain_rec(BDD f,BDD c)1636 static BDD constrain_rec(BDD f, BDD c)
1637 {
1638 BddCacheData *entry;
1639 BDD res;
1640
1641 if (ISONE(c))
1642 return f;
1643 if (ISCONST(f))
1644 return f;
1645 if (c == f)
1646 return BDDONE;
1647 if (ISZERO(c))
1648 return BDDZERO;
1649
1650 entry = BddCache_lookup(&misccache, CONSTRAINHASH(f,c));
1651 if (entry->i.a == f && entry->i.b == c && entry->i.c == miscid)
1652 {
1653 #ifdef CACHESTATS
1654 bddcachestats.opHit++;
1655 #endif
1656 return entry->i.res;
1657 }
1658 #ifdef CACHESTATS
1659 bddcachestats.opMiss++;
1660 #endif
1661
1662 if (LEVEL(f) == LEVEL(c))
1663 {
1664 if (ISZERO(LOW(c)))
1665 res = constrain_rec(HIGH(f), HIGH(c));
1666 else if (ISZERO(HIGH(c)))
1667 res = constrain_rec(LOW(f), LOW(c));
1668 else
1669 {
1670 PUSHREF( constrain_rec(LOW(f), LOW(c)) );
1671 PUSHREF( constrain_rec(HIGH(f), HIGH(c)) );
1672 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
1673 POPREF(2);
1674 }
1675 }
1676 else
1677 if (LEVEL(f) < LEVEL(c))
1678 {
1679 PUSHREF( constrain_rec(LOW(f), c) );
1680 PUSHREF( constrain_rec(HIGH(f), c) );
1681 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
1682 POPREF(2);
1683 }
1684 else
1685 {
1686 if (ISZERO(LOW(c)))
1687 res = constrain_rec(f, HIGH(c));
1688 else if (ISZERO(HIGH(c)))
1689 res = constrain_rec(f, LOW(c));
1690 else
1691 {
1692 PUSHREF( constrain_rec(f, LOW(c)) );
1693 PUSHREF( constrain_rec(f, HIGH(c)) );
1694 res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
1695 POPREF(2);
1696 }
1697 }
1698
1699 entry->i.a = f;
1700 entry->i.b = c;
1701 entry->i.c = miscid;
1702 entry->i.res = res;
1703
1704 return res;
1705 }
1706
1707
1708 /*=== REPLACE ==========================================================*/
1709
1710 /*
1711 NAME {* bdd\_replace *}
1712 SECTION {* operator *}
1713 SHORT {* replaces variables with other variables *}
1714 PROTO {* BDD bdd_replace(BDD r, bddPair *pair) *}
1715 DESCR {* Replaces all variables in the BDD {\tt r} with the variables
1716 defined by {\tt pair}. Each entry in {\tt pair} consists of a
1717 old and a new variable. Whenever the old variable is found in
1718 {\tt r} then a new node with the new variable is inserted instead.
1719 *}
1720 ALSO {* bdd\_newpair, bdd\_setpair, bdd\_setpairs *}
1721 RETURN {* The result of the operation. *}
1722 */
bdd_replace(BDD r,bddPair * pair)1723 BDD bdd_replace(BDD r, bddPair *pair)
1724 {
1725 BDD res;
1726 firstReorder = 1;
1727
1728 CHECKa(r, bddfalse);
1729
1730 again:
1731 if (__likely(bddreordermethod == BDD_REORDER_NONE)
1732 || setjmp(bddexception) == 0)
1733 {
1734 INITREF;
1735 replacepair = pair->result;
1736 replacelast = pair->last;
1737 replaceid = (pair->id << 2) | CACHEID_REPLACE;
1738
1739 if (__likely(firstReorder))
1740 {
1741 res = replace_rec(r);
1742 }
1743 else
1744 {
1745 bdd_disable_reorder();
1746 res = replace_rec(r);
1747 bdd_enable_reorder();
1748 }
1749 }
1750 else
1751 {
1752 bdd_checkreorder();
1753
1754 if (firstReorder-- == 1)
1755 goto again;
1756 res = BDDZERO; /* avoid warning about res being uninitialized */
1757 }
1758
1759 checkresize();
1760 return res;
1761 }
1762
1763
replace_rec(BDD r)1764 static BDD replace_rec(BDD r)
1765 {
1766 BddCacheData *entry;
1767 BDD res;
1768
1769 if (ISCONST(r) || LEVEL(r) > replacelast)
1770 return r;
1771
1772 entry = BddCache_lookup(&replacecache, REPLACEHASH(r));
1773 if (entry->i.a == r && entry->i.c == replaceid)
1774 {
1775 #ifdef CACHESTATS
1776 bddcachestats.opHit++;
1777 #endif
1778 return entry->i.res;
1779 }
1780 #ifdef CACHESTATS
1781 bddcachestats.opMiss++;
1782 #endif
1783
1784 PUSHREF( replace_rec(LOW(r)) );
1785 PUSHREF( replace_rec(HIGH(r)) );
1786
1787 res = bdd_correctify(LEVEL(replacepair[LEVEL(r)]), READREF(2), READREF(1));
1788 POPREF(2);
1789
1790 entry->i.a = r;
1791 entry->i.c = replaceid;
1792 entry->i.res = res;
1793
1794 return res;
1795 }
1796
1797
bdd_correctify(int level,BDD l,BDD r)1798 static BDD bdd_correctify(int level, BDD l, BDD r)
1799 {
1800 BDD res;
1801
1802 if (level < LEVEL(l) && level < LEVEL(r))
1803 return bdd_makenode(level, l, r);
1804
1805 #ifndef NDEBUG
1806 if (level == LEVEL(l) || level == LEVEL(r))
1807 {
1808 bdd_error(BDD_REPLACE);
1809 return 0;
1810 }
1811 #endif
1812
1813 if (LEVEL(l) == LEVEL(r))
1814 {
1815 PUSHREF( bdd_correctify(level, LOW(l), LOW(r)) );
1816 PUSHREF( bdd_correctify(level, HIGH(l), HIGH(r)) );
1817 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1818 }
1819 else
1820 if (LEVEL(l) < LEVEL(r))
1821 {
1822 PUSHREF( bdd_correctify(level, LOW(l), r) );
1823 PUSHREF( bdd_correctify(level, HIGH(l), r) );
1824 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1825 }
1826 else
1827 {
1828 PUSHREF( bdd_correctify(level, l, LOW(r)) );
1829 PUSHREF( bdd_correctify(level, l, HIGH(r)) );
1830 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1831 }
1832 POPREF(2);
1833
1834 return res; /* FIXME: cache ? */
1835 }
1836
1837
1838 /*=== COMPOSE ==========================================================*/
1839
1840 /*
1841 NAME {* bdd\_compose *}
1842 SECTION {* operator *}
1843 SHORT {* functional composition *}
1844 PROTO {* BDD bdd_compose(BDD f, BDD g, int var) *}
1845 DESCR {* Substitutes the variable {\tt var} with the BDD {\tt g} in
1846 the BDD {\tt f}: result $= f[g/var]$. *}
1847 RETURN {* The composed BDD *}
1848 ALSO {* bdd\_veccompose, bdd\_replace, bdd\_restrict *}
1849 */
bdd_compose(BDD f,BDD g,int var)1850 BDD bdd_compose(BDD f, BDD g, int var)
1851 {
1852 BDD res;
1853 firstReorder = 1;
1854
1855 CHECKa(f, bddfalse);
1856 CHECKa(g, bddfalse);
1857
1858 #ifndef NDEBUG
1859 if (var < 0 || var >= bddvarnum)
1860 {
1861 bdd_error(BDD_VAR);
1862 return bddfalse;
1863 }
1864 #endif
1865
1866 again:
1867 if (__likely(bddreordermethod == BDD_REORDER_NONE) ||
1868 setjmp(bddexception) == 0)
1869 {
1870 INITREF;
1871 composelevel = bddvar2level[var];
1872 replaceid = (composelevel << 2) | CACHEID_COMPOSE;
1873
1874 if (__likely(firstReorder))
1875 {
1876 res = compose_rec(f, g);
1877 }
1878 else
1879 {
1880 bdd_disable_reorder();
1881 res = compose_rec(f, g);
1882 bdd_enable_reorder();
1883 }
1884 }
1885 else
1886 {
1887 bdd_checkreorder();
1888
1889 if (firstReorder-- == 1)
1890 goto again;
1891 res = BDDZERO; /* avoid warning about res being uninitialized */
1892 }
1893
1894 checkresize();
1895 return res;
1896 }
1897
compose_rec(BDD l,BDD r)1898 static BDD compose_rec(BDD l, BDD r)
1899 {
1900 LOCAL_REC_STACKS;
1901 int index;
1902
1903 goto work;
1904 do
1905 {
1906 index = POPINT_();
1907 if (index < 0)
1908 {
1909 l = POPINT_();
1910 r = POPINT_();
1911 work:;
1912 int lvl_l = LEVEL(l);
1913 if (lvl_l > composelevel)
1914 RETURN(l);
1915
1916 BddCacheData *entry2 =
1917 BddCache_index(&replacecache, COMPOSEHASH(l, r), index);
1918 if (entry2->i.a == l && entry2->i.b == r && entry2->i.c == replaceid)
1919 {
1920 #ifdef CACHESTATS
1921 bddcachestats.opHit++;
1922 #endif
1923 /* C: -1 l r --- */
1924 /* R: --- res */
1925 RETURN(entry2->i.res);
1926 }
1927 #ifdef CACHESTATS
1928 bddcachestats.opMiss++;
1929 #endif
1930 if (lvl_l < composelevel)
1931 {
1932 /* C: -1 l r --- (-1 ll rl) -1 lr rr index lvl l r */
1933 int lvl_r = LEVEL(r);
1934 if (lvl_l == lvl_r)
1935 {
1936 PUSH4INT_(r, l, lvl_l, index);
1937 PUSH3INT_(HIGH(r), HIGH(l), -1);
1938 r = LOW(r);
1939 l = LOW(l);
1940 }
1941 else if (lvl_l < lvl_r)
1942 {
1943 PUSH4INT_(r, l, lvl_l, index);
1944 PUSH3INT_(r, HIGH(l), -1);
1945 l = LOW(l);
1946 }
1947 else /* (lvl_l > lvl_r) */
1948 {
1949 PUSH4INT_(r, l, lvl_r, index);
1950 PUSH3INT_(HIGH(r), l, -1);
1951 r = LOW(r);
1952 }
1953 goto work;
1954 }
1955 else
1956 {
1957 /* C: -1 l r --- */
1958 /* R: --- res */
1959 SYNC_REC_STACKS;
1960 BDD res = ite_rec(r, HIGH(l), LOW(l));
1961 PUSHREF_(res);
1962 entry2->i.a = l;
1963 entry2->i.c = replaceid;
1964 entry2->i.b = r;
1965 entry2->i.res = res;
1966 }
1967 }
1968 else
1969 {
1970 /* C: index lvl l r --- */
1971 /* R: rres lres --- res */
1972 /* res=(lvl, lres, rres) is the result of applyop(l,r) */
1973 /* and it should be stored in *entry. */
1974 BDD rres = READREF_(1);
1975 BDD lres = READREF_(2);
1976 int lvl = POPINT_();
1977 BDD l = POPINT_();
1978 BDD r = POPINT_();
1979 SYNC_REC_STACKS;
1980 BDD res = bdd_makenode(lvl, lres, rres);
1981 POPREF_(2);
1982 BddCacheData* entry = replacecache.table + index;
1983 entry->i.a = l;
1984 entry->i.c = replaceid;
1985 entry->i.b = r;
1986 entry->i.res = res;
1987 PUSHREF_(res);
1988 }
1989 }
1990 while (NONEMPTY_REC_STACK);
1991
1992 BDD res = READREF_(1);
1993 POPREF_(1);
1994 SYNC_REC_STACKS;
1995 return res;
1996 }
1997
1998
1999 /*
2000 NAME {* bdd\_veccompose *}
2001 SECTION {* operator *}
2002 SHORT {* simultaneous functional composition *}
2003 PROTO {* BDD bdd_veccompose(BDD f, bddPair *pair) *}
2004 DESCR {* Uses the pairs of variables and BDDs in {\tt pair} to make
2005 the simultaneous substitution: $f[g_1/V_1, \ldots, g_n/V_n]$.
2006 In this way one or more BDDs
2007 may be substituted in one step. The BDDs in
2008 {\tt pair} may depend on the variables they are substituting.
2009 {\tt bdd\_compose} may be used instead of
2010 {\tt bdd\_replace} but is not as efficient when $g_i$ is a
2011 single variable, the same applies to {\tt bdd\_restrict}.
2012 Note that simultaneous substitution is not necessarily the same
2013 as repeated substitution. Example:
2014 $(x_1 \disj x_2)[x_3/x_1,x_4/x_3] = (x_3 \disj x_2) \neq
2015 ((x_1 \disj x_2)[x_3/x_1])[x_4/x_3] = (x_4 \disj x_2)$. *}
2016 RETURN {* The composed BDD *}
2017 ALSO {* bdd\_compose, bdd\_replace, bdd\_restrict *}
2018 */
bdd_veccompose(BDD f,bddPair * pair)2019 BDD bdd_veccompose(BDD f, bddPair *pair)
2020 {
2021 BDD res;
2022 firstReorder = 1;
2023
2024 CHECKa(f, bddfalse);
2025
2026 again:
2027 if (__likely(bddreordermethod == BDD_REORDER_NONE) ||
2028 setjmp(bddexception) == 0)
2029 {
2030 INITREF;
2031 replacepair = pair->result;
2032 replaceid = (pair->id << 2) | CACHEID_VECCOMPOSE;
2033 replacelast = pair->last;
2034
2035 if (__likely(firstReorder))
2036 {
2037 res = veccompose_rec(f);
2038 }
2039 else
2040 {
2041 bdd_disable_reorder();
2042 res = veccompose_rec(f);
2043 bdd_enable_reorder();
2044 }
2045 }
2046 else
2047 {
2048 bdd_checkreorder();
2049
2050 if (firstReorder-- == 1)
2051 goto again;
2052 res = BDDZERO; /* avoid warning about res being uninitialized */
2053 }
2054
2055 checkresize();
2056 return res;
2057 }
2058
2059
veccompose_rec(BDD f)2060 static BDD veccompose_rec(BDD f)
2061 {
2062 BddCacheData *entry;
2063 register BDD res;
2064
2065 if (LEVEL(f) > replacelast)
2066 return f;
2067
2068 entry = BddCache_lookup(&replacecache, VECCOMPOSEHASH(f));
2069 if (entry->i.a == f && entry->i.c == replaceid)
2070 {
2071 #ifdef CACHESTATS
2072 bddcachestats.opHit++;
2073 #endif
2074 return entry->i.res;
2075 }
2076 #ifdef CACHESTATS
2077 bddcachestats.opMiss++;
2078 #endif
2079
2080 PUSHREF( veccompose_rec(LOW(f)) );
2081 PUSHREF( veccompose_rec(HIGH(f)) );
2082 res = ite_rec(replacepair[LEVEL(f)], READREF(1), READREF(2));
2083 POPREF(2);
2084
2085 entry->i.a = f;
2086 entry->i.c = replaceid;
2087 entry->i.res = res;
2088
2089 return res;
2090 }
2091
2092
2093 /*=== SIMPLIFY =========================================================*/
2094
2095 /*
2096 NAME {* bdd\_simplify *}
2097 SECTION {* operator *}
2098 SHORT {* coudert and Madre's restrict function *}
2099 PROTO {* BDD bdd_simplify(BDD f, BDD d) *}
2100 DESCR {* Tries to simplify the BDD {\tt f} by restricting it to the
2101 domain covered by {\tt d}. No checks are done to see if the
2102 result is actually smaller than the input. This can be done
2103 by the user with a call to {\tt bdd\_nodecount}. *}
2104 ALSO {* bdd\_restrict *}
2105 RETURN {* The simplified BDD *}
2106 */
bdd_simplify(BDD f,BDD d)2107 BDD bdd_simplify(BDD f, BDD d)
2108 {
2109 BDD res;
2110 firstReorder = 1;
2111
2112 CHECKa(f, bddfalse);
2113 CHECKa(d, bddfalse);
2114
2115 again:
2116 if (__likely(bddreordermethod == BDD_REORDER_NONE)
2117 || setjmp(bddexception) == 0)
2118 {
2119 INITREF;
2120 applyop = bddop_or;
2121
2122 if (__likely(firstReorder))
2123 {
2124 res = simplify_rec(f, d);
2125 }
2126 else
2127 {
2128 bdd_disable_reorder();
2129 res = simplify_rec(f, d);
2130 bdd_enable_reorder();
2131 }
2132 }
2133 else
2134 {
2135 bdd_checkreorder();
2136
2137 if (firstReorder-- == 1)
2138 goto again;
2139 res = BDDZERO; /* avoid warning about res being uninitialized */
2140 }
2141
2142 checkresize();
2143 return res;
2144 }
2145
2146
simplify_rec(BDD f,BDD d)2147 static BDD simplify_rec(BDD f, BDD d)
2148 {
2149 BddCacheData *entry;
2150 BDD res;
2151
2152 if (ISONE(d) || ISCONST(f))
2153 return f;
2154 if (d == f)
2155 return BDDONE;
2156 if (ISZERO(d))
2157 return BDDZERO;
2158
2159 entry = BddCache_lookup(&applycache, APPLYHASH(f,d,bddop_simplify));
2160
2161 /* Check entry->b last, because not_rec() does not initialize it. */
2162 if (entry->i.a == f && entry->i.c == bddop_simplify && entry->i.b == d)
2163 {
2164 #ifdef CACHESTATS
2165 bddcachestats.opHit++;
2166 #endif
2167 return entry->i.res;
2168 }
2169 #ifdef CACHESTATS
2170 bddcachestats.opMiss++;
2171 #endif
2172
2173 if (LEVEL(f) == LEVEL(d))
2174 {
2175 if (ISZERO(LOW(d)))
2176 res = simplify_rec(HIGH(f), HIGH(d));
2177 else
2178 if (ISZERO(HIGH(d)))
2179 res = simplify_rec(LOW(f), LOW(d));
2180 else
2181 {
2182 PUSHREF( simplify_rec(LOW(f), LOW(d)) );
2183 PUSHREF( simplify_rec(HIGH(f), HIGH(d)) );
2184 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2185 POPREF(2);
2186 }
2187 }
2188 else
2189 if (LEVEL(f) < LEVEL(d))
2190 {
2191 PUSHREF( simplify_rec(LOW(f), d) );
2192 PUSHREF( simplify_rec(HIGH(f), d) );
2193 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2194 POPREF(2);
2195 }
2196 else /* LEVEL(d) < LEVEL(f) */
2197 {
2198 PUSHREF( apply_rec(LOW(d), HIGH(d)) ); /* Exist quant */
2199 res = simplify_rec(f, READREF(1));
2200 POPREF(1);
2201 }
2202
2203 entry->i.a = f;
2204 entry->i.c = bddop_simplify;
2205 entry->i.b = d;
2206 entry->i.res = res;
2207
2208 return res;
2209 }
2210
2211
2212 /*=== QUANTIFICATION ===================================================*/
2213
quantify(BDD r,BDD var,int op,int comp,int id)2214 static BDD quantify(BDD r, BDD var, int op, int comp, int id)
2215 {
2216 BDD res;
2217 firstReorder = 1;
2218
2219 CHECKa(r, bddfalse);
2220 CHECKa(var, bddfalse);
2221
2222 if (var < 2 && !comp) /* Empty set */
2223 return r;
2224
2225 again:
2226 if (__likely(bddreordermethod == BDD_REORDER_NONE)
2227 || setjmp(bddexception) == 0)
2228 {
2229 if (varset2vartable(var, comp) < 0)
2230 return bddfalse;
2231
2232 INITREF;
2233 quantid = (var << 4) | id; /* FIXME: range */
2234 applyop = op;
2235
2236 if (__likely(firstReorder))
2237 {
2238 res = quant_rec(r);
2239 }
2240 else
2241 {
2242 bdd_disable_reorder();
2243 res = quant_rec(r);
2244 bdd_enable_reorder();
2245 }
2246 }
2247 else
2248 {
2249 bdd_checkreorder();
2250
2251 if (firstReorder-- == 1)
2252 goto again;
2253 res = BDDZERO; /* avoid warning about res being uninitialized */
2254 }
2255
2256 checkresize();
2257 return res;
2258 }
2259
2260 /*
2261 NAME {* bdd\_exist *}
2262 SECTION {* operator *}
2263 SHORT {* existential quantification of variables *}
2264 PROTO {* BDD bdd_exist(BDD r, BDD var) *}
2265 DESCR {* Removes all occurences in {\tt r} of variables in the set
2266 {\tt var} by existential quantification. *}
2267 ALSO {* bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2268 RETURN {* The quantified BDD. *}
2269 */
bdd_exist(BDD r,BDD var)2270 BDD bdd_exist(BDD r, BDD var)
2271 {
2272 return quantify(r, var, bddop_or, 0, CACHEID_EXIST);
2273 }
2274
2275 /*
2276 NAME {* bdd\_existcomp *}
2277 SECTION {* operator *}
2278 SHORT {* existential quantification of other variables *}
2279 PROTO {* BDD bdd_existcomp(BDD r, BDD var) *}
2280 DESCR {* Removes all occurences in {\tt r} of variables {\bf not} in the set
2281 {\tt var} by existential quantification. *}
2282 ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2283 RETURN {* The quantified BDD. *}
2284 */
bdd_existcomp(BDD r,BDD var)2285 BDD bdd_existcomp(BDD r, BDD var)
2286 {
2287 return quantify(r, var, bddop_or, 1, CACHEID_EXISTC);
2288 }
2289
2290
2291 /*
2292 NAME {* bdd\_forall *}
2293 SECTION {* operator *}
2294 SHORT {* universal quantification of variables *}
2295 PROTO {* BDD bdd_forall(BDD r, BDD var) *}
2296 DESCR {* Removes all occurences in {\tt r} of variables in the set
2297 {\tt var} by universal quantification. *}
2298 ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2299 RETURN {* The quantified BDD. *}
2300 */
bdd_forall(BDD r,BDD var)2301 BDD bdd_forall(BDD r, BDD var)
2302 {
2303 return quantify(r, var, bddop_and, 0, CACHEID_EXIST);
2304 }
2305
2306 /*
2307 NAME {* bdd\_forallcomp *}
2308 SECTION {* operator *}
2309 SHORT {* universal quantification of other variables *}
2310 PROTO {* BDD bdd_forallcomp(BDD r, BDD var) *}
2311 DESCR {* Removes all occurences in {\tt r} of variables {\bf not} in the set
2312 {\tt var} by universal quantification. *}
2313 ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2314 RETURN {* The quantified BDD. *}
2315 */
bdd_forallcomp(BDD r,BDD var)2316 BDD bdd_forallcomp(BDD r, BDD var)
2317 {
2318 return quantify(r, var, bddop_and, 1, CACHEID_EXISTC);
2319 }
2320
2321
2322 /*
2323 NAME {* bdd\_unique *}
2324 SECTION {* operator *}
2325 SHORT {* unique quantification of variables *}
2326 PROTO {* BDD bdd_unique(BDD r, BDD var) *}
2327 DESCR {* Removes all occurences in {\tt r} of variables in the set
2328 {\tt var} by unique quantification. This type of quantification
2329 uses a XOR operator instead of an OR operator as in the
2330 existential quantification, and an AND operator as in the
2331 universal quantification. *}
2332 ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2333 RETURN {* The quantified BDD. *}
2334 */
bdd_unique(BDD r,BDD var)2335 BDD bdd_unique(BDD r, BDD var)
2336 {
2337 return quantify(r, var, bddop_xor, 0, CACHEID_UNIQUE);
2338 }
2339
2340 /*
2341 NAME {* bdd\_uniquecomp *}
2342 SECTION {* operator *}
2343 SHORT {* unique quantification of other variables *}
2344 PROTO {* BDD bdd_uniquecomp(BDD r, BDD var) *}
2345 DESCR {* Removes all occurences in {\tt r} of variables now {\bf not} in
2346 the set {\tt var} by unique quantification. *}
2347 ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_uniquecomp, bdd\_makeset *}
2348 RETURN {* The quantified BDD. *}
2349 */
bdd_uniquecomp(BDD r,BDD var)2350 BDD bdd_uniquecomp(BDD r, BDD var)
2351 {
2352 return quantify(r, var, bddop_xor, 1, CACHEID_UNIQUEC);
2353 }
2354
2355
quant_rec(BDD r)2356 static int quant_rec(BDD r)
2357 {
2358 LOCAL_REC_STACKS;
2359 int index;
2360
2361 goto work;
2362 do
2363 {
2364 index = POPINT_();
2365 if (index < 0)
2366 {
2367 r = POPINT_();
2368 work:;
2369 /* C: -1 r --- */
2370 /* R: --- r */
2371 if (ISCONST(r) || LEVEL(r) > quantlast)
2372 {
2373 PUSHREF_(r);
2374 }
2375 else
2376 {
2377 BddCacheData *entry2 =
2378 BddCache_index(&quantcache, QUANTHASH(r), index);
2379 if (entry2->i.a == r && entry2->i.c == quantid)
2380 {
2381 #ifdef CACHESTATS
2382 bddcachestats.opHit++;
2383 #endif
2384 /* C: -1 r --- */
2385 /* R: --- res */
2386 PUSHREF_(entry2->i.res);
2387 }
2388 else
2389 {
2390 #ifdef CACHESTATS
2391 bddcachestats.opMiss++;
2392 #endif
2393 /* C: -1 r --- (-1 lr) -1 rr index r */
2394 PUSH4INT_(r, index, HIGH(r), -1)
2395 r = LOW(r);
2396 goto work;
2397 }
2398 }
2399 }
2400 else
2401 {
2402 /* C: index r --- */
2403 /* R: rres lres --- res */
2404 BDD r = POPINT_();
2405 BDD rres = READREF_(1);
2406 BDD lres = READREF_(2);
2407 BDD res;
2408 int lvl = LEVEL(r);
2409 SYNC_REC_STACKS;
2410 if (INVARSET(lvl))
2411 res = apply_rec(lres, rres);
2412 else
2413 res = bdd_makenode(lvl, lres, rres);
2414 POPREF_(2);
2415 PUSHREF_(res);
2416 BddCacheData* entry = quantcache.table + index;
2417 entry->i.a = r;
2418 entry->i.c = quantid;
2419 entry->i.res = res;
2420 }
2421 }
2422 while (NONEMPTY_REC_STACK);
2423
2424 BDD res = READREF_(1);
2425 POPREF_(1);
2426 SYNC_REC_STACKS;
2427 return res;
2428 }
2429
2430
2431 /*=== APPLY & QUANTIFY =================================================*/
2432
appquantify(BDD l,BDD r,int opr,BDD var,int qop,int comp,int qid)2433 static BDD appquantify(BDD l, BDD r, int opr, BDD var,
2434 int qop, int comp, int qid)
2435 {
2436 BDD res;
2437 firstReorder = 1;
2438
2439 CHECKa(l, bddfalse);
2440 CHECKa(r, bddfalse);
2441 CHECKa(var, bddfalse);
2442
2443 #ifndef NDEBUG
2444 if (opr<0 || opr>bddop_invimp)
2445 {
2446 bdd_error(BDD_OP);
2447 return bddfalse;
2448 }
2449 #endif
2450
2451 if (var < 2 && !comp) /* Empty set */
2452 return bdd_apply(l,r,opr);
2453
2454 again:
2455 if (__likely(bddreordermethod == BDD_REORDER_NONE)
2456 || setjmp(bddexception) == 0)
2457 {
2458 if (varset2vartable(var, comp) < 0)
2459 return bddfalse;
2460
2461 INITREF;
2462 applyop = qop;
2463 appexop = opr;
2464 appexid = (var << 5) | (appexop << 1); /* FIXME: range! */
2465 quantid = (appexid << 4) | qid;
2466
2467 if (__likely(firstReorder))
2468 {
2469 res = appquant_rec(l, r);
2470 }
2471 else
2472 {
2473 bdd_disable_reorder();
2474 res = appquant_rec(l, r);
2475 bdd_enable_reorder();
2476 }
2477 }
2478 else
2479 {
2480 bdd_checkreorder();
2481
2482 if (firstReorder-- == 1)
2483 goto again;
2484 res = BDDZERO; /* avoid warning about res being uninitialized */
2485 }
2486
2487 checkresize();
2488 return res;
2489 }
2490
2491 /*
2492 NAME {* bdd\_appex *}
2493 SECTION {* operator *}
2494 SHORT {* apply operation and existential quantification *}
2495 PROTO {* BDD bdd_appex(BDD left, BDD right, int opr, BDD var) *}
2496 DESCR {* Applies the binary operator {\tt opr} to the arguments
2497 {\tt left} and {\tt right} and then performs an existential
2498 quantification of the variables from the variable set
2499 {\tt var}. This is done in a bottom up manner such that both the
2500 apply and quantification is done on the lower nodes before
2501 stepping up to the higher nodes. This makes the {\tt bdd\_appex}
2502 function much more efficient than an apply operation followed
2503 by a quantification. If the operator is a conjunction then this
2504 is similar to the relational product of the two BDDs.
2505 \index{relational product} *}
2506 ALSO {* bdd\_appexcomp, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2507 RETURN {* The result of the operation. *}
2508 */
bdd_appex(BDD l,BDD r,int opr,BDD var)2509 BDD bdd_appex(BDD l, BDD r, int opr, BDD var)
2510 {
2511 return appquantify(l, r, opr, var, bddop_or, 0, CACHEID_APPEX);
2512 }
2513
2514
2515 /*
2516 NAME {* bdd\_appexcomp *}
2517 SECTION {* operator *}
2518 SHORT {* apply operation and existential (complemented) quantification *}
2519 PROTO {* BDD bdd_appexcomp(BDD left, BDD right, int opr, BDD var) *}
2520 DESCR {* Applies the binary operator {\tt opr} to the arguments
2521 {\tt left} and {\tt right} and then performs an existential
2522 quantification of the variables which are {\bf not} in the variable
2523 set {\tt var}. This is done in a bottom up manner such that both the
2524 apply and quantification is done on the lower nodes before
2525 stepping up to the higher nodes. This makes the {\tt bdd\_appexcomp}
2526 function much more efficient than an apply operation followed
2527 by a quantification. *}
2528 ALSO {* bdd\_appex, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2529 RETURN {* The result of the operation. *}
2530 */
bdd_appexcomp(BDD l,BDD r,int opr,BDD var)2531 BDD bdd_appexcomp(BDD l, BDD r, int opr, BDD var)
2532 {
2533 return appquantify(l, r, opr, var, bddop_or, 1, CACHEID_APPEXC);
2534 }
2535
2536
2537 /*
2538 NAME {* bdd\_appall *}
2539 SECTION {* operator *}
2540 SHORT {* apply operation and universal quantification *}
2541 PROTO {* BDD bdd_appall(BDD left, BDD right, int opr, BDD var) *}
2542 DESCR {* Applies the binary operator {\tt opr} to the arguments
2543 {\tt left} and {\tt right} and then performs a universal
2544 quantification of the variables from the variable set
2545 {\tt var}. This is done in a bottom up manner such that both the
2546 apply and quantification is done on the lower nodes before
2547 stepping up to the higher nodes. This makes the {\tt bdd\_appall}
2548 function much more efficient than an apply operation followed
2549 by a quantification. *}
2550 ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2551 RETURN {* The result of the operation. *}
2552 */
bdd_appall(BDD l,BDD r,int opr,BDD var)2553 BDD bdd_appall(BDD l, BDD r, int opr, BDD var)
2554 {
2555 return appquantify(l, r, opr, var, bddop_and, 0, CACHEID_APPAL);
2556 }
2557
2558
2559 /*
2560 NAME {* bdd\_appallcomp *}
2561 SECTION {* operator *}
2562 SHORT {* apply operation and universal (complemented) quantification *}
2563 PROTO {* BDD bdd_appall(BDD left, BDD right, int opr, BDD var) *}
2564 DESCR {* Applies the binary operator {\tt opr} to the arguments
2565 {\tt left} and {\tt right} and then performs a universal
2566 quantification of the variables which are {\bf not} in the variable
2567 set {\tt var}. This is done in a bottom up manner such that both the
2568 apply and quantification is done on the lower nodes before
2569 stepping up to the higher nodes. This makes the
2570 {\tt bdd\_appallcomp} function much more efficient than an
2571 apply operation followed by a quantification. *}
2572 ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appall, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2573 RETURN {* The result of the operation. *}
2574 */
bdd_appallcomp(BDD l,BDD r,int opr,BDD var)2575 BDD bdd_appallcomp(BDD l, BDD r, int opr, BDD var)
2576 {
2577 return appquantify(l, r, opr, var, bddop_and, 1, CACHEID_APPALC);
2578 }
2579
2580
2581 /*
2582 NAME {* bdd\_appuni *}
2583 SECTION {* operator *}
2584 SHORT {* apply operation and unique quantification *}
2585 PROTO {* BDD bdd_appuni(BDD left, BDD right, int opr, BDD var) *}
2586 DESCR {* Applies the binary operator {\tt opr} to the arguments
2587 {\tt left} and {\tt right} and then performs a unique
2588 quantification of the variables from the variable set
2589 {\tt var}. This is done in a bottom up manner such that both the
2590 apply and quantification is done on the lower nodes before
2591 stepping up to the higher nodes. This makes the {\tt bdd\_appuni}
2592 function much more efficient than an apply operation followed
2593 by a quantification. *}
2594 ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2595 RETURN {* The result of the operation. *}
2596 */
bdd_appuni(BDD l,BDD r,int opr,BDD var)2597 BDD bdd_appuni(BDD l, BDD r, int opr, BDD var)
2598 {
2599 return appquantify(l, r, opr, var, bddop_xor, 0, CACHEID_APPUN);
2600 }
2601
2602
2603 /*
2604 NAME {* bdd\_appunicomp *}
2605 SECTION {* operator *}
2606 SHORT {* apply operation and unique (complemented) quantification *}
2607 PROTO {* BDD bdd_appunicomp(BDD left, BDD right, int opr, BDD var) *}
2608 DESCR {* Applies the binary operator {\tt opr} to the arguments
2609 {\tt left} and {\tt right} and then performs a unique
2610 quantification of the variables which are {\bf not} in the variable
2611 set {\tt var}. This is done in a bottom up manner such that both the
2612 apply and quantification is done on the lower nodes before
2613 stepping up to the higher nodes. This makes the
2614 {\tt bdd\_appunicomp} function much more efficient than an
2615 apply operation followed by a quantification. *}
2616 ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
2617 RETURN {* The result of the operation. *}
2618 */
bdd_appunicomp(BDD l,BDD r,int opr,BDD var)2619 BDD bdd_appunicomp(BDD l, BDD r, int opr, BDD var)
2620 {
2621 return appquantify(l, r, opr, var, bddop_xor, 1, CACHEID_APPUNC);
2622 }
2623
2624
appquant_rec(BDD l,BDD r)2625 static BDD appquant_rec(BDD l, BDD r)
2626 {
2627 LOCAL_REC_STACKS;
2628 int index;
2629
2630 goto work;
2631 do
2632 {
2633 index = POPINT_();
2634 if (index < 0)
2635 {
2636 l = POPINT_();
2637 r = POPINT_();
2638 work:
2639 /* C: -1 l r --- */
2640 /* R: --- res */
2641 if (ISCONST(l) && ISCONST(r))
2642 RETURN(oprres[appexop][l<<1 | r]);
2643
2644 if (LEVEL(l) > quantlast && LEVEL(r) > quantlast)
2645 {
2646 int oldop = applyop;
2647 applyop = appexop;
2648 SYNC_REC_STACKS;
2649 int res = apply_rec(l,r);
2650 PUSHREF_(res);
2651 applyop = oldop;
2652 continue;
2653 }
2654
2655 /* empty macro arguments are undefined in ISO C90 and
2656 ISO C++98, so use + when we do not want to call any
2657 function. */
2658 SYNC_REC_STACKS;
2659 APPLY_SHORTCUTS(appexop, quant_rec);
2660
2661 BddCacheData *entry2 =
2662 BddCache_index(&appexcache, APPEXHASH(l,r,appexop), index);
2663 /* Check entry2->b last, because not_rec() does not
2664 initialize it. */
2665 if (entry2->i.a == l && entry2->i.c == appexid
2666 && entry2->i.b == r)
2667 {
2668 #ifdef CACHESTATS
2669 bddcachestats.opHit++;
2670 #endif
2671 /* C: -1 l r --- */
2672 /* R: --- res */
2673 RETURN(entry2->i.res);
2674 }
2675 #ifdef CACHESTATS
2676 bddcachestats.opMiss++;
2677 #endif
2678 /* C: -1 l r --- (-1 ll rl) -1 lr rr index lvl l r */
2679 int lvl_l = LEVEL(l);
2680 int lvl_r = LEVEL(r);
2681 if (lvl_l == lvl_r)
2682 {
2683 PUSH4INT_(r, l, lvl_l, index);
2684 PUSH3INT_(HIGH(r), HIGH(l), -1);
2685 r = LOW(r);
2686 l = LOW(l);
2687 }
2688 else if (lvl_l < lvl_r)
2689 {
2690 PUSH4INT_(r, l, lvl_l, index);
2691 PUSH3INT_(r, HIGH(l), -1);
2692 l = LOW(l);
2693 }
2694 else /* lvl_l > lvl_r */
2695 {
2696 PUSH4INT_(r, l, lvl_r, index);
2697 PUSH3INT_(HIGH(r), l, -1);
2698 r = LOW(r);
2699 }
2700 goto work;
2701 }
2702 else
2703 {
2704 /* C: index lvl l r --- */
2705 /* R: rres lres --- res */
2706 BDD rres = READREF_(1);
2707 BDD lres = READREF_(2);
2708 int lvl = POPINT_();
2709 BDD l = POPINT_();
2710 BDD r = POPINT_();
2711 BDD res;
2712 SYNC_REC_STACKS;
2713 if (INVARSET(lvl))
2714 res = apply_rec(lres, rres);
2715 else
2716 res = bdd_makenode(lvl, lres, rres);
2717 POPREF_(2);
2718 PUSHREF_(res);
2719 BddCacheData* entry = appexcache.table + index;
2720 entry->i.a = l;
2721 entry->i.c = appexid;
2722 entry->i.b = r;
2723 entry->i.res = res;
2724 }
2725 }
2726 while (NONEMPTY_REC_STACK);
2727
2728 BDD res = READREF_(1);
2729 POPREF_(1);
2730 SYNC_REC_STACKS;
2731 return res;
2732 }
2733
2734
2735 /*************************************************************************
2736 Informational functions
2737 *************************************************************************/
2738
2739 /*=== SUPPORT ==========================================================*/
2740
2741 /*
2742 NAME {* bdd\_support *}
2743 SECTION {* info *}
2744 SHORT {* returns the variable support of a BDD *}
2745 PROTO {* BDD bdd_support(BDD r) *}
2746 DESCR {* Finds all the variables that {\tt r} depends on. That is
2747 the support of {\tt r}. *}
2748 ALSO {* bdd\_makeset *}
2749 RETURN {* A BDD variable set. *}
2750 */
bdd_support(BDD r)2751 BDD bdd_support(BDD r)
2752 {
2753 BddCacheData *entry;
2754 static int supportSize = 0;
2755 int n;
2756 int res=1;
2757
2758 CHECKa(r, bddfalse);
2759
2760 /* Variable sets are conjunctions, so the empty support is bddtrue. */
2761 if (r < 2)
2762 return bddtrue;
2763
2764 entry = BddCache_lookup(&misccache, SUPPORTHASH(r));
2765 if (entry->i.a == r && entry->i.c == CACHEID_SUPPORT)
2766 {
2767 #ifdef CACHESTATS
2768 bddcachestats.opHit++;
2769 #endif
2770 return entry->i.res;
2771 }
2772 #ifdef CACHESTATS
2773 bddcachestats.opMiss++;
2774 #endif
2775
2776 /* On-demand allocation of support set */
2777 if (__unlikely(supportSize < bddvarnum))
2778 {
2779 if (__likely(supportSet))
2780 free(supportSet);
2781 if (__unlikely((supportSet=(int*)malloc(bddvarnum*sizeof(int))) == NULL))
2782 {
2783 bdd_error(BDD_MEMORY);
2784 return bddfalse;
2785 }
2786 memset(supportSet, 0, bddvarnum*sizeof(int));
2787 supportSize = bddvarnum;
2788 supportID = 0;
2789 }
2790
2791 /* Update global variables used to speed up bdd_support()
2792 * - instead of always memsetting support to zero, we use
2793 * a change counter.
2794 * - and instead of reading the whole array afterwards, we just
2795 * look from 'min' to 'max' used BDD variables.
2796 */
2797 if (__unlikely(supportID == 0x0FFFFFFF))
2798 {
2799 /* We probably don't get here -- but let's just be sure */
2800 memset(supportSet, 0, bddvarnum*sizeof(int));
2801 supportID = 0;
2802 }
2803 ++supportID;
2804 supportMin = LEVEL(r);
2805 supportMax = supportMin;
2806
2807 support_rec(r, supportSet);
2808 bdd_unmark(r);
2809
2810 bdd_disable_reorder();
2811
2812 for (n=supportMax ; n>=supportMin ; --n)
2813 if (supportSet[n] == supportID)
2814 {
2815 register BDD tmp;
2816 bdd_addref(res);
2817 tmp = bdd_makenode(n, 0, res);
2818 bdd_delref(res);
2819 res = tmp;
2820 }
2821
2822 bdd_enable_reorder();
2823
2824 entry->i.a = r;
2825 entry->i.c = CACHEID_SUPPORT;
2826 entry->i.res = res;
2827
2828 return res;
2829 }
2830
2831
support_rec(int r,int * support)2832 static void support_rec(int r, int* support)
2833 {
2834 // Reuse bddrefstack as temporary stack
2835 int* bot = bddrefstacktop;
2836 int* top = bot;
2837 goto work;
2838 while (top > bot)
2839 {
2840 r = *--top;
2841 work:
2842 if (r < 2)
2843 continue;
2844 BddNode *node = &bddnodes[r];
2845 if (LEVELp(node) & MARKON || LOWp(node) == -1)
2846 continue;
2847 support[LEVELp(node)] = supportID;
2848 if (LEVELp(node) > supportMax)
2849 supportMax = LEVELp(node);
2850 LEVELp(node) |= MARKON;
2851 *top++ = LOWp(node);
2852 r = HIGHp(node);
2853 goto work;
2854 }
2855 }
2856
2857
2858 /*=== ONE SATISFYING VARIABLE ASSIGNMENT ===============================*/
2859
2860 /*
2861 NAME {* bdd\_satone *}
2862 SECTION {* operator *}
2863 SHORT {* finds one satisfying variable assignment *}
2864 PROTO {* BDD bdd_satone(BDD r) *}
2865 DESCR {* Finds a BDD with at most one variable at each level. This BDD
2866 implies {\tt r} and is not false unless {\tt r} is
2867 false. *}
2868 ALSO {* bdd\_allsat, bdd\_satoneset, bdd\_satprefix, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *}
2869 RETURN {* The result of the operation. *}
2870 */
bdd_satone(BDD r)2871 BDD bdd_satone(BDD r)
2872 {
2873 BDD res;
2874
2875 CHECKa(r, bddfalse);
2876 if (r < 2)
2877 return r;
2878
2879 bdd_disable_reorder();
2880
2881 INITREF;
2882 res = satone_rec(r);
2883
2884 bdd_enable_reorder();
2885
2886 checkresize();
2887 return res;
2888 }
2889
2890
satone_rec(BDD r)2891 static BDD satone_rec(BDD r)
2892 {
2893 LOCAL_REC_STACKS;
2894
2895 while (ISNONCONST(r))
2896 {
2897 BDD low = LOW(r);
2898 int iszero = ISZERO(low);
2899 int lvl = LEVEL(r);
2900 if (iszero)
2901 {
2902 PUSHINT_(lvl);
2903 r = HIGH(r);
2904 }
2905 else
2906 {
2907 PUSHINT_(~lvl);
2908 r = low;
2909 }
2910 }
2911 PUSHREF_(r);
2912 while (NONEMPTY_REC_STACK)
2913 {
2914 /* C: lvl --- */
2915 /* R: r --- res */
2916 BDD r = READREF_(1);
2917 int lvl = POPINT_();
2918 BDD res;
2919 SYNC_REC_STACKS;
2920 if (lvl >= 0)
2921 res = bdd_makenode(lvl, BDDZERO, r);
2922 else
2923 res = bdd_makenode(~lvl, r, BDDZERO);
2924 POPREF_(1);
2925 PUSHREF_(res);
2926 }
2927
2928 BDD res = READREF_(1);
2929 POPREF_(1);
2930 SYNC_REC_STACKS;
2931 return res;
2932 }
2933
2934
2935 /*
2936 NAME {* bdd\_satprefix *}
2937 SECTION {* operator *}
2938 SHORT {* quickly remove a conjunction common to all satisfying assignments *}
2939 PROTO {* BDD bdd_satprefix(BDD* r) *}
2940 DESCR {* Recursively descend into the top of the BDD and return the
2941 prefix common to all satisfying paths. Adjust r to point to
2942 the rest of the BDD. *}
2943 ALSO {* bdd\_allsat, bdd\_satone, bdd\_satoneset, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *}
2944 RETURN {* The result of the operation. *}
2945 */
bdd_satprefix(BDD * r)2946 BDD bdd_satprefix(BDD* r)
2947 {
2948 BDD res;
2949
2950 CHECKa(*r, bddfalse);
2951 if (__unlikely(*r < 2))
2952 return *r;
2953
2954 bdd_disable_reorder();
2955
2956 INITREF;
2957 res = satprefix_rec(r);
2958
2959 bdd_enable_reorder();
2960
2961 checkresize();
2962 return res;
2963
2964 }
2965
satprefix_rec(BDD * r)2966 static BDD satprefix_rec(BDD* r)
2967 {
2968 if (ISCONST(*r))
2969 return *r;
2970
2971 if (ISZERO(LOW(*r)))
2972 {
2973 int lr = LEVEL(*r);
2974 *r = HIGH(*r);
2975 return PUSHREF(bdd_makenode(lr, BDDZERO, satprefix_rec(r)));
2976 }
2977 else if (ISZERO(HIGH(*r)))
2978 {
2979 int lr = LEVEL(*r);
2980 *r = LOW(*r);
2981 return PUSHREF(bdd_makenode(lr, satprefix_rec(r), BDDZERO));
2982 }
2983 else
2984 {
2985 return BDDONE;
2986 }
2987 }
2988
2989 /*
2990 NAME {* bdd\_satoneset *}
2991 SECTION {* operator *}
2992 SHORT {* finds one satisfying variable assignment *}
2993 PROTO {* BDD bdd_satoneset(BDD r, BDD var, BDD pol) *}
2994 DESCR {* Finds a minterm in {\tt r}. The {\tt var} argument is a
2995 variable set that defines a set of variables that {\em must} be
2996 mentioned in the result. The polarity of these variables in
2997 result---in case they are undefined in {\tt r}---are defined
2998 by the {\tt pol} parameter. If {\tt pol} is the false BDD then
2999 the variables will be in negative form, and otherwise they will
3000 be in positive form. *}
3001 ALSO {* bdd\_allsat, bdd\_satone, bdd\_satprefix, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *}
3002 RETURN {* The result of the operation. *}
3003 */
bdd_satoneset(BDD r,BDD var,BDD pol)3004 BDD bdd_satoneset(BDD r, BDD var, BDD pol)
3005 {
3006 BDD res;
3007
3008 CHECKa(r, bddfalse);
3009 if (ISZERO(r))
3010 return r;
3011 #ifndef NDEBUG
3012 if (!ISCONST(pol))
3013 {
3014 bdd_error(BDD_ILLBDD);
3015 return bddfalse;
3016 }
3017 #endif
3018 bdd_disable_reorder();
3019
3020 INITREF;
3021 satPolarity = pol;
3022 res = satoneset_rec(r, var);
3023
3024 bdd_enable_reorder();
3025
3026 checkresize();
3027 return res;
3028 }
3029
satoneset_rec(BDD r,BDD var)3030 static BDD satoneset_rec(BDD r, BDD var)
3031 {
3032 LOCAL_REC_STACKS;
3033
3034 while (!(ISCONST(r) && ISCONST(var)))
3035 {
3036 int lvl_r = LEVEL(r);
3037 int lvl_v = LEVEL(var);
3038 if (lvl_r <= lvl_v)
3039 {
3040 int low_r = LOW(r);
3041 if (ISZERO(low_r))
3042 {
3043 PUSHINT_(lvl_r);
3044 r = HIGH(r);
3045 }
3046 else
3047 {
3048 PUSHINT_(~lvl_r);
3049 r = low_r;
3050 }
3051 if (lvl_r == lvl_v)
3052 var = HIGH(var);
3053 }
3054 else /* lvl_v < lvl_r */
3055 {
3056 if (satPolarity == BDDONE)
3057 PUSHINT_(lvl_v);
3058 else
3059 PUSHINT_(~lvl_v);
3060 var = HIGH(var);
3061 }
3062 }
3063 PUSHREF_(r);
3064 while (NONEMPTY_REC_STACK)
3065 {
3066 BDD r = READREF_(1);
3067 int lvl = POPINT_();
3068 SYNC_REC_STACKS;
3069 BDD res;
3070 if (lvl >= 0)
3071 res = bdd_makenode(lvl, BDDZERO, r);
3072 else
3073 res = bdd_makenode(~lvl, r, BDDZERO);
3074 POPREF_(1);
3075 PUSHREF_(res);
3076 }
3077
3078 BDD res = READREF_(1);
3079 POPREF_(1);
3080 SYNC_REC_STACKS;
3081 return res;
3082 }
3083
3084
3085 /* Compute the smallest distance associated to a satisfying path of f,
3086 but without actually building the corresponding cube. This is done
3087 by computing the distance recursively for all sub BDDs, and storing
3088 those in a hashtable, with the intention of sharing that across
3089 all calls of bdd_satoneshortest with the same weights.
3090
3091 The hash table used for cache stores triples of the form (bdd, rev,
3092 dist) where dist is the distance for bdd, and rev is incremented
3093 everytime bdd_satoneshortest is called with a different set of
3094 weights. One should therefore check that rev from the cache lookup
3095 matches the current rev stored in shortest_rev. bdd_satoneshortest
3096 is in charge of incrementing shortest_rev.
3097 */
3098 static unsigned wlow_ref = 0;
3099 static unsigned whigh_ref = 0;
3100 static unsigned wdc_ref = 0;
3101 static int shortest_rev = 0;
3102
3103 /* This computes the shortest distance, recursively.
3104 Populating the cache. */
satoneshortest_rec(BDD f)3105 static unsigned satoneshortest_rec(BDD f)
3106 {
3107 if (ISONE(f))
3108 return 0;
3109 if (ISZERO(f))
3110 return -1U;
3111 int rev = shortest_rev;
3112 BddCacheData *entry = BddCache_lookup(&misccache, SHORTDISTHASH(f,rev));
3113 if (entry->i.a == f
3114 && entry->i.b == rev
3115 && entry->i.c == CACHEID_SHORTDIST)
3116 {
3117 #ifdef CACHESTATS
3118 bddcachestats.opHit++;
3119 #endif
3120 return (unsigned) entry->i.res;
3121 }
3122 #ifdef CACHESTATS
3123 bddcachestats.opMiss++;
3124 #endif
3125
3126 int lv_next = LEVEL(f) + 1;
3127 int low = LOW(f);
3128 int lv_low = LEVEL(low);
3129 unsigned dist_low = satoneshortest_rec(low);
3130 if (dist_low != -1U)
3131 dist_low += wlow_ref + wdc_ref * (lv_low - lv_next);
3132 int high = HIGH(f);
3133 int lv_high = LEVEL(high);
3134 unsigned dist_high = satoneshortest_rec(high);
3135 if (dist_high != -1U)
3136 dist_high += whigh_ref + wdc_ref * (lv_high - lv_next);
3137
3138 if (dist_high < dist_low)
3139 dist_low = dist_high;
3140
3141 entry->i.a = f;
3142 entry->i.b = rev;
3143 entry->i.c = CACHEID_SHORTDIST;
3144 entry->i.res = (int) dist_low;
3145 return dist_low;
3146 }
3147
3148 /* This computes the BDD for the shortest distance, recursively.
3149 It calls satoneshortest_rec again, but this should be fast thanks to
3150 the cache.
3151 */
bdd_satoneshortest_rec(BDD f)3152 static bdd bdd_satoneshortest_rec(BDD f)
3153 {
3154 if (ISONE(f))
3155 return bddtrue;
3156 if (ISZERO(f))
3157 return bddfalse;
3158
3159 int rev = shortest_rev;
3160 BddCacheData *entry = BddCache_lookup(&misccache, SHORTBDDHASH(f,rev));
3161 if (entry->i.a == f
3162 && entry->i.b == rev
3163 && entry->i.c == CACHEID_SHORTDIST)
3164 {
3165 #ifdef CACHESTATS
3166 bddcachestats.opHit++;
3167 #endif
3168 return entry->i.res;
3169 }
3170 #ifdef CACHESTATS
3171 bddcachestats.opMiss++;
3172 #endif
3173
3174 int lv = LEVEL(f);
3175 int lv_next = lv + 1;
3176 int low = LOW(f);
3177 int lv_low = LEVEL(low);
3178 unsigned dist_low = satoneshortest_rec(low);
3179 if (dist_low != -1U)
3180 dist_low += wlow_ref + wdc_ref * (lv_low - lv_next);
3181
3182 int high = HIGH(f);
3183 int lv_high = LEVEL(high);
3184 unsigned dist_high = satoneshortest_rec(high);
3185 if (dist_high != -1U)
3186 dist_high += whigh_ref + wdc_ref * (lv_high - lv_next);
3187
3188 bdd res;
3189 if (dist_high < dist_low)
3190 {
3191 res = bdd_satoneshortest_rec(high);
3192 res = PUSHREF(bdd_makenode(lv, 0, res));
3193 }
3194 else
3195 {
3196 res = bdd_satoneshortest_rec(low);
3197 res = PUSHREF(bdd_makenode(lv, res, 0));
3198 }
3199
3200 entry->i.a = f;
3201 entry->i.b = rev;
3202 entry->i.c = CACHEID_SHORTBDD;
3203 entry->i.res = res;
3204 return res;
3205 }
3206
3207 /*
3208 return a conjunction representing a satisfying path of f, chosen
3209 among all satisfying paths to minimize the sum of weights given for
3210 positive variables (whigh), negative variables (wlow), and don't care
3211 variables (wdc = Weight of Don't Care).
3212 */
bdd_satoneshortest(BDD f,unsigned wlow,unsigned whigh,unsigned wdc)3213 BDD bdd_satoneshortest(BDD f, unsigned wlow, unsigned whigh, unsigned wdc)
3214 {
3215 if (wlow != wlow_ref || whigh != whigh_ref || wdc != wdc_ref)
3216 {
3217 wlow_ref = wlow;
3218 whigh_ref = whigh;
3219 wdc_ref = wdc;
3220 ++shortest_rev;
3221 }
3222 bdd_disable_reorder();
3223 INITREF;
3224 bdd res = bdd_satoneshortest_rec(f);
3225 bdd_enable_reorder();
3226 checkresize();
3227 return res;
3228 }
3229
3230
3231
3232 /*=== EXACTLY ONE SATISFYING VARIABLE ASSIGNMENT =======================*/
3233
3234 /*
3235 NAME {* bdd\_fullsatone *}
3236 SECTION {* operator *}
3237 SHORT {* finds one satisfying variable assignment *}
3238 PROTO {* BDD bdd_fullsatone(BDD r) *}
3239 DESCR {* Finds a BDD with exactly one variable at all levels. This BDD
3240 implies {\tt r} and is not false unless {\tt r} is
3241 false. *}
3242 ALSO {* bdd\_allsat, bdd\_satone, bdd\_satprefix, bdd\_satoneset, bdd\_satcount, bdd\_satcountln *}
3243 RETURN {* The result of the operation. *}
3244 */
bdd_fullsatone(BDD r)3245 BDD bdd_fullsatone(BDD r)
3246 {
3247 BDD res;
3248 int v;
3249
3250 CHECKa(r, bddfalse);
3251 if (r == 0)
3252 return 0;
3253
3254 bdd_disable_reorder();
3255
3256 INITREF;
3257 res = fullsatone_rec(r);
3258
3259 for (v=LEVEL(r)-1 ; v>=0 ; v--)
3260 {
3261 res = PUSHREF( bdd_makenode(v, res, 0) );
3262 }
3263
3264 bdd_enable_reorder();
3265
3266 checkresize();
3267 return res;
3268 }
3269
3270
fullsatone_rec(int r)3271 static int fullsatone_rec(int r)
3272 {
3273 if (r < 2)
3274 return r;
3275
3276 if (LOW(r) != 0)
3277 {
3278 int res = fullsatone_rec(LOW(r));
3279 int v;
3280
3281 for (v=LEVEL(LOW(r))-1 ; v>LEVEL(r) ; v--)
3282 {
3283 res = PUSHREF( bdd_makenode(v, res, 0) );
3284 }
3285
3286 return PUSHREF( bdd_makenode(LEVEL(r), res, 0) );
3287 }
3288 else
3289 {
3290 int res = fullsatone_rec(HIGH(r));
3291 int v;
3292
3293 for (v=LEVEL(HIGH(r))-1 ; v>LEVEL(r) ; v--)
3294 {
3295 res = PUSHREF( bdd_makenode(v, res, 0) );
3296 }
3297
3298 return PUSHREF( bdd_makenode(LEVEL(r), 0, res) );
3299 }
3300 }
3301
3302
3303 /*=== ALL SATISFYING VARIABLE ASSIGNMENTS ==============================*/
3304
3305 /*
3306 NAME {* bdd\_allsat *}
3307 SECTION {* operator *}
3308 SHORT {* finds all satisfying variable assignments *}
3309 PROTO {* BDD bdd_allsat(BDD r, bddallsathandler handler) *}
3310 DESCR {* Iterates through all legal variable assignments (those
3311 that make the BDD come true) for the bdd {\tt r} and
3312 calls the callback handler {\tt handler} for each of them.
3313 The array passed to {\tt handler} contains one entry for
3314 each of the globally defined variables. Each entry is either
3315 0 if the variable is false, 1 if it is true, and -1 if it
3316 is a don't care.
3317
3318 The following is an example of a callback handler that
3319 prints 'X' for don't cares, '0' for zero, and '1' for one:
3320 \begin{verbatim}
3321 void allsatPrintHandler(signed char* varset, int size)
3322 {
3323 for (int v=0; v<size ; ++v)
3324 {
3325 cout << (varset[v] < 0 ? 'X' : (char)('0' + varset[v]));
3326 }
3327 cout << endl;
3328 }
3329 \end{verbatim}
3330
3331 \noindent
3332 The handler can be used like this:
3333 {\tt bdd\_allsat(r, allsatPrintHandler); } *}
3334
3335 ALSO {* bdd\_satone bdd\_satoneset, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *}
3336 */
bdd_allsat(BDD r,bddallsathandler handler)3337 void bdd_allsat(BDD r, bddallsathandler handler)
3338 {
3339 int v;
3340
3341 CHECKn(r);
3342
3343 if (__unlikely((allsatProfile=(signed char*)malloc(bddvarnum)) == NULL))
3344 {
3345 bdd_error(BDD_MEMORY);
3346 return;
3347 }
3348
3349 for (v=LEVEL(r)-1 ; v>=0 ; --v)
3350 allsatProfile[bddlevel2var[v]] = -1;
3351
3352 allsatHandler = handler;
3353 INITREF;
3354
3355 allsat_rec(r);
3356
3357 free(allsatProfile);
3358 }
3359
3360
allsat_rec(BDD r)3361 static void allsat_rec(BDD r)
3362 {
3363 if (ISONE(r))
3364 {
3365 allsatHandler(allsatProfile, bddvarnum);
3366 return;
3367 }
3368
3369 if (ISZERO(r))
3370 return;
3371
3372 if (!ISZERO(LOW(r)))
3373 {
3374 int v;
3375
3376 allsatProfile[bddlevel2var[LEVEL(r)]] = 0;
3377
3378 for (v=LEVEL(LOW(r))-1 ; v>LEVEL(r) ; --v)
3379 {
3380 allsatProfile[bddlevel2var[v]] = -1;
3381 }
3382
3383 allsat_rec(LOW(r));
3384 }
3385
3386 if (!ISZERO(HIGH(r)))
3387 {
3388 int v;
3389
3390 allsatProfile[bddlevel2var[LEVEL(r)]] = 1;
3391
3392 for (v=LEVEL(HIGH(r))-1 ; v>LEVEL(r) ; --v)
3393 {
3394 allsatProfile[bddlevel2var[v]] = -1;
3395 }
3396
3397 allsat_rec(HIGH(r));
3398 }
3399 }
3400
3401
3402 /*=== COUNT NUMBER OF SATISFYING ASSIGNMENT ============================*/
3403
3404 /*
3405 NAME {* bdd\_satcount *}
3406 EXTRA {* bdd\_setcountset *}
3407 SECTION {* info *}
3408 SHORT {* calculates the number of satisfying variable assignments *}
3409 PROTO {* double bdd_satcount(BDD r)
3410 double bdd_satcountset(BDD r, BDD varset) *}
3411 DESCR {* Calculates how many possible variable assignments there exists
3412 such that {\tt r} is satisfied (true). All defined
3413 variables are considered in the first version. In the
3414 second version, only the variables in the variable
3415 set {\tt varset} are considered. This makes the function a
3416 {\em lot} slower. *}
3417 ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcountln *}
3418 RETURN {* The number of possible assignments. *}
3419 */
bdd_satcount(BDD r)3420 double bdd_satcount(BDD r)
3421 {
3422 double size=1;
3423
3424 CHECKa(r, 0.0);
3425
3426 // Invalidate misccache if the number of variable changed since we
3427 // last used it.
3428 if (misccache_varnum != bddvarnum)
3429 {
3430 BddCache_reset(&misccache);
3431 misccache_varnum = bddvarnum;
3432 }
3433
3434 miscid = CACHEID_SATCOU;
3435 size = pow(2.0, (double)LEVEL(r));
3436
3437 return size * satcount_rec(r);
3438 }
3439
3440
bdd_satcountset(BDD r,BDD varset)3441 double bdd_satcountset(BDD r, BDD varset)
3442 {
3443 double unused = bddvarnum;
3444 BDD n;
3445
3446 if (ISZERO(r))
3447 return 0.0;
3448 if (ISCONST(varset)) /* empty set */
3449 return ISONE(r) ? 1.0 : 0.0;
3450
3451 for (n=varset ; !ISCONST(n) ; n=HIGH(n))
3452 unused--;
3453
3454 unused = bdd_satcount(r) / pow(2.0,unused);
3455
3456 return unused >= 1.0 ? unused : 1.0;
3457 }
3458
3459
satcount_rec(int root)3460 static double satcount_rec(int root)
3461 {
3462 BddCacheData *entry;
3463 BddNode *node;
3464 double size, s;
3465
3466 if (root < 2)
3467 return root;
3468
3469 entry = BddCache_lookup(&misccache, SATCOUHASH(root));
3470 if (entry->d.a == root && entry->d.c == miscid)
3471 return entry->d.res;
3472
3473 node = &bddnodes[root];
3474 size = 0;
3475 s = 1;
3476
3477 s *= pow(2.0, (float)(LEVEL(LOWp(node)) - LEVELp(node) - 1));
3478 size += s * satcount_rec(LOWp(node));
3479
3480 s = 1;
3481 s *= pow(2.0, (float)(LEVEL(HIGHp(node)) - LEVELp(node) - 1));
3482 size += s * satcount_rec(HIGHp(node));
3483
3484 entry->d.a = root;
3485 entry->d.c = miscid;
3486 entry->d.res = size;
3487
3488 return size;
3489 }
3490
3491
3492 /*
3493 NAME {* bdd\_satcountln *}
3494 EXTRA {* bdd\_setcountlnset *}
3495 SECTION {* info *}
3496 SHORT {* calculates the log. number of satisfying variable assignments *}
3497 PROTO {* double bdd_satcountln(BDD r)
3498 double bdd_satcountlnset(BDD r, BDD varset)*}
3499 DESCR {* Calculates how many possible variable assignments there
3500 exists such that {\tt r} is satisfied (true) and returns
3501 the logarithm of this. The result is calculated in such a
3502 manner that it is practically impossible to get an
3503 overflow, which is very possible for {\tt bdd\_satcount} if
3504 the number of defined variables is too large. All defined
3505 variables are considered in the first version. In the
3506 second version, only the variables in the variable
3507 set {\tt varset} are considered. This makes the function
3508 a {\em lot} slower! *}
3509 ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcount *}
3510 RETURN {* The logarithm of the number of possible assignments. *} */
bdd_satcountln(BDD r)3511 double bdd_satcountln(BDD r)
3512 {
3513 double size;
3514
3515 CHECKa(r, 0.0);
3516
3517 // Invalidate misccache if the number of variable changed since we
3518 // last used it.
3519 if (misccache_varnum != bddvarnum)
3520 {
3521 BddCache_reset(&misccache);
3522 misccache_varnum = bddvarnum;
3523 }
3524
3525 miscid = CACHEID_SATCOULN;
3526 size = satcountln_rec(r);
3527
3528 if (size >= 0.0)
3529 size += LEVEL(r);
3530
3531 return size;
3532 }
3533
3534
bdd_satcountlnset(BDD r,BDD varset)3535 double bdd_satcountlnset(BDD r, BDD varset)
3536 {
3537 double unused = bddvarnum;
3538 BDD n;
3539
3540 if (ISCONST(varset)) /* empty set */
3541 return 0.0;
3542
3543 for (n=varset ; !ISCONST(n) ; n=HIGH(n))
3544 unused--;
3545
3546 unused = bdd_satcountln(r) - unused;
3547
3548 return unused >= 0.0 ? unused : 0.0;
3549 }
3550
3551
satcountln_rec(int root)3552 static double satcountln_rec(int root)
3553 {
3554 BddCacheData *entry;
3555 BddNode *node;
3556 double size, s1,s2;
3557
3558 if (root == 0)
3559 return -1.0;
3560 if (root == 1)
3561 return 0.0;
3562
3563 entry = BddCache_lookup(&misccache, SATCOUHASH(root));
3564 if (entry->d.a == root && entry->d.c == miscid)
3565 return entry->d.res;
3566
3567 node = &bddnodes[root];
3568
3569 s1 = satcountln_rec(LOWp(node));
3570 if (s1 >= 0.0)
3571 s1 += LEVEL(LOWp(node)) - LEVELp(node) - 1;
3572
3573 s2 = satcountln_rec(HIGHp(node));
3574 if (s2 >= 0.0)
3575 s2 += LEVEL(HIGHp(node)) - LEVELp(node) - 1;
3576
3577 if (s1 < 0.0)
3578 size = s2;
3579 else if (s2 < 0.0)
3580 size = s1;
3581 else if (s1 < s2)
3582 size = s2 + log1p(pow(2.0,s1-s2)) / M_LN2;
3583 else
3584 size = s1 + log1p(pow(2.0,s2-s1)) / M_LN2;
3585
3586 entry->d.a = root;
3587 entry->d.c = miscid;
3588 entry->d.res = size;
3589
3590 return size;
3591 }
3592
3593
3594 /*=== COUNT NUMBER OF ALLOCATED NODES ==================================*/
3595
3596 /*
3597 NAME {* bdd\_nodecount *}
3598 SECTION {* info *}
3599 SHORT {* counts the number of nodes used for a BDD *}
3600 PROTO {* int bdd_nodecount(BDD r) *}
3601 DESCR {* Traverses the BDD and counts all distinct nodes that are used
3602 for the BDD. *}
3603 RETURN {* The number of nodes. *}
3604 ALSO {* bdd\_pathcount, bdd\_satcount, bdd\_anodecount *}
3605 */
bdd_nodecount(BDD r)3606 int bdd_nodecount(BDD r)
3607 {
3608 int num=0;
3609
3610 CHECK(r);
3611
3612 bdd_markcount(r, &num);
3613 bdd_unmark(r);
3614
3615 return num;
3616 }
3617
3618
3619 /*
3620 NAME {* bdd\_anodecount *}
3621 SECTION {* info *}
3622 SHORT {* counts the number of shared nodes in an array of BDDs *}
3623 PROTO {* int bdd_anodecount(BDD *r, int num) *}
3624 DESCR {* Traverses all of the BDDs in {\tt r} and counts all distinct nodes
3625 that are used in the BDDs--if a node is used in more than one
3626 BDD then it only counts once. The {\tt num} parameter holds the
3627 size of the array. *}
3628 RETURN {* The number of nodes *}
3629 ALSO {* bdd\_nodecount *}
3630 */
bdd_anodecount(BDD * r,int num)3631 int bdd_anodecount(BDD *r, int num)
3632 {
3633 int n;
3634 int cou=0;
3635
3636 for (n=0 ; n<num ; n++)
3637 bdd_markcount(r[n], &cou);
3638
3639 for (n=0 ; n<num ; n++)
3640 bdd_unmark(r[n]);
3641
3642 return cou;
3643 }
3644
3645
3646 /*=== NODE PROFILE =====================================================*/
3647
3648 /*
3649 NAME {* bdd\_varprofile *}
3650 SECTION {* info *}
3651 SHORT {* returns a variable profile *}
3652 PROTO {* int *bdd_varprofile(BDD r) *}
3653 DESCR {* Counts the number of times each variable occurs in the
3654 bdd {\tt r}. The result is stored and returned in an integer array
3655 where the i'th position stores the number of times the i'th
3656 variable occured in the BDD. It is the users responsibility to
3657 free the array again using a call to {\tt free}. *}
3658 RETURN {* A pointer to an integer array with the profile or NULL if an
3659 error occured. *}
3660 */
bdd_varprofile(BDD r)3661 int *bdd_varprofile(BDD r)
3662 {
3663 CHECKa(r, NULL);
3664
3665 if (__unlikely((varprofile=(int*)malloc(sizeof(int)*bddvarnum)) == NULL))
3666 {
3667 bdd_error(BDD_MEMORY);
3668 return NULL;
3669 }
3670
3671 memset(varprofile, 0, sizeof(int)*bddvarnum);
3672 varprofile_rec(r);
3673 bdd_unmark(r);
3674 return varprofile;
3675 }
3676
3677
varprofile_rec(int r)3678 static void varprofile_rec(int r)
3679 {
3680 BddNode *node;
3681
3682 if (r < 2)
3683 return;
3684
3685 node = &bddnodes[r];
3686 if (LEVELp(node) & MARKON)
3687 return;
3688
3689 varprofile[bddlevel2var[LEVELp(node)]]++;
3690 LEVELp(node) |= MARKON;
3691
3692 varprofile_rec(LOWp(node));
3693 varprofile_rec(HIGHp(node));
3694 }
3695
3696
3697 /*=== COUNT NUMBER OF PATHS ============================================*/
3698
3699 /*
3700 NAME {* bdd\_pathcount *}
3701 SECTION {* info *}
3702 SHORT {* count the number of paths leading to the true terminal *}
3703 PROTO {* double bdd_pathcount(BDD r) *}
3704 DESCR {* Counts the number of paths from the root node {\tt r}
3705 leading to the terminal true node. *}
3706 RETURN {* The number of paths *}
3707 ALSO {* bdd\_nodecount, bdd\_satcount *}
3708 */
bdd_pathcount(BDD r)3709 double bdd_pathcount(BDD r)
3710 {
3711 CHECKa(r, 0.0);
3712
3713 miscid = CACHEID_PATHCOU;
3714
3715 return bdd_pathcount_rec(r);
3716 }
3717
3718
bdd_pathcount_rec(BDD r)3719 static double bdd_pathcount_rec(BDD r)
3720 {
3721 BddCacheData *entry;
3722 double size;
3723
3724 if (ISZERO(r))
3725 return 0.0;
3726 if (ISONE(r))
3727 return 1.0;
3728
3729 entry = BddCache_lookup(&misccache, PATHCOUHASH(r));
3730 if (entry->d.a == r && entry->d.c == miscid)
3731 return entry->d.res;
3732
3733 size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r));
3734
3735 entry->d.a = r;
3736 entry->d.c = miscid;
3737 entry->d.res = size;
3738
3739 return size;
3740 }
3741
bdd_have_common_assignment_(BDD left,BDD right)3742 static int bdd_have_common_assignment_(BDD left, BDD right)
3743 {
3744 #ifndef NDEBUG
3745 // arguments can't be constant
3746 if (ISCONST(left))
3747 return bdd_error(BDD_ILLBDD);
3748 if (ISCONST(right))
3749 return bdd_error(BDD_ILLBDD);
3750 #endif
3751
3752 // Always make "left" the smaller one to improve cache usage
3753 if (left > right)
3754 {
3755 BDD tmp = left;
3756 left = right;
3757 right = tmp;
3758 }
3759
3760 BddCacheData *entry = BddCache_lookup(&misccache, COMMONHASH(left,right));
3761 /* Check entry->b last, because not_rec() does not initialize it. */
3762 if (entry->i.a == left && entry->i.c == CACHEID_COMMON && entry->i.b == right)
3763 {
3764 #ifdef CACHESTATS
3765 bddcachestats.opHit++;
3766 #endif
3767 return entry->i.res;
3768 }
3769 #ifdef CACHESTATS
3770 bddcachestats.opMiss++;
3771 #endif
3772
3773 // Do they share the top variable?
3774 int vl = LEVEL(left);
3775 int vr = LEVEL(right);
3776
3777 // Try avoiding as many recursive calls as possible
3778 int res;
3779 if (vl < vr)
3780 {
3781 // left has to "catch up"
3782 // We know that right is not constant
3783 BDD l_left = LOW(left);
3784 BDD h_left = HIGH(left);
3785 res = ISONE(l_left) || (l_left == right)
3786 || ISONE(h_left) || (h_left == right)
3787 || (!ISZERO(l_left) && bdd_have_common_assignment_(l_left, right))
3788 || (!ISZERO(h_left) && bdd_have_common_assignment_(h_left, right));
3789 }
3790 else if (vr < vl)
3791 {
3792 // right has to "catch up"
3793 // We know that left is not constant
3794 BDD l_right = LOW(right);
3795 BDD h_right = HIGH(right);
3796 res = ISONE(l_right) || (l_right == left)
3797 || ISONE(h_right) || (h_right == left)
3798 || (!ISZERO(l_right) && bdd_have_common_assignment_(left,
3799 l_right))
3800 || (!ISZERO(h_right) && bdd_have_common_assignment_(left,
3801 h_right));
3802 }
3803 else
3804 {
3805 // They evolve jointly
3806 BDD l_left = LOW(left);
3807 BDD h_left = HIGH(left);
3808 BDD l_right = LOW(right);
3809 BDD h_right = HIGH(right);
3810
3811 res = ((!ISZERO(l_left) && !ISZERO(l_right))
3812 && (ISONE(l_left) || ISONE(l_right) || l_left == l_right
3813 || bdd_have_common_assignment_(l_left, l_right)))
3814 || ((!ISZERO(h_left) && !ISZERO(h_right))
3815 && (ISONE(h_left) || ISONE(h_right) || h_left == h_right
3816 || bdd_have_common_assignment_(h_left, h_right)));
3817 }
3818
3819 entry->i.a = left;
3820 entry->i.c = CACHEID_COMMON;
3821 entry->i.b = right;
3822 entry->i.res = res;
3823 return res;
3824 }
3825
3826 /*=== DECIDE IF TWO BDDS SHARE AT LEAST ONE ASSIGNMENT ================*/
3827
3828 /*
3829 NAME {* bdd\_have\_common\_assignment *}
3830 SECTION {* info *}
3831 SHORT {* Decide if two bdds share an satisfying assignement *}
3832 PROTO {* int bdd_have_common_assignment(BDD l, BDD r) *}
3833 DESCR {* Returns 1 iff l&r != bddfalse *}
3834 RETURN {* 0 or 1 *}
3835 */
bdd_have_common_assignment(BDD left,BDD right)3836 int bdd_have_common_assignment(BDD left, BDD right)
3837 {
3838 // If one of them is false -> false
3839 if (ISZERO(left) || ISZERO(right))
3840 return 0;
3841
3842 // If one of them is true and the other is not false
3843 // or if they are identical -> true
3844 if (ISONE(left) || ISONE(right) || left == right)
3845 return 1;
3846 // Now both of them are not constant
3847
3848 return bdd_have_common_assignment_(left, right);
3849 }
3850
3851 /*=== DECIDE IF A BDD is a cube ================*/
3852
3853 /*
3854 NAME {* bdd\_is\_cube *}
3855 SECTION {* info *}
3856 SHORT {* Decide if a bdd represents a cube *}
3857 PROTO {* int bdd_is_cube(BDD b) *}
3858 DESCR {* Returns 1 iff the given bdd is a conjunction of atomics and
3859 negations of atomics. Returns 0 if input is false, 1
3860 if input is true*}
3861 RETURN {* 0 or 1 *}
3862 */
bdd_is_cube(BDD b)3863 int bdd_is_cube(BDD b)
3864 {
3865 if (ISZERO(b))
3866 return 0;
3867
3868 while (!ISONE(b))
3869 {
3870 BDD l = LOW(b);
3871 BDD h = HIGH(b);
3872
3873 // Cube : high / low / do not care
3874 if (!ISZERO(l) && !ISZERO(h))
3875 return 0;
3876
3877 if (!ISZERO(l))
3878 b = l;
3879 else
3880 b = h;
3881 }
3882
3883 return 1;
3884 }
3885
3886 /*************************************************************************
3887 Other internal functions
3888 *************************************************************************/
3889
varset2vartable(BDD r,int comp)3890 static int varset2vartable(BDD r, int comp)
3891 {
3892 BDD n;
3893
3894 #ifndef NDEBUG
3895 if (r < 2 && !comp)
3896 return bdd_error(BDD_VARSET);
3897 #endif
3898
3899 quantvarsetID++;
3900 quantvarsetcomp = comp;
3901
3902 if (quantvarsetID == INT_MAX)
3903 {
3904 memset(quantvarset, 0, sizeof(int)*bddvarnum);
3905 quantvarsetID = 1;
3906 }
3907
3908 for (n=r ; n > 1 ; n=HIGH(n))
3909 {
3910 quantvarset[LEVEL(n)] = quantvarsetID;
3911 quantlast = LEVEL(n);
3912 }
3913
3914 /* When the varset is complemented, make sure all variables will
3915 be tested. */
3916 if (comp)
3917 quantlast = bddvarnum;
3918
3919 return 0;
3920 }
3921
3922
varset2svartable(BDD r)3923 static int varset2svartable(BDD r)
3924 {
3925 BDD n;
3926
3927 #ifndef NDEBUG
3928 if (r < 2)
3929 return bdd_error(BDD_VARSET);
3930 #endif
3931
3932 quantvarsetID++;
3933
3934 if (quantvarsetID == INT_MAX/2)
3935 {
3936 memset(quantvarset, 0, sizeof(int)*bddvarnum);
3937 quantvarsetID = 1;
3938 }
3939
3940 for (n=r ; !ISCONST(n) ; )
3941 {
3942 if (ISZERO(LOW(n)))
3943 {
3944 quantvarset[LEVEL(n)] = quantvarsetID;
3945 n = HIGH(n);
3946 }
3947 else
3948 {
3949 quantvarset[LEVEL(n)] = -quantvarsetID;
3950 n = LOW(n);
3951 }
3952 quantlast = LEVEL(n);
3953 }
3954
3955 return 0;
3956 }
3957
3958
3959 /* EOF */
3960