source: vis_dev/glu-2.3/src/cuBdd/cuddCof.c @ 104

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

library glu 2.3
File size: 9.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddCof.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Cofactoring functions.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_Cofactor()
12                </ul>
13               Internal procedures included in this module:
14                <ul>
15                <li> cuddGetBranches()
16                <li> cuddCheckCube()
17                <li> cuddCofactorRecur()
18                </ul>
19              ]
20
21  SeeAlso     []
22
23  Author      [Fabio Somenzi]
24
25  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
26
27  All rights reserved.
28
29  Redistribution and use in source and binary forms, with or without
30  modification, are permitted provided that the following conditions
31  are met:
32
33  Redistributions of source code must retain the above copyright
34  notice, this list of conditions and the following disclaimer.
35
36  Redistributions in binary form must reproduce the above copyright
37  notice, this list of conditions and the following disclaimer in the
38  documentation and/or other materials provided with the distribution.
39
40  Neither the name of the University of Colorado nor the names of its
41  contributors may be used to endorse or promote products derived from
42  this software without specific prior written permission.
43
44  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
45  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
46  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
47  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
48  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
49  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
50  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
51  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
52  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
53  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
54  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
55  POSSIBILITY OF SUCH DAMAGE.]
56
57******************************************************************************/
58
59#include "util.h"
60#include "cuddInt.h"
61
62/*---------------------------------------------------------------------------*/
63/* Constant declarations                                                     */
64/*---------------------------------------------------------------------------*/
65
66
67/*---------------------------------------------------------------------------*/
68/* Stucture declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Type declarations                                                         */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Variable declarations                                                     */
79/*---------------------------------------------------------------------------*/
80
81#ifndef lint
82static char rcsid[] DD_UNUSED = "$Id: cuddCof.c,v 1.9 2004/08/13 18:04:47 fabio Exp $";
83#endif
84
85/*---------------------------------------------------------------------------*/
86/* Macro declarations                                                        */
87/*---------------------------------------------------------------------------*/
88
89
90/**AutomaticStart*************************************************************/
91
92/*---------------------------------------------------------------------------*/
93/* Static function prototypes                                                */
94/*---------------------------------------------------------------------------*/
95
96
97/**AutomaticEnd***************************************************************/
98
99
100/*---------------------------------------------------------------------------*/
101/* Definition of exported functions                                          */
102/*---------------------------------------------------------------------------*/
103
104
105/**Function********************************************************************
106
107  Synopsis    [Computes the cofactor of f with respect to g.]
108
109  Description [Computes the cofactor of f with respect to g; g must be
110  the BDD or the ADD of a cube. Returns a pointer to the cofactor if
111  successful; NULL otherwise.]
112
113  SideEffects [None]
114
115  SeeAlso     [Cudd_bddConstrain Cudd_bddRestrict]
116
117******************************************************************************/
118DdNode *
119Cudd_Cofactor(
120  DdManager * dd,
121  DdNode * f,
122  DdNode * g)
123{
124    DdNode *res,*zero;
125
126    zero = Cudd_Not(DD_ONE(dd));
127    if (g == zero || g == DD_ZERO(dd)) {
128        (void) fprintf(dd->err,"Cudd_Cofactor: Invalid restriction 1\n");
129        dd->errorCode = CUDD_INVALID_ARG;
130        return(NULL);
131    }
132    do {
133        dd->reordered = 0;
134        res = cuddCofactorRecur(dd,f,g);
135    } while (dd->reordered == 1);
136    return(res);
137
138} /* end of Cudd_Cofactor */
139
140
141/*---------------------------------------------------------------------------*/
142/* Definition of internal functions                                          */
143/*---------------------------------------------------------------------------*/
144
145
146/**Function********************************************************************
147
148  Synopsis    [Computes the children of g.]
149
150  Description []
151
152  SideEffects [None]
153
154  SeeAlso     []
155
156******************************************************************************/
157void
158cuddGetBranches(
159  DdNode * g,
160  DdNode ** g1,
161  DdNode ** g0)
162{
163    DdNode      *G = Cudd_Regular(g);
164
165    *g1 = cuddT(G);
166    *g0 = cuddE(G);
167    if (Cudd_IsComplement(g)) {
168        *g1 = Cudd_Not(*g1);
169        *g0 = Cudd_Not(*g0);
170    }
171
172} /* end of cuddGetBranches */
173
174
175/**Function********************************************************************
176
177  Synopsis    [Checks whether g is the BDD of a cube.]
178
179  Description [Checks whether g is the BDD of a cube. Returns 1 in case
180  of success; 0 otherwise. The constant 1 is a valid cube, but all other
181  constant functions cause cuddCheckCube to return 0.]
182
183  SideEffects [None]
184
185  SeeAlso     []
186
187******************************************************************************/
188int
189cuddCheckCube(
190  DdManager * dd,
191  DdNode * g)
192{
193    DdNode *g1,*g0,*one,*zero;
194   
195    one = DD_ONE(dd);
196    if (g == one) return(1);
197    if (Cudd_IsConstant(g)) return(0);
198
199    zero = Cudd_Not(one);
200    cuddGetBranches(g,&g1,&g0);
201
202    if (g0 == zero) {
203        return(cuddCheckCube(dd, g1));
204    }
205    if (g1 == zero) {
206        return(cuddCheckCube(dd, g0));
207    }
208    return(0);
209
210} /* end of cuddCheckCube */
211
212
213/**Function********************************************************************
214
215  Synopsis    [Performs the recursive step of Cudd_Cofactor.]
216
217  Description [Performs the recursive step of Cudd_Cofactor. Returns a
218  pointer to the cofactor if successful; NULL otherwise.]
219
220  SideEffects [None]
221
222  SeeAlso     [Cudd_Cofactor]
223
224******************************************************************************/
225DdNode *
226cuddCofactorRecur(
227  DdManager * dd,
228  DdNode * f,
229  DdNode * g)
230{
231    DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;
232    unsigned int topf,topg;
233    int comple;
234
235    statLine(dd);
236    F = Cudd_Regular(f);
237    if (cuddIsConstant(F)) return(f);
238
239    one = DD_ONE(dd);
240
241    /* The invariant g != 0 is true on entry to this procedure and is
242    ** recursively maintained by it. Therefore it suffices to test g
243    ** against one to make sure it is not constant.
244    */
245    if (g == one) return(f);
246    /* From now on, f and g are known not to be constants. */
247
248    comple = f != F;
249    r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);
250    if (r != NULL) {
251        return(Cudd_NotCond(r,comple));
252    }
253
254    topf = dd->perm[F->index];
255    G = Cudd_Regular(g);
256    topg = dd->perm[G->index];
257
258    /* We take the cofactors of F because we are going to rely on
259    ** the fact that the cofactors of the complement are the complements
260    ** of the cofactors to better utilize the cache. Variable comple
261    ** remembers whether we have to complement the result or not.
262    */
263    if (topf <= topg) {
264        f1 = cuddT(F); f0 = cuddE(F);
265    } else {
266        f1 = f0 = F;
267    }
268    if (topg <= topf) {
269        g1 = cuddT(G); g0 = cuddE(G);
270        if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }
271    } else {
272        g1 = g0 = g;
273    }
274
275    zero = Cudd_Not(one);
276    if (topf >= topg) {
277        if (g0 == zero || g0 == DD_ZERO(dd)) {
278            r = cuddCofactorRecur(dd, f1, g1);
279        } else if (g1 == zero || g1 == DD_ZERO(dd)) {
280            r = cuddCofactorRecur(dd, f0, g0);
281        } else {
282            (void) fprintf(dd->out,
283                           "Cudd_Cofactor: Invalid restriction 2\n");
284            dd->errorCode = CUDD_INVALID_ARG;
285            return(NULL);
286        }
287        if (r == NULL) return(NULL);
288    } else /* if (topf < topg) */ {
289        t = cuddCofactorRecur(dd, f1, g);
290        if (t == NULL) return(NULL);
291        cuddRef(t);
292        e = cuddCofactorRecur(dd, f0, g);
293        if (e == NULL) {
294            Cudd_RecursiveDeref(dd, t);
295            return(NULL);
296        }
297        cuddRef(e);
298
299        if (t == e) {
300            r = t;
301        } else if (Cudd_IsComplement(t)) {
302            r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));
303            if (r != NULL)
304                r = Cudd_Not(r);
305        } else {
306            r = cuddUniqueInter(dd,(int)F->index,t,e);
307        }
308        if (r == NULL) {
309            Cudd_RecursiveDeref(dd ,e);
310            Cudd_RecursiveDeref(dd ,t);
311            return(NULL);
312        }
313        cuddDeref(t);
314        cuddDeref(e);
315    }
316
317    cuddCacheInsert2(dd,Cudd_Cofactor,F,g,r);
318
319    return(Cudd_NotCond(r,comple));
320
321} /* end of cuddCofactorRecur */
322
323
324/*---------------------------------------------------------------------------*/
325/* Definition of static functions                                            */
326/*---------------------------------------------------------------------------*/
327
Note: See TracBrowser for help on using the repository browser.