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

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

library glu 2.3

File size: 35.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddSat.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for the solution of satisfiability related
8  problems.]
9
10  Description [External procedures included in this file:
11                <ul>
12                <li> Cudd_Eval()
13                <li> Cudd_ShortestPath()
14                <li> Cudd_LargestCube()
15                <li> Cudd_ShortestLength()
16                <li> Cudd_Decreasing()
17                <li> Cudd_Increasing()
18                <li> Cudd_EquivDC()
19                <li> Cudd_bddLeqUnless()
20                <li> Cudd_EqualSupNorm()
21                <li> Cudd_bddMakePrime()
22                </ul>
23        Internal procedures included in this module:
24                <ul>
25                <li> cuddBddMakePrime()
26                </ul>
27        Static procedures included in this module:
28                <ul>
29                <li> freePathPair()
30                <li> getShortest()
31                <li> getPath()
32                <li> getLargest()
33                <li> getCube()
34                </ul>]
35
36  Author      [Seh-Woong Jeong, 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#define DD_BIGGY        1000000
80
81/*---------------------------------------------------------------------------*/
82/* Stucture declarations                                                     */
83/*---------------------------------------------------------------------------*/
84
85/*---------------------------------------------------------------------------*/
86/* Type declarations                                                         */
87/*---------------------------------------------------------------------------*/
88
89typedef struct cuddPathPair {
90    int pos;
91    int neg;
92} cuddPathPair;
93
94/*---------------------------------------------------------------------------*/
95/* Variable declarations                                                     */
96/*---------------------------------------------------------------------------*/
97
98#ifndef lint
99static char rcsid[] DD_UNUSED = "$Id: cuddSat.c,v 1.36 2009/03/08 02:49:02 fabio Exp $";
100#endif
101
102static  DdNode  *one, *zero;
103
104/*---------------------------------------------------------------------------*/
105/* Macro declarations                                                        */
106/*---------------------------------------------------------------------------*/
107
108#define WEIGHT(weight, col)     ((weight) == NULL ? 1 : weight[col])
109
110#ifdef __cplusplus
111extern "C" {
112#endif
113
114/**AutomaticStart*************************************************************/
115
116/*---------------------------------------------------------------------------*/
117/* Static function prototypes                                                */
118/*---------------------------------------------------------------------------*/
119
120static enum st_retval freePathPair (char *key, char *value, char *arg);
121static cuddPathPair getShortest (DdNode *root, int *cost, int *support, st_table *visited);
122static DdNode * getPath (DdManager *manager, st_table *visited, DdNode *f, int *weight, int cost);
123static cuddPathPair getLargest (DdNode *root, st_table *visited);
124static DdNode * getCube (DdManager *manager, st_table *visited, DdNode *f, int cost);
125
126/**AutomaticEnd***************************************************************/
127
128#ifdef __cplusplus
129}
130#endif
131
132/*---------------------------------------------------------------------------*/
133/* Definition of exported functions                                          */
134/*---------------------------------------------------------------------------*/
135
136
137/**Function********************************************************************
138
139  Synopsis    [Returns the value of a DD for a given variable assignment.]
140
141  Description [Finds the value of a DD for a given variable
142  assignment. The variable assignment is passed in an array of int's,
143  that should specify a zero or a one for each variable in the support
144  of the function. Returns a pointer to a constant node. No new nodes
145  are produced.]
146
147  SideEffects [None]
148
149  SeeAlso     [Cudd_bddLeq Cudd_addEvalConst]
150
151******************************************************************************/
152DdNode *
153Cudd_Eval(
154  DdManager * dd,
155  DdNode * f,
156  int * inputs)
157{
158    int comple;
159    DdNode *ptr;
160
161    comple = Cudd_IsComplement(f);
162    ptr = Cudd_Regular(f);
163
164    while (!cuddIsConstant(ptr)) {
165        if (inputs[ptr->index] == 1) {
166            ptr = cuddT(ptr);
167        } else {
168            comple ^= Cudd_IsComplement(cuddE(ptr));
169            ptr = Cudd_Regular(cuddE(ptr));
170        }
171    }
172    return(Cudd_NotCond(ptr,comple));
173
174} /* end of Cudd_Eval */
175
176
177/**Function********************************************************************
178
179  Synopsis    [Finds a shortest path in a DD.]
180
181  Description [Finds a shortest path in a DD. f is the DD we want to
182  get the shortest path for; weight\[i\] is the weight of the THEN arc
183  coming from the node whose index is i. If weight is NULL, then unit
184  weights are assumed for all THEN arcs. All ELSE arcs have 0 weight.
185  If non-NULL, both weight and support should point to arrays with at
186  least as many entries as there are variables in the manager.
187  Returns the shortest path as the BDD of a cube.]
188
189  SideEffects [support contains on return the true support of f.
190  If support is NULL on entry, then Cudd_ShortestPath does not compute
191  the true support info. length contains the length of the path.]
192
193  SeeAlso     [Cudd_ShortestLength Cudd_LargestCube]
194
195******************************************************************************/
196DdNode *
197Cudd_ShortestPath(
198  DdManager * manager,
199  DdNode * f,
200  int * weight,
201  int * support,
202  int * length)
203{
204    DdNode      *F;
205    st_table    *visited;
206    DdNode      *sol;
207    cuddPathPair *rootPair;
208    int         complement, cost;
209    int         i;
210
211    one = DD_ONE(manager);
212    zero = DD_ZERO(manager);
213
214    /* Initialize support. Support does not depend on variable order.
215    ** Hence, it does not need to be reinitialized if reordering occurs.
216    */
217    if (support) {
218      for (i = 0; i < manager->size; i++) {
219        support[i] = 0;
220      }
221    }
222
223    if (f == Cudd_Not(one) || f == zero) {
224      *length = DD_BIGGY;
225      return(Cudd_Not(one));
226    }
227    /* From this point on, a path exists. */
228
229    do {
230        manager->reordered = 0;
231
232        /* Initialize visited table. */
233        visited = st_init_table(st_ptrcmp, st_ptrhash);
234
235        /* Now get the length of the shortest path(s) from f to 1. */
236        (void) getShortest(f, weight, support, visited);
237
238        complement = Cudd_IsComplement(f);
239
240        F = Cudd_Regular(f);
241
242        if (!st_lookup(visited, F, &rootPair)) return(NULL);
243
244        if (complement) {
245          cost = rootPair->neg;
246        } else {
247          cost = rootPair->pos;
248        }
249
250        /* Recover an actual shortest path. */
251        sol = getPath(manager,visited,f,weight,cost);
252
253        st_foreach(visited, freePathPair, NULL);
254        st_free_table(visited);
255
256    } while (manager->reordered == 1);
257
258    *length = cost;
259    return(sol);
260
261} /* end of Cudd_ShortestPath */
262
263
264/**Function********************************************************************
265
266  Synopsis    [Finds a largest cube in a DD.]
267
268  Description [Finds a largest cube in a DD. f is the DD we want to
269  get the largest cube for. The problem is translated into the one of
270  finding a shortest path in f, when both THEN and ELSE arcs are assumed to
271  have unit length. This yields a largest cube in the disjoint cover
272  corresponding to the DD. Therefore, it is not necessarily the largest
273  implicant of f.  Returns the largest cube as a BDD.]
274
275  SideEffects [The number of literals of the cube is returned in length.]
276
277  SeeAlso     [Cudd_ShortestPath]
278
279******************************************************************************/
280DdNode *
281Cudd_LargestCube(
282  DdManager * manager,
283  DdNode * f,
284  int * length)
285{
286    register    DdNode  *F;
287    st_table    *visited;
288    DdNode      *sol;
289    cuddPathPair *rootPair;
290    int         complement, cost;
291
292    one = DD_ONE(manager);
293    zero = DD_ZERO(manager);
294
295    if (f == Cudd_Not(one) || f == zero) {
296        *length = DD_BIGGY;
297        return(Cudd_Not(one));
298    }
299    /* From this point on, a path exists. */
300
301    do {
302        manager->reordered = 0;
303
304        /* Initialize visited table. */
305        visited = st_init_table(st_ptrcmp, st_ptrhash);
306
307        /* Now get the length of the shortest path(s) from f to 1. */
308        (void) getLargest(f, visited);
309
310        complement = Cudd_IsComplement(f);
311
312        F = Cudd_Regular(f);
313
314        if (!st_lookup(visited, F, &rootPair)) return(NULL);
315
316        if (complement) {
317          cost = rootPair->neg;
318        } else {
319          cost = rootPair->pos;
320        }
321
322        /* Recover an actual shortest path. */
323        sol = getCube(manager,visited,f,cost);
324
325        st_foreach(visited, freePathPair, NULL);
326        st_free_table(visited);
327
328    } while (manager->reordered == 1);
329
330    *length = cost;
331    return(sol);
332
333} /* end of Cudd_LargestCube */
334
335
336/**Function********************************************************************
337
338  Synopsis    [Find the length of the shortest path(s) in a DD.]
339
340  Description [Find the length of the shortest path(s) in a DD. f is
341  the DD we want to get the shortest path for; weight\[i\] is the
342  weight of the THEN edge coming from the node whose index is i. All
343  ELSE edges have 0 weight. Returns the length of the shortest
344  path(s) if such a path is found; a large number if the function is
345  identically 0, and CUDD_OUT_OF_MEM in case of failure.]
346
347  SideEffects [None]
348
349  SeeAlso     [Cudd_ShortestPath]
350
351******************************************************************************/
352int
353Cudd_ShortestLength(
354  DdManager * manager,
355  DdNode * f,
356  int * weight)
357{
358    register    DdNode  *F;
359    st_table    *visited;
360    cuddPathPair *my_pair;
361    int         complement, cost;
362
363    one = DD_ONE(manager);
364    zero = DD_ZERO(manager);
365
366    if (f == Cudd_Not(one) || f == zero) {
367        return(DD_BIGGY);
368    }
369
370    /* From this point on, a path exists. */
371    /* Initialize visited table and support. */
372    visited = st_init_table(st_ptrcmp, st_ptrhash);
373
374    /* Now get the length of the shortest path(s) from f to 1. */
375    (void) getShortest(f, weight, NULL, visited);
376
377    complement = Cudd_IsComplement(f);
378
379    F = Cudd_Regular(f);
380
381    if (!st_lookup(visited, F, &my_pair)) return(CUDD_OUT_OF_MEM);
382   
383    if (complement) {
384        cost = my_pair->neg;
385    } else {
386        cost = my_pair->pos;
387    }
388
389    st_foreach(visited, freePathPair, NULL);
390    st_free_table(visited);
391
392    return(cost);
393
394} /* end of Cudd_ShortestLength */
395
396
397/**Function********************************************************************
398
399  Synopsis    [Determines whether a BDD is negative unate in a
400  variable.]
401
402  Description [Determines whether the function represented by BDD f is
403  negative unate (monotonic decreasing) in variable i. Returns the
404  constant one is f is unate and the (logical) constant zero if it is not.
405  This function does not generate any new nodes.]
406
407  SideEffects [None]
408
409  SeeAlso     [Cudd_Increasing]
410
411******************************************************************************/
412DdNode *
413Cudd_Decreasing(
414  DdManager * dd,
415  DdNode * f,
416  int  i)
417{
418    unsigned int topf, level;
419    DdNode *F, *fv, *fvn, *res;
420    DD_CTFP cacheOp;
421
422    statLine(dd);
423#ifdef DD_DEBUG
424    assert(0 <= i && i < dd->size);
425#endif
426
427    F = Cudd_Regular(f);
428    topf = cuddI(dd,F->index);
429
430    /* Check terminal case. If topf > i, f does not depend on var.
431    ** Therefore, f is unate in i.
432    */
433    level = (unsigned) dd->perm[i];
434    if (topf > level) {
435        return(DD_ONE(dd));
436    }
437
438    /* From now on, f is not constant. */
439
440    /* Check cache. */
441    cacheOp = (DD_CTFP) Cudd_Decreasing;
442    res = cuddCacheLookup2(dd,cacheOp,f,dd->vars[i]);
443    if (res != NULL) {
444        return(res);
445    }
446
447    /* Compute cofactors. */
448    fv = cuddT(F); fvn = cuddE(F);
449    if (F != f) {
450        fv = Cudd_Not(fv);
451        fvn = Cudd_Not(fvn);
452    }
453
454    if (topf == (unsigned) level) {
455        /* Special case: if fv is regular, fv(1,...,1) = 1;
456        ** If in addition fvn is complemented, fvn(1,...,1) = 0.
457        ** But then f(1,1,...,1) > f(0,1,...,1). Hence f is not
458        ** monotonic decreasing in i.
459        */
460        if (!Cudd_IsComplement(fv) && Cudd_IsComplement(fvn)) {
461            return(Cudd_Not(DD_ONE(dd)));
462        }
463        res = Cudd_bddLeq(dd,fv,fvn) ? DD_ONE(dd) : Cudd_Not(DD_ONE(dd));
464    } else {
465        res = Cudd_Decreasing(dd,fv,i);
466        if (res == DD_ONE(dd)) {
467            res = Cudd_Decreasing(dd,fvn,i);
468        }
469    }
470
471    cuddCacheInsert2(dd,cacheOp,f,dd->vars[i],res);
472    return(res);
473
474} /* end of Cudd_Decreasing */
475
476
477/**Function********************************************************************
478
479  Synopsis    [Determines whether a BDD is positive unate in a
480  variable.]
481
482  Description [Determines whether the function represented by BDD f is
483  positive unate (monotonic increasing) in variable i. It is based on
484  Cudd_Decreasing and the fact that f is monotonic increasing in i if
485  and only if its complement is monotonic decreasing in i.]
486
487  SideEffects [None]
488
489  SeeAlso     [Cudd_Decreasing]
490
491******************************************************************************/
492DdNode *
493Cudd_Increasing(
494  DdManager * dd,
495  DdNode * f,
496  int  i)
497{
498    return(Cudd_Decreasing(dd,Cudd_Not(f),i));
499
500} /* end of Cudd_Increasing */
501
502
503/**Function********************************************************************
504
505  Synopsis    [Tells whether F and G are identical wherever D is 0.]
506
507  Description [Tells whether F and G are identical wherever D is 0.  F
508  and G are either two ADDs or two BDDs.  D is either a 0-1 ADD or a
509  BDD.  The function returns 1 if F and G are equivalent, and 0
510  otherwise.  No new nodes are created.]
511
512  SideEffects [None]
513
514  SeeAlso     [Cudd_bddLeqUnless]
515
516******************************************************************************/
517int
518Cudd_EquivDC(
519  DdManager * dd,
520  DdNode * F,
521  DdNode * G,
522  DdNode * D)
523{
524    DdNode *tmp, *One, *Gr, *Dr;
525    DdNode *Fv, *Fvn, *Gv, *Gvn, *Dv, *Dvn;
526    int res;
527    unsigned int flevel, glevel, dlevel, top;
528
529    One = DD_ONE(dd);
530
531    statLine(dd);
532    /* Check terminal cases. */
533    if (D == One || F == G) return(1);
534    if (D == Cudd_Not(One) || D == DD_ZERO(dd) || F == Cudd_Not(G)) return(0);
535
536    /* From now on, D is non-constant. */
537
538    /* Normalize call to increase cache efficiency. */
539    if (F > G) {
540        tmp = F;
541        F = G;
542        G = tmp;
543    }
544    if (Cudd_IsComplement(F)) {
545        F = Cudd_Not(F);
546        G = Cudd_Not(G);
547    }
548
549    /* From now on, F is regular. */
550
551    /* Check cache. */
552    tmp = cuddCacheLookup(dd,DD_EQUIV_DC_TAG,F,G,D);
553    if (tmp != NULL) return(tmp == One);
554
555    /* Find splitting variable. */
556    flevel = cuddI(dd,F->index);
557    Gr = Cudd_Regular(G);
558    glevel = cuddI(dd,Gr->index);
559    top = ddMin(flevel,glevel);
560    Dr = Cudd_Regular(D);
561    dlevel = dd->perm[Dr->index];
562    top = ddMin(top,dlevel);
563
564    /* Compute cofactors. */
565    if (top == flevel) {
566        Fv = cuddT(F);
567        Fvn = cuddE(F);
568    } else {
569        Fv = Fvn = F;
570    }
571    if (top == glevel) {
572        Gv = cuddT(Gr);
573        Gvn = cuddE(Gr);
574        if (G != Gr) {
575            Gv = Cudd_Not(Gv);
576            Gvn = Cudd_Not(Gvn);
577        }
578    } else {
579        Gv = Gvn = G;
580    }
581    if (top == dlevel) {
582        Dv = cuddT(Dr);
583        Dvn = cuddE(Dr);
584        if (D != Dr) {
585            Dv = Cudd_Not(Dv);
586            Dvn = Cudd_Not(Dvn);
587        }
588    } else {
589        Dv = Dvn = D;
590    }
591
592    /* Solve recursively. */
593    res = Cudd_EquivDC(dd,Fv,Gv,Dv);
594    if (res != 0) {
595        res = Cudd_EquivDC(dd,Fvn,Gvn,Dvn);
596    }
597    cuddCacheInsert(dd,DD_EQUIV_DC_TAG,F,G,D,(res) ? One : Cudd_Not(One));
598
599    return(res);
600
601} /* end of Cudd_EquivDC */
602
603
604/**Function********************************************************************
605
606  Synopsis    [Tells whether f is less than of equal to G unless D is 1.]
607
608  Description [Tells whether f is less than of equal to G unless D is
609  1.  f, g, and D are BDDs.  The function returns 1 if f is less than
610  of equal to G, and 0 otherwise.  No new nodes are created.]
611
612  SideEffects [None]
613
614  SeeAlso     [Cudd_EquivDC Cudd_bddLeq Cudd_bddIteConstant]
615
616******************************************************************************/
617int
618Cudd_bddLeqUnless(
619  DdManager *dd,
620  DdNode *f,
621  DdNode *g,
622  DdNode *D)
623{
624    DdNode *tmp, *One, *F, *G;
625    DdNode *Ft, *Fe, *Gt, *Ge, *Dt, *De;
626    int res;
627    unsigned int flevel, glevel, dlevel, top;
628
629    statLine(dd);
630
631    One = DD_ONE(dd);
632
633    /* Check terminal cases. */
634    if (f == g || g == One || f == Cudd_Not(One) || D == One ||
635        D == f || D == Cudd_Not(g)) return(1);
636    /* Check for two-operand cases. */
637    if (D == Cudd_Not(One) || D == g || D == Cudd_Not(f))
638        return(Cudd_bddLeq(dd,f,g));
639    if (g == Cudd_Not(One) || g == Cudd_Not(f)) return(Cudd_bddLeq(dd,f,D));
640    if (f == One) return(Cudd_bddLeq(dd,Cudd_Not(g),D));
641
642    /* From now on, f, g, and D are non-constant, distinct, and
643    ** non-complementary. */
644
645    /* Normalize call to increase cache efficiency.  We rely on the
646    ** fact that f <= g unless D is equivalent to not(g) <= not(f)
647    ** unless D and to f <= D unless g.  We make sure that D is
648    ** regular, and that at most one of f and g is complemented.  We also
649    ** ensure that when two operands can be swapped, the one with the
650    ** lowest address comes first. */
651
652    if (Cudd_IsComplement(D)) {
653        if (Cudd_IsComplement(g)) {
654            /* Special case: if f is regular and g is complemented,
655            ** f(1,...,1) = 1 > 0 = g(1,...,1).  If D(1,...,1) = 0, return 0.
656            */
657            if (!Cudd_IsComplement(f)) return(0);
658            /* !g <= D unless !f  or  !D <= g unless !f */
659            tmp = D;
660            D = Cudd_Not(f);
661            if (g < tmp) {
662                f = Cudd_Not(g);
663                g = tmp;
664            } else {
665                f = Cudd_Not(tmp);
666            }
667        } else {
668            if (Cudd_IsComplement(f)) {
669                /* !D <= !f unless g  or  !D <= g unless !f */
670                tmp = f;
671                f = Cudd_Not(D);
672                if (tmp < g) {
673                    D = g;
674                    g = Cudd_Not(tmp);
675                } else {
676                    D = Cudd_Not(tmp);
677                }
678            } else {
679                /* f <= D unless g  or  !D <= !f unless g */
680                tmp = D;
681                D = g;
682                if (tmp < f) {
683                    g = Cudd_Not(f);
684                    f = Cudd_Not(tmp);
685                } else {
686                    g = tmp;
687                }
688            }
689        }
690    } else {
691        if (Cudd_IsComplement(g)) {
692            if (Cudd_IsComplement(f)) {
693                /* !g <= !f unless D  or  !g <= D unless !f */
694                tmp = f;
695                f = Cudd_Not(g);
696                if (D < tmp) {
697                    g = D;
698                    D = Cudd_Not(tmp);
699                } else {
700                    g = Cudd_Not(tmp);
701                }
702            } else {
703                /* f <= g unless D  or  !g <= !f unless D */
704                if (g < f) {
705                    tmp = g;
706                    g = Cudd_Not(f);
707                    f = Cudd_Not(tmp);
708                }
709            }
710        } else {
711            /* f <= g unless D  or  f <= D unless g */
712            if (D < g) {
713                tmp = D;
714                D = g;
715                g = tmp;
716            }
717        }
718    }
719
720    /* From now on, D is regular. */
721
722    /* Check cache. */
723    tmp = cuddCacheLookup(dd,DD_BDD_LEQ_UNLESS_TAG,f,g,D);
724    if (tmp != NULL) return(tmp == One);
725
726    /* Find splitting variable. */
727    F = Cudd_Regular(f);
728    flevel = dd->perm[F->index];
729    G = Cudd_Regular(g);
730    glevel = dd->perm[G->index];
731    top = ddMin(flevel,glevel);
732    dlevel = dd->perm[D->index];
733    top = ddMin(top,dlevel);
734
735    /* Compute cofactors. */
736    if (top == flevel) {
737        Ft = cuddT(F);
738        Fe = cuddE(F);
739        if (F != f) {
740            Ft = Cudd_Not(Ft);
741            Fe = Cudd_Not(Fe);
742        }
743    } else {
744        Ft = Fe = f;
745    }
746    if (top == glevel) {
747        Gt = cuddT(G);
748        Ge = cuddE(G);
749        if (G != g) {
750            Gt = Cudd_Not(Gt);
751            Ge = Cudd_Not(Ge);
752        }
753    } else {
754        Gt = Ge = g;
755    }
756    if (top == dlevel) {
757        Dt = cuddT(D);
758        De = cuddE(D);
759    } else {
760        Dt = De = D;
761    }
762
763    /* Solve recursively. */
764    res = Cudd_bddLeqUnless(dd,Ft,Gt,Dt);
765    if (res != 0) {
766        res = Cudd_bddLeqUnless(dd,Fe,Ge,De);
767    }
768    cuddCacheInsert(dd,DD_BDD_LEQ_UNLESS_TAG,f,g,D,Cudd_NotCond(One,!res));
769
770    return(res);
771
772} /* end of Cudd_bddLeqUnless */
773
774
775/**Function********************************************************************
776
777  Synopsis    [Compares two ADDs for equality within tolerance.]
778
779  Description [Compares two ADDs for equality within tolerance. Two
780  ADDs are reported to be equal if the maximum difference between them
781  (the sup norm of their difference) is less than or equal to the
782  tolerance parameter. Returns 1 if the two ADDs are equal (within
783  tolerance); 0 otherwise. If parameter <code>pr</code> is positive
784  the first failure is reported to the standard output.]
785
786  SideEffects [None]
787
788  SeeAlso     []
789
790******************************************************************************/
791int
792Cudd_EqualSupNorm(
793  DdManager * dd /* manager */,
794  DdNode * f /* first ADD */,
795  DdNode * g /* second ADD */,
796  CUDD_VALUE_TYPE  tolerance /* maximum allowed difference */,
797  int  pr /* verbosity level */)
798{
799    DdNode *fv, *fvn, *gv, *gvn, *r;
800    unsigned int topf, topg;
801
802    statLine(dd);
803    /* Check terminal cases. */
804    if (f == g) return(1);
805    if (Cudd_IsConstant(f) && Cudd_IsConstant(g)) {
806        if (ddEqualVal(cuddV(f),cuddV(g),tolerance)) {
807            return(1);
808        } else {
809            if (pr>0) {
810                (void) fprintf(dd->out,"Offending nodes:\n");
811                (void) fprintf(dd->out,
812                               "f: address = %p\t value = %40.30f\n",
813                               (void *) f, cuddV(f));
814                (void) fprintf(dd->out,
815                               "g: address = %p\t value = %40.30f\n",
816                               (void *) g, cuddV(g));
817            }
818            return(0);
819        }
820    }
821
822    /* We only insert the result in the cache if the comparison is
823    ** successful. Therefore, if we hit we return 1. */
824    r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNorm,f,g);
825    if (r != NULL) {
826        return(1);
827    }
828
829    /* Compute the cofactors and solve the recursive subproblems. */
830    topf = cuddI(dd,f->index);
831    topg = cuddI(dd,g->index);
832
833    if (topf <= topg) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;}
834    if (topg <= topf) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;}
835
836    if (!Cudd_EqualSupNorm(dd,fv,gv,tolerance,pr)) return(0);
837    if (!Cudd_EqualSupNorm(dd,fvn,gvn,tolerance,pr)) return(0);
838
839    cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNorm,f,g,DD_ONE(dd));
840
841    return(1);
842
843} /* end of Cudd_EqualSupNorm */
844
845
846/**Function********************************************************************
847
848  Synopsis    [Expands cube to a prime implicant of f.]
849
850  Description [Expands cube to a prime implicant of f. Returns the prime
851  if successful; NULL otherwise.  In particular, NULL is returned if cube
852  is not a real cube or is not an implicant of f.]
853
854  SideEffects [None]
855
856  SeeAlso     []
857
858******************************************************************************/
859DdNode *
860Cudd_bddMakePrime(
861  DdManager *dd /* manager */,
862  DdNode *cube /* cube to be expanded */,
863  DdNode *f /* function of which the cube is to be made a prime */)
864{
865    DdNode *res;
866
867    if (!Cudd_bddLeq(dd,cube,f)) return(NULL);
868
869    do {
870        dd->reordered = 0;
871        res = cuddBddMakePrime(dd,cube,f);
872    } while (dd->reordered == 1);
873    return(res);
874
875} /* end of Cudd_bddMakePrime */
876
877
878/*---------------------------------------------------------------------------*/
879/* Definition of internal functions                                          */
880/*---------------------------------------------------------------------------*/
881
882
883/**Function********************************************************************
884
885  Synopsis    [Performs the recursive step of Cudd_bddMakePrime.]
886
887  Description [Performs the recursive step of Cudd_bddMakePrime.
888  Returns the prime if successful; NULL otherwise.]
889
890  SideEffects [None]
891
892  SeeAlso     []
893
894******************************************************************************/
895DdNode *
896cuddBddMakePrime(
897  DdManager *dd /* manager */,
898  DdNode *cube /* cube to be expanded */,
899  DdNode *f /* function of which the cube is to be made a prime */)
900{
901    DdNode *scan;
902    DdNode *t, *e;
903    DdNode *res = cube;
904    DdNode *zero = Cudd_Not(DD_ONE(dd));
905
906    Cudd_Ref(res);
907    scan = cube;
908    while (!Cudd_IsConstant(scan)) {
909        DdNode *reg = Cudd_Regular(scan);
910        DdNode *var = dd->vars[reg->index];
911        DdNode *expanded = Cudd_bddExistAbstract(dd,res,var);
912        if (expanded == NULL) {
913            return(NULL);
914        }
915        Cudd_Ref(expanded);
916        if (Cudd_bddLeq(dd,expanded,f)) {
917            Cudd_RecursiveDeref(dd,res);
918            res = expanded;
919        } else {
920            Cudd_RecursiveDeref(dd,expanded);
921        }
922        cuddGetBranches(scan,&t,&e);
923        if (t == zero) {
924            scan = e;
925        } else if (e == zero) {
926            scan = t;
927        } else {
928            Cudd_RecursiveDeref(dd,res);
929            return(NULL);       /* cube is not a cube */
930        }
931    }
932
933    if (scan == DD_ONE(dd)) {
934        Cudd_Deref(res);
935        return(res);
936    } else {
937        Cudd_RecursiveDeref(dd,res);
938        return(NULL);
939    }
940
941} /* end of cuddBddMakePrime */
942
943
944/*---------------------------------------------------------------------------*/
945/* Definition of static functions                                            */
946/*---------------------------------------------------------------------------*/
947
948
949/**Function********************************************************************
950
951  Synopsis    [Frees the entries of the visited symbol table.]
952
953  Description [Frees the entries of the visited symbol table. Returns
954  ST_CONTINUE.]
955
956  SideEffects [None]
957
958******************************************************************************/
959static enum st_retval
960freePathPair(
961  char * key,
962  char * value,
963  char * arg)
964{
965    cuddPathPair *pair;
966
967    pair = (cuddPathPair *) value;
968        FREE(pair);
969    return(ST_CONTINUE);
970
971} /* end of freePathPair */
972
973
974/**Function********************************************************************
975
976  Synopsis    [Finds the length of the shortest path(s) in a DD.]
977
978  Description [Finds the length of the shortest path(s) in a DD.
979  Uses a local symbol table to store the lengths for each
980  node. Only the lengths for the regular nodes are entered in the table,
981  because those for the complement nodes are simply obtained by swapping
982  the two lenghts.
983  Returns a pair of lengths: the length of the shortest path to 1;
984  and the length of the shortest path to 0. This is done so as to take
985  complement arcs into account.]
986
987  SideEffects [Accumulates the support of the DD in support.]
988
989  SeeAlso     []
990
991******************************************************************************/
992static cuddPathPair
993getShortest(
994  DdNode * root,
995  int * cost,
996  int * support,
997  st_table * visited)
998{
999    cuddPathPair *my_pair, res_pair, pair_T, pair_E;
1000    DdNode      *my_root, *T, *E;
1001    int         weight;
1002
1003    my_root = Cudd_Regular(root);
1004
1005    if (st_lookup(visited, my_root, &my_pair)) {
1006        if (Cudd_IsComplement(root)) {
1007            res_pair.pos = my_pair->neg;
1008            res_pair.neg = my_pair->pos;
1009        } else {
1010            res_pair.pos = my_pair->pos;
1011            res_pair.neg = my_pair->neg;
1012        }
1013        return(res_pair);
1014    }
1015
1016    /* In the case of a BDD the following test is equivalent to
1017    ** testing whether the BDD is the constant 1. This formulation,
1018    ** however, works for ADDs as well, by assuming the usual
1019    ** dichotomy of 0 and != 0.
1020    */
1021    if (cuddIsConstant(my_root)) {
1022        if (my_root != zero) {
1023            res_pair.pos = 0;
1024            res_pair.neg = DD_BIGGY;
1025        } else {
1026            res_pair.pos = DD_BIGGY;
1027            res_pair.neg = 0;
1028        }
1029    } else {
1030        T = cuddT(my_root);
1031        E = cuddE(my_root);
1032
1033        pair_T = getShortest(T, cost, support, visited);
1034        pair_E = getShortest(E, cost, support, visited);
1035        weight = WEIGHT(cost, my_root->index);
1036        res_pair.pos = ddMin(pair_T.pos+weight, pair_E.pos);
1037        res_pair.neg = ddMin(pair_T.neg+weight, pair_E.neg);
1038
1039        /* Update support. */
1040        if (support != NULL) {
1041            support[my_root->index] = 1;
1042        }
1043    }
1044
1045    my_pair = ALLOC(cuddPathPair, 1);
1046    if (my_pair == NULL) {
1047        if (Cudd_IsComplement(root)) {
1048            int tmp = res_pair.pos;
1049            res_pair.pos = res_pair.neg;
1050            res_pair.neg = tmp;
1051        }
1052        return(res_pair);
1053    }
1054    my_pair->pos = res_pair.pos;
1055    my_pair->neg = res_pair.neg;
1056
1057    st_insert(visited, (char *)my_root, (char *)my_pair);
1058    if (Cudd_IsComplement(root)) {
1059        res_pair.pos = my_pair->neg;
1060        res_pair.neg = my_pair->pos;
1061    } else {
1062        res_pair.pos = my_pair->pos;
1063        res_pair.neg = my_pair->neg;
1064    }
1065    return(res_pair);
1066
1067} /* end of getShortest */
1068
1069
1070/**Function********************************************************************
1071
1072  Synopsis    [Build a BDD for a shortest path of f.]
1073
1074  Description [Build a BDD for a shortest path of f.
1075  Given the minimum length from the root, and the minimum
1076  lengths for each node (in visited), apply triangulation at each node.
1077  Of the two children of each node on a shortest path, at least one is
1078  on a shortest path. In case of ties the procedure chooses the THEN
1079  children.
1080  Returns a pointer to the cube BDD representing the path if
1081  successful; NULL otherwise.]
1082
1083  SideEffects [None]
1084
1085  SeeAlso     []
1086
1087******************************************************************************/
1088static DdNode *
1089getPath(
1090  DdManager * manager,
1091  st_table * visited,
1092  DdNode * f,
1093  int * weight,
1094  int  cost)
1095{
1096    DdNode      *sol, *tmp;
1097    DdNode      *my_dd, *T, *E;
1098    cuddPathPair *T_pair, *E_pair;
1099    int         Tcost, Ecost;
1100    int         complement;
1101
1102    my_dd = Cudd_Regular(f);
1103    complement = Cudd_IsComplement(f);
1104
1105    sol = one;
1106    cuddRef(sol);
1107
1108    while (!cuddIsConstant(my_dd)) {
1109        Tcost = cost - WEIGHT(weight, my_dd->index);
1110        Ecost = cost;
1111
1112        T = cuddT(my_dd);
1113        E = cuddE(my_dd);
1114
1115        if (complement) {T = Cudd_Not(T); E = Cudd_Not(E);}
1116
1117        st_lookup(visited, Cudd_Regular(T), &T_pair);
1118        if ((Cudd_IsComplement(T) && T_pair->neg == Tcost) ||
1119        (!Cudd_IsComplement(T) && T_pair->pos == Tcost)) {
1120            tmp = cuddBddAndRecur(manager,manager->vars[my_dd->index],sol);
1121            if (tmp == NULL) {
1122                Cudd_RecursiveDeref(manager,sol);
1123                return(NULL);
1124            }
1125            cuddRef(tmp);
1126            Cudd_RecursiveDeref(manager,sol);
1127            sol = tmp;
1128
1129            complement =  Cudd_IsComplement(T);
1130            my_dd = Cudd_Regular(T);
1131            cost = Tcost;
1132            continue;
1133        }
1134        st_lookup(visited, Cudd_Regular(E), &E_pair);
1135        if ((Cudd_IsComplement(E) && E_pair->neg == Ecost) ||
1136        (!Cudd_IsComplement(E) && E_pair->pos == Ecost)) {
1137            tmp = cuddBddAndRecur(manager,Cudd_Not(manager->vars[my_dd->index]),sol);
1138            if (tmp == NULL) {
1139                Cudd_RecursiveDeref(manager,sol);
1140                return(NULL);
1141            }
1142            cuddRef(tmp);
1143            Cudd_RecursiveDeref(manager,sol);
1144            sol = tmp;
1145            complement = Cudd_IsComplement(E);
1146            my_dd = Cudd_Regular(E);
1147            cost = Ecost;
1148            continue;
1149        }
1150        (void) fprintf(manager->err,"We shouldn't be here!!\n");
1151        manager->errorCode = CUDD_INTERNAL_ERROR;
1152        return(NULL);
1153    }
1154
1155    cuddDeref(sol);
1156    return(sol);
1157
1158} /* end of getPath */
1159
1160
1161/**Function********************************************************************
1162
1163  Synopsis    [Finds the size of the largest cube(s) in a DD.]
1164
1165  Description [Finds the size of the largest cube(s) in a DD.
1166  This problem is translated into finding the shortest paths from a node
1167  when both THEN and ELSE arcs have unit lengths.
1168  Uses a local symbol table to store the lengths for each
1169  node. Only the lengths for the regular nodes are entered in the table,
1170  because those for the complement nodes are simply obtained by swapping
1171  the two lenghts.
1172  Returns a pair of lengths: the length of the shortest path to 1;
1173  and the length of the shortest path to 0. This is done so as to take
1174  complement arcs into account.]
1175
1176  SideEffects [none]
1177
1178  SeeAlso     []
1179
1180******************************************************************************/
1181static cuddPathPair
1182getLargest(
1183  DdNode * root,
1184  st_table * visited)
1185{
1186    cuddPathPair *my_pair, res_pair, pair_T, pair_E;
1187    DdNode      *my_root, *T, *E;
1188
1189    my_root = Cudd_Regular(root);
1190
1191    if (st_lookup(visited, my_root, &my_pair)) {
1192        if (Cudd_IsComplement(root)) {
1193            res_pair.pos = my_pair->neg;
1194            res_pair.neg = my_pair->pos;
1195        } else {
1196            res_pair.pos = my_pair->pos;
1197            res_pair.neg = my_pair->neg;
1198        }
1199        return(res_pair);
1200    }
1201
1202    /* In the case of a BDD the following test is equivalent to
1203    ** testing whether the BDD is the constant 1. This formulation,
1204    ** however, works for ADDs as well, by assuming the usual
1205    ** dichotomy of 0 and != 0.
1206    */
1207    if (cuddIsConstant(my_root)) {
1208        if (my_root != zero) {
1209            res_pair.pos = 0;
1210            res_pair.neg = DD_BIGGY;
1211        } else {
1212            res_pair.pos = DD_BIGGY;
1213            res_pair.neg = 0;
1214        }
1215    } else {
1216        T = cuddT(my_root);
1217        E = cuddE(my_root);
1218
1219        pair_T = getLargest(T, visited);
1220        pair_E = getLargest(E, visited);
1221        res_pair.pos = ddMin(pair_T.pos, pair_E.pos) + 1;
1222        res_pair.neg = ddMin(pair_T.neg, pair_E.neg) + 1;
1223    }
1224
1225    my_pair = ALLOC(cuddPathPair, 1);
1226    if (my_pair == NULL) {      /* simply do not cache this result */
1227        if (Cudd_IsComplement(root)) {
1228            int tmp = res_pair.pos;
1229            res_pair.pos = res_pair.neg;
1230            res_pair.neg = tmp;
1231        }
1232        return(res_pair);
1233    }
1234    my_pair->pos = res_pair.pos;
1235    my_pair->neg = res_pair.neg;
1236
1237    /* Caching may fail without affecting correctness. */
1238    st_insert(visited, (char *)my_root, (char *)my_pair);
1239    if (Cudd_IsComplement(root)) {
1240        res_pair.pos = my_pair->neg;
1241        res_pair.neg = my_pair->pos;
1242    } else {
1243        res_pair.pos = my_pair->pos;
1244        res_pair.neg = my_pair->neg;
1245    }
1246    return(res_pair);
1247
1248} /* end of getLargest */
1249
1250
1251/**Function********************************************************************
1252
1253  Synopsis    [Build a BDD for a largest cube of f.]
1254
1255  Description [Build a BDD for a largest cube of f.
1256  Given the minimum length from the root, and the minimum
1257  lengths for each node (in visited), apply triangulation at each node.
1258  Of the two children of each node on a shortest path, at least one is
1259  on a shortest path. In case of ties the procedure chooses the THEN
1260  children.
1261  Returns a pointer to the cube BDD representing the path if
1262  successful; NULL otherwise.]
1263
1264  SideEffects [None]
1265
1266  SeeAlso     []
1267
1268******************************************************************************/
1269static DdNode *
1270getCube(
1271  DdManager * manager,
1272  st_table * visited,
1273  DdNode * f,
1274  int  cost)
1275{
1276    DdNode      *sol, *tmp;
1277    DdNode      *my_dd, *T, *E;
1278    cuddPathPair *T_pair, *E_pair;
1279    int         Tcost, Ecost;
1280    int         complement;
1281
1282    my_dd = Cudd_Regular(f);
1283    complement = Cudd_IsComplement(f);
1284
1285    sol = one;
1286    cuddRef(sol);
1287
1288    while (!cuddIsConstant(my_dd)) {
1289        Tcost = cost - 1;
1290        Ecost = cost - 1;
1291
1292        T = cuddT(my_dd);
1293        E = cuddE(my_dd);
1294
1295        if (complement) {T = Cudd_Not(T); E = Cudd_Not(E);}
1296
1297        if (!st_lookup(visited, Cudd_Regular(T), &T_pair)) return(NULL);
1298        if ((Cudd_IsComplement(T) && T_pair->neg == Tcost) ||
1299        (!Cudd_IsComplement(T) && T_pair->pos == Tcost)) {
1300            tmp = cuddBddAndRecur(manager,manager->vars[my_dd->index],sol);
1301            if (tmp == NULL) {
1302                Cudd_RecursiveDeref(manager,sol);
1303                return(NULL);
1304            }
1305            cuddRef(tmp);
1306            Cudd_RecursiveDeref(manager,sol);
1307            sol = tmp;
1308
1309            complement =  Cudd_IsComplement(T);
1310            my_dd = Cudd_Regular(T);
1311            cost = Tcost;
1312            continue;
1313        }
1314        if (!st_lookup(visited, Cudd_Regular(E), &E_pair)) return(NULL);
1315        if ((Cudd_IsComplement(E) && E_pair->neg == Ecost) ||
1316        (!Cudd_IsComplement(E) && E_pair->pos == Ecost)) {
1317            tmp = cuddBddAndRecur(manager,Cudd_Not(manager->vars[my_dd->index]),sol);
1318            if (tmp == NULL) {
1319                Cudd_RecursiveDeref(manager,sol);
1320                return(NULL);
1321            }
1322            cuddRef(tmp);
1323            Cudd_RecursiveDeref(manager,sol);
1324            sol = tmp;
1325            complement = Cudd_IsComplement(E);
1326            my_dd = Cudd_Regular(E);
1327            cost = Ecost;
1328            continue;
1329        }
1330        (void) fprintf(manager->err,"We shouldn't be here!\n");
1331        manager->errorCode = CUDD_INTERNAL_ERROR;
1332        return(NULL);
1333    }
1334
1335    cuddDeref(sol);
1336    return(sol);
1337
1338} /* end of getCube */
Note: See TracBrowser for help on using the repository browser.