distr/cudd/cuddAddAbs.c

   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
  85 static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
  86 #endif
  87
  88 static  DdNode  *two;
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Macro declarations                                                        */
  92 /*---------------------------------------------------------------------------*/
  93
  94
  95 /**AutomaticStart*************************************************************/
  96
  97 /*---------------------------------------------------------------------------*/
  98 /* Static function prototypes                                                */
  99 /*---------------------------------------------------------------------------*/
 100
 101 static 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 ******************************************************************************/
 124 DdNode *
 125 Cudd_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 ******************************************************************************/
 173 DdNode *
 174 Cudd_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 ******************************************************************************/
 211 DdNode *
 212 Cudd_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 ******************************************************************************/
 251 DdNode *
 252 cuddAddExistAbstractRecur(
 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 ******************************************************************************/
 356 DdNode *
 357 cuddAddUnivAbstractRecur(
 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 ******************************************************************************/
 464 DdNode *
 465 cuddAddOrAbstractRecur(
 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 ******************************************************************************/
 565 static int
 566 addCheckPositiveCube(
 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