source: vis_dev/glu-2.3/src/cuBdd/cuddAddApply.c @ 91

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

library glu 2.3
File size: 23.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddAddApply.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Apply functions for ADDs and their operators.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_addApply()
12                <li> Cudd_addMonadicApply()
13                <li> Cudd_addPlus()
14                <li> Cudd_addTimes()
15                <li> Cudd_addThreshold()
16                <li> Cudd_addSetNZ()
17                <li> Cudd_addDivide()
18                <li> Cudd_addMinus()
19                <li> Cudd_addMinimum()
20                <li> Cudd_addMaximum()
21                <li> Cudd_addOneZeroMaximum()
22                <li> Cudd_addDiff()
23                <li> Cudd_addAgreement()
24                <li> Cudd_addOr()
25                <li> Cudd_addNand()
26                <li> Cudd_addNor()
27                <li> Cudd_addXor()
28                <li> Cudd_addXnor()
29                </ul>
30            Internal procedures included in this module:
31                <ul>
32                <li> cuddAddApplyRecur()
33                <li> cuddAddMonadicApplyRecur()
34                </ul>]
35
36  Author      [Fabio Somenzi]
37
38  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
39
40  All rights reserved.
41
42  Redistribution and use in source and binary forms, with or without
43  modification, are permitted provided that the following conditions
44  are met:
45
46  Redistributions of source code must retain the above copyright
47  notice, this list of conditions and the following disclaimer.
48
49  Redistributions in binary form must reproduce the above copyright
50  notice, this list of conditions and the following disclaimer in the
51  documentation and/or other materials provided with the distribution.
52
53  Neither the name of the University of Colorado nor the names of its
54  contributors may be used to endorse or promote products derived from
55  this software without specific prior written permission.
56
57  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
58  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
59  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
60  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
61  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
62  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
63  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
64  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
65  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
66  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
67  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
68  POSSIBILITY OF SUCH DAMAGE.]
69
70******************************************************************************/
71
72#include "util.h"
73#include "cuddInt.h"
74
75/*---------------------------------------------------------------------------*/
76/* Constant declarations                                                     */
77/*---------------------------------------------------------------------------*/
78
79
80/*---------------------------------------------------------------------------*/
81/* Stucture declarations                                                     */
82/*---------------------------------------------------------------------------*/
83
84
85/*---------------------------------------------------------------------------*/
86/* Type declarations                                                         */
87/*---------------------------------------------------------------------------*/
88
89
90/*---------------------------------------------------------------------------*/
91/* Variable declarations                                                     */
92/*---------------------------------------------------------------------------*/
93
94#ifndef lint
95static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio Exp $";
96#endif
97
98
99/*---------------------------------------------------------------------------*/
100/* Macro declarations                                                        */
101/*---------------------------------------------------------------------------*/
102
103
104/**AutomaticStart*************************************************************/
105
106/*---------------------------------------------------------------------------*/
107/* Static function prototypes                                                */
108/*---------------------------------------------------------------------------*/
109
110
111/**AutomaticEnd***************************************************************/
112
113
114/*---------------------------------------------------------------------------*/
115/* Definition of exported functions                                          */
116/*---------------------------------------------------------------------------*/
117
118/**Function********************************************************************
119
120  Synopsis    [Applies op to the corresponding discriminants of f and g.]
121
122  Description [Applies op to the corresponding discriminants of f and g.
123  Returns a pointer to the result if succssful; NULL otherwise.]
124
125  SideEffects [None]
126
127  SeeAlso     [Cudd_addMonadicApply Cudd_addPlus Cudd_addTimes
128  Cudd_addThreshold Cudd_addSetNZ Cudd_addDivide Cudd_addMinus Cudd_addMinimum
129  Cudd_addMaximum Cudd_addOneZeroMaximum Cudd_addDiff Cudd_addAgreement
130  Cudd_addOr Cudd_addNand Cudd_addNor Cudd_addXor Cudd_addXnor]
131
132******************************************************************************/
133DdNode *
134Cudd_addApply(
135  DdManager * dd,
136  DD_AOP op,
137  DdNode * f,
138  DdNode * g)
139{
140    DdNode *res;
141
142    do {
143        dd->reordered = 0;
144        res = cuddAddApplyRecur(dd,op,f,g);
145    } while (dd->reordered == 1);
146    return(res);
147
148} /* end of Cudd_addApply */
149
150
151/**Function********************************************************************
152
153  Synopsis    [Integer and floating point addition.]
154
155  Description [Integer and floating point addition. Returns NULL if not
156  a terminal case; f+g otherwise.]
157
158  SideEffects [None]
159
160  SeeAlso     [Cudd_addApply]
161
162******************************************************************************/
163DdNode *
164Cudd_addPlus(
165  DdManager * dd,
166  DdNode ** f,
167  DdNode ** g)
168{
169    DdNode *res;
170    DdNode *F, *G;
171    CUDD_VALUE_TYPE value;
172
173    F = *f; G = *g;
174    if (F == DD_ZERO(dd)) return(G);
175    if (G == DD_ZERO(dd)) return(F);
176    if (cuddIsConstant(F) && cuddIsConstant(G)) {
177        value = cuddV(F)+cuddV(G);
178        res = cuddUniqueConst(dd,value);
179        return(res);
180    }
181    if (F > G) { /* swap f and g */
182        *f = G;
183        *g = F;
184    }
185    return(NULL);
186
187} /* end of Cudd_addPlus */
188
189
190/**Function********************************************************************
191
192  Synopsis    [Integer and floating point multiplication.]
193
194  Description [Integer and floating point multiplication. Returns NULL
195  if not a terminal case; f * g otherwise.  This function can be used also
196  to take the AND of two 0-1 ADDs.]
197
198  SideEffects [None]
199
200  SeeAlso     [Cudd_addApply]
201
202******************************************************************************/
203DdNode *
204Cudd_addTimes(
205  DdManager * dd,
206  DdNode ** f,
207  DdNode ** g)
208{
209    DdNode *res;
210    DdNode *F, *G;
211    CUDD_VALUE_TYPE value;
212
213    F = *f; G = *g;
214    if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
215    if (F == DD_ONE(dd)) return(G);
216    if (G == DD_ONE(dd)) return(F);
217    if (cuddIsConstant(F) && cuddIsConstant(G)) {
218        value = cuddV(F)*cuddV(G);
219        res = cuddUniqueConst(dd,value);
220        return(res);
221    }
222    if (F > G) { /* swap f and g */
223        *f = G;
224        *g = F;
225    }
226    return(NULL);
227
228} /* end of Cudd_addTimes */
229
230
231/**Function********************************************************************
232
233  Synopsis    [f if f&gt;=g; 0 if f&lt;g.]
234
235  Description [Threshold operator for Apply (f if f &gt;=g; 0 if f&lt;g).
236  Returns NULL if not a terminal case; f op g otherwise.]
237
238  SideEffects [None]
239
240  SeeAlso     [Cudd_addApply]
241
242******************************************************************************/
243DdNode *
244Cudd_addThreshold(
245  DdManager * dd,
246  DdNode ** f,
247  DdNode ** g)
248{
249    DdNode *F, *G;
250
251    F = *f; G = *g;
252    if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
253    if (cuddIsConstant(F) && cuddIsConstant(G)) {
254        if (cuddV(F) >= cuddV(G)) {
255            return(F);
256        } else {
257            return(DD_ZERO(dd));
258        }
259    }
260    return(NULL);
261
262} /* end of Cudd_addThreshold */
263
264
265/**Function********************************************************************
266
267  Synopsis    [This operator sets f to the value of g wherever g != 0.]
268
269  Description [This operator sets f to the value of g wherever g != 0.
270  Returns NULL if not a terminal case; f op g otherwise.]
271
272  SideEffects [None]
273
274  SeeAlso     [Cudd_addApply]
275
276******************************************************************************/
277DdNode *
278Cudd_addSetNZ(
279  DdManager * dd,
280  DdNode ** f,
281  DdNode ** g)
282{
283    DdNode *F, *G;
284
285    F = *f; G = *g;
286    if (F == G) return(F);
287    if (F == DD_ZERO(dd)) return(G);
288    if (G == DD_ZERO(dd)) return(F);
289    if (cuddIsConstant(G)) return(G);
290    return(NULL);
291
292} /* end of Cudd_addSetNZ */
293
294
295/**Function********************************************************************
296
297  Synopsis    [Integer and floating point division.]
298
299  Description [Integer and floating point division. Returns NULL if not
300  a terminal case; f / g otherwise.]
301
302  SideEffects [None]
303
304  SeeAlso     [Cudd_addApply]
305
306******************************************************************************/
307DdNode *
308Cudd_addDivide(
309  DdManager * dd,
310  DdNode ** f,
311  DdNode ** g)
312{
313    DdNode *res;
314    DdNode *F, *G;
315    CUDD_VALUE_TYPE value;
316
317    F = *f; G = *g;
318    /* We would like to use F == G -> F/G == 1, but F and G may
319    ** contain zeroes. */
320    if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
321    if (G == DD_ONE(dd)) return(F);
322    if (cuddIsConstant(F) && cuddIsConstant(G)) {
323        value = cuddV(F)/cuddV(G);
324        res = cuddUniqueConst(dd,value);
325        return(res);
326    }
327    return(NULL);
328
329} /* end of Cudd_addDivide */
330
331
332/**Function********************************************************************
333
334  Synopsis    [Integer and floating point subtraction.]
335
336  Description [Integer and floating point subtraction. Returns NULL if
337  not a terminal case; f - g otherwise.]
338
339  SideEffects [None]
340
341  SeeAlso     [Cudd_addApply]
342
343******************************************************************************/
344DdNode *
345Cudd_addMinus(
346  DdManager * dd,
347  DdNode ** f,
348  DdNode ** g)
349{
350    DdNode *res;
351    DdNode *F, *G;
352    CUDD_VALUE_TYPE value;
353
354    F = *f; G = *g;
355    if (F == G) return(DD_ZERO(dd));
356    if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
357    if (G == DD_ZERO(dd)) return(F);
358    if (cuddIsConstant(F) && cuddIsConstant(G)) {
359        value = cuddV(F)-cuddV(G);
360        res = cuddUniqueConst(dd,value);
361        return(res);
362    }
363    return(NULL);
364
365} /* end of Cudd_addMinus */
366
367
368/**Function********************************************************************
369
370  Synopsis    [Integer and floating point min.]
371
372  Description [Integer and floating point min for Cudd_addApply.
373  Returns NULL if not a terminal case; min(f,g) otherwise.]
374
375  SideEffects [None]
376
377  SeeAlso     [Cudd_addApply]
378
379******************************************************************************/
380DdNode *
381Cudd_addMinimum(
382  DdManager * dd,
383  DdNode ** f,
384  DdNode ** g)
385{
386    DdNode *F, *G;
387
388    F = *f; G = *g;
389    if (F == DD_PLUS_INFINITY(dd)) return(G);
390    if (G == DD_PLUS_INFINITY(dd)) return(F);
391    if (F == G) return(F);
392#if 0
393    /* These special cases probably do not pay off. */
394    if (F == DD_MINUS_INFINITY(dd)) return(F);
395    if (G == DD_MINUS_INFINITY(dd)) return(G);
396#endif
397    if (cuddIsConstant(F) && cuddIsConstant(G)) {
398        if (cuddV(F) <= cuddV(G)) {
399            return(F);
400        } else {
401            return(G);
402        }
403    }
404    if (F > G) { /* swap f and g */
405        *f = G;
406        *g = F;
407    }
408    return(NULL);
409
410} /* end of Cudd_addMinimum */
411
412
413/**Function********************************************************************
414
415  Synopsis    [Integer and floating point max.]
416
417  Description [Integer and floating point max for Cudd_addApply.
418  Returns NULL if not a terminal case; max(f,g) otherwise.]
419
420  SideEffects [None]
421
422  SeeAlso     [Cudd_addApply]
423
424******************************************************************************/
425DdNode *
426Cudd_addMaximum(
427  DdManager * dd,
428  DdNode ** f,
429  DdNode ** g)
430{
431    DdNode *F, *G;
432
433    F = *f; G = *g;
434    if (F == G) return(F);
435    if (F == DD_MINUS_INFINITY(dd)) return(G);
436    if (G == DD_MINUS_INFINITY(dd)) return(F);
437#if 0
438    /* These special cases probably do not pay off. */
439    if (F == DD_PLUS_INFINITY(dd)) return(F);
440    if (G == DD_PLUS_INFINITY(dd)) return(G);
441#endif
442    if (cuddIsConstant(F) && cuddIsConstant(G)) {
443        if (cuddV(F) >= cuddV(G)) {
444            return(F);
445        } else {
446            return(G);
447        }
448    }
449    if (F > G) { /* swap f and g */
450        *f = G;
451        *g = F;
452    }
453    return(NULL);
454
455} /* end of Cudd_addMaximum */
456
457
458/**Function********************************************************************
459
460  Synopsis    [Returns 1 if f &gt; g and 0 otherwise.]
461
462  Description [Returns 1 if f &gt; g and 0 otherwise. Used in
463  conjunction with Cudd_addApply. Returns NULL if not a terminal
464  case.]
465
466  SideEffects [None]
467
468  SeeAlso     [Cudd_addApply]
469
470******************************************************************************/
471DdNode *
472Cudd_addOneZeroMaximum(
473  DdManager * dd,
474  DdNode ** f,
475  DdNode ** g)
476{
477
478    if (*f == *g) return(DD_ZERO(dd));
479    if (*g == DD_PLUS_INFINITY(dd))
480        return DD_ZERO(dd);
481    if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
482        if (cuddV(*f) > cuddV(*g)) {
483            return(DD_ONE(dd));
484        } else {
485            return(DD_ZERO(dd));
486        }
487    }
488
489    return(NULL);
490
491} /* end of Cudd_addOneZeroMaximum */
492
493
494/**Function********************************************************************
495
496  Synopsis    [Returns plusinfinity if f=g; returns min(f,g) if f!=g.]
497
498  Description [Returns NULL if not a terminal case; f op g otherwise,
499  where f op g is plusinfinity if f=g; min(f,g) if f!=g.]
500
501  SideEffects [None]
502
503  SeeAlso     [Cudd_addApply]
504
505******************************************************************************/
506DdNode *
507Cudd_addDiff(
508  DdManager * dd,
509  DdNode ** f,
510  DdNode ** g)
511{
512    DdNode *F, *G;
513
514    F = *f; G = *g;
515    if (F == G) return(DD_PLUS_INFINITY(dd));
516    if (F == DD_PLUS_INFINITY(dd)) return(G);
517    if (G == DD_PLUS_INFINITY(dd)) return(F);
518    if (cuddIsConstant(F) && cuddIsConstant(G)) {
519        if (cuddV(F) != cuddV(G)) {
520            if (cuddV(F) < cuddV(G)) {
521                return(F);
522            } else {
523                return(G);
524            }
525        } else {
526            return(DD_PLUS_INFINITY(dd));
527        }
528    }
529    return(NULL);
530
531} /* end of Cudd_addDiff */
532
533
534/**Function********************************************************************
535
536  Synopsis    [f if f==g; background if f!=g.]
537
538  Description [Returns NULL if not a terminal case; f op g otherwise,
539  where f op g is f if f==g; background if f!=g.]
540
541  SideEffects [None]
542
543  SeeAlso     [Cudd_addApply]
544
545******************************************************************************/
546DdNode *
547Cudd_addAgreement(
548  DdManager * dd,
549  DdNode ** f,
550  DdNode ** g)
551{
552    DdNode *F, *G;
553
554    F = *f; G = *g;
555    if (F == G) return(F);
556    if (F == dd->background) return(F);
557    if (G == dd->background) return(G);
558    if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
559    return(NULL);
560
561} /* end of Cudd_addAgreement */
562
563
564/**Function********************************************************************
565
566  Synopsis    [Disjunction of two 0-1 ADDs.]
567
568  Description [Disjunction of two 0-1 ADDs. Returns NULL
569  if not a terminal case; f OR g otherwise.]
570
571  SideEffects [None]
572
573  SeeAlso     [Cudd_addApply]
574
575******************************************************************************/
576DdNode *
577Cudd_addOr(
578  DdManager * dd,
579  DdNode ** f,
580  DdNode ** g)
581{
582    DdNode *F, *G;
583
584    F = *f; G = *g;
585    if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
586    if (cuddIsConstant(F)) return(G);
587    if (cuddIsConstant(G)) return(F);
588    if (F == G) return(F);
589    if (F > G) { /* swap f and g */
590        *f = G;
591        *g = F;
592    }
593    return(NULL);
594
595} /* end of Cudd_addOr */
596
597
598/**Function********************************************************************
599
600  Synopsis    [NAND of two 0-1 ADDs.]
601
602  Description [NAND of two 0-1 ADDs. Returns NULL
603  if not a terminal case; f NAND g otherwise.]
604
605  SideEffects [None]
606
607  SeeAlso     [Cudd_addApply]
608
609******************************************************************************/
610DdNode *
611Cudd_addNand(
612  DdManager * dd,
613  DdNode ** f,
614  DdNode ** g)
615{
616    DdNode *F, *G;
617
618    F = *f; G = *g;
619    if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
620    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
621    if (F > G) { /* swap f and g */
622        *f = G;
623        *g = F;
624    }
625    return(NULL);
626
627} /* end of Cudd_addNand */
628
629
630/**Function********************************************************************
631
632  Synopsis    [NOR of two 0-1 ADDs.]
633
634  Description [NOR of two 0-1 ADDs. Returns NULL
635  if not a terminal case; f NOR g otherwise.]
636
637  SideEffects [None]
638
639  SeeAlso     [Cudd_addApply]
640
641******************************************************************************/
642DdNode *
643Cudd_addNor(
644  DdManager * dd,
645  DdNode ** f,
646  DdNode ** g)
647{
648    DdNode *F, *G;
649
650    F = *f; G = *g;
651    if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
652    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
653    if (F > G) { /* swap f and g */
654        *f = G;
655        *g = F;
656    }
657    return(NULL);
658
659} /* end of Cudd_addNor */
660
661
662/**Function********************************************************************
663
664  Synopsis    [XOR of two 0-1 ADDs.]
665
666  Description [XOR of two 0-1 ADDs. Returns NULL
667  if not a terminal case; f XOR g otherwise.]
668
669  SideEffects [None]
670
671  SeeAlso     [Cudd_addApply]
672
673******************************************************************************/
674DdNode *
675Cudd_addXor(
676  DdManager * dd,
677  DdNode ** f,
678  DdNode ** g)
679{
680    DdNode *F, *G;
681
682    F = *f; G = *g;
683    if (F == G) return(DD_ZERO(dd));
684    if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
685    if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
686    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
687    if (F > G) { /* swap f and g */
688        *f = G;
689        *g = F;
690    }
691    return(NULL);
692
693} /* end of Cudd_addXor */
694
695
696/**Function********************************************************************
697
698  Synopsis    [XNOR of two 0-1 ADDs.]
699
700  Description [XNOR of two 0-1 ADDs. Returns NULL
701  if not a terminal case; f XNOR g otherwise.]
702
703  SideEffects [None]
704
705  SeeAlso     [Cudd_addApply]
706
707******************************************************************************/
708DdNode *
709Cudd_addXnor(
710  DdManager * dd,
711  DdNode ** f,
712  DdNode ** g)
713{
714    DdNode *F, *G;
715
716    F = *f; G = *g;
717    if (F == G) return(DD_ONE(dd));
718    if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
719    if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
720    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
721    if (F > G) { /* swap f and g */
722        *f = G;
723        *g = F;
724    }
725    return(NULL);
726
727} /* end of Cudd_addXnor */
728
729
730/**Function********************************************************************
731
732  Synopsis    [Applies op to the discriminants of f.]
733
734  Description [Applies op to the discriminants of f.
735  Returns a pointer to the result if succssful; NULL otherwise.]
736
737  SideEffects [None]
738
739  SeeAlso     [Cudd_addApply Cudd_addLog]
740
741******************************************************************************/
742DdNode *
743Cudd_addMonadicApply(
744  DdManager * dd,
745  DD_MAOP op,
746  DdNode * f)
747{
748    DdNode *res;
749
750    do {
751        dd->reordered = 0;
752        res = cuddAddMonadicApplyRecur(dd,op,f);
753    } while (dd->reordered == 1);
754    return(res);
755
756} /* end of Cudd_addMonadicApply */
757
758
759/**Function********************************************************************
760
761  Synopsis    [Natural logarithm of an ADD.]
762
763  Description [Natural logarithm of an ADDs. Returns NULL
764  if not a terminal case; log(f) otherwise.  The discriminants of f must
765  be positive double's.]
766
767  SideEffects [None]
768
769  SeeAlso     [Cudd_addMonadicApply]
770
771******************************************************************************/
772DdNode *
773Cudd_addLog(
774  DdManager * dd,
775  DdNode * f)
776{
777    if (cuddIsConstant(f)) {
778        CUDD_VALUE_TYPE value = log(cuddV(f));
779        DdNode *res = cuddUniqueConst(dd,value);
780        return(res);
781    }
782    return(NULL);
783
784} /* end of Cudd_addLog */
785
786
787/*---------------------------------------------------------------------------*/
788/* Definition of internal functions                                          */
789/*---------------------------------------------------------------------------*/
790
791
792/**Function********************************************************************
793
794  Synopsis    [Performs the recursive step of Cudd_addApply.]
795
796  Description [Performs the recursive step of Cudd_addApply. Returns a
797  pointer to the result if successful; NULL otherwise.]
798
799  SideEffects [None]
800
801  SeeAlso     [cuddAddMonadicApplyRecur]
802
803******************************************************************************/
804DdNode *
805cuddAddApplyRecur(
806  DdManager * dd,
807  DD_AOP op,
808  DdNode * f,
809  DdNode * g)
810{
811    DdNode *res,
812           *fv, *fvn, *gv, *gvn,
813           *T, *E;
814    unsigned int ford, gord;
815    unsigned int index;
816    DD_CTFP cacheOp;
817
818    /* Check terminal cases. Op may swap f and g to increase the
819     * cache hit rate.
820     */
821    statLine(dd);
822    res = (*op)(dd,&f,&g);
823    if (res != NULL) return(res);
824
825    /* Check cache. */
826    cacheOp = (DD_CTFP) op;
827    res = cuddCacheLookup2(dd,cacheOp,f,g);
828    if (res != NULL) return(res);
829
830    /* Recursive step. */
831    ford = cuddI(dd,f->index);
832    gord = cuddI(dd,g->index);
833    if (ford <= gord) {
834        index = f->index;
835        fv = cuddT(f);
836        fvn = cuddE(f);
837    } else {
838        index = g->index;
839        fv = fvn = f;
840    }
841    if (gord <= ford) {
842        gv = cuddT(g);
843        gvn = cuddE(g);
844    } else {
845        gv = gvn = g;
846    }
847
848    T = cuddAddApplyRecur(dd,op,fv,gv);
849    if (T == NULL) return(NULL);
850    cuddRef(T);
851
852    E = cuddAddApplyRecur(dd,op,fvn,gvn);
853    if (E == NULL) {
854        Cudd_RecursiveDeref(dd,T);
855        return(NULL);
856    }
857    cuddRef(E);
858
859    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
860    if (res == NULL) {
861        Cudd_RecursiveDeref(dd, T);
862        Cudd_RecursiveDeref(dd, E);
863        return(NULL);
864    }
865    cuddDeref(T);
866    cuddDeref(E);
867
868    /* Store result. */
869    cuddCacheInsert2(dd,cacheOp,f,g,res);
870
871    return(res);
872
873} /* end of cuddAddApplyRecur */
874
875
876/**Function********************************************************************
877
878  Synopsis    [Performs the recursive step of Cudd_addMonadicApply.]
879
880  Description [Performs the recursive step of Cudd_addMonadicApply. Returns a
881  pointer to the result if successful; NULL otherwise.]
882
883  SideEffects [None]
884
885  SeeAlso     [cuddAddApplyRecur]
886
887******************************************************************************/
888DdNode *
889cuddAddMonadicApplyRecur(
890  DdManager * dd,
891  DD_MAOP op,
892  DdNode * f)
893{
894    DdNode *res, *ft, *fe, *T, *E;
895    unsigned int index;
896
897    /* Check terminal cases. */
898    statLine(dd);
899    res = (*op)(dd,f);
900    if (res != NULL) return(res);
901
902    /* Check cache. */
903    res = cuddCacheLookup1(dd,op,f);
904    if (res != NULL) return(res);
905
906    /* Recursive step. */
907    index = f->index;
908    ft = cuddT(f);
909    fe = cuddE(f);
910
911    T = cuddAddMonadicApplyRecur(dd,op,ft);
912    if (T == NULL) return(NULL);
913    cuddRef(T);
914
915    E = cuddAddMonadicApplyRecur(dd,op,fe);
916    if (E == NULL) {
917        Cudd_RecursiveDeref(dd,T);
918        return(NULL);
919    }
920    cuddRef(E);
921
922    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
923    if (res == NULL) {
924        Cudd_RecursiveDeref(dd, T);
925        Cudd_RecursiveDeref(dd, E);
926        return(NULL);
927    }
928    cuddDeref(T);
929    cuddDeref(E);
930
931    /* Store result. */
932    cuddCacheInsert1(dd,op,f,res);
933
934    return(res);
935
936} /* end of cuddAddMonadicApplyRecur */
937
938
939/*---------------------------------------------------------------------------*/
940/* Definition of static functions                                            */
941/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.