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