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

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

library glu 2.3

File size: 33.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddBddIte.c]
4
5  PackageName [cudd]
6
7  Synopsis    [BDD ITE function and satellites.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_bddIte()
12                <li> Cudd_bddIteConstant()
13                <li> Cudd_bddIntersect()
14                <li> Cudd_bddAnd()
15                <li> Cudd_bddAndLimit()
16                <li> Cudd_bddOr()
17                <li> Cudd_bddNand()
18                <li> Cudd_bddNor()
19                <li> Cudd_bddXor()
20                <li> Cudd_bddXnor()
21                <li> Cudd_bddLeq()
22                </ul>
23       Internal procedures included in this module:
24                <ul>
25                <li> cuddBddIteRecur()
26                <li> cuddBddIntersectRecur()
27                <li> cuddBddAndRecur()
28                <li> cuddBddXorRecur()
29                </ul>
30       Static procedures included in this module:
31                <ul>
32                <li> bddVarToConst()
33                <li> bddVarToCanonical()
34                <li> bddVarToCanonicalSimple()
35                </ul>]
36
37  SeeAlso     []
38
39  Author      [Fabio Somenzi]
40
41  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
42
43  All rights reserved.
44
45  Redistribution and use in source and binary forms, with or without
46  modification, are permitted provided that the following conditions
47  are met:
48
49  Redistributions of source code must retain the above copyright
50  notice, this list of conditions and the following disclaimer.
51
52  Redistributions in binary form must reproduce the above copyright
53  notice, this list of conditions and the following disclaimer in the
54  documentation and/or other materials provided with the distribution.
55
56  Neither the name of the University of Colorado nor the names of its
57  contributors may be used to endorse or promote products derived from
58  this software without specific prior written permission.
59
60  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
61  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
62  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
63  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
64  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
65  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
66  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
67  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
68  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
69  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
70  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
71  POSSIBILITY OF SUCH DAMAGE.]
72
73******************************************************************************/
74
75#include "util.h"
76#include "cuddInt.h"
77
78
79/*---------------------------------------------------------------------------*/
80/* Constant declarations                                                     */
81/*---------------------------------------------------------------------------*/
82
83
84/*---------------------------------------------------------------------------*/
85/* Stucture declarations                                                     */
86/*---------------------------------------------------------------------------*/
87
88
89/*---------------------------------------------------------------------------*/
90/* Type declarations                                                         */
91/*---------------------------------------------------------------------------*/
92
93
94/*---------------------------------------------------------------------------*/
95/* Variable declarations                                                     */
96/*---------------------------------------------------------------------------*/
97
98#ifndef lint
99static char rcsid[] DD_UNUSED = "$Id: cuddBddIte.c,v 1.24 2004/08/13 18:04:46 fabio Exp $";
100#endif
101
102/*---------------------------------------------------------------------------*/
103/* Macro declarations                                                        */
104/*---------------------------------------------------------------------------*/
105
106
107/**AutomaticStart*************************************************************/
108
109/*---------------------------------------------------------------------------*/
110/* Static function prototypes                                                */
111/*---------------------------------------------------------------------------*/
112
113static void bddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one);
114static int bddVarToCanonical (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp);
115static int bddVarToCanonicalSimple (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp);
116
117/**AutomaticEnd***************************************************************/
118
119
120/*---------------------------------------------------------------------------*/
121/* Definition of exported functions                                          */
122/*---------------------------------------------------------------------------*/
123
124
125/**Function********************************************************************
126
127  Synopsis    [Implements ITE(f,g,h).]
128
129  Description [Implements ITE(f,g,h). Returns a pointer to the
130  resulting BDD if successful; NULL if the intermediate result blows
131  up.]
132
133  SideEffects [None]
134
135  SeeAlso     [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect]
136
137******************************************************************************/
138DdNode *
139Cudd_bddIte(
140  DdManager * dd,
141  DdNode * f,
142  DdNode * g,
143  DdNode * h)
144{
145    DdNode *res;
146
147    do {
148        dd->reordered = 0;
149        res = cuddBddIteRecur(dd,f,g,h);
150    } while (dd->reordered == 1);
151    return(res);
152
153} /* end of Cudd_bddIte */
154
155
156/**Function********************************************************************
157
158  Synopsis    [Implements ITEconstant(f,g,h).]
159
160  Description [Implements ITEconstant(f,g,h). Returns a pointer to the
161  resulting BDD (which may or may not be constant) or DD_NON_CONSTANT.
162  No new nodes are created.]
163
164  SideEffects [None]
165
166  SeeAlso     [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]
167
168******************************************************************************/
169DdNode *
170Cudd_bddIteConstant(
171  DdManager * dd,
172  DdNode * f,
173  DdNode * g,
174  DdNode * h)
175{
176    DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
177    DdNode       *one = DD_ONE(dd);
178    DdNode       *zero = Cudd_Not(one);
179    int          comple;
180    unsigned int topf, topg, toph, v;
181
182    statLine(dd);
183    /* Trivial cases. */
184    if (f == one)                       /* ITE(1,G,H) => G */
185        return(g);
186   
187    if (f == zero)                      /* ITE(0,G,H) => H */
188        return(h);
189   
190    /* f now not a constant. */
191    bddVarToConst(f, &g, &h, one);      /* possibly convert g or h */
192                                        /* to constants */
193
194    if (g == h)                         /* ITE(F,G,G) => G */
195        return(g);
196
197    if (Cudd_IsConstant(g) && Cudd_IsConstant(h)) 
198        return(DD_NON_CONSTANT);        /* ITE(F,1,0) or ITE(F,0,1) */
199                                        /* => DD_NON_CONSTANT */
200   
201    if (g == Cudd_Not(h))
202        return(DD_NON_CONSTANT);        /* ITE(F,G,G') => DD_NON_CONSTANT */
203                                        /* if F != G and F != G' */
204   
205    comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);
206
207    /* Cache lookup. */
208    r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);
209    if (r != NULL) {
210        return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));
211    }
212
213    v = ddMin(topg, toph);
214
215    /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */
216    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
217        return(DD_NON_CONSTANT);
218    }
219
220    /* Compute cofactors. */
221    if (topf <= v) {
222        v = ddMin(topf, v);             /* v = top_var(F,G,H) */
223        Fv = cuddT(f); Fnv = cuddE(f);
224    } else {
225        Fv = Fnv = f;
226    }
227
228    if (topg == v) {
229        Gv = cuddT(g); Gnv = cuddE(g);
230    } else {
231        Gv = Gnv = g;
232    }
233
234    if (toph == v) {
235        H = Cudd_Regular(h);
236        Hv = cuddT(H); Hnv = cuddE(H);
237        if (Cudd_IsComplement(h)) {
238            Hv = Cudd_Not(Hv);
239            Hnv = Cudd_Not(Hnv);
240        }
241    } else {
242        Hv = Hnv = h;
243    }
244
245    /* Recursion. */
246    t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);
247    if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) {
248        cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
249        return(DD_NON_CONSTANT);
250    }
251    e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);
252    if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) {
253        cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
254        return(DD_NON_CONSTANT);
255    }
256    cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t);
257    return(Cudd_NotCond(t,comple));
258
259} /* end of Cudd_bddIteConstant */
260
261
262/**Function********************************************************************
263
264  Synopsis    [Returns a function included in the intersection of f and g.]
265
266  Description [Computes a function included in the intersection of f and
267  g. (That is, a witness that the intersection is not empty.)
268  Cudd_bddIntersect tries to build as few new nodes as possible. If the
269  only result of interest is whether f and g intersect,
270  Cudd_bddLeq should be used instead.]
271
272  SideEffects [None]
273
274  SeeAlso     [Cudd_bddLeq Cudd_bddIteConstant]
275
276******************************************************************************/
277DdNode *
278Cudd_bddIntersect(
279  DdManager * dd /* manager */,
280  DdNode * f /* first operand */,
281  DdNode * g /* second operand */)
282{
283    DdNode *res;
284
285    do {
286        dd->reordered = 0;
287        res = cuddBddIntersectRecur(dd,f,g);
288    } while (dd->reordered == 1);
289
290    return(res);
291
292} /* end of Cudd_bddIntersect */
293
294
295/**Function********************************************************************
296
297  Synopsis    [Computes the conjunction of two BDDs f and g.]
298
299  Description [Computes the conjunction of two BDDs f and g. Returns a
300  pointer to the resulting BDD if successful; NULL if the intermediate
301  result blows up.]
302
303  SideEffects [None]
304
305  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect
306  Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
307
308******************************************************************************/
309DdNode *
310Cudd_bddAnd(
311  DdManager * dd,
312  DdNode * f,
313  DdNode * g)
314{
315    DdNode *res;
316
317    do {
318        dd->reordered = 0;
319        res = cuddBddAndRecur(dd,f,g);
320    } while (dd->reordered == 1);
321    return(res);
322
323} /* end of Cudd_bddAnd */
324
325
326/**Function********************************************************************
327
328  Synopsis    [Computes the conjunction of two BDDs f and g.  Returns
329  NULL if too many nodes are required.]
330
331  Description [Computes the conjunction of two BDDs f and g. Returns a
332  pointer to the resulting BDD if successful; NULL if the intermediate
333  result blows up or more new nodes than <code>limit</code> are
334  required.]
335
336  SideEffects [None]
337
338  SeeAlso     [Cudd_bddAnd]
339
340******************************************************************************/
341DdNode *
342Cudd_bddAndLimit(
343  DdManager * dd,
344  DdNode * f,
345  DdNode * g,
346  unsigned int limit)
347{
348    DdNode *res;
349    unsigned int saveLimit = dd->maxLive;
350
351    dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
352    do {
353        dd->reordered = 0;
354        res = cuddBddAndRecur(dd,f,g);
355    } while (dd->reordered == 1);
356    dd->maxLive = saveLimit;
357    return(res);
358
359} /* end of Cudd_bddAndLimit */
360
361
362/**Function********************************************************************
363
364  Synopsis    [Computes the disjunction of two BDDs f and g.]
365
366  Description [Computes the disjunction of two BDDs f and g. Returns a
367  pointer to the resulting BDD if successful; NULL if the intermediate
368  result blows up.]
369
370  SideEffects [None]
371
372  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor
373  Cudd_bddXor Cudd_bddXnor]
374
375******************************************************************************/
376DdNode *
377Cudd_bddOr(
378  DdManager * dd,
379  DdNode * f,
380  DdNode * g)
381{
382    DdNode *res;
383
384    do {
385        dd->reordered = 0;
386        res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
387    } while (dd->reordered == 1);
388    res = Cudd_NotCond(res,res != NULL);
389    return(res);
390
391} /* end of Cudd_bddOr */
392
393
394/**Function********************************************************************
395
396  Synopsis    [Computes the NAND of two BDDs f and g.]
397
398  Description [Computes the NAND of two BDDs f and g. Returns a
399  pointer to the resulting BDD if successful; NULL if the intermediate
400  result blows up.]
401
402  SideEffects [None]
403
404  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor
405  Cudd_bddXor Cudd_bddXnor]
406
407******************************************************************************/
408DdNode *
409Cudd_bddNand(
410  DdManager * dd,
411  DdNode * f,
412  DdNode * g)
413{
414    DdNode *res;
415
416    do {
417        dd->reordered = 0;
418        res = cuddBddAndRecur(dd,f,g);
419    } while (dd->reordered == 1);
420    res = Cudd_NotCond(res,res != NULL);
421    return(res);
422
423} /* end of Cudd_bddNand */
424
425
426/**Function********************************************************************
427
428  Synopsis    [Computes the NOR of two BDDs f and g.]
429
430  Description [Computes the NOR of two BDDs f and g. Returns a
431  pointer to the resulting BDD if successful; NULL if the intermediate
432  result blows up.]
433
434  SideEffects [None]
435
436  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand
437  Cudd_bddXor Cudd_bddXnor]
438
439******************************************************************************/
440DdNode *
441Cudd_bddNor(
442  DdManager * dd,
443  DdNode * f,
444  DdNode * g)
445{
446    DdNode *res;
447
448    do {
449        dd->reordered = 0;
450        res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
451    } while (dd->reordered == 1);
452    return(res);
453
454} /* end of Cudd_bddNor */
455
456
457/**Function********************************************************************
458
459  Synopsis    [Computes the exclusive OR of two BDDs f and g.]
460
461  Description [Computes the exclusive OR of two BDDs f and g. Returns a
462  pointer to the resulting BDD if successful; NULL if the intermediate
463  result blows up.]
464
465  SideEffects [None]
466
467  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
468  Cudd_bddNand Cudd_bddNor Cudd_bddXnor]
469
470******************************************************************************/
471DdNode *
472Cudd_bddXor(
473  DdManager * dd,
474  DdNode * f,
475  DdNode * g)
476{
477    DdNode *res;
478
479    do {
480        dd->reordered = 0;
481        res = cuddBddXorRecur(dd,f,g);
482    } while (dd->reordered == 1);
483    return(res);
484
485} /* end of Cudd_bddXor */
486
487
488/**Function********************************************************************
489
490  Synopsis    [Computes the exclusive NOR of two BDDs f and g.]
491
492  Description [Computes the exclusive NOR of two BDDs f and g. Returns a
493  pointer to the resulting BDD if successful; NULL if the intermediate
494  result blows up.]
495
496  SideEffects [None]
497
498  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
499  Cudd_bddNand Cudd_bddNor Cudd_bddXor]
500
501******************************************************************************/
502DdNode *
503Cudd_bddXnor(
504  DdManager * dd,
505  DdNode * f,
506  DdNode * g)
507{
508    DdNode *res;
509
510    do {
511        dd->reordered = 0;
512        res = cuddBddXorRecur(dd,f,Cudd_Not(g));
513    } while (dd->reordered == 1);
514    return(res);
515
516} /* end of Cudd_bddXnor */
517
518
519/**Function********************************************************************
520
521  Synopsis    [Determines whether f is less than or equal to g.]
522
523  Description [Returns 1 if f is less than or equal to g; 0 otherwise.
524  No new nodes are created.]
525
526  SideEffects [None]
527
528  SeeAlso     [Cudd_bddIteConstant Cudd_addEvalConst]
529
530******************************************************************************/
531int
532Cudd_bddLeq(
533  DdManager * dd,
534  DdNode * f,
535  DdNode * g)
536{
537    DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn;
538    unsigned int topf, topg, res;
539
540    statLine(dd);
541    /* Terminal cases and normalization. */
542    if (f == g) return(1);
543
544    if (Cudd_IsComplement(g)) {
545        /* Special case: if f is regular and g is complemented,
546        ** f(1,...,1) = 1 > 0 = g(1,...,1).
547        */
548        if (!Cudd_IsComplement(f)) return(0);
549        /* Both are complemented: Swap and complement because
550        ** f <= g <=> g' <= f' and we want the second argument to be regular.
551        */
552        tmp = g;
553        g = Cudd_Not(f);
554        f = Cudd_Not(tmp);
555    } else if (Cudd_IsComplement(f) && g < f) {
556        tmp = g;
557        g = Cudd_Not(f);
558        f = Cudd_Not(tmp);
559    }
560
561    /* Now g is regular and, if f is not regular, f < g. */
562    one = DD_ONE(dd);
563    if (g == one) return(1);    /* no need to test against zero */
564    if (f == one) return(0);    /* since at this point g != one */
565    if (Cudd_Not(f) == g) return(0); /* because neither is constant */
566    zero = Cudd_Not(one);
567    if (f == zero) return(1);
568
569    /* Here neither f nor g is constant. */
570
571    /* Check cache. */
572    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);
573    if (tmp != NULL) {
574        return(tmp == one);
575    }
576
577    /* Compute cofactors. */
578    F = Cudd_Regular(f);
579    topf = dd->perm[F->index];
580    topg = dd->perm[g->index];
581    if (topf <= topg) {
582        fv = cuddT(F); fvn = cuddE(F);
583        if (f != F) {
584            fv = Cudd_Not(fv);
585            fvn = Cudd_Not(fvn);
586        }
587    } else {
588        fv = fvn = f;
589    }
590    if (topg <= topf) {
591        gv = cuddT(g); gvn = cuddE(g);
592    } else {
593        gv = gvn = g;
594    }
595
596    /* Recursive calls. Since we want to maximize the probability of
597    ** the special case f(1,...,1) > g(1,...,1), we consider the negative
598    ** cofactors first. Indeed, the complementation parity of the positive
599    ** cofactors is the same as the one of the parent functions.
600    */
601    res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
602
603    /* Store result in cache and return. */
604    cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero));
605    return(res);
606
607} /* end of Cudd_bddLeq */
608
609
610/*---------------------------------------------------------------------------*/
611/* Definition of internal functions                                          */
612/*---------------------------------------------------------------------------*/
613
614
615/**Function********************************************************************
616
617  Synopsis    [Implements the recursive step of Cudd_bddIte.]
618
619  Description [Implements the recursive step of Cudd_bddIte. Returns a
620  pointer to the resulting BDD. NULL if the intermediate result blows
621  up or if reordering occurs.]
622
623  SideEffects [None]
624
625  SeeAlso     []
626
627******************************************************************************/
628DdNode *
629cuddBddIteRecur(
630  DdManager * dd,
631  DdNode * f,
632  DdNode * g,
633  DdNode * h)
634{
635    DdNode       *one, *zero, *res;
636    DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
637    unsigned int topf, topg, toph, v;
638    int          index;
639    int          comple;
640
641    statLine(dd);
642    /* Terminal cases. */
643
644    /* One variable cases. */
645    if (f == (one = DD_ONE(dd)))        /* ITE(1,G,H) = G */
646        return(g);
647   
648    if (f == (zero = Cudd_Not(one)))    /* ITE(0,G,H) = H */
649        return(h);
650   
651    /* From now on, f is known not to be a constant. */
652    if (g == one || f == g) {   /* ITE(F,F,H) = ITE(F,1,H) = F + H */
653        if (h == zero) {        /* ITE(F,1,0) = F */
654            return(f);
655        } else {
656            res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));
657            return(Cudd_NotCond(res,res != NULL));
658        }
659    } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
660        if (h == one) {         /* ITE(F,0,1) = !F */
661            return(Cudd_Not(f));
662        } else {
663            res = cuddBddAndRecur(dd,Cudd_Not(f),h);
664            return(res);
665        }
666    }
667    if (h == zero || f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
668        res = cuddBddAndRecur(dd,f,g);
669        return(res);
670    } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
671        res = cuddBddAndRecur(dd,f,Cudd_Not(g));
672        return(Cudd_NotCond(res,res != NULL));
673    }
674
675    /* Check remaining one variable case. */
676    if (g == h) {               /* ITE(F,G,G) = G */
677        return(g);
678    } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */
679        res = cuddBddXorRecur(dd,f,h);
680        return(res);
681    }
682   
683    /* From here, there are no constants. */
684    comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);
685
686    /* f & g are now regular pointers */
687
688    v = ddMin(topg, toph);
689
690    /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */
691    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
692        r = cuddUniqueInter(dd, (int) f->index, g, h);
693        return(Cudd_NotCond(r,comple && r != NULL));
694    }
695
696    /* Check cache. */
697    r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);
698    if (r != NULL) {
699        return(Cudd_NotCond(r,comple));
700    }
701
702    /* Compute cofactors. */
703    if (topf <= v) {
704        v = ddMin(topf, v);     /* v = top_var(F,G,H) */
705        index = f->index;
706        Fv = cuddT(f); Fnv = cuddE(f);
707    } else {
708        Fv = Fnv = f;
709    }
710    if (topg == v) {
711        index = g->index;
712        Gv = cuddT(g); Gnv = cuddE(g);
713    } else {
714        Gv = Gnv = g;
715    }
716    if (toph == v) {
717        H = Cudd_Regular(h);
718        index = H->index;
719        Hv = cuddT(H); Hnv = cuddE(H);
720        if (Cudd_IsComplement(h)) {
721            Hv = Cudd_Not(Hv);
722            Hnv = Cudd_Not(Hnv);
723        }
724    } else {
725        Hv = Hnv = h;
726    }
727
728    /* Recursive step. */
729    t = cuddBddIteRecur(dd,Fv,Gv,Hv);
730    if (t == NULL) return(NULL);
731    cuddRef(t);
732
733    e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv);
734    if (e == NULL) {
735        Cudd_IterDerefBdd(dd,t);
736        return(NULL);
737    }
738    cuddRef(e);
739
740    r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
741    if (r == NULL) {
742        Cudd_IterDerefBdd(dd,t);
743        Cudd_IterDerefBdd(dd,e);
744        return(NULL);
745    }
746    cuddDeref(t);
747    cuddDeref(e);
748
749    cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r);
750    return(Cudd_NotCond(r,comple));
751
752} /* end of cuddBddIteRecur */
753
754
755/**Function********************************************************************
756
757  Synopsis    [Implements the recursive step of Cudd_bddIntersect.]
758
759  Description []
760
761  SideEffects [None]
762
763  SeeAlso     [Cudd_bddIntersect]
764
765******************************************************************************/
766DdNode *
767cuddBddIntersectRecur(
768  DdManager * dd,
769  DdNode * f,
770  DdNode * g)
771{
772    DdNode *res;
773    DdNode *F, *G, *t, *e;
774    DdNode *fv, *fnv, *gv, *gnv;
775    DdNode *one, *zero;
776    unsigned int index, topf, topg;
777
778    statLine(dd);
779    one = DD_ONE(dd);
780    zero = Cudd_Not(one);
781
782    /* Terminal cases. */
783    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
784    if (f == g || g == one) return(f);
785    if (f == one) return(g);
786
787    /* At this point f and g are not constant. */
788    if (f > g) { DdNode *tmp = f; f = g; g = tmp; }
789    res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
790    if (res != NULL) return(res);
791
792    /* Find splitting variable. Here we can skip the use of cuddI,
793    ** because the operands are known to be non-constant.
794    */
795    F = Cudd_Regular(f);
796    topf = dd->perm[F->index];
797    G = Cudd_Regular(g);
798    topg = dd->perm[G->index];
799
800    /* Compute cofactors. */
801    if (topf <= topg) {
802        index = F->index;
803        fv = cuddT(F);
804        fnv = cuddE(F);
805        if (Cudd_IsComplement(f)) {
806            fv = Cudd_Not(fv);
807            fnv = Cudd_Not(fnv);
808        }
809    } else {
810        index = G->index;
811        fv = fnv = f;
812    }
813
814    if (topg <= topf) {
815        gv = cuddT(G);
816        gnv = cuddE(G);
817        if (Cudd_IsComplement(g)) {
818            gv = Cudd_Not(gv);
819            gnv = Cudd_Not(gnv);
820        }
821    } else {
822        gv = gnv = g;
823    }
824
825    /* Compute partial results. */
826    t = cuddBddIntersectRecur(dd,fv,gv);
827    if (t == NULL) return(NULL);
828    cuddRef(t);
829    if (t != zero) {
830        e = zero;
831    } else {
832        e = cuddBddIntersectRecur(dd,fnv,gnv);
833        if (e == NULL) {
834            Cudd_IterDerefBdd(dd, t);
835            return(NULL);
836        }
837    }
838    cuddRef(e);
839
840    if (t == e) { /* both equal zero */
841        res = t;
842    } else if (Cudd_IsComplement(t)) {
843        res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));
844        if (res == NULL) {
845            Cudd_IterDerefBdd(dd, t);
846            Cudd_IterDerefBdd(dd, e);
847            return(NULL);
848        }
849        res = Cudd_Not(res);
850    } else {
851        res = cuddUniqueInter(dd,(int)index,t,e);
852        if (res == NULL) {
853            Cudd_IterDerefBdd(dd, t);
854            Cudd_IterDerefBdd(dd, e);
855            return(NULL);
856        }
857    }
858    cuddDeref(e);
859    cuddDeref(t);
860
861    cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res);
862
863    return(res);
864
865} /* end of cuddBddIntersectRecur */
866
867
868/**Function********************************************************************
869
870  Synopsis [Implements the recursive step of Cudd_bddAnd.]
871
872  Description [Implements the recursive step of Cudd_bddAnd by taking
873  the conjunction of two BDDs.  Returns a pointer to the result is
874  successful; NULL otherwise.]
875
876  SideEffects [None]
877
878  SeeAlso     [Cudd_bddAnd]
879
880******************************************************************************/
881DdNode *
882cuddBddAndRecur(
883  DdManager * manager,
884  DdNode * f,
885  DdNode * g)
886{
887    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
888    DdNode *one, *r, *t, *e;
889    unsigned int topf, topg, index;
890
891    statLine(manager);
892    one = DD_ONE(manager);
893
894    /* Terminal cases. */
895    F = Cudd_Regular(f);
896    G = Cudd_Regular(g);
897    if (F == G) {
898        if (f == g) return(f);
899        else return(Cudd_Not(one));
900    }
901    if (F == one) {
902        if (f == one) return(g);
903        else return(f);
904    }
905    if (G == one) {
906        if (g == one) return(f);
907        else return(g);
908    }
909
910    /* At this point f and g are not constant. */
911    if (f > g) { /* Try to increase cache efficiency. */
912        DdNode *tmp = f;
913        f = g;
914        g = tmp;
915        F = Cudd_Regular(f);
916        G = Cudd_Regular(g);
917    }
918
919    /* Check cache. */
920    if (F->ref != 1 || G->ref != 1) {
921        r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
922        if (r != NULL) return(r);
923    }
924
925    /* Here we can skip the use of cuddI, because the operands are known
926    ** to be non-constant.
927    */
928    topf = manager->perm[F->index];
929    topg = manager->perm[G->index];
930
931    /* Compute cofactors. */
932    if (topf <= topg) {
933        index = F->index;
934        fv = cuddT(F);
935        fnv = cuddE(F);
936        if (Cudd_IsComplement(f)) {
937            fv = Cudd_Not(fv);
938            fnv = Cudd_Not(fnv);
939        }
940    } else {
941        index = G->index;
942        fv = fnv = f;
943    }
944
945    if (topg <= topf) {
946        gv = cuddT(G);
947        gnv = cuddE(G);
948        if (Cudd_IsComplement(g)) {
949            gv = Cudd_Not(gv);
950            gnv = Cudd_Not(gnv);
951        }
952    } else {
953        gv = gnv = g;
954    }
955
956    t = cuddBddAndRecur(manager, fv, gv);
957    if (t == NULL) return(NULL);
958    cuddRef(t);
959
960    e = cuddBddAndRecur(manager, fnv, gnv);
961    if (e == NULL) {
962        Cudd_IterDerefBdd(manager, t);
963        return(NULL);
964    }
965    cuddRef(e);
966
967    if (t == e) {
968        r = t;
969    } else {
970        if (Cudd_IsComplement(t)) {
971            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
972            if (r == NULL) {
973                Cudd_IterDerefBdd(manager, t);
974                Cudd_IterDerefBdd(manager, e);
975                return(NULL);
976            }
977            r = Cudd_Not(r);
978        } else {
979            r = cuddUniqueInter(manager,(int)index,t,e);
980            if (r == NULL) {
981                Cudd_IterDerefBdd(manager, t);
982                Cudd_IterDerefBdd(manager, e);
983                return(NULL);
984            }
985        }
986    }
987    cuddDeref(e);
988    cuddDeref(t);
989    if (F->ref != 1 || G->ref != 1)
990        cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
991    return(r);
992
993} /* end of cuddBddAndRecur */
994
995
996/**Function********************************************************************
997
998  Synopsis [Implements the recursive step of Cudd_bddXor.]
999
1000  Description [Implements the recursive step of Cudd_bddXor by taking
1001  the exclusive OR of two BDDs.  Returns a pointer to the result is
1002  successful; NULL otherwise.]
1003
1004  SideEffects [None]
1005
1006  SeeAlso     [Cudd_bddXor]
1007
1008******************************************************************************/
1009DdNode *
1010cuddBddXorRecur(
1011  DdManager * manager,
1012  DdNode * f,
1013  DdNode * g)
1014{
1015    DdNode *fv, *fnv, *G, *gv, *gnv;
1016    DdNode *one, *zero, *r, *t, *e;
1017    unsigned int topf, topg, index;
1018
1019    statLine(manager);
1020    one = DD_ONE(manager);
1021    zero = Cudd_Not(one);
1022
1023    /* Terminal cases. */
1024    if (f == g) return(zero);
1025    if (f == Cudd_Not(g)) return(one);
1026    if (f > g) { /* Try to increase cache efficiency and simplify tests. */
1027        DdNode *tmp = f;
1028        f = g;
1029        g = tmp;
1030    }
1031    if (g == zero) return(f);
1032    if (g == one) return(Cudd_Not(f));
1033    if (Cudd_IsComplement(f)) {
1034        f = Cudd_Not(f);
1035        g = Cudd_Not(g);
1036    }
1037    /* Now the first argument is regular. */
1038    if (f == one) return(Cudd_Not(g));
1039
1040    /* At this point f and g are not constant. */
1041
1042    /* Check cache. */
1043    r = cuddCacheLookup2(manager, Cudd_bddXor, f, g);
1044    if (r != NULL) return(r);
1045
1046    /* Here we can skip the use of cuddI, because the operands are known
1047    ** to be non-constant.
1048    */
1049    topf = manager->perm[f->index];
1050    G = Cudd_Regular(g);
1051    topg = manager->perm[G->index];
1052
1053    /* Compute cofactors. */
1054    if (topf <= topg) {
1055        index = f->index;
1056        fv = cuddT(f);
1057        fnv = cuddE(f);
1058    } else {
1059        index = G->index;
1060        fv = fnv = f;
1061    }
1062
1063    if (topg <= topf) {
1064        gv = cuddT(G);
1065        gnv = cuddE(G);
1066        if (Cudd_IsComplement(g)) {
1067            gv = Cudd_Not(gv);
1068            gnv = Cudd_Not(gnv);
1069        }
1070    } else {
1071        gv = gnv = g;
1072    }
1073
1074    t = cuddBddXorRecur(manager, fv, gv);
1075    if (t == NULL) return(NULL);
1076    cuddRef(t);
1077
1078    e = cuddBddXorRecur(manager, fnv, gnv);
1079    if (e == NULL) {
1080        Cudd_IterDerefBdd(manager, t);
1081        return(NULL);
1082    }
1083    cuddRef(e);
1084
1085    if (t == e) {
1086        r = t;
1087    } else {
1088        if (Cudd_IsComplement(t)) {
1089            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
1090            if (r == NULL) {
1091                Cudd_IterDerefBdd(manager, t);
1092                Cudd_IterDerefBdd(manager, e);
1093                return(NULL);
1094            }
1095            r = Cudd_Not(r);
1096        } else {
1097            r = cuddUniqueInter(manager,(int)index,t,e);
1098            if (r == NULL) {
1099                Cudd_IterDerefBdd(manager, t);
1100                Cudd_IterDerefBdd(manager, e);
1101                return(NULL);
1102            }
1103        }
1104    }
1105    cuddDeref(e);
1106    cuddDeref(t);
1107    cuddCacheInsert2(manager, Cudd_bddXor, f, g, r);
1108    return(r);
1109
1110} /* end of cuddBddXorRecur */
1111
1112
1113/*---------------------------------------------------------------------------*/
1114/* Definition of static functions                                            */
1115/*---------------------------------------------------------------------------*/
1116
1117
1118/**Function********************************************************************
1119
1120  Synopsis [Replaces variables with constants if possible.]
1121
1122  Description [This function performs part of the transformation to
1123  standard form by replacing variables with constants if possible.]
1124
1125  SideEffects [None]
1126
1127  SeeAlso     [bddVarToCanonical bddVarToCanonicalSimple]
1128
1129******************************************************************************/
1130static void
1131bddVarToConst(
1132  DdNode * f,
1133  DdNode ** gp,
1134  DdNode ** hp,
1135  DdNode * one)
1136{
1137    DdNode *g = *gp;
1138    DdNode *h = *hp;
1139
1140    if (f == g) {    /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1141        *gp = one;
1142    } else if (f == Cudd_Not(g)) {    /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
1143        *gp = Cudd_Not(one);
1144    }
1145    if (f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1146        *hp = Cudd_Not(one);
1147    } else if (f == Cudd_Not(h)) {    /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
1148        *hp = one;
1149    }
1150
1151} /* end of bddVarToConst */
1152
1153
1154/**Function********************************************************************
1155
1156  Synopsis [Picks unique member from equiv expressions.]
1157
1158  Description [Reduces 2 variable expressions to canonical form.]
1159
1160  SideEffects [None]
1161
1162  SeeAlso     [bddVarToConst bddVarToCanonicalSimple]
1163
1164******************************************************************************/
1165static int
1166bddVarToCanonical(
1167  DdManager * dd,
1168  DdNode ** fp,
1169  DdNode ** gp,
1170  DdNode ** hp,
1171  unsigned int * topfp,
1172  unsigned int * topgp,
1173  unsigned int * tophp)
1174{
1175    register DdNode             *F, *G, *H, *r, *f, *g, *h;
1176    register unsigned int       topf, topg, toph;
1177    DdNode                      *one = dd->one;
1178    int                         comple, change;
1179
1180    f = *fp;
1181    g = *gp;
1182    h = *hp;
1183    F = Cudd_Regular(f);
1184    G = Cudd_Regular(g);
1185    H = Cudd_Regular(h);
1186    topf = cuddI(dd,F->index);
1187    topg = cuddI(dd,G->index);
1188    toph = cuddI(dd,H->index);
1189
1190    change = 0;
1191
1192    if (G == one) {                     /* ITE(F,c,H) */
1193        if ((topf > toph) || (topf == toph && f > h)) {
1194            r = h;
1195            h = f;
1196            f = r;                      /* ITE(F,1,H) = ITE(H,1,F) */
1197            if (g != one) {     /* g == zero */
1198                f = Cudd_Not(f);                /* ITE(F,0,H) = ITE(!H,0,!F) */
1199                h = Cudd_Not(h);
1200            }
1201            change = 1;
1202        }
1203    } else if (H == one) {              /* ITE(F,G,c) */
1204        if ((topf > topg) || (topf == topg && f > g)) {
1205            r = g;
1206            g = f;
1207            f = r;                      /* ITE(F,G,0) = ITE(G,F,0) */
1208            if (h == one) {
1209                f = Cudd_Not(f);                /* ITE(F,G,1) = ITE(!G,!F,1) */
1210                g = Cudd_Not(g);
1211            }
1212            change = 1;
1213        }
1214    } else if (g == Cudd_Not(h)) {      /* ITE(F,G,!G) = ITE(G,F,!F) */
1215        if ((topf > topg) || (topf == topg && f > g)) {
1216            r = f;
1217            f = g;
1218            g = r;
1219            h = Cudd_Not(r);
1220            change = 1;
1221        }
1222    }
1223    /* adjust pointers so that the first 2 arguments to ITE are regular */
1224    if (Cudd_IsComplement(f) != 0) {    /* ITE(!F,G,H) = ITE(F,H,G) */
1225        f = Cudd_Not(f);
1226        r = g;
1227        g = h;
1228        h = r;
1229        change = 1;
1230    }
1231    comple = 0;
1232    if (Cudd_IsComplement(g) != 0) {    /* ITE(F,!G,H) = !ITE(F,G,!H) */
1233        g = Cudd_Not(g);
1234        h = Cudd_Not(h);
1235        change = 1;
1236        comple = 1;
1237    }
1238    if (change != 0) {
1239        *fp = f;
1240        *gp = g;
1241        *hp = h;
1242    }
1243    *topfp = cuddI(dd,f->index);
1244    *topgp = cuddI(dd,g->index);
1245    *tophp = cuddI(dd,Cudd_Regular(h)->index);
1246
1247    return(comple);
1248
1249} /* end of bddVarToCanonical */
1250
1251
1252/**Function********************************************************************
1253
1254  Synopsis [Picks unique member from equiv expressions.]
1255
1256  Description [Makes sure the first two pointers are regular.  This
1257  mat require the complementation of the result, which is signaled by
1258  returning 1 instead of 0.  This function is simpler than the general
1259  case because it assumes that no two arguments are the same or
1260  complementary, and no argument is constant.]
1261
1262  SideEffects [None]
1263
1264  SeeAlso     [bddVarToConst bddVarToCanonical]
1265
1266******************************************************************************/
1267static int
1268bddVarToCanonicalSimple(
1269  DdManager * dd,
1270  DdNode ** fp,
1271  DdNode ** gp,
1272  DdNode ** hp,
1273  unsigned int * topfp,
1274  unsigned int * topgp,
1275  unsigned int * tophp)
1276{
1277    register DdNode             *r, *f, *g, *h;
1278    int                         comple, change;
1279
1280    f = *fp;
1281    g = *gp;
1282    h = *hp;
1283
1284    change = 0;
1285
1286    /* adjust pointers so that the first 2 arguments to ITE are regular */
1287    if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */
1288        f = Cudd_Not(f);
1289        r = g;
1290        g = h;
1291        h = r;
1292        change = 1;
1293    }
1294    comple = 0;
1295    if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
1296        g = Cudd_Not(g);
1297        h = Cudd_Not(h);
1298        change = 1;
1299        comple = 1;
1300    }
1301    if (change) {
1302        *fp = f;
1303        *gp = g;
1304        *hp = h;
1305    }
1306
1307    /* Here we can skip the use of cuddI, because the operands are known
1308    ** to be non-constant.
1309    */
1310    *topfp = dd->perm[f->index];
1311    *topgp = dd->perm[g->index];
1312    *tophp = dd->perm[Cudd_Regular(h)->index];
1313
1314    return(comple);
1315
1316} /* end of bddVarToCanonicalSimple */
1317
Note: See TracBrowser for help on using the repository browser.