source: vis_dev/glu-2.3/src/cuBdd/cuddGenCof.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 56.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddGenCof.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Generalized cofactors for BDDs and ADDs.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_bddConstrain()
12                <li> Cudd_bddRestrict()
13                <li> Cudd_bddNPAnd()
14                <li> Cudd_addConstrain()
15                <li> Cudd_bddConstrainDecomp()
16                <li> Cudd_addRestrict()
17                <li> Cudd_bddCharToVect()
18                <li> Cudd_bddLICompaction()
19                <li> Cudd_bddSqueeze()
20                <li> Cudd_SubsetCompress()
21                <li> Cudd_SupersetCompress()
22                </ul>
23            Internal procedures included in this module:
24                <ul>
25                <li> cuddBddConstrainRecur()
26                <li> cuddBddRestrictRecur()
27                <li> cuddBddNPAndRecur()
28                <li> cuddAddConstrainRecur()
29                <li> cuddAddRestrictRecur()
30                <li> cuddBddLICompaction()
31                </ul>
32            Static procedures included in this module:
33                <ul>
34                <li> cuddBddConstrainDecomp()
35                <li> cuddBddCharToVect()
36                <li> cuddBddLICMarkEdges()
37                <li> cuddBddLICBuildResult()
38                <li> cuddBddSqueeze()
39                </ul>
40                ]
41
42  Author      [Fabio Somenzi]
43
44  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
45
46  All rights reserved.
47
48  Redistribution and use in source and binary forms, with or without
49  modification, are permitted provided that the following conditions
50  are met:
51
52  Redistributions of source code must retain the above copyright
53  notice, this list of conditions and the following disclaimer.
54
55  Redistributions in binary form must reproduce the above copyright
56  notice, this list of conditions and the following disclaimer in the
57  documentation and/or other materials provided with the distribution.
58
59  Neither the name of the University of Colorado nor the names of its
60  contributors may be used to endorse or promote products derived from
61  this software without specific prior written permission.
62
63  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
64  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
65  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
66  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
67  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
68  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
69  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
70  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
71  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
72  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
73  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
74  POSSIBILITY OF SUCH DAMAGE.]
75
76******************************************************************************/
77
78#include "util.h"
79#include "cuddInt.h"
80
81
82/*---------------------------------------------------------------------------*/
83/* Constant declarations                                                     */
84/*---------------------------------------------------------------------------*/
85
86/* Codes for edge markings in Cudd_bddLICompaction.  The codes are defined
87** so that they can be bitwise ORed to implement the code priority scheme.
88*/
89#define DD_LIC_DC 0
90#define DD_LIC_1  1
91#define DD_LIC_0  2
92#define DD_LIC_NL 3
93
94/*---------------------------------------------------------------------------*/
95/* Stucture declarations                                                     */
96/*---------------------------------------------------------------------------*/
97
98
99/*---------------------------------------------------------------------------*/
100/* Type declarations                                                         */
101/*---------------------------------------------------------------------------*/
102
103/* Key for the cache used in the edge marking phase. */
104typedef struct MarkCacheKey {
105    DdNode *f;
106    DdNode *c;
107} MarkCacheKey;
108
109/*---------------------------------------------------------------------------*/
110/* Variable declarations                                                     */
111/*---------------------------------------------------------------------------*/
112
113#ifndef lint
114static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.38 2005/05/14 17:27:11 fabio Exp $";
115#endif
116
117/*---------------------------------------------------------------------------*/
118/* Macro declarations                                                        */
119/*---------------------------------------------------------------------------*/
120
121#ifdef __cplusplus
122extern "C" {
123#endif
124
125/**AutomaticStart*************************************************************/
126
127/*---------------------------------------------------------------------------*/
128/* Static function prototypes                                                */
129/*---------------------------------------------------------------------------*/
130
131static int cuddBddConstrainDecomp (DdManager *dd, DdNode *f, DdNode **decomp);
132static DdNode * cuddBddCharToVect (DdManager *dd, DdNode *f, DdNode *x);
133static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache);
134static DdNode * cuddBddLICBuildResult (DdManager *dd, DdNode *f, st_table *cache, st_table *table);
135static int MarkCacheHash (char *ptr, int modulus);
136static int MarkCacheCompare (const char *ptr1, const char *ptr2);
137static enum st_retval MarkCacheCleanUp (char *key, char *value, char *arg);
138static DdNode * cuddBddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
139
140/**AutomaticEnd***************************************************************/
141
142#ifdef __cplusplus
143}
144#endif
145
146/*---------------------------------------------------------------------------*/
147/* Definition of exported functions                                          */
148/*---------------------------------------------------------------------------*/
149
150
151/**Function********************************************************************
152
153  Synopsis    [Computes f constrain c.]
154
155  Description [Computes f constrain c (f @ c).
156  Uses a canonical form: (f' @ c) = ( f @ c)'.  (Note: this is not true
157  for c.)  List of special cases:
158    <ul>
159    <li> f @ 0 = 0
160    <li> f @ 1 = f
161    <li> 0 @ c = 0
162    <li> 1 @ c = 1
163    <li> f @ f = 1
164    <li> f @ f'= 0
165    </ul>
166  Returns a pointer to the result if successful; NULL otherwise. Note that if
167  F=(f1,...,fn) and reordering takes place while computing F @ c, then the
168  image restriction property (Img(F,c) = Img(F @ c)) is lost.]
169
170  SideEffects [None]
171
172  SeeAlso     [Cudd_bddRestrict Cudd_addConstrain]
173
174******************************************************************************/
175DdNode *
176Cudd_bddConstrain(
177  DdManager * dd,
178  DdNode * f,
179  DdNode * c)
180{
181    DdNode *res;
182
183    do {
184        dd->reordered = 0;
185        res = cuddBddConstrainRecur(dd,f,c);
186    } while (dd->reordered == 1);
187    return(res);
188
189} /* end of Cudd_bddConstrain */
190
191
192/**Function********************************************************************
193
194  Synopsis [BDD restrict according to Coudert and Madre's algorithm
195  (ICCAD90).]
196
197  Description [BDD restrict according to Coudert and Madre's algorithm
198  (ICCAD90). Returns the restricted BDD if successful; otherwise NULL.
199  If application of restrict results in a BDD larger than the input
200  BDD, the input BDD is returned.]
201
202  SideEffects [None]
203
204  SeeAlso     [Cudd_bddConstrain Cudd_addRestrict]
205
206******************************************************************************/
207DdNode *
208Cudd_bddRestrict(
209  DdManager * dd,
210  DdNode * f,
211  DdNode * c)
212{
213    DdNode *suppF, *suppC, *commonSupport;
214    DdNode *cplus, *res;
215    int retval;
216    int sizeF, sizeRes;
217
218    /* Check terminal cases here to avoid computing supports in trivial cases.
219    ** This also allows us notto check later for the case c == 0, in which
220    ** there is no common support. */
221    if (c == Cudd_Not(DD_ONE(dd))) return(Cudd_Not(DD_ONE(dd)));
222    if (Cudd_IsConstant(f)) return(f);
223    if (f == c) return(DD_ONE(dd));
224    if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
225
226    /* Check if supports intersect. */
227    retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC);
228    if (retval == 0) {
229        return(NULL);
230    }
231    cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC);
232    Cudd_IterDerefBdd(dd,suppF);
233
234    if (commonSupport == DD_ONE(dd)) {
235        Cudd_IterDerefBdd(dd,commonSupport);
236        Cudd_IterDerefBdd(dd,suppC);
237        return(f);
238    }
239    Cudd_IterDerefBdd(dd,commonSupport);
240
241    /* Abstract from c the variables that do not appear in f. */
242    cplus = Cudd_bddExistAbstract(dd, c, suppC);
243    if (cplus == NULL) {
244        Cudd_IterDerefBdd(dd,suppC);
245        return(NULL);
246    }
247    cuddRef(cplus);
248    Cudd_IterDerefBdd(dd,suppC);
249
250    do {
251        dd->reordered = 0;
252        res = cuddBddRestrictRecur(dd, f, cplus);
253    } while (dd->reordered == 1);
254    if (res == NULL) {
255        Cudd_IterDerefBdd(dd,cplus);
256        return(NULL);
257    }
258    cuddRef(res);
259    Cudd_IterDerefBdd(dd,cplus);
260    /* Make restric safe by returning the smaller of the input and the
261    ** result. */
262    sizeF = Cudd_DagSize(f);
263    sizeRes = Cudd_DagSize(res);
264    if (sizeF <= sizeRes) {
265        Cudd_IterDerefBdd(dd, res);
266        return(f);
267    } else {
268        cuddDeref(res);
269        return(res);
270    }
271
272} /* end of Cudd_bddRestrict */
273
274
275/**Function********************************************************************
276
277  Synopsis    [Computes f non-polluting-and g.]
278
279  Description [Computes f non-polluting-and g.  The non-polluting AND
280  of f and g is a hybrid of AND and Restrict.  From Restrict, this
281  operation takes the idea of existentially quantifying the top
282  variable of the second operand if it does not appear in the first.
283  Therefore, the variables that appear in the result also appear in f.
284  For the rest, the function behaves like AND.  Since the two operands
285  play different roles, non-polluting AND is not commutative.
286
287  Returns a pointer to the result if successful; NULL otherwise.]
288
289  SideEffects [None]
290
291  SeeAlso     [Cudd_bddConstrain Cudd_bddRestrict]
292
293******************************************************************************/
294DdNode *
295Cudd_bddNPAnd(
296  DdManager * dd,
297  DdNode * f,
298  DdNode * g)
299{
300    DdNode *res;
301
302    do {
303        dd->reordered = 0;
304        res = cuddBddNPAndRecur(dd,f,g);
305    } while (dd->reordered == 1);
306    return(res);
307
308} /* end of Cudd_bddNPAnd */
309
310
311/**Function********************************************************************
312
313  Synopsis    [Computes f constrain c for ADDs.]
314
315  Description [Computes f constrain c (f @ c), for f an ADD and c a 0-1
316  ADD.  List of special cases:
317    <ul>
318    <li> F @ 0 = 0
319    <li> F @ 1 = F
320    <li> 0 @ c = 0
321    <li> 1 @ c = 1
322    <li> F @ F = 1
323    </ul>
324  Returns a pointer to the result if successful; NULL otherwise.]
325
326  SideEffects [None]
327
328  SeeAlso     [Cudd_bddConstrain]
329
330******************************************************************************/
331DdNode *
332Cudd_addConstrain(
333  DdManager * dd,
334  DdNode * f,
335  DdNode * c)
336{
337    DdNode *res;
338
339    do {
340        dd->reordered = 0;
341        res = cuddAddConstrainRecur(dd,f,c);
342    } while (dd->reordered == 1);
343    return(res);
344
345} /* end of Cudd_addConstrain */
346
347
348/**Function********************************************************************
349
350  Synopsis [BDD conjunctive decomposition as in McMillan's CAV96 paper.]
351
352  Description [BDD conjunctive decomposition as in McMillan's CAV96
353  paper.  The decomposition is canonical only for a given variable
354  order. If canonicity is required, variable ordering must be disabled
355  after the decomposition has been computed. Returns an array with one
356  entry for each BDD variable in the manager if successful; otherwise
357  NULL. The components of the solution have their reference counts
358  already incremented (unlike the results of most other functions in
359  the package.]
360
361  SideEffects [None]
362
363  SeeAlso     [Cudd_bddConstrain Cudd_bddExistAbstract]
364
365******************************************************************************/
366DdNode **
367Cudd_bddConstrainDecomp(
368  DdManager * dd,
369  DdNode * f)
370{
371    DdNode **decomp;
372    int res;
373    int i;
374
375    /* Create an initialize decomposition array. */
376    decomp = ALLOC(DdNode *,dd->size);
377    if (decomp == NULL) {
378        dd->errorCode = CUDD_MEMORY_OUT;
379        return(NULL);
380    }
381    for (i = 0; i < dd->size; i++) {
382        decomp[i] = NULL;
383    }
384    do {
385        dd->reordered = 0;
386        /* Clean up the decomposition array in case reordering took place. */
387        for (i = 0; i < dd->size; i++) {
388            if (decomp[i] != NULL) {
389                Cudd_IterDerefBdd(dd, decomp[i]);
390                decomp[i] = NULL;
391            }
392        }
393        res = cuddBddConstrainDecomp(dd,f,decomp);
394    } while (dd->reordered == 1);
395    if (res == 0) {
396        FREE(decomp);
397        return(NULL);
398    }
399    /* Missing components are constant ones. */
400    for (i = 0; i < dd->size; i++) {
401        if (decomp[i] == NULL) {
402            decomp[i] = DD_ONE(dd);
403            cuddRef(decomp[i]);
404        }
405    }
406    return(decomp);
407
408} /* end of Cudd_bddConstrainDecomp */
409
410
411/**Function********************************************************************
412
413  Synopsis [ADD restrict according to Coudert and Madre's algorithm
414  (ICCAD90).]
415
416  Description [ADD restrict according to Coudert and Madre's algorithm
417  (ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
418  If application of restrict results in an ADD larger than the input
419  ADD, the input ADD is returned.]
420
421  SideEffects [None]
422
423  SeeAlso     [Cudd_addConstrain Cudd_bddRestrict]
424
425******************************************************************************/
426DdNode *
427Cudd_addRestrict(
428  DdManager * dd,
429  DdNode * f,
430  DdNode * c)
431{
432    DdNode *supp_f, *supp_c;
433    DdNode *res, *commonSupport;
434    int intersection;
435    int sizeF, sizeRes;
436
437    /* Check if supports intersect. */
438    supp_f = Cudd_Support(dd, f);
439    if (supp_f == NULL) {
440        return(NULL);
441    }
442    cuddRef(supp_f);
443    supp_c = Cudd_Support(dd, c);
444    if (supp_c == NULL) {
445        Cudd_RecursiveDeref(dd,supp_f);
446        return(NULL);
447    }
448    cuddRef(supp_c);
449    commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
450    if (commonSupport == NULL) {
451        Cudd_RecursiveDeref(dd,supp_f);
452        Cudd_RecursiveDeref(dd,supp_c);
453        return(NULL);
454    }
455    cuddRef(commonSupport);
456    Cudd_RecursiveDeref(dd,supp_f);
457    Cudd_RecursiveDeref(dd,supp_c);
458    intersection = commonSupport != DD_ONE(dd);
459    Cudd_RecursiveDeref(dd,commonSupport);
460
461    if (intersection) {
462        do {
463            dd->reordered = 0;
464            res = cuddAddRestrictRecur(dd, f, c);
465        } while (dd->reordered == 1);
466        sizeF = Cudd_DagSize(f);
467        sizeRes = Cudd_DagSize(res);
468        if (sizeF <= sizeRes) {
469            cuddRef(res);
470            Cudd_RecursiveDeref(dd, res);
471            return(f);
472        } else {
473            return(res);
474        }
475    } else {
476        return(f);
477    }
478
479} /* end of Cudd_addRestrict */
480
481
482/**Function********************************************************************
483
484  Synopsis    [Computes a vector whose image equals a non-zero function.]
485
486  Description [Computes a vector of BDDs whose image equals a non-zero
487  function.
488  The result depends on the variable order. The i-th component of the vector
489  depends only on the first i variables in the order.  Each BDD in the vector
490  is not larger than the BDD of the given characteristic function.  This
491  function is based on the description of char-to-vect in "Verification of
492  Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C.
493  Berthet and J. C. Madre.
494  Returns a pointer to an array containing the result if successful; NULL
495  otherwise. The size of the array equals the number of variables in the
496  manager. The components of the solution have their reference counts
497  already incremented (unlike the results of most other functions in
498  the package).]
499
500  SideEffects [None]
501
502  SeeAlso     [Cudd_bddConstrain]
503
504******************************************************************************/
505DdNode **
506Cudd_bddCharToVect(
507  DdManager * dd,
508  DdNode * f)
509{
510    int i, j;
511    DdNode **vect;
512    DdNode *res = NULL;
513
514    if (f == Cudd_Not(DD_ONE(dd))) return(NULL);
515
516    vect = ALLOC(DdNode *, dd->size);
517    if (vect == NULL) {
518        dd->errorCode = CUDD_MEMORY_OUT;
519        return(NULL);
520    }
521
522    do {
523        dd->reordered = 0;
524        for (i = 0; i < dd->size; i++) {
525            res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]);
526            if (res == NULL) {
527                /* Clean up the vector array in case reordering took place. */
528                for (j = 0; j < i; j++) {
529                    Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]);
530                }
531                break;
532            }
533            cuddRef(res);
534            vect[dd->invperm[i]] = res;
535        }
536    } while (dd->reordered == 1);
537    if (res == NULL) {
538        FREE(vect);
539        return(NULL);
540    }
541    return(vect);
542
543} /* end of Cudd_bddCharToVect */
544
545
546/**Function********************************************************************
547
548  Synopsis    [Performs safe minimization of a BDD.]
549
550  Description [Performs safe minimization of a BDD. Given the BDD
551  <code>f</code> of a function to be minimized and a BDD
552  <code>c</code> representing the care set, Cudd_bddLICompaction
553  produces the BDD of a function that agrees with <code>f</code>
554  wherever <code>c</code> is 1.  Safe minimization means that the size
555  of the result is guaranteed not to exceed the size of
556  <code>f</code>. This function is based on the DAC97 paper by Hong et
557  al..  Returns a pointer to the result if successful; NULL
558  otherwise.]
559
560  SideEffects [None]
561
562  SeeAlso     [Cudd_bddRestrict]
563
564******************************************************************************/
565DdNode *
566Cudd_bddLICompaction(
567  DdManager * dd /* manager */,
568  DdNode * f /* function to be minimized */,
569  DdNode * c /* constraint (care set) */)
570{
571    DdNode *res;
572
573    do {
574        dd->reordered = 0;
575        res = cuddBddLICompaction(dd,f,c);
576    } while (dd->reordered == 1);
577    return(res);
578
579} /* end of Cudd_bddLICompaction */
580
581
582/**Function********************************************************************
583
584  Synopsis    [Finds a small BDD in a function interval.]
585
586  Description [Finds a small BDD in a function interval. Given BDDs
587  <code>l</code> and <code>u</code>, representing the lower bound and
588  upper bound of a function interval, Cudd_bddSqueeze produces the BDD
589  of a function within the interval with a small BDD.  Returns a
590  pointer to the result if successful; NULL otherwise.]
591
592  SideEffects [None]
593
594  SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction]
595
596******************************************************************************/
597DdNode *
598Cudd_bddSqueeze(
599  DdManager * dd /* manager */,
600  DdNode * l /* lower bound */,
601  DdNode * u /* upper bound */)
602{
603    DdNode *res;
604    int sizeRes, sizeL, sizeU;
605
606    do {
607        dd->reordered = 0;
608        res = cuddBddSqueeze(dd,l,u);
609    } while (dd->reordered == 1);
610    if (res == NULL) return(NULL);
611    /* We now compare the result with the bounds and return the smallest.
612    ** We first compare to u, so that in case l == 0 and u == 1, we return
613    ** 0 as in other minimization algorithms. */
614    sizeRes = Cudd_DagSize(res);
615    sizeU = Cudd_DagSize(u);
616    if (sizeU <= sizeRes) {
617        cuddRef(res);
618        Cudd_IterDerefBdd(dd,res);
619        res = u;
620        sizeRes = sizeU;
621    }
622    sizeL = Cudd_DagSize(l);
623    if (sizeL <= sizeRes) {
624        cuddRef(res);
625        Cudd_IterDerefBdd(dd,res);
626        res = l;
627        sizeRes = sizeL;
628    }
629    return(res);
630
631} /* end of Cudd_bddSqueeze */
632
633
634/**Function********************************************************************
635
636  Synopsis    [Finds a small BDD that agrees with <code>f</code> over
637  <code>c</code>.]
638
639  Description [Finds a small BDD that agrees with <code>f</code> over
640  <code>c</code>.  Returns a pointer to the result if successful; NULL
641  otherwise.]
642
643  SideEffects [None]
644
645  SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction Cudd_bddSqueeze]
646
647******************************************************************************/
648DdNode *
649Cudd_bddMinimize(
650  DdManager * dd,
651  DdNode * f,
652  DdNode * c)
653{
654    DdNode *cplus, *res;
655
656    if (c == Cudd_Not(DD_ONE(dd))) return(c);
657    if (Cudd_IsConstant(f)) return(f);
658    if (f == c) return(DD_ONE(dd));
659    if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
660
661    cplus = Cudd_RemapOverApprox(dd,c,0,0,1.0);
662    if (cplus == NULL) return(NULL);
663    cuddRef(cplus);
664    res = Cudd_bddLICompaction(dd,f,cplus);
665    if (res == NULL) {
666        Cudd_IterDerefBdd(dd,cplus);
667        return(NULL);
668    }
669    cuddRef(res);
670    Cudd_IterDerefBdd(dd,cplus);
671    cuddDeref(res);
672    return(res);
673
674} /* end of Cudd_bddMinimize */
675
676
677/**Function********************************************************************
678
679  Synopsis    [Find a dense subset of BDD <code>f</code>.]
680
681  Description [Finds a dense subset of BDD <code>f</code>. Density is
682  the ratio of number of minterms to number of nodes.  Uses several
683  techniques in series. It is more expensive than other subsetting
684  procedures, but often produces better results. See
685  Cudd_SubsetShortPaths for a description of the threshold and nvars
686  parameters.  Returns a pointer to the result if successful; NULL
687  otherwise.]
688
689  SideEffects [None]
690
691  SeeAlso     [Cudd_SubsetRemap Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch
692  Cudd_bddSqueeze]
693
694******************************************************************************/
695DdNode *
696Cudd_SubsetCompress(
697  DdManager * dd /* manager */,
698  DdNode * f /* BDD whose subset is sought */,
699  int  nvars /* number of variables in the support of f */,
700  int  threshold /* maximum number of nodes in the subset */)
701{
702    DdNode *res, *tmp1, *tmp2;
703
704    tmp1 = Cudd_SubsetShortPaths(dd, f, nvars, threshold, 0);
705    if (tmp1 == NULL) return(NULL);
706    cuddRef(tmp1);
707    tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0);
708    if (tmp2 == NULL) {
709        Cudd_IterDerefBdd(dd,tmp1);
710        return(NULL);
711    }
712    cuddRef(tmp2);
713    Cudd_IterDerefBdd(dd,tmp1);
714    res = Cudd_bddSqueeze(dd,tmp2,f);
715    if (res == NULL) {
716        Cudd_IterDerefBdd(dd,tmp2);
717        return(NULL);
718    }
719    cuddRef(res);
720    Cudd_IterDerefBdd(dd,tmp2);
721    cuddDeref(res);
722    return(res);
723
724} /* end of Cudd_SubsetCompress */
725
726
727/**Function********************************************************************
728
729  Synopsis    [Find a dense superset of BDD <code>f</code>.]
730
731  Description [Finds a dense superset of BDD <code>f</code>. Density is
732  the ratio of number of minterms to number of nodes.  Uses several
733  techniques in series. It is more expensive than other supersetting
734  procedures, but often produces better results. See
735  Cudd_SupersetShortPaths for a description of the threshold and nvars
736  parameters.  Returns a pointer to the result if successful; NULL
737  otherwise.]
738
739  SideEffects [None]
740
741  SeeAlso     [Cudd_SubsetCompress Cudd_SupersetRemap Cudd_SupersetShortPaths
742  Cudd_SupersetHeavyBranch Cudd_bddSqueeze]
743
744******************************************************************************/
745DdNode *
746Cudd_SupersetCompress(
747  DdManager * dd /* manager */,
748  DdNode * f /* BDD whose superset is sought */,
749  int  nvars /* number of variables in the support of f */,
750  int  threshold /* maximum number of nodes in the superset */)
751{
752    DdNode *subset;
753
754    subset = Cudd_SubsetCompress(dd, Cudd_Not(f),nvars,threshold);
755
756    return(Cudd_NotCond(subset, (subset != NULL)));
757
758} /* end of Cudd_SupersetCompress */
759
760
761/*---------------------------------------------------------------------------*/
762/* Definition of internal functions                                          */
763/*---------------------------------------------------------------------------*/
764
765
766/**Function********************************************************************
767
768  Synopsis    [Performs the recursive step of Cudd_bddConstrain.]
769
770  Description [Performs the recursive step of Cudd_bddConstrain.
771  Returns a pointer to the result if successful; NULL otherwise.]
772
773  SideEffects [None]
774
775  SeeAlso     [Cudd_bddConstrain]
776
777******************************************************************************/
778DdNode *
779cuddBddConstrainRecur(
780  DdManager * dd,
781  DdNode * f,
782  DdNode * c)
783{
784    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
785    DdNode       *one, *zero;
786    unsigned int topf, topc;
787    int          index;
788    int          comple = 0;
789
790    statLine(dd);
791    one = DD_ONE(dd);
792    zero = Cudd_Not(one);
793
794    /* Trivial cases. */
795    if (c == one)               return(f);
796    if (c == zero)              return(zero);
797    if (Cudd_IsConstant(f))     return(f);
798    if (f == c)                 return(one);
799    if (f == Cudd_Not(c))       return(zero);
800
801    /* Make canonical to increase the utilization of the cache. */
802    if (Cudd_IsComplement(f)) {
803        f = Cudd_Not(f);
804        comple = 1;
805    }
806    /* Now f is a regular pointer to a non-constant node; c is also
807    ** non-constant, but may be complemented.
808    */
809
810    /* Check the cache. */
811    r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c);
812    if (r != NULL) {
813        return(Cudd_NotCond(r,comple));
814    }
815   
816    /* Recursive step. */
817    topf = dd->perm[f->index];
818    topc = dd->perm[Cudd_Regular(c)->index];
819    if (topf <= topc) {
820        index = f->index;
821        Fv = cuddT(f); Fnv = cuddE(f);
822    } else {
823        index = Cudd_Regular(c)->index;
824        Fv = Fnv = f;
825    }
826    if (topc <= topf) {
827        Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
828        if (Cudd_IsComplement(c)) {
829            Cv = Cudd_Not(Cv);
830            Cnv = Cudd_Not(Cnv);
831        }
832    } else {
833        Cv = Cnv = c;
834    }
835
836    if (!Cudd_IsConstant(Cv)) {
837        t = cuddBddConstrainRecur(dd, Fv, Cv);
838        if (t == NULL)
839            return(NULL);
840    } else if (Cv == one) {
841        t = Fv;
842    } else {            /* Cv == zero: return Fnv @ Cnv */
843        if (Cnv == one) {
844            r = Fnv;
845        } else {
846            r = cuddBddConstrainRecur(dd, Fnv, Cnv);
847            if (r == NULL)
848                return(NULL);
849        }
850        return(Cudd_NotCond(r,comple));
851    }
852    cuddRef(t);
853
854    if (!Cudd_IsConstant(Cnv)) {
855        e = cuddBddConstrainRecur(dd, Fnv, Cnv);
856        if (e == NULL) {
857            Cudd_IterDerefBdd(dd, t);
858            return(NULL);
859        }
860    } else if (Cnv == one) {
861        e = Fnv;
862    } else {            /* Cnv == zero: return Fv @ Cv previously computed */
863        cuddDeref(t);
864        return(Cudd_NotCond(t,comple));
865    }
866    cuddRef(e);
867
868    if (Cudd_IsComplement(t)) {
869        t = Cudd_Not(t);
870        e = Cudd_Not(e);
871        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
872        if (r == NULL) {
873            Cudd_IterDerefBdd(dd, e);
874            Cudd_IterDerefBdd(dd, t);
875            return(NULL);
876        }
877        r = Cudd_Not(r);
878    } else {
879        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
880        if (r == NULL) {
881            Cudd_IterDerefBdd(dd, e);
882            Cudd_IterDerefBdd(dd, t);
883            return(NULL);
884        }
885    }
886    cuddDeref(t);
887    cuddDeref(e);
888
889    cuddCacheInsert2(dd, Cudd_bddConstrain, f, c, r);
890    return(Cudd_NotCond(r,comple));
891
892} /* end of cuddBddConstrainRecur */
893
894
895/**Function********************************************************************
896
897  Synopsis    [Performs the recursive step of Cudd_bddRestrict.]
898
899  Description [Performs the recursive step of Cudd_bddRestrict.
900  Returns the restricted BDD if successful; otherwise NULL.]
901
902  SideEffects [None]
903
904  SeeAlso     [Cudd_bddRestrict]
905
906******************************************************************************/
907DdNode *
908cuddBddRestrictRecur(
909  DdManager * dd,
910  DdNode * f,
911  DdNode * c)
912{
913    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
914    unsigned int topf, topc;
915    int          index;
916    int          comple = 0;
917
918    statLine(dd);
919    one = DD_ONE(dd);
920    zero = Cudd_Not(one);
921
922    /* Trivial cases */
923    if (c == one)               return(f);
924    if (c == zero)              return(zero);
925    if (Cudd_IsConstant(f))     return(f);
926    if (f == c)                 return(one);
927    if (f == Cudd_Not(c))       return(zero);
928
929    /* Make canonical to increase the utilization of the cache. */
930    if (Cudd_IsComplement(f)) {
931        f = Cudd_Not(f);
932        comple = 1;
933    }
934    /* Now f is a regular pointer to a non-constant node; c is also
935    ** non-constant, but may be complemented.
936    */
937
938    /* Check the cache. */
939    r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c);
940    if (r != NULL) {
941        return(Cudd_NotCond(r,comple));
942    }
943
944    topf = dd->perm[f->index];
945    topc = dd->perm[Cudd_Regular(c)->index];
946
947    if (topc < topf) {  /* abstract top variable from c */
948        DdNode *d, *s1, *s2;
949
950        /* Find complements of cofactors of c. */
951        if (Cudd_IsComplement(c)) {
952            s1 = cuddT(Cudd_Regular(c));
953            s2 = cuddE(Cudd_Regular(c));
954        } else {
955            s1 = Cudd_Not(cuddT(c));
956            s2 = Cudd_Not(cuddE(c));
957        }
958        /* Take the OR by applying DeMorgan. */
959        d = cuddBddAndRecur(dd, s1, s2);
960        if (d == NULL) return(NULL);
961        d = Cudd_Not(d);
962        cuddRef(d);
963        r = cuddBddRestrictRecur(dd, f, d);
964        if (r == NULL) {
965            Cudd_IterDerefBdd(dd, d);
966            return(NULL);
967        }
968        cuddRef(r);
969        Cudd_IterDerefBdd(dd, d);
970        cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
971        cuddDeref(r);
972        return(Cudd_NotCond(r,comple));
973    }
974
975    /* Recursive step. Here topf <= topc. */
976    index = f->index;
977    Fv = cuddT(f); Fnv = cuddE(f);
978    if (topc == topf) {
979        Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
980        if (Cudd_IsComplement(c)) {
981            Cv = Cudd_Not(Cv);
982            Cnv = Cudd_Not(Cnv);
983        }
984    } else {
985        Cv = Cnv = c;
986    }
987
988    if (!Cudd_IsConstant(Cv)) {
989        t = cuddBddRestrictRecur(dd, Fv, Cv);
990        if (t == NULL) return(NULL);
991    } else if (Cv == one) {
992        t = Fv;
993    } else {            /* Cv == zero: return(Fnv @ Cnv) */
994        if (Cnv == one) {
995            r = Fnv;
996        } else {
997            r = cuddBddRestrictRecur(dd, Fnv, Cnv);
998            if (r == NULL) return(NULL);
999        }
1000        return(Cudd_NotCond(r,comple));
1001    }
1002    cuddRef(t);
1003
1004    if (!Cudd_IsConstant(Cnv)) {
1005        e = cuddBddRestrictRecur(dd, Fnv, Cnv);
1006        if (e == NULL) {
1007            Cudd_IterDerefBdd(dd, t);
1008            return(NULL);
1009        }
1010    } else if (Cnv == one) {
1011        e = Fnv;
1012    } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
1013        cuddDeref(t);
1014        return(Cudd_NotCond(t,comple));
1015    }
1016    cuddRef(e);
1017
1018    if (Cudd_IsComplement(t)) {
1019        t = Cudd_Not(t);
1020        e = Cudd_Not(e);
1021        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1022        if (r == NULL) {
1023            Cudd_IterDerefBdd(dd, e);
1024            Cudd_IterDerefBdd(dd, t);
1025            return(NULL);
1026        }
1027        r = Cudd_Not(r);
1028    } else {
1029        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1030        if (r == NULL) {
1031            Cudd_IterDerefBdd(dd, e);
1032            Cudd_IterDerefBdd(dd, t);
1033            return(NULL);
1034        }
1035    }
1036    cuddDeref(t);
1037    cuddDeref(e);
1038
1039    cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
1040    return(Cudd_NotCond(r,comple));
1041
1042} /* end of cuddBddRestrictRecur */
1043
1044
1045/**Function********************************************************************
1046
1047  Synopsis [Implements the recursive step of Cudd_bddAnd.]
1048
1049  Description [Implements the recursive step of Cudd_bddNPAnd.
1050  Returns a pointer to the result is successful; NULL otherwise.]
1051
1052  SideEffects [None]
1053
1054  SeeAlso     [Cudd_bddNPAnd]
1055
1056******************************************************************************/
1057DdNode *
1058cuddBddNPAndRecur(
1059  DdManager * manager,
1060  DdNode * f,
1061  DdNode * g)
1062{
1063    DdNode *F, *ft, *fe, *G, *gt, *ge;
1064    DdNode *one, *r, *t, *e;
1065    unsigned int topf, topg, index;
1066
1067    statLine(manager);
1068    one = DD_ONE(manager);
1069
1070    /* Terminal cases. */
1071    F = Cudd_Regular(f);
1072    G = Cudd_Regular(g);
1073    if (F == G) {
1074        if (f == g) return(one);
1075        else return(Cudd_Not(one));
1076    }
1077    if (G == one) {
1078        if (g == one) return(f);
1079        else return(g);
1080    }
1081    if (F == one) {
1082        return(f);
1083    }
1084
1085    /* At this point f and g are not constant. */
1086    /* Check cache. */
1087    if (F->ref != 1 || G->ref != 1) {
1088        r = cuddCacheLookup2(manager, Cudd_bddNPAnd, f, g);
1089        if (r != NULL) return(r);
1090    }
1091
1092    /* Here we can skip the use of cuddI, because the operands are known
1093    ** to be non-constant.
1094    */
1095    topf = manager->perm[F->index];
1096    topg = manager->perm[G->index];
1097
1098    if (topg < topf) {  /* abstract top variable from g */
1099        DdNode *d;
1100
1101        /* Find complements of cofactors of g. */
1102        if (Cudd_IsComplement(g)) {
1103            gt = cuddT(G);
1104            ge = cuddE(G);
1105        } else {
1106            gt = Cudd_Not(cuddT(g));
1107            ge = Cudd_Not(cuddE(g));
1108        }
1109        /* Take the OR by applying DeMorgan. */
1110        d = cuddBddAndRecur(manager, gt, ge);
1111        if (d == NULL) return(NULL);
1112        d = Cudd_Not(d);
1113        cuddRef(d);
1114        r = cuddBddNPAndRecur(manager, f, d);
1115        if (r == NULL) {
1116            Cudd_IterDerefBdd(manager, d);
1117            return(NULL);
1118        }
1119        cuddRef(r);
1120        Cudd_IterDerefBdd(manager, d);
1121        cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r);
1122        cuddDeref(r);
1123        return(r);
1124    }
1125
1126    /* Compute cofactors. */
1127    index = F->index;
1128    ft = cuddT(F);
1129    fe = cuddE(F);
1130    if (Cudd_IsComplement(f)) {
1131      ft = Cudd_Not(ft);
1132      fe = Cudd_Not(fe);
1133    }
1134
1135    if (topg == topf) {
1136        gt = cuddT(G);
1137        ge = cuddE(G);
1138        if (Cudd_IsComplement(g)) {
1139            gt = Cudd_Not(gt);
1140            ge = Cudd_Not(ge);
1141        }
1142    } else {
1143        gt = ge = g;
1144    }
1145
1146    t = cuddBddAndRecur(manager, ft, gt);
1147    if (t == NULL) return(NULL);
1148    cuddRef(t);
1149
1150    e = cuddBddAndRecur(manager, fe, ge);
1151    if (e == NULL) {
1152        Cudd_IterDerefBdd(manager, t);
1153        return(NULL);
1154    }
1155    cuddRef(e);
1156
1157    if (t == e) {
1158        r = t;
1159    } else {
1160        if (Cudd_IsComplement(t)) {
1161            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
1162            if (r == NULL) {
1163                Cudd_IterDerefBdd(manager, t);
1164                Cudd_IterDerefBdd(manager, e);
1165                return(NULL);
1166            }
1167            r = Cudd_Not(r);
1168        } else {
1169            r = cuddUniqueInter(manager,(int)index,t,e);
1170            if (r == NULL) {
1171                Cudd_IterDerefBdd(manager, t);
1172                Cudd_IterDerefBdd(manager, e);
1173                return(NULL);
1174            }
1175        }
1176    }
1177    cuddDeref(e);
1178    cuddDeref(t);
1179    if (F->ref != 1 || G->ref != 1)
1180        cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r);
1181    return(r);
1182
1183} /* end of cuddBddNPAndRecur */
1184
1185
1186/**Function********************************************************************
1187
1188  Synopsis    [Performs the recursive step of Cudd_addConstrain.]
1189
1190  Description [Performs the recursive step of Cudd_addConstrain.
1191  Returns a pointer to the result if successful; NULL otherwise.]
1192
1193  SideEffects [None]
1194
1195  SeeAlso     [Cudd_addConstrain]
1196
1197******************************************************************************/
1198DdNode *
1199cuddAddConstrainRecur(
1200  DdManager * dd,
1201  DdNode * f,
1202  DdNode * c)
1203{
1204    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
1205    DdNode       *one, *zero;
1206    unsigned int topf, topc;
1207    int          index;
1208
1209    statLine(dd);
1210    one = DD_ONE(dd);
1211    zero = DD_ZERO(dd);
1212
1213    /* Trivial cases. */
1214    if (c == one)               return(f);
1215    if (c == zero)              return(zero);
1216    if (Cudd_IsConstant(f))     return(f);
1217    if (f == c)                 return(one);
1218
1219    /* Now f and c are non-constant. */
1220
1221    /* Check the cache. */
1222    r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c);
1223    if (r != NULL) {
1224        return(r);
1225    }
1226   
1227    /* Recursive step. */
1228    topf = dd->perm[f->index];
1229    topc = dd->perm[c->index];
1230    if (topf <= topc) {
1231        index = f->index;
1232        Fv = cuddT(f); Fnv = cuddE(f);
1233    } else {
1234        index = c->index;
1235        Fv = Fnv = f;
1236    }
1237    if (topc <= topf) {
1238        Cv = cuddT(c); Cnv = cuddE(c);
1239    } else {
1240        Cv = Cnv = c;
1241    }
1242
1243    if (!Cudd_IsConstant(Cv)) {
1244        t = cuddAddConstrainRecur(dd, Fv, Cv);
1245        if (t == NULL)
1246            return(NULL);
1247    } else if (Cv == one) {
1248        t = Fv;
1249    } else {            /* Cv == zero: return Fnv @ Cnv */
1250        if (Cnv == one) {
1251            r = Fnv;
1252        } else {
1253            r = cuddAddConstrainRecur(dd, Fnv, Cnv);
1254            if (r == NULL)
1255                return(NULL);
1256        }
1257        return(r);
1258    }
1259    cuddRef(t);
1260
1261    if (!Cudd_IsConstant(Cnv)) {
1262        e = cuddAddConstrainRecur(dd, Fnv, Cnv);
1263        if (e == NULL) {
1264            Cudd_RecursiveDeref(dd, t);
1265            return(NULL);
1266        }
1267    } else if (Cnv == one) {
1268        e = Fnv;
1269    } else {            /* Cnv == zero: return Fv @ Cv previously computed */
1270        cuddDeref(t);
1271        return(t);
1272    }
1273    cuddRef(e);
1274
1275    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1276    if (r == NULL) {
1277        Cudd_RecursiveDeref(dd, e);
1278        Cudd_RecursiveDeref(dd, t);
1279        return(NULL);
1280    }
1281    cuddDeref(t);
1282    cuddDeref(e);
1283
1284    cuddCacheInsert2(dd, Cudd_addConstrain, f, c, r);
1285    return(r);
1286
1287} /* end of cuddAddConstrainRecur */
1288
1289
1290/**Function********************************************************************
1291
1292  Synopsis    [Performs the recursive step of Cudd_addRestrict.]
1293
1294  Description [Performs the recursive step of Cudd_addRestrict.
1295  Returns the restricted ADD if successful; otherwise NULL.]
1296
1297  SideEffects [None]
1298
1299  SeeAlso     [Cudd_addRestrict]
1300
1301******************************************************************************/
1302DdNode *
1303cuddAddRestrictRecur(
1304  DdManager * dd,
1305  DdNode * f,
1306  DdNode * c)
1307{
1308    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
1309    unsigned int topf, topc;
1310    int          index;
1311
1312    statLine(dd);
1313    one = DD_ONE(dd);
1314    zero = DD_ZERO(dd);
1315
1316    /* Trivial cases */
1317    if (c == one)               return(f);
1318    if (c == zero)              return(zero);
1319    if (Cudd_IsConstant(f))     return(f);
1320    if (f == c)                 return(one);
1321
1322    /* Now f and c are non-constant. */
1323
1324    /* Check the cache. */
1325    r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c);
1326    if (r != NULL) {
1327        return(r);
1328    }
1329
1330    topf = dd->perm[f->index];
1331    topc = dd->perm[c->index];
1332
1333    if (topc < topf) {  /* abstract top variable from c */
1334        DdNode *d, *s1, *s2;
1335
1336        /* Find cofactors of c. */
1337        s1 = cuddT(c);
1338        s2 = cuddE(c);
1339        /* Take the OR by applying DeMorgan. */
1340        d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2);
1341        if (d == NULL) return(NULL);
1342        cuddRef(d);
1343        r = cuddAddRestrictRecur(dd, f, d);
1344        if (r == NULL) {
1345            Cudd_RecursiveDeref(dd, d);
1346            return(NULL);
1347        }
1348        cuddRef(r);
1349        Cudd_RecursiveDeref(dd, d);
1350        cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
1351        cuddDeref(r);
1352        return(r);
1353    }
1354
1355    /* Recursive step. Here topf <= topc. */
1356    index = f->index;
1357    Fv = cuddT(f); Fnv = cuddE(f);
1358    if (topc == topf) {
1359        Cv = cuddT(c); Cnv = cuddE(c);
1360    } else {
1361        Cv = Cnv = c;
1362    }
1363
1364    if (!Cudd_IsConstant(Cv)) {
1365        t = cuddAddRestrictRecur(dd, Fv, Cv);
1366        if (t == NULL) return(NULL);
1367    } else if (Cv == one) {
1368        t = Fv;
1369    } else {            /* Cv == zero: return(Fnv @ Cnv) */
1370        if (Cnv == one) {
1371            r = Fnv;
1372        } else {
1373            r = cuddAddRestrictRecur(dd, Fnv, Cnv);
1374            if (r == NULL) return(NULL);
1375        }
1376        return(r);
1377    }
1378    cuddRef(t);
1379
1380    if (!Cudd_IsConstant(Cnv)) {
1381        e = cuddAddRestrictRecur(dd, Fnv, Cnv);
1382        if (e == NULL) {
1383            Cudd_RecursiveDeref(dd, t);
1384            return(NULL);
1385        }
1386    } else if (Cnv == one) {
1387        e = Fnv;
1388    } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
1389        cuddDeref(t);
1390        return(t);
1391    }
1392    cuddRef(e);
1393
1394    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1395    if (r == NULL) {
1396        Cudd_RecursiveDeref(dd, e);
1397        Cudd_RecursiveDeref(dd, t);
1398        return(NULL);
1399    }
1400    cuddDeref(t);
1401    cuddDeref(e);
1402
1403    cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
1404    return(r);
1405
1406} /* end of cuddAddRestrictRecur */
1407
1408
1409
1410/**Function********************************************************************
1411
1412  Synopsis    [Performs safe minimization of a BDD.]
1413
1414  Description [Performs safe minimization of a BDD. Given the BDD
1415  <code>f</code> of a function to be minimized and a BDD
1416  <code>c</code> representing the care set, Cudd_bddLICompaction
1417  produces the BDD of a function that agrees with <code>f</code>
1418  wherever <code>c</code> is 1.  Safe minimization means that the size
1419  of the result is guaranteed not to exceed the size of
1420  <code>f</code>. This function is based on the DAC97 paper by Hong et
1421  al..  Returns a pointer to the result if successful; NULL
1422  otherwise.]
1423
1424  SideEffects [None]
1425
1426  SeeAlso     [Cudd_bddLICompaction]
1427
1428******************************************************************************/
1429DdNode *
1430cuddBddLICompaction(
1431  DdManager * dd /* manager */,
1432  DdNode * f /* function to be minimized */,
1433  DdNode * c /* constraint (care set) */)
1434{
1435    st_table *marktable, *markcache, *buildcache;
1436    DdNode *res, *zero;
1437
1438    zero = Cudd_Not(DD_ONE(dd));
1439    if (c == zero) return(zero);
1440
1441    /* We need to use local caches for both steps of this operation.
1442    ** The results of the edge marking step are only valid as long as the
1443    ** edge markings themselves are available. However, the edge markings
1444    ** are lost at the end of one invocation of Cudd_bddLICompaction.
1445    ** Hence, the cache entries for the edge marking step must be
1446    ** invalidated at the end of this function.
1447    ** For the result of the building step we argue as follows. The result
1448    ** for a node and a given constrain depends on the BDD in which the node
1449    ** appears. Hence, the same node and constrain may give different results
1450    ** in successive invocations.
1451    */
1452    marktable = st_init_table(st_ptrcmp,st_ptrhash);
1453    if (marktable == NULL) {
1454        return(NULL);
1455    }
1456    markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
1457    if (markcache == NULL) {
1458        st_free_table(marktable);
1459        return(NULL);
1460    }
1461    if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
1462        st_foreach(markcache, MarkCacheCleanUp, NULL);
1463        st_free_table(marktable);
1464        st_free_table(markcache);
1465        return(NULL);
1466    }
1467    st_foreach(markcache, MarkCacheCleanUp, NULL);
1468    st_free_table(markcache);
1469    buildcache = st_init_table(st_ptrcmp,st_ptrhash);
1470    if (buildcache == NULL) {
1471        st_free_table(marktable);
1472        return(NULL);
1473    }
1474    res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
1475    st_free_table(buildcache);
1476    st_free_table(marktable);
1477    return(res);
1478
1479} /* end of cuddBddLICompaction */
1480
1481
1482/*---------------------------------------------------------------------------*/
1483/* Definition of static functions                                            */
1484/*---------------------------------------------------------------------------*/
1485
1486
1487/**Function********************************************************************
1488
1489  Synopsis    [Performs the recursive step of Cudd_bddConstrainDecomp.]
1490
1491  Description [Performs the recursive step of Cudd_bddConstrainDecomp.
1492  Returns f super (i) if successful; otherwise NULL.]
1493
1494  SideEffects [None]
1495
1496  SeeAlso     [Cudd_bddConstrainDecomp]
1497
1498******************************************************************************/
1499static int
1500cuddBddConstrainDecomp(
1501  DdManager * dd,
1502  DdNode * f,
1503  DdNode ** decomp)
1504{
1505    DdNode *F, *fv, *fvn;
1506    DdNode *fAbs;
1507    DdNode *result;
1508    int ok;
1509
1510    if (Cudd_IsConstant(f)) return(1);
1511    /* Compute complements of cofactors. */
1512    F = Cudd_Regular(f);
1513    fv = cuddT(F);
1514    fvn = cuddE(F);
1515    if (F == f) {
1516        fv = Cudd_Not(fv);
1517        fvn = Cudd_Not(fvn);
1518    }
1519    /* Compute abstraction of top variable. */
1520    fAbs = cuddBddAndRecur(dd, fv, fvn);
1521    if (fAbs == NULL) {
1522        return(0);
1523    }
1524    cuddRef(fAbs);
1525    fAbs = Cudd_Not(fAbs);
1526    /* Recursively find the next abstraction and the components of the
1527    ** decomposition. */
1528    ok = cuddBddConstrainDecomp(dd, fAbs, decomp);
1529    if (ok == 0) {
1530        Cudd_IterDerefBdd(dd,fAbs);
1531        return(0);
1532    }
1533    /* Compute the component of the decomposition corresponding to the
1534    ** top variable and store it in the decomposition array. */
1535    result = cuddBddConstrainRecur(dd, f, fAbs);
1536    if (result == NULL) {
1537        Cudd_IterDerefBdd(dd,fAbs);
1538        return(0);
1539    }
1540    cuddRef(result);
1541    decomp[F->index] = result;
1542    Cudd_IterDerefBdd(dd, fAbs);
1543    return(1);
1544
1545} /* end of cuddBddConstrainDecomp */
1546
1547
1548/**Function********************************************************************
1549
1550  Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]
1551
1552  Description [Performs the recursive step of Cudd_bddCharToVect.
1553  This function maintains the invariant that f is non-zero.
1554  Returns the i-th component of the vector if successful; otherwise NULL.]
1555
1556  SideEffects [None]
1557
1558  SeeAlso     [Cudd_bddCharToVect]
1559
1560******************************************************************************/
1561static DdNode *
1562cuddBddCharToVect(
1563  DdManager * dd,
1564  DdNode * f,
1565  DdNode * x)
1566{
1567    unsigned int topf;
1568    unsigned int level;
1569    int comple;
1570
1571    DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;
1572
1573    statLine(dd);
1574    /* Check the cache. */
1575    res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
1576    if (res != NULL) {
1577        return(res);
1578    }
1579
1580    F = Cudd_Regular(f);
1581
1582    topf = cuddI(dd,F->index);
1583    level = dd->perm[x->index];
1584
1585    if (topf > level) return(x);
1586
1587    one = DD_ONE(dd);
1588    zero = Cudd_Not(one);
1589
1590    comple = F != f;
1591    fT = Cudd_NotCond(cuddT(F),comple);
1592    fE = Cudd_NotCond(cuddE(F),comple);
1593
1594    if (topf == level) {
1595        if (fT == zero) return(zero);
1596        if (fE == zero) return(one);
1597        return(x);
1598    }
1599
1600    /* Here topf < level. */
1601    if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
1602    if (fE == zero) return(cuddBddCharToVect(dd, fT, x));
1603
1604    T = cuddBddCharToVect(dd, fT, x);
1605    if (T == NULL) {
1606        return(NULL);
1607    }
1608    cuddRef(T);
1609    E = cuddBddCharToVect(dd, fE, x);
1610    if (E == NULL) {
1611        Cudd_IterDerefBdd(dd,T);
1612        return(NULL);
1613    }
1614    cuddRef(E);
1615    res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
1616    if (res == NULL) {
1617        Cudd_IterDerefBdd(dd,T);
1618        Cudd_IterDerefBdd(dd,E);
1619        return(NULL);
1620    }
1621    cuddDeref(T);
1622    cuddDeref(E);
1623    cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
1624    return(res);
1625
1626} /* end of cuddBddCharToVect */
1627
1628
1629/**Function********************************************************************
1630
1631  Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]
1632
1633  Description [Performs the edge marking step of Cudd_bddLICompaction.
1634  Returns the LUB of the markings of the two outgoing edges of <code>f</code>
1635  if successful; otherwise CUDD_OUT_OF_MEM.]
1636
1637  SideEffects [None]
1638
1639  SeeAlso     [Cudd_bddLICompaction cuddBddLICBuildResult]
1640
1641******************************************************************************/
1642static int
1643cuddBddLICMarkEdges(
1644  DdManager * dd,
1645  DdNode * f,
1646  DdNode * c,
1647  st_table * table,
1648  st_table * cache)
1649{
1650    DdNode *Fv, *Fnv, *Cv, *Cnv;
1651    DdNode *one, *zero;
1652    unsigned int topf, topc;
1653    int comple;
1654    int resT, resE, res, retval;
1655    char **slot;
1656    MarkCacheKey *key;
1657
1658    one = DD_ONE(dd);
1659    zero = Cudd_Not(one);
1660
1661    /* Terminal cases. */
1662    if (c == zero) return(DD_LIC_DC);
1663    if (f == one)  return(DD_LIC_1);
1664    if (f == zero) return(DD_LIC_0);
1665
1666    /* Make canonical to increase the utilization of the cache. */
1667    comple = Cudd_IsComplement(f);
1668    f = Cudd_Regular(f);
1669    /* Now f is a regular pointer to a non-constant node; c may be
1670    ** constant, or it may be complemented.
1671    */
1672
1673    /* Check the cache. */
1674    key = ALLOC(MarkCacheKey, 1);
1675    if (key == NULL) {
1676        dd->errorCode = CUDD_MEMORY_OUT;
1677        return(CUDD_OUT_OF_MEM);
1678    }
1679    key->f = f; key->c = c;
1680    if (st_lookup_int(cache, (char *)key, &res)) {
1681        FREE(key);
1682        if (comple) {
1683            if (res == DD_LIC_0) res = DD_LIC_1;
1684            else if (res == DD_LIC_1) res = DD_LIC_0;
1685        }
1686        return(res);
1687    }
1688
1689    /* Recursive step. */
1690    topf = dd->perm[f->index];
1691    topc = cuddI(dd,Cudd_Regular(c)->index);
1692    if (topf <= topc) {
1693        Fv = cuddT(f); Fnv = cuddE(f);
1694    } else {
1695        Fv = Fnv = f;
1696    }
1697    if (topc <= topf) {
1698        /* We know that c is not constant because f is not. */
1699        Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
1700        if (Cudd_IsComplement(c)) {
1701            Cv = Cudd_Not(Cv);
1702            Cnv = Cudd_Not(Cnv);
1703        }
1704    } else {
1705        Cv = Cnv = c;
1706    }
1707
1708    resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
1709    if (resT == CUDD_OUT_OF_MEM) {
1710        FREE(key);
1711        return(CUDD_OUT_OF_MEM);
1712    }
1713    resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
1714    if (resE == CUDD_OUT_OF_MEM) {
1715        FREE(key);
1716        return(CUDD_OUT_OF_MEM);
1717    }
1718
1719    /* Update edge markings. */
1720    if (topf <= topc) {
1721        retval = st_find_or_add(table, (char *)f, (char ***)&slot);
1722        if (retval == 0) {
1723            *slot = (char *) (ptrint)((resT << 2) | resE);
1724        } else if (retval == 1) {
1725            *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
1726        } else {
1727            FREE(key);
1728            return(CUDD_OUT_OF_MEM);
1729        }
1730    }
1731
1732    /* Cache result. */
1733    res = resT | resE;
1734    if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
1735        FREE(key);
1736        return(CUDD_OUT_OF_MEM);
1737    }
1738
1739    /* Take into account possible complementation. */
1740    if (comple) {
1741        if (res == DD_LIC_0) res = DD_LIC_1;
1742        else if (res == DD_LIC_1) res = DD_LIC_0;
1743    }
1744    return(res);
1745
1746} /* end of cuddBddLICMarkEdges */
1747
1748
1749/**Function********************************************************************
1750
1751  Synopsis    [Builds the result of Cudd_bddLICompaction.]
1752
1753  Description [Builds the results of Cudd_bddLICompaction.
1754  Returns a pointer to the minimized BDD if successful; otherwise NULL.]
1755
1756  SideEffects [None]
1757
1758  SeeAlso     [Cudd_bddLICompaction cuddBddLICMarkEdges]
1759
1760******************************************************************************/
1761static DdNode *
1762cuddBddLICBuildResult(
1763  DdManager * dd,
1764  DdNode * f,
1765  st_table * cache,
1766  st_table * table)
1767{
1768    DdNode *Fv, *Fnv, *r, *t, *e;
1769    DdNode *one, *zero;
1770    int index;
1771    int comple;
1772    int markT, markE, markings;
1773
1774    one = DD_ONE(dd);
1775    zero = Cudd_Not(one);
1776
1777    if (Cudd_IsConstant(f)) return(f);
1778    /* Make canonical to increase the utilization of the cache. */
1779    comple = Cudd_IsComplement(f);
1780    f = Cudd_Regular(f);
1781
1782    /* Check the cache. */
1783    if (st_lookup(cache, f, &r)) {
1784        return(Cudd_NotCond(r,comple));
1785    }
1786
1787    /* Retrieve the edge markings. */
1788    if (st_lookup_int(table, (char *)f, &markings) == 0)
1789        return(NULL);
1790    markT = markings >> 2;
1791    markE = markings & 3;
1792
1793    index = f->index;
1794    Fv = cuddT(f); Fnv = cuddE(f);
1795
1796    if (markT == DD_LIC_NL) {
1797        t = cuddBddLICBuildResult(dd,Fv,cache,table);
1798        if (t == NULL) {
1799            return(NULL);
1800        }
1801    } else if (markT == DD_LIC_1) {
1802        t = one;
1803    } else {
1804        t = zero;
1805    }
1806    cuddRef(t);
1807    if (markE == DD_LIC_NL) {
1808        e = cuddBddLICBuildResult(dd,Fnv,cache,table);
1809        if (e == NULL) {
1810            Cudd_IterDerefBdd(dd,t);
1811            return(NULL);
1812        }
1813    } else if (markE == DD_LIC_1) {
1814        e = one;
1815    } else {
1816        e = zero;
1817    }
1818    cuddRef(e);
1819
1820    if (markT == DD_LIC_DC && markE != DD_LIC_DC) {
1821        r = e;
1822    } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) {
1823        r = t;
1824    } else {
1825        if (Cudd_IsComplement(t)) {
1826            t = Cudd_Not(t);
1827            e = Cudd_Not(e);
1828            r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1829            if (r == NULL) {
1830                Cudd_IterDerefBdd(dd, e);
1831                Cudd_IterDerefBdd(dd, t);
1832                return(NULL);
1833            }
1834            r = Cudd_Not(r);
1835        } else {
1836            r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1837            if (r == NULL) {
1838                Cudd_IterDerefBdd(dd, e);
1839                Cudd_IterDerefBdd(dd, t);
1840                return(NULL);
1841            }
1842        }
1843    }
1844    cuddDeref(t);
1845    cuddDeref(e);
1846
1847    if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
1848        cuddRef(r);
1849        Cudd_IterDerefBdd(dd,r);
1850        return(NULL);
1851    }
1852
1853    return(Cudd_NotCond(r,comple));
1854
1855} /* end of cuddBddLICBuildResult */
1856
1857
1858/**Function********************************************************************
1859
1860  Synopsis    [Hash function for the computed table of cuddBddLICMarkEdges.]
1861
1862  Description [Hash function for the computed table of
1863  cuddBddLICMarkEdges.  Returns the bucket number.]
1864
1865  SideEffects [None]
1866
1867  SeeAlso     [Cudd_bddLICompaction]
1868
1869******************************************************************************/
1870static int
1871MarkCacheHash(
1872  char * ptr,
1873  int  modulus)
1874{
1875    int val = 0;
1876    MarkCacheKey *entry;
1877
1878    entry = (MarkCacheKey *) ptr;
1879
1880    val = (int) (ptrint) entry->f;
1881    val = val * 997 + (int) (ptrint) entry->c;
1882
1883    return ((val < 0) ? -val : val) % modulus;
1884
1885} /* end of MarkCacheHash */
1886
1887
1888/**Function********************************************************************
1889
1890  Synopsis    [Comparison function for the computed table of
1891  cuddBddLICMarkEdges.]
1892
1893  Description [Comparison function for the computed table of
1894  cuddBddLICMarkEdges. Returns 0 if the two nodes of the key are equal; 1
1895  otherwise.]
1896
1897  SideEffects [None]
1898
1899  SeeAlso     [Cudd_bddLICompaction]
1900
1901******************************************************************************/
1902static int
1903MarkCacheCompare(
1904  const char * ptr1,
1905  const char * ptr2)
1906{
1907    MarkCacheKey *entry1, *entry2;
1908
1909    entry1 = (MarkCacheKey *) ptr1;
1910    entry2 = (MarkCacheKey *) ptr2;
1911   
1912    return((entry1->f != entry2->f) || (entry1->c != entry2->c));
1913
1914} /* end of MarkCacheCompare */
1915
1916
1917
1918/**Function********************************************************************
1919
1920  Synopsis    [Frees memory associated with computed table of
1921  cuddBddLICMarkEdges.]
1922
1923  Description [Frees memory associated with computed table of
1924  cuddBddLICMarkEdges. Returns ST_CONTINUE.]
1925
1926  SideEffects [None]
1927
1928  SeeAlso     [Cudd_bddLICompaction]
1929
1930******************************************************************************/
1931static enum st_retval
1932MarkCacheCleanUp(
1933  char * key,
1934  char * value,
1935  char * arg)
1936{
1937    MarkCacheKey *entry;
1938
1939    entry = (MarkCacheKey *) key;
1940    FREE(entry);
1941    return ST_CONTINUE;
1942
1943} /* end of MarkCacheCleanUp */
1944
1945
1946/**Function********************************************************************
1947
1948  Synopsis    [Performs the recursive step of Cudd_bddSqueeze.]
1949
1950  Description [Performs the recursive step of Cudd_bddSqueeze.  This
1951  procedure exploits the fact that if we complement and swap the
1952  bounds of the interval we obtain a valid solution by taking the
1953  complement of the solution to the original problem. Therefore, we
1954  can enforce the condition that the upper bound is always regular.
1955  Returns a pointer to the result if successful; NULL otherwise.]
1956
1957  SideEffects [None]
1958
1959  SeeAlso     [Cudd_bddSqueeze]
1960
1961******************************************************************************/
1962static DdNode *
1963cuddBddSqueeze(
1964  DdManager * dd,
1965  DdNode * l,
1966  DdNode * u)
1967{
1968    DdNode *one, *zero, *r, *lt, *le, *ut, *ue, *t, *e;
1969#if 0
1970    DdNode *ar;
1971#endif
1972    int comple = 0;
1973    unsigned int topu, topl;
1974    int index;
1975
1976    statLine(dd);
1977    if (l == u) {
1978        return(l);
1979    }
1980    one = DD_ONE(dd);
1981    zero = Cudd_Not(one);
1982    /* The only case when l == zero && u == one is at the top level,
1983    ** where returning either one or zero is OK. In all other cases
1984    ** the procedure will detect such a case and will perform
1985    ** remapping. Therefore the order in which we test l and u at this
1986    ** point is immaterial. */
1987    if (l == zero) return(l);
1988    if (u == one)  return(u);
1989
1990    /* Make canonical to increase the utilization of the cache. */
1991    if (Cudd_IsComplement(u)) {
1992        DdNode *temp;
1993        temp = Cudd_Not(l);
1994        l = Cudd_Not(u);
1995        u = temp;
1996        comple = 1;
1997    }
1998    /* At this point u is regular and non-constant; l is non-constant, but
1999    ** may be complemented. */
2000
2001    /* Here we could check the relative sizes. */
2002
2003    /* Check the cache. */
2004    r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u);
2005    if (r != NULL) {
2006        return(Cudd_NotCond(r,comple));
2007    }
2008
2009    /* Recursive step. */
2010    topu = dd->perm[u->index];
2011    topl = dd->perm[Cudd_Regular(l)->index];
2012    if (topu <= topl) {
2013        index = u->index;
2014        ut = cuddT(u); ue = cuddE(u);
2015    } else {
2016        index = Cudd_Regular(l)->index;
2017        ut = ue = u;
2018    }
2019    if (topl <= topu) {
2020        lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l));
2021        if (Cudd_IsComplement(l)) {
2022            lt = Cudd_Not(lt);
2023            le = Cudd_Not(le);
2024        }
2025    } else {
2026        lt = le = l;
2027    }
2028
2029    /* If one interval is contained in the other, use the smaller
2030    ** interval. This corresponds to one-sided matching. */
2031    if ((lt == zero || Cudd_bddLeq(dd,lt,le)) &&
2032        (ut == one  || Cudd_bddLeq(dd,ue,ut))) { /* remap */
2033        r = cuddBddSqueeze(dd, le, ue);
2034        if (r == NULL)
2035            return(NULL);
2036        return(Cudd_NotCond(r,comple));
2037    } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) &&
2038               (ue == one  || Cudd_bddLeq(dd,ut,ue))) { /* remap */
2039        r = cuddBddSqueeze(dd, lt, ut);
2040        if (r == NULL)
2041            return(NULL);
2042        return(Cudd_NotCond(r,comple));
2043    } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) &&
2044               (ue == one  || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */
2045        t = cuddBddSqueeze(dd, lt, ut);
2046        cuddRef(t);
2047        if (Cudd_IsComplement(t)) {
2048            r = cuddUniqueInter(dd, index, Cudd_Not(t), t);
2049            if (r == NULL) {
2050                Cudd_IterDerefBdd(dd, t);
2051                return(NULL);
2052            }
2053            r = Cudd_Not(r);
2054        } else {
2055            r = cuddUniqueInter(dd, index, t, Cudd_Not(t));
2056            if (r == NULL) {
2057                Cudd_IterDerefBdd(dd, t);
2058                return(NULL);
2059            }
2060        }
2061        cuddDeref(t);
2062        if (r == NULL)
2063            return(NULL);
2064        cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
2065        return(Cudd_NotCond(r,comple));
2066    } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) &&
2067               (ut == one  || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */
2068        e = cuddBddSqueeze(dd, le, ue);
2069        cuddRef(e);
2070        if (Cudd_IsComplement(e)) {
2071            r = cuddUniqueInter(dd, index, Cudd_Not(e), e);
2072            if (r == NULL) {
2073                Cudd_IterDerefBdd(dd, e);
2074                return(NULL);
2075            }
2076        } else {
2077            r = cuddUniqueInter(dd, index, e, Cudd_Not(e));
2078            if (r == NULL) {
2079                Cudd_IterDerefBdd(dd, e);
2080                return(NULL);
2081            }
2082            r = Cudd_Not(r);
2083        }
2084        cuddDeref(e);
2085        if (r == NULL)
2086            return(NULL);
2087        cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
2088        return(Cudd_NotCond(r,comple));
2089    }
2090
2091#if 0
2092    /* If the two intervals intersect, take a solution from
2093    ** the intersection of the intervals. This guarantees that the
2094    ** splitting variable will not appear in the result.
2095    ** This approach corresponds to two-sided matching, and is very
2096    ** expensive. */
2097    if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) {
2098        DdNode *au, *al;
2099        au = cuddBddAndRecur(dd,ut,ue);
2100        if (au == NULL)
2101            return(NULL);
2102        cuddRef(au);
2103        al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le));
2104        if (al == NULL) {
2105            Cudd_IterDerefBdd(dd,au);
2106            return(NULL);
2107        }
2108        cuddRef(al);
2109        al = Cudd_Not(al);
2110        ar = cuddBddSqueeze(dd, al, au);
2111        if (ar == NULL) {
2112            Cudd_IterDerefBdd(dd,au);
2113            Cudd_IterDerefBdd(dd,al);
2114            return(NULL);
2115        }
2116        cuddRef(ar);
2117        Cudd_IterDerefBdd(dd,au);
2118        Cudd_IterDerefBdd(dd,al);
2119    } else {
2120        ar = NULL;
2121    }
2122#endif
2123
2124    t = cuddBddSqueeze(dd, lt, ut);
2125    if (t == NULL) {
2126        return(NULL);
2127    }
2128    cuddRef(t);
2129    e = cuddBddSqueeze(dd, le, ue);
2130    if (e == NULL) {
2131        Cudd_IterDerefBdd(dd,t);
2132        return(NULL);
2133    }
2134    cuddRef(e);
2135
2136    if (Cudd_IsComplement(t)) {
2137        t = Cudd_Not(t);
2138        e = Cudd_Not(e);
2139        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2140        if (r == NULL) {
2141            Cudd_IterDerefBdd(dd, e);
2142            Cudd_IterDerefBdd(dd, t);
2143            return(NULL);
2144        }
2145        r = Cudd_Not(r);
2146    } else {
2147        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2148        if (r == NULL) {
2149            Cudd_IterDerefBdd(dd, e);
2150            Cudd_IterDerefBdd(dd, t);
2151            return(NULL);
2152        }
2153    }
2154    cuddDeref(t);
2155    cuddDeref(e);
2156
2157#if 0
2158    /* Check whether there is a result obtained by abstraction and whether
2159    ** it is better than the one obtained by recursion. */
2160    cuddRef(r);
2161    if (ar != NULL) {
2162        if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) {
2163            Cudd_IterDerefBdd(dd, r);
2164            r = ar;
2165        } else {
2166            Cudd_IterDerefBdd(dd, ar);
2167        }
2168    }
2169    cuddDeref(r);
2170#endif
2171
2172    cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
2173    return(Cudd_NotCond(r,comple));
2174
2175} /* end of cuddBddSqueeze */
Note: See TracBrowser for help on using the repository browser.