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 "misc/util/util_hack.h"
63 #include "cuddInt.h"
64
65 ABC_NAMESPACE_IMPL_START
66
67
68
69 /*---------------------------------------------------------------------------*/
70 /* Constant declarations */
71 /*---------------------------------------------------------------------------*/
72
73
74 /*---------------------------------------------------------------------------*/
75 /* Stucture declarations */
76 /*---------------------------------------------------------------------------*/
77
78
79 /*---------------------------------------------------------------------------*/
80 /* Type declarations */
81 /*---------------------------------------------------------------------------*/
82
83
84 /*---------------------------------------------------------------------------*/
85 /* Variable declarations */
86 /*---------------------------------------------------------------------------*/
87
88 #ifndef lint
89 static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
90 #endif
91
92 static DdNode *two;
93
94 /*---------------------------------------------------------------------------*/
95 /* Macro declarations */
96 /*---------------------------------------------------------------------------*/
97
98
99 /**AutomaticStart*************************************************************/
100
101 /*---------------------------------------------------------------------------*/
102 /* Static function prototypes */
103 /*---------------------------------------------------------------------------*/
104
105 static int addCheckPositiveCube (DdManager *manager, DdNode *cube);
106
107 /**AutomaticEnd***************************************************************/
108
109
110 /*---------------------------------------------------------------------------*/
111 /* Definition of exported functions */
112 /*---------------------------------------------------------------------------*/
113
114 /**Function********************************************************************
115
116 Synopsis [Existentially Abstracts all the variables in cube from f.]
117
118 Description [Abstracts all the variables in cube from f by summing
119 over all possible values taken by the variables. Returns the
120 abstracted ADD.]
121
122 SideEffects [None]
123
124 SeeAlso [Cudd_addUnivAbstract Cudd_bddExistAbstract
125 Cudd_addOrAbstract]
126
127 ******************************************************************************/
128 DdNode *
Cudd_addExistAbstract(DdManager * manager,DdNode * f,DdNode * cube)129 Cudd_addExistAbstract(
130 DdManager * manager,
131 DdNode * f,
132 DdNode * cube)
133 {
134 DdNode *res;
135
136 two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
137 if (two == NULL) return(NULL);
138 cuddRef(two);
139
140 if (addCheckPositiveCube(manager, cube) == 0) {
141 (void) fprintf(manager->err,"Error: Can only abstract cubes");
142 return(NULL);
143 }
144
145 do {
146 manager->reordered = 0;
147 res = cuddAddExistAbstractRecur(manager, f, cube);
148 } while (manager->reordered == 1);
149
150 if (res == NULL) {
151 Cudd_RecursiveDeref(manager,two);
152 return(NULL);
153 }
154 cuddRef(res);
155 Cudd_RecursiveDeref(manager,two);
156 cuddDeref(res);
157
158 return(res);
159
160 } /* end of Cudd_addExistAbstract */
161
162
163 /**Function********************************************************************
164
165 Synopsis [Universally Abstracts all the variables in cube from f.]
166
167 Description [Abstracts all the variables in cube from f by taking
168 the product over all possible values taken by the variable. Returns
169 the abstracted ADD if successful; NULL otherwise.]
170
171 SideEffects [None]
172
173 SeeAlso [Cudd_addExistAbstract Cudd_bddUnivAbstract
174 Cudd_addOrAbstract]
175
176 ******************************************************************************/
177 DdNode *
Cudd_addUnivAbstract(DdManager * manager,DdNode * f,DdNode * cube)178 Cudd_addUnivAbstract(
179 DdManager * manager,
180 DdNode * f,
181 DdNode * cube)
182 {
183 DdNode *res;
184
185 if (addCheckPositiveCube(manager, cube) == 0) {
186 (void) fprintf(manager->err,"Error: Can only abstract cubes");
187 return(NULL);
188 }
189
190 do {
191 manager->reordered = 0;
192 res = cuddAddUnivAbstractRecur(manager, f, cube);
193 } while (manager->reordered == 1);
194
195 return(res);
196
197 } /* end of Cudd_addUnivAbstract */
198
199
200 /**Function********************************************************************
201
202 Synopsis [Disjunctively abstracts all the variables in cube from the
203 0-1 ADD f.]
204
205 Description [Abstracts all the variables in cube from the 0-1 ADD f
206 by taking the disjunction over all possible values taken by the
207 variables. Returns the abstracted ADD if successful; NULL
208 otherwise.]
209
210 SideEffects [None]
211
212 SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract]
213
214 ******************************************************************************/
215 DdNode *
Cudd_addOrAbstract(DdManager * manager,DdNode * f,DdNode * cube)216 Cudd_addOrAbstract(
217 DdManager * manager,
218 DdNode * f,
219 DdNode * cube)
220 {
221 DdNode *res;
222
223 if (addCheckPositiveCube(manager, cube) == 0) {
224 (void) fprintf(manager->err,"Error: Can only abstract cubes");
225 return(NULL);
226 }
227
228 do {
229 manager->reordered = 0;
230 res = cuddAddOrAbstractRecur(manager, f, cube);
231 } while (manager->reordered == 1);
232 return(res);
233
234 } /* end of Cudd_addOrAbstract */
235
236
237 /*---------------------------------------------------------------------------*/
238 /* Definition of internal functions */
239 /*---------------------------------------------------------------------------*/
240
241
242 /**Function********************************************************************
243
244 Synopsis [Performs the recursive step of Cudd_addExistAbstract.]
245
246 Description [Performs the recursive step of Cudd_addExistAbstract.
247 Returns the ADD obtained by abstracting the variables of cube from f,
248 if successful; NULL otherwise.]
249
250 SideEffects [None]
251
252 SeeAlso []
253
254 ******************************************************************************/
255 DdNode *
cuddAddExistAbstractRecur(DdManager * manager,DdNode * f,DdNode * cube)256 cuddAddExistAbstractRecur(
257 DdManager * manager,
258 DdNode * f,
259 DdNode * cube)
260 {
261 DdNode *T, *E, *res, *res1, *res2, *zero;
262
263 statLine(manager);
264 zero = DD_ZERO(manager);
265
266 /* Cube is guaranteed to be a cube at this point. */
267 if (f == zero || cuddIsConstant(cube)) {
268 return(f);
269 }
270
271 /* Abstract a variable that does not appear in f => multiply by 2. */
272 if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
273 res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube));
274 if (res1 == NULL) return(NULL);
275 cuddRef(res1);
276 /* Use the "internal" procedure to be alerted in case of
277 ** dynamic reordering. If dynamic reordering occurs, we
278 ** have to abort the entire abstraction.
279 */
280 res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two);
281 if (res == NULL) {
282 Cudd_RecursiveDeref(manager,res1);
283 return(NULL);
284 }
285 cuddRef(res);
286 Cudd_RecursiveDeref(manager,res1);
287 cuddDeref(res);
288 return(res);
289 }
290
291 if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) {
292 return(res);
293 }
294
295 T = cuddT(f);
296 E = cuddE(f);
297
298 /* If the two indices are the same, so are their levels. */
299 if (f->index == cube->index) {
300 res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube));
301 if (res1 == NULL) return(NULL);
302 cuddRef(res1);
303 res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube));
304 if (res2 == NULL) {
305 Cudd_RecursiveDeref(manager,res1);
306 return(NULL);
307 }
308 cuddRef(res2);
309 res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2);
310 if (res == NULL) {
311 Cudd_RecursiveDeref(manager,res1);
312 Cudd_RecursiveDeref(manager,res2);
313 return(NULL);
314 }
315 cuddRef(res);
316 Cudd_RecursiveDeref(manager,res1);
317 Cudd_RecursiveDeref(manager,res2);
318 cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
319 cuddDeref(res);
320 return(res);
321 } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
322 res1 = cuddAddExistAbstractRecur(manager, T, cube);
323 if (res1 == NULL) return(NULL);
324 cuddRef(res1);
325 res2 = cuddAddExistAbstractRecur(manager, E, cube);
326 if (res2 == NULL) {
327 Cudd_RecursiveDeref(manager,res1);
328 return(NULL);
329 }
330 cuddRef(res2);
331 res = (res1 == res2) ? res1 :
332 cuddUniqueInter(manager, (int) f->index, res1, res2);
333 if (res == NULL) {
334 Cudd_RecursiveDeref(manager,res1);
335 Cudd_RecursiveDeref(manager,res2);
336 return(NULL);
337 }
338 cuddDeref(res1);
339 cuddDeref(res2);
340 cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
341 return(res);
342 }
343
344 } /* end of cuddAddExistAbstractRecur */
345
346
347 /**Function********************************************************************
348
349 Synopsis [Performs the recursive step of Cudd_addUnivAbstract.]
350
351 Description [Performs the recursive step of Cudd_addUnivAbstract.
352 Returns the ADD obtained by abstracting the variables of cube from f,
353 if successful; NULL otherwise.]
354
355 SideEffects [None]
356
357 SeeAlso []
358
359 ******************************************************************************/
360 DdNode *
cuddAddUnivAbstractRecur(DdManager * manager,DdNode * f,DdNode * cube)361 cuddAddUnivAbstractRecur(
362 DdManager * manager,
363 DdNode * f,
364 DdNode * cube)
365 {
366 DdNode *T, *E, *res, *res1, *res2, *one, *zero;
367
368 statLine(manager);
369 one = DD_ONE(manager);
370 zero = DD_ZERO(manager);
371
372 /* Cube is guaranteed to be a cube at this point.
373 ** zero and one are the only constatnts c such that c*c=c.
374 */
375 if (f == zero || f == one || cube == one) {
376 return(f);
377 }
378
379 /* Abstract a variable that does not appear in f. */
380 if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
381 res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
382 if (res1 == NULL) return(NULL);
383 cuddRef(res1);
384 /* Use the "internal" procedure to be alerted in case of
385 ** dynamic reordering. If dynamic reordering occurs, we
386 ** have to abort the entire abstraction.
387 */
388 res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
389 if (res == NULL) {
390 Cudd_RecursiveDeref(manager,res1);
391 return(NULL);
392 }
393 cuddRef(res);
394 Cudd_RecursiveDeref(manager,res1);
395 cuddDeref(res);
396 return(res);
397 }
398
399 if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
400 return(res);
401 }
402
403 T = cuddT(f);
404 E = cuddE(f);
405
406 /* If the two indices are the same, so are their levels. */
407 if (f->index == cube->index) {
408 res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
409 if (res1 == NULL) return(NULL);
410 cuddRef(res1);
411 res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
412 if (res2 == NULL) {
413 Cudd_RecursiveDeref(manager,res1);
414 return(NULL);
415 }
416 cuddRef(res2);
417 res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
418 if (res == NULL) {
419 Cudd_RecursiveDeref(manager,res1);
420 Cudd_RecursiveDeref(manager,res2);
421 return(NULL);
422 }
423 cuddRef(res);
424 Cudd_RecursiveDeref(manager,res1);
425 Cudd_RecursiveDeref(manager,res2);
426 cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
427 cuddDeref(res);
428 return(res);
429 } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
430 res1 = cuddAddUnivAbstractRecur(manager, T, cube);
431 if (res1 == NULL) return(NULL);
432 cuddRef(res1);
433 res2 = cuddAddUnivAbstractRecur(manager, E, cube);
434 if (res2 == NULL) {
435 Cudd_RecursiveDeref(manager,res1);
436 return(NULL);
437 }
438 cuddRef(res2);
439 res = (res1 == res2) ? res1 :
440 cuddUniqueInter(manager, (int) f->index, res1, res2);
441 if (res == NULL) {
442 Cudd_RecursiveDeref(manager,res1);
443 Cudd_RecursiveDeref(manager,res2);
444 return(NULL);
445 }
446 cuddDeref(res1);
447 cuddDeref(res2);
448 cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
449 return(res);
450 }
451
452 } /* end of cuddAddUnivAbstractRecur */
453
454
455 /**Function********************************************************************
456
457 Synopsis [Performs the recursive step of Cudd_addOrAbstract.]
458
459 Description [Performs the recursive step of Cudd_addOrAbstract.
460 Returns the ADD obtained by abstracting the variables of cube from f,
461 if successful; NULL otherwise.]
462
463 SideEffects [None]
464
465 SeeAlso []
466
467 ******************************************************************************/
468 DdNode *
cuddAddOrAbstractRecur(DdManager * manager,DdNode * f,DdNode * cube)469 cuddAddOrAbstractRecur(
470 DdManager * manager,
471 DdNode * f,
472 DdNode * cube)
473 {
474 DdNode *T, *E, *res, *res1, *res2, *one;
475
476 statLine(manager);
477 one = DD_ONE(manager);
478
479 /* Cube is guaranteed to be a cube at this point. */
480 if (cuddIsConstant(f) || cube == one) {
481 return(f);
482 }
483
484 /* Abstract a variable that does not appear in f. */
485 if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
486 res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
487 return(res);
488 }
489
490 if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
491 return(res);
492 }
493
494 T = cuddT(f);
495 E = cuddE(f);
496
497 /* If the two indices are the same, so are their levels. */
498 if (f->index == cube->index) {
499 res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
500 if (res1 == NULL) return(NULL);
501 cuddRef(res1);
502 if (res1 != one) {
503 res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
504 if (res2 == NULL) {
505 Cudd_RecursiveDeref(manager,res1);
506 return(NULL);
507 }
508 cuddRef(res2);
509 res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
510 if (res == NULL) {
511 Cudd_RecursiveDeref(manager,res1);
512 Cudd_RecursiveDeref(manager,res2);
513 return(NULL);
514 }
515 cuddRef(res);
516 Cudd_RecursiveDeref(manager,res1);
517 Cudd_RecursiveDeref(manager,res2);
518 } else {
519 res = res1;
520 }
521 cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
522 cuddDeref(res);
523 return(res);
524 } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
525 res1 = cuddAddOrAbstractRecur(manager, T, cube);
526 if (res1 == NULL) return(NULL);
527 cuddRef(res1);
528 res2 = cuddAddOrAbstractRecur(manager, E, cube);
529 if (res2 == NULL) {
530 Cudd_RecursiveDeref(manager,res1);
531 return(NULL);
532 }
533 cuddRef(res2);
534 res = (res1 == res2) ? res1 :
535 cuddUniqueInter(manager, (int) f->index, res1, res2);
536 if (res == NULL) {
537 Cudd_RecursiveDeref(manager,res1);
538 Cudd_RecursiveDeref(manager,res2);
539 return(NULL);
540 }
541 cuddDeref(res1);
542 cuddDeref(res2);
543 cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
544 return(res);
545 }
546
547 } /* end of cuddAddOrAbstractRecur */
548
549
550
551 /*---------------------------------------------------------------------------*/
552 /* Definition of static functions */
553 /*---------------------------------------------------------------------------*/
554
555
556 /**Function********************************************************************
557
558 Synopsis [Checks whether cube is an ADD representing the product
559 of positive literals.]
560
561 Description [Checks whether cube is an ADD representing the product of
562 positive literals. Returns 1 in case of success; 0 otherwise.]
563
564 SideEffects [None]
565
566 SeeAlso []
567
568 ******************************************************************************/
569 static int
addCheckPositiveCube(DdManager * manager,DdNode * cube)570 addCheckPositiveCube(
571 DdManager * manager,
572 DdNode * cube)
573 {
574 if (Cudd_IsComplement(cube)) return(0);
575 if (cube == DD_ONE(manager)) return(1);
576 if (cuddIsConstant(cube)) return(0);
577 if (cuddE(cube) == DD_ZERO(manager)) {
578 return(addCheckPositiveCube(manager, cuddT(cube)));
579 }
580 return(0);
581
582 } /* end of addCheckPositiveCube */
583
584
585 ABC_NAMESPACE_IMPL_END
586
587
588
589