source: vis_dev/glu-2.3/src/cuBdd/cuddAddAbs.c @ 67

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

library glu 2.3
File size: 17.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddAddAbs.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Quantification functions for ADDs.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_addExistAbstract()
12                <li> Cudd_addUnivAbstract()
13                <li> Cudd_addOrAbstract()
14                </ul>
15        Internal procedures included in this module:
16                <ul>
17                <li> cuddAddExistAbstractRecur()
18                <li> cuddAddUnivAbstractRecur()
19                <li> cuddAddOrAbstractRecur()
20                </ul>
21        Static procedures included in this module:
22                <ul>
23                <li> addCheckPositiveCube()
24                </ul>]
25
26  Author      [Fabio Somenzi]
27
28  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
29
30  All rights reserved.
31
32  Redistribution and use in source and binary forms, with or without
33  modification, are permitted provided that the following conditions
34  are met:
35
36  Redistributions of source code must retain the above copyright
37  notice, this list of conditions and the following disclaimer.
38
39  Redistributions in binary form must reproduce the above copyright
40  notice, this list of conditions and the following disclaimer in the
41  documentation and/or other materials provided with the distribution.
42
43  Neither the name of the University of Colorado nor the names of its
44  contributors may be used to endorse or promote products derived from
45  this software without specific prior written permission.
46
47  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
48  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
49  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
50  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
51  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
52  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
53  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
54  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
55  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
56  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
57  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
58  POSSIBILITY OF SUCH DAMAGE.]
59
60******************************************************************************/
61
62#include "util.h"
63#include "cuddInt.h"
64
65/*---------------------------------------------------------------------------*/
66/* Constant declarations                                                     */
67/*---------------------------------------------------------------------------*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Stucture declarations                                                     */
72/*---------------------------------------------------------------------------*/
73
74
75/*---------------------------------------------------------------------------*/
76/* Type declarations                                                         */
77/*---------------------------------------------------------------------------*/
78
79
80/*---------------------------------------------------------------------------*/
81/* Variable declarations                                                     */
82/*---------------------------------------------------------------------------*/
83
84#ifndef lint
85static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
86#endif
87
88static  DdNode  *two;
89
90/*---------------------------------------------------------------------------*/
91/* Macro declarations                                                        */
92/*---------------------------------------------------------------------------*/
93
94
95/**AutomaticStart*************************************************************/
96
97/*---------------------------------------------------------------------------*/
98/* Static function prototypes                                                */
99/*---------------------------------------------------------------------------*/
100
101static int addCheckPositiveCube (DdManager *manager, DdNode *cube);
102
103/**AutomaticEnd***************************************************************/
104
105
106/*---------------------------------------------------------------------------*/
107/* Definition of exported functions                                          */
108/*---------------------------------------------------------------------------*/
109
110/**Function********************************************************************
111
112  Synopsis    [Existentially Abstracts all the variables in cube from f.]
113
114  Description [Abstracts all the variables in cube from f by summing
115  over all possible values taken by the variables. Returns the
116  abstracted ADD.]
117
118  SideEffects [None]
119
120  SeeAlso     [Cudd_addUnivAbstract Cudd_bddExistAbstract
121  Cudd_addOrAbstract]
122
123******************************************************************************/
124DdNode *
125Cudd_addExistAbstract(
126  DdManager * manager,
127  DdNode * f,
128  DdNode * cube)
129{
130    DdNode *res;
131
132    two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
133    if (two == NULL) return(NULL);
134    cuddRef(two);
135
136    if (addCheckPositiveCube(manager, cube) == 0) {
137        (void) fprintf(manager->err,"Error: Can only abstract cubes");
138        return(NULL);
139    }
140
141    do {
142        manager->reordered = 0;
143        res = cuddAddExistAbstractRecur(manager, f, cube);
144    } while (manager->reordered == 1);
145
146    if (res == NULL) {
147        Cudd_RecursiveDeref(manager,two);
148        return(NULL);
149    }
150    cuddRef(res);
151    Cudd_RecursiveDeref(manager,two);
152    cuddDeref(res);
153
154    return(res);
155
156} /* end of Cudd_addExistAbstract */
157
158
159/**Function********************************************************************
160
161  Synopsis    [Universally Abstracts all the variables in cube from f.]
162
163  Description [Abstracts all the variables in cube from f by taking
164  the product over all possible values taken by the variable. Returns
165  the abstracted ADD if successful; NULL otherwise.]
166
167  SideEffects [None]
168
169  SeeAlso     [Cudd_addExistAbstract Cudd_bddUnivAbstract
170  Cudd_addOrAbstract]
171
172******************************************************************************/
173DdNode *
174Cudd_addUnivAbstract(
175  DdManager * manager,
176  DdNode * f,
177  DdNode * cube)
178{
179    DdNode              *res;
180
181    if (addCheckPositiveCube(manager, cube) == 0) {
182        (void) fprintf(manager->err,"Error:  Can only abstract cubes");
183        return(NULL);
184    }
185
186    do {
187        manager->reordered = 0;
188        res = cuddAddUnivAbstractRecur(manager, f, cube);
189    } while (manager->reordered == 1);
190
191    return(res);
192
193} /* end of Cudd_addUnivAbstract */
194
195
196/**Function********************************************************************
197
198  Synopsis    [Disjunctively abstracts all the variables in cube from the
199  0-1 ADD f.]
200
201  Description [Abstracts all the variables in cube from the 0-1 ADD f
202  by taking the disjunction over all possible values taken by the
203  variables.  Returns the abstracted ADD if successful; NULL
204  otherwise.]
205
206  SideEffects [None]
207
208  SeeAlso     [Cudd_addUnivAbstract Cudd_addExistAbstract]
209
210******************************************************************************/
211DdNode *
212Cudd_addOrAbstract(
213  DdManager * manager,
214  DdNode * f,
215  DdNode * cube)
216{
217    DdNode *res;
218
219    if (addCheckPositiveCube(manager, cube) == 0) {
220        (void) fprintf(manager->err,"Error: Can only abstract cubes");
221        return(NULL);
222    }
223
224    do {
225        manager->reordered = 0;
226        res = cuddAddOrAbstractRecur(manager, f, cube);
227    } while (manager->reordered == 1);
228    return(res);
229
230} /* end of Cudd_addOrAbstract */
231
232
233/*---------------------------------------------------------------------------*/
234/* Definition of internal functions                                          */
235/*---------------------------------------------------------------------------*/
236
237
238/**Function********************************************************************
239
240  Synopsis    [Performs the recursive step of Cudd_addExistAbstract.]
241
242  Description [Performs the recursive step of Cudd_addExistAbstract.
243  Returns the ADD obtained by abstracting the variables of cube from f,
244  if successful; NULL otherwise.]
245
246  SideEffects [None]
247
248  SeeAlso     []
249
250******************************************************************************/
251DdNode *
252cuddAddExistAbstractRecur(
253  DdManager * manager,
254  DdNode * f,
255  DdNode * cube)
256{
257    DdNode      *T, *E, *res, *res1, *res2, *zero;
258
259    statLine(manager);
260    zero = DD_ZERO(manager);
261
262    /* Cube is guaranteed to be a cube at this point. */       
263    if (f == zero || cuddIsConstant(cube)) { 
264        return(f);
265    }
266
267    /* Abstract a variable that does not appear in f => multiply by 2. */
268    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
269        res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube));
270        if (res1 == NULL) return(NULL);
271        cuddRef(res1);
272        /* Use the "internal" procedure to be alerted in case of
273        ** dynamic reordering. If dynamic reordering occurs, we
274        ** have to abort the entire abstraction.
275        */
276        res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two);
277        if (res == NULL) {
278            Cudd_RecursiveDeref(manager,res1);
279            return(NULL);
280        }
281        cuddRef(res);
282        Cudd_RecursiveDeref(manager,res1);
283        cuddDeref(res);
284        return(res);
285    }
286
287    if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) {
288        return(res);
289    }
290
291    T = cuddT(f);
292    E = cuddE(f);
293
294    /* If the two indices are the same, so are their levels. */
295    if (f->index == cube->index) {
296        res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube));
297        if (res1 == NULL) return(NULL);
298        cuddRef(res1);
299        res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube));
300        if (res2 == NULL) {
301            Cudd_RecursiveDeref(manager,res1);
302            return(NULL);
303        }
304        cuddRef(res2);
305        res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2);
306        if (res == NULL) {
307            Cudd_RecursiveDeref(manager,res1);
308            Cudd_RecursiveDeref(manager,res2);
309            return(NULL);
310        }
311        cuddRef(res);
312        Cudd_RecursiveDeref(manager,res1);
313        Cudd_RecursiveDeref(manager,res2);
314        cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
315        cuddDeref(res);
316        return(res);
317    } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
318        res1 = cuddAddExistAbstractRecur(manager, T, cube);
319        if (res1 == NULL) return(NULL);
320        cuddRef(res1);
321        res2 = cuddAddExistAbstractRecur(manager, E, cube);
322        if (res2 == NULL) {
323            Cudd_RecursiveDeref(manager,res1);
324            return(NULL);
325        }
326        cuddRef(res2);
327        res = (res1 == res2) ? res1 :
328            cuddUniqueInter(manager, (int) f->index, res1, res2);
329        if (res == NULL) {
330            Cudd_RecursiveDeref(manager,res1);
331            Cudd_RecursiveDeref(manager,res2);
332            return(NULL);
333        }
334        cuddDeref(res1);
335        cuddDeref(res2);
336        cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
337        return(res);
338    }       
339
340} /* end of cuddAddExistAbstractRecur */
341
342
343/**Function********************************************************************
344
345  Synopsis    [Performs the recursive step of Cudd_addUnivAbstract.]
346
347  Description [Performs the recursive step of Cudd_addUnivAbstract.
348  Returns the ADD obtained by abstracting the variables of cube from f,
349  if successful; NULL otherwise.]
350
351  SideEffects [None]
352
353  SeeAlso     []
354
355******************************************************************************/
356DdNode *
357cuddAddUnivAbstractRecur(
358  DdManager * manager,
359  DdNode * f,
360  DdNode * cube)
361{
362    DdNode      *T, *E, *res, *res1, *res2, *one, *zero;
363
364    statLine(manager);
365    one = DD_ONE(manager);
366    zero = DD_ZERO(manager);
367
368    /* Cube is guaranteed to be a cube at this point.
369    ** zero and one are the only constatnts c such that c*c=c.
370    */
371    if (f == zero || f == one || cube == one) { 
372        return(f);
373    }
374
375    /* Abstract a variable that does not appear in f. */
376    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
377        res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
378        if (res1 == NULL) return(NULL);
379        cuddRef(res1);
380        /* Use the "internal" procedure to be alerted in case of
381        ** dynamic reordering. If dynamic reordering occurs, we
382        ** have to abort the entire abstraction.
383        */
384        res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
385        if (res == NULL) {
386            Cudd_RecursiveDeref(manager,res1);
387            return(NULL);
388        }
389        cuddRef(res);
390        Cudd_RecursiveDeref(manager,res1);
391        cuddDeref(res);
392        return(res);
393    }
394
395    if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
396        return(res);
397    }
398
399    T = cuddT(f);
400    E = cuddE(f);
401
402    /* If the two indices are the same, so are their levels. */
403    if (f->index == cube->index) {
404        res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
405        if (res1 == NULL) return(NULL);
406        cuddRef(res1);
407        res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
408        if (res2 == NULL) {
409            Cudd_RecursiveDeref(manager,res1);
410            return(NULL);
411        }
412        cuddRef(res2);
413        res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
414        if (res == NULL) {
415            Cudd_RecursiveDeref(manager,res1);
416            Cudd_RecursiveDeref(manager,res2);
417            return(NULL);
418        }
419        cuddRef(res);
420        Cudd_RecursiveDeref(manager,res1);
421        Cudd_RecursiveDeref(manager,res2);
422        cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
423        cuddDeref(res);
424        return(res);
425    } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
426        res1 = cuddAddUnivAbstractRecur(manager, T, cube);
427        if (res1 == NULL) return(NULL);
428        cuddRef(res1);
429        res2 = cuddAddUnivAbstractRecur(manager, E, cube);
430        if (res2 == NULL) {
431            Cudd_RecursiveDeref(manager,res1);
432            return(NULL);
433        }
434        cuddRef(res2);
435        res = (res1 == res2) ? res1 :
436            cuddUniqueInter(manager, (int) f->index, res1, res2);
437        if (res == NULL) {
438            Cudd_RecursiveDeref(manager,res1);
439            Cudd_RecursiveDeref(manager,res2);
440            return(NULL);
441        }
442        cuddDeref(res1);
443        cuddDeref(res2);
444        cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
445        return(res);
446    }
447
448} /* end of cuddAddUnivAbstractRecur */
449
450
451/**Function********************************************************************
452
453  Synopsis    [Performs the recursive step of Cudd_addOrAbstract.]
454
455  Description [Performs the recursive step of Cudd_addOrAbstract.
456  Returns the ADD obtained by abstracting the variables of cube from f,
457  if successful; NULL otherwise.]
458
459  SideEffects [None]
460
461  SeeAlso     []
462
463******************************************************************************/
464DdNode *
465cuddAddOrAbstractRecur(
466  DdManager * manager,
467  DdNode * f,
468  DdNode * cube)
469{
470    DdNode      *T, *E, *res, *res1, *res2, *one;
471
472    statLine(manager);
473    one = DD_ONE(manager);
474
475    /* Cube is guaranteed to be a cube at this point. */
476    if (cuddIsConstant(f) || cube == one) { 
477        return(f);
478    }
479
480    /* Abstract a variable that does not appear in f. */
481    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
482        res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
483        return(res);
484    }
485
486    if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
487        return(res);
488    }
489
490    T = cuddT(f);
491    E = cuddE(f);
492
493    /* If the two indices are the same, so are their levels. */
494    if (f->index == cube->index) {
495        res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
496        if (res1 == NULL) return(NULL);
497        cuddRef(res1);
498        if (res1 != one) {
499            res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
500            if (res2 == NULL) {
501                Cudd_RecursiveDeref(manager,res1);
502                return(NULL);
503            }
504            cuddRef(res2);
505            res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
506            if (res == NULL) {
507                Cudd_RecursiveDeref(manager,res1);
508                Cudd_RecursiveDeref(manager,res2);
509                return(NULL);
510            }
511            cuddRef(res);
512            Cudd_RecursiveDeref(manager,res1);
513            Cudd_RecursiveDeref(manager,res2);
514        } else {
515            res = res1;
516        }
517        cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
518        cuddDeref(res);
519        return(res);
520    } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
521        res1 = cuddAddOrAbstractRecur(manager, T, cube);
522        if (res1 == NULL) return(NULL);
523        cuddRef(res1);
524        res2 = cuddAddOrAbstractRecur(manager, E, cube);
525        if (res2 == NULL) {
526            Cudd_RecursiveDeref(manager,res1);
527            return(NULL);
528        }
529        cuddRef(res2);
530        res = (res1 == res2) ? res1 :
531            cuddUniqueInter(manager, (int) f->index, res1, res2);
532        if (res == NULL) {
533            Cudd_RecursiveDeref(manager,res1);
534            Cudd_RecursiveDeref(manager,res2);
535            return(NULL);
536        }
537        cuddDeref(res1);
538        cuddDeref(res2);
539        cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
540        return(res);
541    }
542
543} /* end of cuddAddOrAbstractRecur */
544
545
546
547/*---------------------------------------------------------------------------*/
548/* Definition of static functions                                            */
549/*---------------------------------------------------------------------------*/
550
551
552/**Function********************************************************************
553
554  Synopsis    [Checks whether cube is an ADD representing the product
555  of positive literals.]
556
557  Description [Checks whether cube is an ADD representing the product of
558  positive literals. Returns 1 in case of success; 0 otherwise.]
559
560  SideEffects [None]
561
562  SeeAlso     []
563
564******************************************************************************/
565static int
566addCheckPositiveCube(
567  DdManager * manager,
568  DdNode * cube)
569{
570    if (Cudd_IsComplement(cube)) return(0);
571    if (cube == DD_ONE(manager)) return(1);
572    if (cuddIsConstant(cube)) return(0);
573    if (cuddE(cube) == DD_ZERO(manager)) {
574        return(addCheckPositiveCube(manager, cuddT(cube)));
575    }
576    return(0);
577
578} /* end of addCheckPositiveCube */
579
Note: See TracBrowser for help on using the repository browser.