distr/cudd/cuddCompose.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddCompose.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functional composition and variable permutation of DDs.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddCompose()
  12                 <li> Cudd_addCompose()
  13                 <li> Cudd_addPermute()
  14                 <li> Cudd_addSwapVariables()
  15                 <li> Cudd_bddPermute()
  16                 <li> Cudd_bddVarMap()
  17                 <li> Cudd_SetVarMap()
  18                 <li> Cudd_bddSwapVariables()
  19                 <li> Cudd_bddAdjPermuteX()
  20                 <li> Cudd_addVectorCompose()
  21                 <li> Cudd_addGeneralVectorCompose()
  22                 <li> Cudd_addNonSimCompose()
  23                 <li> Cudd_bddVectorCompose()
  24                 </ul>
  25                Internal procedures included in this module:
  26                 <ul>
  27                 <li> cuddBddComposeRecur()
  28                 <li> cuddAddComposeRecur()
  29                 </ul>
  30                Static procedures included in this module:
  31                 <ul>
  32                 <li> cuddAddPermuteRecur()
  33                 <li> cuddBddPermuteRecur()
  34                 <li> cuddBddVarMapRecur()
  35                 <li> cuddAddVectorComposeRecur()
  36                 <li> cuddAddGeneralVectorComposeRecur()
  37                 <li> cuddAddNonSimComposeRecur()
  38                 <li> cuddBddVectorComposeRecur()
  39                 <li> ddIsIthAddVar()
  40                 <li> ddIsIthAddVarPair()
  41                </ul>
  42   The permutation functions use a local cache because the results to
  43   be remembered depend on the permutation being applied.  Since the
  44   permutation is just an array, it cannot be stored in the global
  45   cache. There are different procedured for BDDs and ADDs. This is
  46   because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
  47   the procedures could be merged.]
  48
  49   Author      [Fabio Somenzi and Kavita Ravi]
  50
  51   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  52
  53   All rights reserved.
  54
  55   Redistribution and use in source and binary forms, with or without
  56   modification, are permitted provided that the following conditions
  57   are met:
  58
  59   Redistributions of source code must retain the above copyright
  60   notice, this list of conditions and the following disclaimer.
  61
  62   Redistributions in binary form must reproduce the above copyright
  63   notice, this list of conditions and the following disclaimer in the
  64   documentation and/or other materials provided with the distribution.
  65
  66   Neither the name of the University of Colorado nor the names of its
  67   contributors may be used to endorse or promote products derived from
  68   this software without specific prior written permission.
  69
  70   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  71   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  72   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  73   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  74   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  75   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  76   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  77   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  78   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  79   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  80   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  81   POSSIBILITY OF SUCH DAMAGE.]
  82
  83 ******************************************************************************/
  84
  85 #include "util.h"
  86 #include "cuddInt.h"
  87
  88
  89 /*---------------------------------------------------------------------------*/
  90 /* Constant declarations                                                     */
  91 /*---------------------------------------------------------------------------*/
  92
  93 /*---------------------------------------------------------------------------*/
  94 /* Stucture declarations                                                     */
  95 /*---------------------------------------------------------------------------*/
  96
  97 /*---------------------------------------------------------------------------*/
  98 /* Type declarations                                                         */
  99 /*---------------------------------------------------------------------------*/
 100
 101 /*---------------------------------------------------------------------------*/
 102 /* Variable declarations                                                     */
 103 /*---------------------------------------------------------------------------*/
 104
 105 #ifndef lint
 106 static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $";
 107 #endif
 108
 109 #ifdef DD_DEBUG
 110 static int addPermuteRecurHits;
 111 static int bddPermuteRecurHits;
 112 static int bddVectorComposeHits;
 113 static int addVectorComposeHits;
 114
 115 static int addGeneralVectorComposeHits;
 116 #endif
 117
 118 /*---------------------------------------------------------------------------*/
 119 /* Macro declarations                                                        */
 120 /*---------------------------------------------------------------------------*/
 121
 122
 123 /**AutomaticStart*************************************************************/
 124
 125 /*---------------------------------------------------------------------------*/
 126 /* Static function prototypes                                                */
 127 /*---------------------------------------------------------------------------*/
 128
 129 static DdNode * cuddAddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
 130 static DdNode * cuddBddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
 131 static DdNode * cuddBddVarMapRecur (DdManager *manager, DdNode *f);
 132 static DdNode * cuddAddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
 133 static DdNode * cuddAddNonSimComposeRecur (DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub);
 134 static DdNode * cuddBddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
 135 DD_INLINE static int ddIsIthAddVar (DdManager *dd, DdNode *f, unsigned int i);
 136
 137 static DdNode * cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest);
 138 DD_INLINE static int ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i);
 139
 140 /**AutomaticEnd***************************************************************/
 141
 142
 143 /*---------------------------------------------------------------------------*/
 144 /* Definition of exported functions                                          */
 145 /*---------------------------------------------------------------------------*/
 146
 147
 148 /**Function********************************************************************
 149
 150   Synopsis    [Substitutes g for x_v in the BDD for f.]
 151
 152   Description [Substitutes g for x_v in the BDD for f. v is the index of the
 153   variable to be substituted. Cudd_bddCompose passes the corresponding
 154   projection function to the recursive procedure, so that the cache may
 155   be used.  Returns the composed BDD if successful; NULL otherwise.]
 156
 157   SideEffects [None]
 158
 159   SeeAlso     [Cudd_addCompose]
 160
 161 ******************************************************************************/
 162 DdNode *
 163 Cudd_bddCompose(
 164   DdManager * dd,
 165   DdNode * f,
 166   DdNode * g,
 167   int  v)
 168 {
 169     DdNode *proj, *res;
 170
 171     /* Sanity check. */
 172     if (v < 0 || v >= dd->size) return(NULL);
 173
 174     proj =  dd->vars[v];
 175     do {
 176         dd->reordered = 0;
 177         res = cuddBddComposeRecur(dd,f,g,proj);
 178     } while (dd->reordered == 1);
 179     return(res);
 180
 181 } /* end of Cudd_bddCompose */
 182
 183
 184 /**Function********************************************************************
 185
 186   Synopsis    [Substitutes g for x_v in the ADD for f.]
 187
 188   Description [Substitutes g for x_v in the ADD for f. v is the index of the
 189   variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
 190   the corresponding projection function to the recursive procedure, so
 191   that the cache may be used.  Returns the composed ADD if successful;
 192   NULL otherwise.]
 193
 194   SideEffects [None]
 195
 196   SeeAlso     [Cudd_bddCompose]
 197
 198 ******************************************************************************/
 199 DdNode *
 200 Cudd_addCompose(
 201   DdManager * dd,
 202   DdNode * f,
 203   DdNode * g,
 204   int  v)
 205 {
 206     DdNode *proj, *res;
 207
 208     /* Sanity check. */
 209     if (v < 0 || v >= dd->size) return(NULL);
 210
 211     proj =  dd->vars[v];
 212     do {
 213         dd->reordered = 0;
 214         res = cuddAddComposeRecur(dd,f,g,proj);
 215     } while (dd->reordered == 1);
 216     return(res);
 217
 218 } /* end of Cudd_addCompose */
 219
 220
 221 /**Function********************************************************************
 222
 223   Synopsis    [Permutes the variables of an ADD.]
 224
 225   Description [Given a permutation in array permut, creates a new ADD
 226   with permuted variables. There should be an entry in array permut
 227   for each variable in the manager. The i-th entry of permut holds the
 228   index of the variable that is to substitute the i-th
 229   variable. Returns a pointer to the resulting ADD if successful; NULL
 230   otherwise.]
 231
 232   SideEffects [None]
 233
 234   SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]
 235
 236 ******************************************************************************/
 237 DdNode *
 238 Cudd_addPermute(
 239   DdManager * manager,
 240   DdNode * node,
 241   int * permut)
 242 {
 243     DdHashTable         *table;
 244     DdNode              *res;
 245
 246     do {
 247         manager->reordered = 0;
 248         table = cuddHashTableInit(manager,1,2);
 249         if (table == NULL) return(NULL);
 250         /* Recursively solve the problem. */
 251         res = cuddAddPermuteRecur(manager,table,node,permut);
 252         if (res != NULL) cuddRef(res);
 253         /* Dispose of local cache. */
 254         cuddHashTableQuit(table);
 255     } while (manager->reordered == 1);
 256
 257     if (res != NULL) cuddDeref(res);
 258     return(res);
 259
 260 } /* end of Cudd_addPermute */
 261
 262
 263 /**Function********************************************************************
 264
 265   Synopsis [Swaps two sets of variables of the same size (x and y) in
 266   the ADD f.]
 267
 268   Description [Swaps two sets of variables of the same size (x and y) in
 269   the ADD f.  The size is given by n. The two sets of variables are
 270   assumed to be disjoint. Returns a pointer to the resulting ADD if
 271   successful; NULL otherwise.]
 272
 273   SideEffects [None]
 274
 275   SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]
 276
 277 ******************************************************************************/
 278 DdNode *
 279 Cudd_addSwapVariables(
 280   DdManager * dd,
 281   DdNode * f,
 282   DdNode ** x,
 283   DdNode ** y,
 284   int  n)
 285 {
 286     DdNode *swapped;
 287     int  i, j, k;
 288     int  *permut;
 289
 290     permut = ALLOC(int,dd->size);
 291     if (permut == NULL) {
 292         dd->errorCode = CUDD_MEMORY_OUT;
 293         return(NULL);
 294     }
 295     for (i = 0; i < dd->size; i++) permut[i] = i;
 296     for (i = 0; i < n; i++) {
 297         j = x[i]->index;
 298         k = y[i]->index;
 299         permut[j] = k;
 300         permut[k] = j;
 301     }
 302
 303     swapped = Cudd_addPermute(dd,f,permut);
 304     FREE(permut);
 305
 306     return(swapped);
 307
 308 } /* end of Cudd_addSwapVariables */
 309
 310
 311 /**Function********************************************************************
 312
 313   Synopsis    [Permutes the variables of a BDD.]
 314
 315   Description [Given a permutation in array permut, creates a new BDD
 316   with permuted variables. There should be an entry in array permut
 317   for each variable in the manager. The i-th entry of permut holds the
 318   index of the variable that is to substitute the i-th variable.
 319   Returns a pointer to the resulting BDD if successful; NULL
 320   otherwise.]
 321
 322   SideEffects [None]
 323
 324   SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]
 325
 326 ******************************************************************************/
 327 DdNode *
 328 Cudd_bddPermute(
 329   DdManager * manager,
 330   DdNode * node,
 331   int * permut)
 332 {
 333     DdHashTable         *table;
 334     DdNode              *res;
 335
 336     do {
 337         manager->reordered = 0;
 338         table = cuddHashTableInit(manager,1,2);
 339         if (table == NULL) return(NULL);
 340         res = cuddBddPermuteRecur(manager,table,node,permut);
 341         if (res != NULL) cuddRef(res);
 342         /* Dispose of local cache. */
 343         cuddHashTableQuit(table);
 344
 345     } while (manager->reordered == 1);
 346
 347     if (res != NULL) cuddDeref(res);
 348     return(res);
 349
 350 } /* end of Cudd_bddPermute */
 351
 352
 353 /**Function********************************************************************
 354
 355   Synopsis    [Remaps the variables of a BDD using the default variable map.]
 356
 357   Description [Remaps the variables of a BDD using the default
 358   variable map.  A typical use of this function is to swap two sets of
 359   variables.  The variable map must be registered with Cudd_SetVarMap.
 360   Returns a pointer to the resulting BDD if successful; NULL
 361   otherwise.]
 362
 363   SideEffects [None]
 364
 365   SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]
 366
 367 ******************************************************************************/
 368 DdNode *
 369 Cudd_bddVarMap(
 370   DdManager * manager /* DD manager */,
 371   DdNode * f /* function in which to remap variables */)
 372 {
 373     DdNode *res;
 374
 375     if (manager->map == NULL) return(NULL);
 376     do {
 377         manager->reordered = 0;
 378         res = cuddBddVarMapRecur(manager, f);
 379     } while (manager->reordered == 1);
 380
 381     return(res);
 382
 383 } /* end of Cudd_bddVarMap */
 384
 385
 386 /**Function********************************************************************
 387
 388   Synopsis [Registers a variable mapping with the manager.]
 389
 390   Description [Registers with the manager a variable mapping described
 391   by two sets of variables.  This variable mapping is then used by
 392   functions like Cudd_bddVarMap.  This function is convenient for
 393   those applications that perform the same mapping several times.
 394   However, if several different permutations are used, it may be more
 395   efficient not to rely on the registered mapping, because changing
 396   mapping causes the cache to be cleared.  (The initial setting,
 397   however, does not clear the cache.) The two sets of variables (x and
 398   y) must have the same size (x and y).  The size is given by n. The
 399   two sets of variables are normally disjoint, but this restriction is
 400   not imposeded by the function. When new variables are created, the
 401   map is automatically extended (each new variable maps to
 402   itself). The typical use, however, is to wait until all variables
 403   are created, and then create the map.  Returns 1 if the mapping is
 404   successfully registered with the manager; 0 otherwise.]
 405
 406   SideEffects [Modifies the manager. May clear the cache.]
 407
 408   SeeAlso     [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]
 409
 410 ******************************************************************************/
 411 int
 412 Cudd_SetVarMap (
 413   DdManager *manager /* DD manager */,
 414   DdNode **x /* first array of variables */,
 415   DdNode **y /* second array of variables */,
 416   int n /* length of both arrays */)
 417 {
 418     int i;
 419
 420     if (manager->map != NULL) {
 421         cuddCacheFlush(manager);
 422     } else {
 423         manager->map = ALLOC(int,manager->maxSize);
 424         if (manager->map == NULL) {
 425             manager->errorCode = CUDD_MEMORY_OUT;
 426             return(0);
 427         }
 428         manager->memused += sizeof(int) * manager->maxSize;
 429     }
 430     /* Initialize the map to the identity. */
 431     for (i = 0; i < manager->size; i++) {
 432         manager->map[i] = i;
 433     }
 434     /* Create the map. */
 435     for (i = 0; i < n; i++) {
 436         manager->map[x[i]->index] = y[i]->index;
 437         manager->map[y[i]->index] = x[i]->index;
 438     }
 439     return(1);
 440
 441 } /* end of Cudd_SetVarMap */
 442
 443
 444 /**Function********************************************************************
 445
 446   Synopsis [Swaps two sets of variables of the same size (x and y) in
 447   the BDD f.]
 448
 449   Description [Swaps two sets of variables of the same size (x and y)
 450   in the BDD f. The size is given by n. The two sets of variables are
 451   assumed to be disjoint.  Returns a pointer to the resulting BDD if
 452   successful; NULL otherwise.]
 453
 454   SideEffects [None]
 455
 456   SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]
 457
 458 ******************************************************************************/
 459 DdNode *
 460 Cudd_bddSwapVariables(
 461   DdManager * dd,
 462   DdNode * f,
 463   DdNode ** x,
 464   DdNode ** y,
 465   int  n)
 466 {
 467     DdNode *swapped;
 468     int  i, j, k;
 469     int  *permut;
 470
 471     permut = ALLOC(int,dd->size);
 472     if (permut == NULL) {
 473         dd->errorCode = CUDD_MEMORY_OUT;
 474         return(NULL);
 475     }
 476     for (i = 0; i < dd->size; i++) permut[i] = i;
 477     for (i = 0; i < n; i++) {
 478         j = x[i]->index;
 479         k = y[i]->index;
 480         permut[j] = k;
 481         permut[k] = j;
 482     }
 483
 484     swapped = Cudd_bddPermute(dd,f,permut);
 485     FREE(permut);
 486
 487     return(swapped);
 488
 489 } /* end of Cudd_bddSwapVariables */
 490
 491
 492 /**Function********************************************************************
 493
 494   Synopsis [Rearranges a set of variables in the BDD B.]
 495
 496   Description [Rearranges a set of variables in the BDD B. The size of
 497   the set is given by n. This procedure is intended for the
 498   `randomization' of the priority functions. Returns a pointer to the
 499   BDD if successful; NULL otherwise.]
 500
 501   SideEffects [None]
 502
 503   SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables
 504   Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]
 505
 506 ******************************************************************************/
 507 DdNode *
 508 Cudd_bddAdjPermuteX(
 509   DdManager * dd,
 510   DdNode * B,
 511   DdNode ** x,
 512   int  n)
 513 {
 514     DdNode *swapped;
 515     int  i, j, k;
 516     int  *permut;
 517
 518     permut = ALLOC(int,dd->size);
 519     if (permut == NULL) {
 520         dd->errorCode = CUDD_MEMORY_OUT;
 521         return(NULL);
 522     }
 523     for (i = 0; i < dd->size; i++) permut[i] = i;
 524     for (i = 0; i < n-2; i += 3) {
 525         j = x[i]->index;
 526         k = x[i+1]->index;
 527         permut[j] = k;
 528         permut[k] = j;
 529     }
 530
 531     swapped = Cudd_bddPermute(dd,B,permut);
 532     FREE(permut);
 533
 534     return(swapped);
 535
 536 } /* end of Cudd_bddAdjPermuteX */
 537
 538
 539 /**Function********************************************************************
 540
 541   Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]
 542
 543   Description [Given a vector of 0-1 ADDs, creates a new ADD by
 544   substituting the 0-1 ADDs for the variables of the ADD f.  There
 545   should be an entry in vector for each variable in the manager.
 546   If no substitution is sought for a given variable, the corresponding
 547   projection function should be specified in the vector.
 548   This function implements simultaneous composition.
 549   Returns a pointer to the resulting ADD if successful; NULL
 550   otherwise.]
 551
 552   SideEffects [None]
 553
 554   SeeAlso     [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
 555   Cudd_bddVectorCompose]
 556
 557 ******************************************************************************/
 558 DdNode *
 559 Cudd_addVectorCompose(
 560   DdManager * dd,
 561   DdNode * f,
 562   DdNode ** vector)
 563 {
 564     DdHashTable         *table;
 565     DdNode              *res;
 566     int                 deepest;
 567     int                 i;
 568
 569     do {
 570         dd->reordered = 0;
 571         /* Initialize local cache. */
 572         table = cuddHashTableInit(dd,1,2);
 573         if (table == NULL) return(NULL);
 574
 575         /* Find deepest real substitution. */
 576         for (deepest = dd->size - 1; deepest >= 0; deepest--) {
 577             i = dd->invperm[deepest];
 578             if (!ddIsIthAddVar(dd,vector[i],i)) {
 579                 break;
 580             }
 581         }
 582
 583         /* Recursively solve the problem. */
 584         res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
 585         if (res != NULL) cuddRef(res);
 586
 587         /* Dispose of local cache. */
 588         cuddHashTableQuit(table);
 589     } while (dd->reordered == 1);
 590
 591     if (res != NULL) cuddDeref(res);
 592     return(res);
 593
 594 } /* end of Cudd_addVectorCompose */
 595
 596
 597 /**Function********************************************************************
 598
 599   Synopsis    [Composes an ADD with a vector of ADDs.]
 600
 601   Description [Given a vector of ADDs, creates a new ADD by substituting the
 602   ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
 603   for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
 604   be an entry in vector for each variable in the manager.  If no substitution
 605   is sought for a given variable, the corresponding projection function should
 606   be specified in the vector.  This function implements simultaneous
 607   composition.  Returns a pointer to the resulting ADD if successful; NULL
 608   otherwise.]
 609
 610   SideEffects [None]
 611
 612   SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
 613   Cudd_addCompose Cudd_bddVectorCompose]
 614
 615 ******************************************************************************/
 616 DdNode *
 617 Cudd_addGeneralVectorCompose(
 618   DdManager * dd,
 619   DdNode * f,
 620   DdNode ** vectorOn,
 621   DdNode ** vectorOff)
 622 {
 623     DdHashTable         *table;
 624     DdNode              *res;
 625     int                 deepest;
 626     int                 i;
 627
 628     do {
 629         dd->reordered = 0;
 630         /* Initialize local cache. */
 631         table = cuddHashTableInit(dd,1,2);
 632         if (table == NULL) return(NULL);
 633
 634         /* Find deepest real substitution. */
 635         for (deepest = dd->size - 1; deepest >= 0; deepest--) {
 636             i = dd->invperm[deepest];
 637             if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
 638                 break;
 639             }
 640         }
 641
 642         /* Recursively solve the problem. */
 643         res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
 644                                                vectorOff,deepest);
 645         if (res != NULL) cuddRef(res);
 646
 647         /* Dispose of local cache. */
 648         cuddHashTableQuit(table);
 649     } while (dd->reordered == 1);
 650
 651     if (res != NULL) cuddDeref(res);
 652     return(res);
 653
 654 } /* end of Cudd_addGeneralVectorCompose */
 655
 656
 657 /**Function********************************************************************
 658
 659   Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]
 660
 661   Description [Given a vector of 0-1 ADDs, creates a new ADD by
 662   substituting the 0-1 ADDs for the variables of the ADD f.  There
 663   should be an entry in vector for each variable in the manager.
 664   This function implements non-simultaneous composition. If any of the
 665   functions being composed depends on any of the variables being
 666   substituted, then the result depends on the order of composition,
 667   which in turn depends on the variable order: The variables farther from
 668   the roots in the order are substituted first.
 669   Returns a pointer to the resulting ADD if successful; NULL
 670   otherwise.]
 671
 672   SideEffects [None]
 673
 674   SeeAlso     [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]
 675
 676 ******************************************************************************/
 677 DdNode *
 678 Cudd_addNonSimCompose(
 679   DdManager * dd,
 680   DdNode * f,
 681   DdNode ** vector)
 682 {
 683     DdNode              *cube, *key, *var, *tmp, *piece;
 684     DdNode              *res;
 685     int                 i, lastsub;
 686
 687     /* The cache entry for this function is composed of three parts:
 688     ** f itself, the replacement relation, and the cube of the
 689     ** variables being substituted.
 690     ** The replacement relation is the product of the terms (yi EXNOR gi).
 691     ** This apporach allows us to use the global cache for this function,
 692     ** with great savings in memory with respect to using arrays for the
 693     ** cache entries.
 694     ** First we build replacement relation and cube of substituted
 695     ** variables from the vector specifying the desired composition.
 696     */
 697     key = DD_ONE(dd);
 698     cuddRef(key);
 699     cube = DD_ONE(dd);
 700     cuddRef(cube);
 701     for (i = (int) dd->size - 1; i >= 0; i--) {
 702         if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
 703             continue;
 704         }
 705         var = Cudd_addIthVar(dd,i);
 706         if (var == NULL) {
 707             Cudd_RecursiveDeref(dd,key);
 708             Cudd_RecursiveDeref(dd,cube);
 709             return(NULL);
 710         }
 711         cuddRef(var);
 712         /* Update cube. */
 713         tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
 714         if (tmp == NULL) {
 715             Cudd_RecursiveDeref(dd,key);
 716             Cudd_RecursiveDeref(dd,cube);
 717             Cudd_RecursiveDeref(dd,var);
 718             return(NULL);
 719         }
 720         cuddRef(tmp);
 721         Cudd_RecursiveDeref(dd,cube);
 722         cube = tmp;
 723         /* Update replacement relation. */
 724         piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
 725         if (piece == NULL) {
 726             Cudd_RecursiveDeref(dd,key);
 727             Cudd_RecursiveDeref(dd,var);
 728             return(NULL);
 729         }
 730         cuddRef(piece);
 731         Cudd_RecursiveDeref(dd,var);
 732         tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
 733         if (tmp == NULL) {
 734             Cudd_RecursiveDeref(dd,key);
 735             Cudd_RecursiveDeref(dd,piece);
 736             return(NULL);
 737         }
 738         cuddRef(tmp);
 739         Cudd_RecursiveDeref(dd,key);
 740         Cudd_RecursiveDeref(dd,piece);
 741         key = tmp;
 742     }
 743
 744     /* Now try composition, until no reordering occurs. */
 745     do {
 746         /* Find real substitution with largest index. */
 747         for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
 748             if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
 749                 break;
 750             }
 751         }
 752
 753         /* Recursively solve the problem. */
 754         dd->reordered = 0;
 755         res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
 756         if (res != NULL) cuddRef(res);
 757
 758     } while (dd->reordered == 1);
 759
 760     Cudd_RecursiveDeref(dd,key);
 761     Cudd_RecursiveDeref(dd,cube);
 762     if (res != NULL) cuddDeref(res);
 763     return(res);
 764
 765 } /* end of Cudd_addNonSimCompose */
 766
 767
 768 /**Function********************************************************************
 769
 770   Synopsis    [Composes a BDD with a vector of BDDs.]
 771
 772   Description [Given a vector of BDDs, creates a new BDD by
 773   substituting the BDDs for the variables of the BDD f.  There
 774   should be an entry in vector for each variable in the manager.
 775   If no substitution is sought for a given variable, the corresponding
 776   projection function should be specified in the vector.
 777   This function implements simultaneous composition.
 778   Returns a pointer to the resulting BDD if successful; NULL
 779   otherwise.]
 780
 781   SideEffects [None]
 782
 783   SeeAlso     [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]
 784
 785 ******************************************************************************/
 786 DdNode *
 787 Cudd_bddVectorCompose(
 788   DdManager * dd,
 789   DdNode * f,
 790   DdNode ** vector)
 791 {
 792     DdHashTable         *table;
 793     DdNode              *res;
 794     int                 deepest;
 795     int                 i;
 796
 797     do {
 798         dd->reordered = 0;
 799         /* Initialize local cache. */
 800         table = cuddHashTableInit(dd,1,2);
 801         if (table == NULL) return(NULL);
 802
 803         /* Find deepest real substitution. */
 804         for (deepest = dd->size - 1; deepest >= 0; deepest--) {
 805             i = dd->invperm[deepest];
 806             if (vector[i] != dd->vars[i]) {
 807                 break;
 808             }
 809         }
 810
 811         /* Recursively solve the problem. */
 812         res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
 813         if (res != NULL) cuddRef(res);
 814
 815         /* Dispose of local cache. */
 816         cuddHashTableQuit(table);
 817     } while (dd->reordered == 1);
 818
 819     if (res != NULL) cuddDeref(res);
 820     return(res);
 821
 822 } /* end of Cudd_bddVectorCompose */
 823
 824
 825 /*---------------------------------------------------------------------------*/
 826 /* Definition of internal functions                                          */
 827 /*---------------------------------------------------------------------------*/
 828
 829
 830 /**Function********************************************************************
 831
 832   Synopsis    [Performs the recursive step of Cudd_bddCompose.]
 833
 834   Description [Performs the recursive step of Cudd_bddCompose.
 835   Exploits the fact that the composition of f' with g
 836   produces the complement of the composition of f with g to better
 837   utilize the cache.  Returns the composed BDD if successful; NULL
 838   otherwise.]
 839
 840   SideEffects [None]
 841
 842   SeeAlso     [Cudd_bddCompose]
 843
 844 ******************************************************************************/
 845 DdNode *
 846 cuddBddComposeRecur(
 847   DdManager * dd,
 848   DdNode * f,
 849   DdNode * g,
 850   DdNode * proj)
 851 {
 852     DdNode      *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
 853     unsigned int v, topf, topg, topindex;
 854     int         comple;
 855
 856     statLine(dd);
 857     v = dd->perm[proj->index];
 858     F = Cudd_Regular(f);
 859     topf = cuddI(dd,F->index);
 860
 861     /* Terminal case. Subsumes the test for constant f. */
 862     if (topf > v) return(f);
 863
 864     /* We solve the problem for a regular pointer, and then complement
 865     ** the result if the pointer was originally complemented.
 866     */
 867     comple = Cudd_IsComplement(f);
 868
 869     /* Check cache. */
 870     r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
 871     if (r != NULL) {
 872         return(Cudd_NotCond(r,comple));
 873     }
 874
 875     if (topf == v) {
 876         /* Compose. */
 877         f1 = cuddT(F);
 878         f0 = cuddE(F);
 879         r = cuddBddIteRecur(dd, g, f1, f0);
 880         if (r == NULL) return(NULL);
 881     } else {
 882         /* Compute cofactors of f and g. Remember the index of the top
 883         ** variable.
 884         */
 885         G = Cudd_Regular(g);
 886         topg = cuddI(dd,G->index);
 887         if (topf > topg) {
 888             topindex = G->index;
 889             f1 = f0 = F;
 890         } else {
 891             topindex = F->index;
 892             f1 = cuddT(F);
 893             f0 = cuddE(F);
 894         }
 895         if (topg > topf) {
 896             g1 = g0 = g;
 897         } else {
 898             g1 = cuddT(G);
 899             g0 = cuddE(G);
 900             if (g != G) {
 901                 g1 = Cudd_Not(g1);
 902                 g0 = Cudd_Not(g0);
 903             }
 904         }
 905         /* Recursive step. */
 906         t = cuddBddComposeRecur(dd, f1, g1, proj);
 907         if (t == NULL) return(NULL);
 908         cuddRef(t);
 909         e = cuddBddComposeRecur(dd, f0, g0, proj);
 910         if (e == NULL) {
 911             Cudd_IterDerefBdd(dd, t);
 912             return(NULL);
 913         }
 914         cuddRef(e);
 915
 916         r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
 917         if (r == NULL) {
 918             Cudd_IterDerefBdd(dd, t);
 919             Cudd_IterDerefBdd(dd, e);
 920             return(NULL);
 921         }
 922         cuddRef(r);
 923         Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
 924         Cudd_IterDerefBdd(dd, e);
 925         cuddDeref(r);
 926     }
 927
 928     cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);
 929
 930     return(Cudd_NotCond(r,comple));
 931
 932 } /* end of cuddBddComposeRecur */
 933
 934
 935 /**Function********************************************************************
 936
 937   Synopsis    [Performs the recursive step of Cudd_addCompose.]
 938
 939   Description [Performs the recursive step of Cudd_addCompose.
 940   Returns the composed BDD if successful; NULL otherwise.]
 941
 942   SideEffects [None]
 943
 944   SeeAlso     [Cudd_addCompose]
 945
 946 ******************************************************************************/
 947 DdNode *
 948 cuddAddComposeRecur(
 949   DdManager * dd,
 950   DdNode * f,
 951   DdNode * g,
 952   DdNode * proj)
 953 {
 954     DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
 955     unsigned int v, topf, topg, topindex;
 956
 957     statLine(dd);
 958     v = dd->perm[proj->index];
 959     topf = cuddI(dd,f->index);
 960
 961     /* Terminal case. Subsumes the test for constant f. */
 962     if (topf > v) return(f);
 963
 964     /* Check cache. */
 965     r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
 966     if (r != NULL) {
 967         return(r);
 968     }
 969
 970     if (topf == v) {
 971         /* Compose. */
 972         f1 = cuddT(f);
 973         f0 = cuddE(f);
 974         r = cuddAddIteRecur(dd, g, f1, f0);
 975         if (r == NULL) return(NULL);
 976     } else {
 977         /* Compute cofactors of f and g. Remember the index of the top
 978         ** variable.
 979         */
 980         topg = cuddI(dd,g->index);
 981         if (topf > topg) {
 982             topindex = g->index;
 983             f1 = f0 = f;
 984         } else {
 985             topindex = f->index;
 986             f1 = cuddT(f);
 987             f0 = cuddE(f);
 988         }
 989         if (topg > topf) {
 990             g1 = g0 = g;
 991         } else {
 992             g1 = cuddT(g);
 993             g0 = cuddE(g);
 994         }
 995         /* Recursive step. */
 996         t = cuddAddComposeRecur(dd, f1, g1, proj);
 997         if (t == NULL) return(NULL);
 998         cuddRef(t);
 999         e = cuddAddComposeRecur(dd, f0, g0, proj);
1000         if (e == NULL) {
1001             Cudd_RecursiveDeref(dd, t);
1002             return(NULL);
1003         }
1004         cuddRef(e);
1005
1006         if (t == e) {
1007             r = t;
1008         } else {
1009             r = cuddUniqueInter(dd, (int) topindex, t, e);
1010             if (r == NULL) {
1011                 Cudd_RecursiveDeref(dd, t);
1012                 Cudd_RecursiveDeref(dd, e);
1013                 return(NULL);
1014             }
1015         }
1016         cuddDeref(t);
1017         cuddDeref(e);
1018     }
1019
1020     cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);
1021
1022     return(r);
1023
1024 } /* end of cuddAddComposeRecur */
1025
1026
1027 /*---------------------------------------------------------------------------*/
1028 /* Definition of static functions                                            */
1029 /*---------------------------------------------------------------------------*/
1030
1031
1032 /**Function********************************************************************
1033
1034   Synopsis    [Implements the recursive step of Cudd_addPermute.]
1035
1036   Description [ Recursively puts the ADD in the order given in the
1037   array permut. Checks for trivial cases to terminate recursion, then
1038   splits on the children of this node.  Once the solutions for the
1039   children are obtained, it puts into the current position the node
1040   from the rest of the ADD that should be here. Then returns this ADD.
1041   The key here is that the node being visited is NOT put in its proper
1042   place by this instance, but rather is switched when its proper
1043   position is reached in the recursion tree.<p>
1044   The DdNode * that is returned is the same ADD as passed in as node,
1045   but in the new order.]
1046
1047   SideEffects [None]
1048
1049   SeeAlso     [Cudd_addPermute cuddBddPermuteRecur]
1050
1051 ******************************************************************************/
1052 static DdNode *
1053 cuddAddPermuteRecur(
1054   DdManager * manager /* DD manager */,
1055   DdHashTable * table /* computed table */,
1056   DdNode * node /* ADD to be reordered */,
1057   int * permut /* permutation array */)
1058 {
1059     DdNode      *T,*E;
1060     DdNode      *res,*var;
1061     int         index;
1062
1063     statLine(manager);
1064     /* Check for terminal case of constant node. */
1065     if (cuddIsConstant(node)) {
1066         return(node);
1067     }
1068
1069     /* If problem already solved, look up answer and return. */
1070     if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
1071 #ifdef DD_DEBUG
1072         addPermuteRecurHits++;
1073 #endif
1074         return(res);
1075     }
1076
1077     /* Split and recur on children of this node. */
1078     T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
1079     if (T == NULL) return(NULL);
1080     cuddRef(T);
1081     E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
1082     if (E == NULL) {
1083         Cudd_RecursiveDeref(manager, T);
1084         return(NULL);
1085     }
1086     cuddRef(E);
1087
1088     /* Move variable that should be in this position to this position
1089     ** by creating a single var ADD for that variable, and calling
1090     ** cuddAddIteRecur with the T and E we just created.
1091     */
1092     index = permut[node->index];
1093     var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
1094     if (var == NULL) return(NULL);
1095     cuddRef(var);
1096     res = cuddAddIteRecur(manager,var,T,E);
1097     if (res == NULL) {
1098         Cudd_RecursiveDeref(manager,var);
1099         Cudd_RecursiveDeref(manager, T);
1100         Cudd_RecursiveDeref(manager, E);
1101         return(NULL);
1102     }
1103     cuddRef(res);
1104     Cudd_RecursiveDeref(manager,var);
1105     Cudd_RecursiveDeref(manager, T);
1106     Cudd_RecursiveDeref(manager, E);
1107
1108     /* Do not keep the result if the reference count is only 1, since
1109     ** it will not be visited again.
1110     */
1111     if (node->ref != 1) {
1112         ptrint fanout = (ptrint) node->ref;
1113         cuddSatDec(fanout);
1114         if (!cuddHashTableInsert1(table,node,res,fanout)) {
1115             Cudd_RecursiveDeref(manager, res);
1116             return(NULL);
1117         }
1118     }
1119     cuddDeref(res);
1120     return(res);
1121
1122 } /* end of cuddAddPermuteRecur */
1123
1124
1125 /**Function********************************************************************
1126
1127   Synopsis    [Implements the recursive step of Cudd_bddPermute.]
1128
1129   Description [ Recursively puts the BDD in the order given in the array permut.
1130   Checks for trivial cases to terminate recursion, then splits on the
1131   children of this node.  Once the solutions for the children are
1132   obtained, it puts into the current position the node from the rest of
1133   the BDD that should be here. Then returns this BDD.
1134   The key here is that the node being visited is NOT put in its proper
1135   place by this instance, but rather is switched when its proper position
1136   is reached in the recursion tree.<p>
1137   The DdNode * that is returned is the same BDD as passed in as node,
1138   but in the new order.]
1139
1140   SideEffects [None]
1141
1142   SeeAlso     [Cudd_bddPermute cuddAddPermuteRecur]
1143
1144 ******************************************************************************/
1145 static DdNode *
1146 cuddBddPermuteRecur(
1147   DdManager * manager /* DD manager */,
1148   DdHashTable * table /* computed table */,
1149   DdNode * node /* BDD to be reordered */,
1150   int * permut /* permutation array */)
1151 {
1152     DdNode      *N,*T,*E;
1153     DdNode      *res;
1154     int         index;
1155
1156     statLine(manager);
1157     N = Cudd_Regular(node);
1158
1159     /* Check for terminal case of constant node. */
1160     if (cuddIsConstant(N)) {
1161         return(node);
1162     }
1163
1164     /* If problem already solved, look up answer and return. */
1165     if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
1166 #ifdef DD_DEBUG
1167         bddPermuteRecurHits++;
1168 #endif
1169         return(Cudd_NotCond(res,N != node));
1170     }
1171
1172     /* Split and recur on children of this node. */
1173     T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
1174     if (T == NULL) return(NULL);
1175     cuddRef(T);
1176     E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
1177     if (E == NULL) {
1178         Cudd_IterDerefBdd(manager, T);
1179         return(NULL);
1180     }
1181     cuddRef(E);
1182
1183     /* Move variable that should be in this position to this position
1184     ** by retrieving the single var BDD for that variable, and calling
1185     ** cuddBddIteRecur with the T and E we just created.
1186     */
1187     index = permut[N->index];
1188     res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1189     if (res == NULL) {
1190         Cudd_IterDerefBdd(manager, T);
1191         Cudd_IterDerefBdd(manager, E);
1192         return(NULL);
1193     }
1194     cuddRef(res);
1195     Cudd_IterDerefBdd(manager, T);
1196     Cudd_IterDerefBdd(manager, E);
1197
1198     /* Do not keep the result if the reference count is only 1, since
1199     ** it will not be visited again.
1200     */
1201     if (N->ref != 1) {
1202         ptrint fanout = (ptrint) N->ref;
1203         cuddSatDec(fanout);
1204         if (!cuddHashTableInsert1(table,N,res,fanout)) {
1205             Cudd_IterDerefBdd(manager, res);
1206             return(NULL);
1207         }
1208     }
1209     cuddDeref(res);
1210     return(Cudd_NotCond(res,N != node));
1211
1212 } /* end of cuddBddPermuteRecur */
1213
1214
1215 /**Function********************************************************************
1216
1217   Synopsis    [Implements the recursive step of Cudd_bddVarMap.]
1218
1219   Description [Implements the recursive step of Cudd_bddVarMap.
1220   Returns a pointer to the result if successful; NULL otherwise.]
1221
1222   SideEffects [None]
1223
1224   SeeAlso     [Cudd_bddVarMap]
1225
1226 ******************************************************************************/
1227 static DdNode *
1228 cuddBddVarMapRecur(
1229   DdManager *manager /* DD manager */,
1230   DdNode *f /* BDD to be remapped */)
1231 {
1232     DdNode      *F, *T, *E;
1233     DdNode      *res;
1234     int         index;
1235
1236     statLine(manager);
1237     F = Cudd_Regular(f);
1238
1239     /* Check for terminal case of constant node. */
1240     if (cuddIsConstant(F)) {
1241         return(f);
1242     }
1243
1244     /* If problem already solved, look up answer and return. */
1245     if (F->ref != 1 &&
1246         (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
1247         return(Cudd_NotCond(res,F != f));
1248     }
1249
1250     /* Split and recur on children of this node. */
1251     T = cuddBddVarMapRecur(manager,cuddT(F));
1252     if (T == NULL) return(NULL);
1253     cuddRef(T);
1254     E = cuddBddVarMapRecur(manager,cuddE(F));
1255     if (E == NULL) {
1256         Cudd_IterDerefBdd(manager, T);
1257         return(NULL);
1258     }
1259     cuddRef(E);
1260
1261     /* Move variable that should be in this position to this position
1262     ** by retrieving the single var BDD for that variable, and calling
1263     ** cuddBddIteRecur with the T and E we just created.
1264     */
1265     index = manager->map[F->index];
1266     res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1267     if (res == NULL) {
1268         Cudd_IterDerefBdd(manager, T);
1269         Cudd_IterDerefBdd(manager, E);
1270         return(NULL);
1271     }
1272     cuddRef(res);
1273     Cudd_IterDerefBdd(manager, T);
1274     Cudd_IterDerefBdd(manager, E);
1275
1276     /* Do not keep the result if the reference count is only 1, since
1277     ** it will not be visited again.
1278     */
1279     if (F->ref != 1) {
1280         cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
1281     }
1282     cuddDeref(res);
1283     return(Cudd_NotCond(res,F != f));
1284
1285 } /* end of cuddBddVarMapRecur */
1286
1287
1288 /**Function********************************************************************
1289
1290   Synopsis    [Performs the recursive step of Cudd_addVectorCompose.]
1291
1292   Description []
1293
1294   SideEffects [None]
1295
1296   SeeAlso     []
1297
1298 ******************************************************************************/
1299 static DdNode *
1300 cuddAddVectorComposeRecur(
1301   DdManager * dd /* DD manager */,
1302   DdHashTable * table /* computed table */,
1303   DdNode * f /* ADD in which to compose */,
1304   DdNode ** vector /* functions to substitute */,
1305   int  deepest /* depth of deepest substitution */)
1306 {
1307     DdNode      *T,*E;
1308     DdNode      *res;
1309
1310     statLine(dd);
1311     /* If we are past the deepest substitution, return f. */
1312     if (cuddI(dd,f->index) > deepest) {
1313         return(f);
1314     }
1315
1316     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1317 #ifdef DD_DEBUG
1318         addVectorComposeHits++;
1319 #endif
1320         return(res);
1321     }
1322
1323     /* Split and recur on children of this node. */
1324     T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
1325     if (T == NULL)  return(NULL);
1326     cuddRef(T);
1327     E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
1328     if (E == NULL) {
1329         Cudd_RecursiveDeref(dd, T);
1330         return(NULL);
1331     }
1332     cuddRef(E);
1333
1334     /* Retrieve the 0-1 ADD for the current top variable and call
1335     ** cuddAddIteRecur with the T and E we just created.
1336     */
1337     res = cuddAddIteRecur(dd,vector[f->index],T,E);
1338     if (res == NULL) {
1339         Cudd_RecursiveDeref(dd, T);
1340         Cudd_RecursiveDeref(dd, E);
1341         return(NULL);
1342     }
1343     cuddRef(res);
1344     Cudd_RecursiveDeref(dd, T);
1345     Cudd_RecursiveDeref(dd, E);
1346
1347     /* Do not keep the result if the reference count is only 1, since
1348     ** it will not be visited again
1349     */
1350     if (f->ref != 1) {
1351         ptrint fanout = (ptrint) f->ref;
1352         cuddSatDec(fanout);
1353         if (!cuddHashTableInsert1(table,f,res,fanout)) {
1354             Cudd_RecursiveDeref(dd, res);
1355             return(NULL);
1356         }
1357     }
1358     cuddDeref(res);
1359     return(res);
1360
1361 } /* end of cuddAddVectorComposeRecur */
1362
1363
1364 /**Function********************************************************************
1365
1366   Synopsis    [Performs the recursive step of Cudd_addGeneralVectorCompose.]
1367
1368   Description []
1369
1370   SideEffects [None]
1371
1372   SeeAlso     []
1373
1374 ******************************************************************************/
1375 static DdNode *
1376 cuddAddGeneralVectorComposeRecur(
1377   DdManager * dd /* DD manager */,
1378   DdHashTable * table /* computed table */,
1379   DdNode * f /* ADD in which to compose */,
1380   DdNode ** vectorOn /* functions to substitute for x_i */,
1381   DdNode ** vectorOff /* functions to substitute for x_i' */,
1382   int  deepest /* depth of deepest substitution */)
1383 {
1384     DdNode      *T,*E,*t,*e;
1385     DdNode      *res;
1386
1387     /* If we are past the deepest substitution, return f. */
1388     if (cuddI(dd,f->index) > deepest) {
1389         return(f);
1390     }
1391
1392     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1393 #ifdef DD_DEBUG
1394         addGeneralVectorComposeHits++;
1395 #endif
1396         return(res);
1397     }
1398
1399     /* Split and recur on children of this node. */
1400     T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
1401                                          vectorOn,vectorOff,deepest);
1402     if (T == NULL)  return(NULL);
1403     cuddRef(T);
1404     E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
1405                                          vectorOn,vectorOff,deepest);
1406     if (E == NULL) {
1407         Cudd_RecursiveDeref(dd, T);
1408         return(NULL);
1409     }
1410     cuddRef(E);
1411
1412     /* Retrieve the compose ADDs for the current top variable and call
1413     ** cuddAddApplyRecur with the T and E we just created.
1414     */
1415     t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
1416     if (t == NULL) {
1417       Cudd_RecursiveDeref(dd,T);
1418       Cudd_RecursiveDeref(dd,E);
1419       return(NULL);
1420     }
1421     cuddRef(t);
1422     e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
1423     if (e == NULL) {
1424       Cudd_RecursiveDeref(dd,T);
1425       Cudd_RecursiveDeref(dd,E);
1426       Cudd_RecursiveDeref(dd,t);
1427       return(NULL);
1428     }
1429     cuddRef(e);
1430     res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
1431     if (res == NULL) {
1432       Cudd_RecursiveDeref(dd,T);
1433       Cudd_RecursiveDeref(dd,E);
1434       Cudd_RecursiveDeref(dd,t);
1435       Cudd_RecursiveDeref(dd,e);
1436       return(NULL);
1437     }
1438     cuddRef(res);
1439     Cudd_RecursiveDeref(dd,T);
1440     Cudd_RecursiveDeref(dd,E);
1441     Cudd_RecursiveDeref(dd,t);
1442     Cudd_RecursiveDeref(dd,e);
1443
1444     /* Do not keep the result if the reference count is only 1, since
1445     ** it will not be visited again
1446     */
1447     if (f->ref != 1) {
1448         ptrint fanout = (ptrint) f->ref;
1449         cuddSatDec(fanout);
1450         if (!cuddHashTableInsert1(table,f,res,fanout)) {
1451             Cudd_RecursiveDeref(dd, res);
1452             return(NULL);
1453         }
1454     }
1455     cuddDeref(res);
1456     return(res);
1457
1458 } /* end of cuddAddGeneralVectorComposeRecur */
1459
1460
1461 /**Function********************************************************************
1462
1463   Synopsis    [Performs the recursive step of Cudd_addNonSimCompose.]
1464
1465   Description []
1466
1467   SideEffects [None]
1468
1469   SeeAlso     []
1470
1471 ******************************************************************************/
1472 static DdNode *
1473 cuddAddNonSimComposeRecur(
1474   DdManager * dd,
1475   DdNode * f,
1476   DdNode ** vector,
1477   DdNode * key,
1478   DdNode * cube,
1479   int  lastsub)
1480 {
1481     DdNode *f1, *f0, *key1, *key0, *cube1, *var;
1482     DdNode *T,*E;
1483     DdNode *r;
1484     unsigned int top, topf, topk, topc;
1485     unsigned int index;
1486     int i;
1487     DdNode **vect1;
1488     DdNode **vect0;
1489
1490     statLine(dd);
1491     /* If we are past the deepest substitution, return f. */
1492     if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
1493         return(f);
1494     }
1495
1496     /* If problem already solved, look up answer and return. */
1497     r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
1498     if (r != NULL) {
1499         return(r);
1500     }
1501
1502     /* Find top variable. we just need to look at f, key, and cube,
1503     ** because all the varibles in the gi are in key.
1504     */
1505     topf = cuddI(dd,f->index);
1506     topk = cuddI(dd,key->index);
1507     top = ddMin(topf,topk);
1508     topc = cuddI(dd,cube->index);
1509     top = ddMin(top,topc);
1510     index = dd->invperm[top];
1511
1512     /* Compute the cofactors. */
1513     if (topf == top) {
1514         f1 = cuddT(f);
1515         f0 = cuddE(f);
1516     } else {
1517         f1 = f0 = f;
1518     }
1519     if (topc == top) {
1520         cube1 = cuddT(cube);
1521         /* We want to eliminate vector[index] from key. Otherwise
1522         ** cache performance is severely affected. Hence we
1523         ** existentially quantify the variable with index "index" from key.
1524         */
1525         var = Cudd_addIthVar(dd, (int) index);
1526         if (var == NULL) {
1527             return(NULL);
1528         }
1529         cuddRef(var);
1530         key1 = cuddAddExistAbstractRecur(dd, key, var);
1531         if (key1 == NULL) {
1532             Cudd_RecursiveDeref(dd,var);
1533             return(NULL);
1534         }
1535         cuddRef(key1);
1536         Cudd_RecursiveDeref(dd,var);
1537         key0 = key1;
1538     } else {
1539         cube1 = cube;
1540         if (topk == top) {
1541             key1 = cuddT(key);
1542             key0 = cuddE(key);
1543         } else {
1544             key1 = key0 = key;
1545         }
1546         cuddRef(key1);
1547     }
1548
1549     /* Allocate two new vectors for the cofactors of vector. */
1550     vect1 = ALLOC(DdNode *,lastsub);
1551     if (vect1 == NULL) {
1552         dd->errorCode = CUDD_MEMORY_OUT;
1553         Cudd_RecursiveDeref(dd,key1);
1554         return(NULL);
1555     }
1556     vect0 = ALLOC(DdNode *,lastsub);
1557     if (vect0 == NULL) {
1558         dd->errorCode = CUDD_MEMORY_OUT;
1559         Cudd_RecursiveDeref(dd,key1);
1560         FREE(vect1);
1561         return(NULL);
1562     }
1563
1564     /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
1565     ** we do not need them.
1566     */
1567     for (i = 0; i < lastsub; i++) {
1568         DdNode *gi = vector[i];
1569         if (gi == NULL) {
1570             vect1[i] = vect0[i] = NULL;
1571         } else if (gi->index == index) {
1572             vect1[i] = cuddT(gi);
1573             vect0[i] = cuddE(gi);
1574         } else {
1575             vect1[i] = vect0[i] = gi;
1576         }
1577     }
1578     vect1[index] = vect0[index] = NULL;
1579
1580     /* Recur on children. */
1581     T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
1582     FREE(vect1);
1583     if (T == NULL) {
1584         Cudd_RecursiveDeref(dd,key1);
1585         FREE(vect0);
1586         return(NULL);
1587     }
1588     cuddRef(T);
1589     E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
1590     FREE(vect0);
1591     if (E == NULL) {
1592         Cudd_RecursiveDeref(dd,key1);
1593         Cudd_RecursiveDeref(dd,T);
1594         return(NULL);
1595     }
1596     cuddRef(E);
1597     Cudd_RecursiveDeref(dd,key1);
1598
1599     /* Retrieve the 0-1 ADD for the current top variable from vector,
1600     ** and call cuddAddIteRecur with the T and E we just created.
1601     */
1602     r = cuddAddIteRecur(dd,vector[index],T,E);
1603     if (r == NULL) {
1604         Cudd_RecursiveDeref(dd,T);
1605         Cudd_RecursiveDeref(dd,E);
1606         return(NULL);
1607     }
1608     cuddRef(r);
1609     Cudd_RecursiveDeref(dd,T);
1610     Cudd_RecursiveDeref(dd,E);
1611     cuddDeref(r);
1612
1613     /* Store answer to trim recursion. */
1614     cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);
1615
1616     return(r);
1617
1618 } /* end of cuddAddNonSimComposeRecur */
1619
1620
1621 /**Function********************************************************************
1622
1623   Synopsis    [Performs the recursive step of Cudd_bddVectorCompose.]
1624
1625   Description []
1626
1627   SideEffects [None]
1628
1629   SeeAlso     []
1630
1631 ******************************************************************************/
1632 static DdNode *
1633 cuddBddVectorComposeRecur(
1634   DdManager * dd /* DD manager */,
1635   DdHashTable * table /* computed table */,
1636   DdNode * f /* BDD in which to compose */,
1637   DdNode ** vector /* functions to be composed */,
1638   int deepest /* depth of the deepest substitution */)
1639 {
1640     DdNode      *F,*T,*E;
1641     DdNode      *res;
1642
1643     statLine(dd);
1644     F = Cudd_Regular(f);
1645
1646     /* If we are past the deepest substitution, return f. */
1647     if (cuddI(dd,F->index) > deepest) {
1648         return(f);
1649     }
1650
1651     /* If problem already solved, look up answer and return. */
1652     if ((res = cuddHashTableLookup1(table,F)) != NULL) {
1653 #ifdef DD_DEBUG
1654         bddVectorComposeHits++;
1655 #endif
1656         return(Cudd_NotCond(res,F != f));
1657     }
1658
1659     /* Split and recur on children of this node. */
1660     T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
1661     if (T == NULL) return(NULL);
1662     cuddRef(T);
1663     E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
1664     if (E == NULL) {
1665         Cudd_IterDerefBdd(dd, T);
1666         return(NULL);
1667     }
1668     cuddRef(E);
1669
1670     /* Call cuddBddIteRecur with the BDD that replaces the current top
1671     ** variable and the T and E we just created.
1672     */
1673     res = cuddBddIteRecur(dd,vector[F->index],T,E);
1674     if (res == NULL) {
1675         Cudd_IterDerefBdd(dd, T);
1676         Cudd_IterDerefBdd(dd, E);
1677         return(NULL);
1678     }
1679     cuddRef(res);
1680     Cudd_IterDerefBdd(dd, T);
1681     Cudd_IterDerefBdd(dd, E);
1682
1683     /* Do not keep the result if the reference count is only 1, since
1684     ** it will not be visited again.
1685     */
1686     if (F->ref != 1) {
1687         ptrint fanout = (ptrint) F->ref;
1688         cuddSatDec(fanout);
1689         if (!cuddHashTableInsert1(table,F,res,fanout)) {
1690             Cudd_IterDerefBdd(dd, res);
1691             return(NULL);
1692         }
1693     }
1694     cuddDeref(res);
1695     return(Cudd_NotCond(res,F != f));
1696
1697 } /* end of cuddBddVectorComposeRecur */
1698
1699
1700 /**Function********************************************************************
1701
1702   Synopsis    [Comparison of a function to the i-th ADD variable.]
1703
1704   Description [Comparison of a function to the i-th ADD variable. Returns 1 if
1705   the function is the i-th ADD variable; 0 otherwise.]
1706
1707   SideEffects [None]
1708
1709   SeeAlso     []
1710
1711 ******************************************************************************/
1712 DD_INLINE
1713 static int
1714 ddIsIthAddVar(
1715   DdManager * dd,
1716   DdNode * f,
1717   unsigned int  i)
1718 {
1719     return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));
1720
1721 } /* end of ddIsIthAddVar */
1722
1723
1724 /**Function********************************************************************
1725
1726   Synopsis    [Comparison of a pair of functions to the i-th ADD variable.]
1727
1728   Description [Comparison of a pair of functions to the i-th ADD
1729   variable. Returns 1 if the functions are the i-th ADD variable and its
1730   complement; 0 otherwise.]
1731
1732   SideEffects [None]
1733
1734   SeeAlso     []
1735
1736 ******************************************************************************/
1737 DD_INLINE
1738 static int
1739 ddIsIthAddVarPair(
1740   DdManager * dd,
1741   DdNode * f,
1742   DdNode * g,
1743   unsigned int  i)
1744 {
1745     return(f->index == i && g->index == i &&
1746            cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
1747            cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));
1748
1749 } /* end of ddIsIthAddVarPair */