distr/cudd/cuddUtil.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddUtil.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Utility functions.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_PrintMinterm()
  12                 <li> Cudd_bddPrintCover()
  13                 <li> Cudd_PrintDebug()
  14                 <li> Cudd_DagSize()
  15                 <li> Cudd_EstimateCofactor()
  16                 <li> Cudd_EstimateCofactorSimple()
  17                 <li> Cudd_SharingSize()
  18                 <li> Cudd_CountMinterm()
  19                 <li> Cudd_EpdCountMinterm()
  20                 <li> Cudd_CountPath()
  21                 <li> Cudd_CountPathsToNonZero()
  22                 <li> Cudd_Support()
  23                 <li> Cudd_SupportIndex()
  24                 <li> Cudd_SupportSize()
  25                 <li> Cudd_VectorSupport()
  26                 <li> Cudd_VectorSupportIndex()
  27                 <li> Cudd_VectorSupportSize()
  28                 <li> Cudd_ClassifySupport()
  29                 <li> Cudd_CountLeaves()
  30                 <li> Cudd_bddPickOneCube()
  31                 <li> Cudd_bddPickOneMinterm()
  32                 <li> Cudd_bddPickArbitraryMinterms()
  33                 <li> Cudd_SubsetWithMaskVars()
  34                 <li> Cudd_FirstCube()
  35                 <li> Cudd_NextCube()
  36                 <li> Cudd_bddComputeCube()
  37                 <li> Cudd_addComputeCube()
  38                 <li> Cudd_FirstNode()
  39                 <li> Cudd_NextNode()
  40                 <li> Cudd_GenFree()
  41                 <li> Cudd_IsGenEmpty()
  42                 <li> Cudd_IndicesToCube()
  43                 <li> Cudd_PrintVersion()
  44                 <li> Cudd_AverageDistance()
  45                 <li> Cudd_Random()
  46                 <li> Cudd_Srandom()
  47                 <li> Cudd_Density()
  48                 </ul>
  49         Internal procedures included in this module:
  50                 <ul>
  51                 <li> cuddP()
  52                 <li> cuddStCountfree()
  53                 <li> cuddCollectNodes()
  54                 <li> cuddNodeArray()
  55                 </ul>
  56         Static procedures included in this module:
  57                 <ul>
  58                 <li> dp2()
  59                 <li> ddPrintMintermAux()
  60                 <li> ddDagInt()
  61                 <li> ddCountMintermAux()
  62                 <li> ddEpdCountMintermAux()
  63                 <li> ddCountPathAux()
  64                 <li> ddSupportStep()
  65                 <li> ddClearFlag()
  66                 <li> ddLeavesInt()
  67                 <li> ddPickArbitraryMinterms()
  68                 <li> ddPickRepresentativeCube()
  69                 <li> ddEpdFree()
  70                 </ul>]
  71
  72   Author      [Fabio Somenzi]
  73
  74   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  75
  76   All rights reserved.
  77
  78   Redistribution and use in source and binary forms, with or without
  79   modification, are permitted provided that the following conditions
  80   are met:
  81
  82   Redistributions of source code must retain the above copyright
  83   notice, this list of conditions and the following disclaimer.
  84
  85   Redistributions in binary form must reproduce the above copyright
  86   notice, this list of conditions and the following disclaimer in the
  87   documentation and/or other materials provided with the distribution.
  88
  89   Neither the name of the University of Colorado nor the names of its
  90   contributors may be used to endorse or promote products derived from
  91   this software without specific prior written permission.
  92
  93   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  94   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  95   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  96   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  97   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  98   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  99   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 100   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 101   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 102   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
 103   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 104   POSSIBILITY OF SUCH DAMAGE.]
 105
 106 ******************************************************************************/
 107
 108 #include "util.h"
 109 #include "cuddInt.h"
 110
 111 /*---------------------------------------------------------------------------*/
 112 /* Constant declarations                                                     */
 113 /*---------------------------------------------------------------------------*/
 114
 115 /* Random generator constants. */
 116 #define MODULUS1 2147483563
 117 #define LEQA1 40014
 118 #define LEQQ1 53668
 119 #define LEQR1 12211
 120 #define MODULUS2 2147483399
 121 #define LEQA2 40692
 122 #define LEQQ2 52774
 123 #define LEQR2 3791
 124 #define STAB_SIZE 64
 125 #define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
 126
 127 /*---------------------------------------------------------------------------*/
 128 /* Stucture declarations                                                     */
 129 /*---------------------------------------------------------------------------*/
 130
 131 /*---------------------------------------------------------------------------*/
 132 /* Type declarations                                                         */
 133 /*---------------------------------------------------------------------------*/
 134
 135
 136 /*---------------------------------------------------------------------------*/
 137 /* Variable declarations                                                     */
 138 /*---------------------------------------------------------------------------*/
 139
 140 #ifndef lint
 141 static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.81 2009/03/08 02:49:02 fabio Exp $";
 142 #endif
 143
 144 static  DdNode  *background, *zero;
 145
 146 static  long cuddRand = 0;
 147 static  long cuddRand2;
 148 static  long shuffleSelect;
 149 static  long shuffleTable[STAB_SIZE];
 150
 151 /*---------------------------------------------------------------------------*/
 152 /* Macro declarations                                                        */
 153 /*---------------------------------------------------------------------------*/
 154
 155 #define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
 156
 157 #ifdef __cplusplus
 158 extern "C" {
 159 #endif
 160
 161 /**AutomaticStart*************************************************************/
 162
 163 /*---------------------------------------------------------------------------*/
 164 /* Static function prototypes                                                */
 165 /*---------------------------------------------------------------------------*/
 166
 167 static int dp2 (DdManager *dd, DdNode *f, st_table *t);
 168 static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list);
 169 static int ddDagInt (DdNode *n);
 170 static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index);
 171 static int cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr);
 172 static DdNode * cuddUniqueLookup (DdManager * unique, int  index, DdNode * T, DdNode * E);
 173 static int cuddEstimateCofactorSimple (DdNode * node, int i);
 174 static double ddCountMintermAux (DdNode *node, double max, DdHashTable *table);
 175 static int ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st_table *table);
 176 static double ddCountPathAux (DdNode *node, st_table *table);
 177 static double ddCountPathsToNonZero (DdNode * N, st_table * table);
 178 static void ddSupportStep (DdNode *f, int *support);
 179 static void ddClearFlag (DdNode *f);
 180 static int ddLeavesInt (DdNode *n);
 181 static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string);
 182 static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string);
 183 static enum st_retval ddEpdFree (char * key, char * value, char * arg);
 184
 185 /**AutomaticEnd***************************************************************/
 186
 187 #ifdef __cplusplus
 188 }
 189 #endif
 190
 191 /*---------------------------------------------------------------------------*/
 192 /* Definition of exported functions                                          */
 193 /*---------------------------------------------------------------------------*/
 194
 195
 196 /**Function********************************************************************
 197
 198   Synopsis    [Prints a disjoint sum of products.]
 199
 200   Description [Prints a disjoint sum of product cover for the function
 201   rooted at node. Each product corresponds to a path from node to a
 202   leaf node different from the logical zero, and different from the
 203   background value. Uses the package default output file.  Returns 1
 204   if successful; 0 otherwise.]
 205
 206   SideEffects [None]
 207
 208   SeeAlso     [Cudd_PrintDebug Cudd_bddPrintCover]
 209
 210 ******************************************************************************/
 211 int
 212 Cudd_PrintMinterm(
 213   DdManager * manager,
 214   DdNode * node)
 215 {
 216     int         i, *list;
 217
 218     background = manager->background;
 219     zero = Cudd_Not(manager->one);
 220     list = ALLOC(int,manager->size);
 221     if (list == NULL) {
 222         manager->errorCode = CUDD_MEMORY_OUT;
 223         return(0);
 224     }
 225     for (i = 0; i < manager->size; i++) list[i] = 2;
 226     ddPrintMintermAux(manager,node,list);
 227     FREE(list);
 228     return(1);
 229
 230 } /* end of Cudd_PrintMinterm */
 231
 232
 233 /**Function********************************************************************
 234
 235   Synopsis    [Prints a sum of prime implicants of a BDD.]
 236
 237   Description [Prints a sum of product cover for an incompletely
 238   specified function given by a lower bound and an upper bound.  Each
 239   product is a prime implicant obtained by expanding the product
 240   corresponding to a path from node to the constant one.  Uses the
 241   package default output file.  Returns 1 if successful; 0 otherwise.]
 242
 243   SideEffects [None]
 244
 245   SeeAlso     [Cudd_PrintMinterm]
 246
 247 ******************************************************************************/
 248 int
 249 Cudd_bddPrintCover(
 250   DdManager *dd,
 251   DdNode *l,
 252   DdNode *u)
 253 {
 254     int *array;
 255     int q, result;
 256     DdNode *lb;
 257 #ifdef DD_DEBUG
 258     DdNode *cover;
 259 #endif
 260
 261     array = ALLOC(int, Cudd_ReadSize(dd));
 262     if (array == NULL) return(0);
 263     lb = l;
 264     cuddRef(lb);
 265 #ifdef DD_DEBUG
 266     cover = Cudd_ReadLogicZero(dd);
 267     cuddRef(cover);
 268 #endif
 269     while (lb != Cudd_ReadLogicZero(dd)) {
 270         DdNode *implicant, *prime, *tmp;
 271         int length;
 272         implicant = Cudd_LargestCube(dd,lb,&length);
 273         if (implicant == NULL) {
 274             Cudd_RecursiveDeref(dd,lb);
 275             FREE(array);
 276             return(0);
 277         }
 278         cuddRef(implicant);
 279         prime = Cudd_bddMakePrime(dd,implicant,u);
 280         if (prime == NULL) {
 281             Cudd_RecursiveDeref(dd,lb);
 282             Cudd_RecursiveDeref(dd,implicant);
 283             FREE(array);
 284             return(0);
 285         }
 286         cuddRef(prime);
 287         Cudd_RecursiveDeref(dd,implicant);
 288         tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
 289         if (tmp == NULL) {
 290             Cudd_RecursiveDeref(dd,lb);
 291             Cudd_RecursiveDeref(dd,prime);
 292             FREE(array);
 293             return(0);
 294         }
 295         cuddRef(tmp);
 296         Cudd_RecursiveDeref(dd,lb);
 297         lb = tmp;
 298         result = Cudd_BddToCubeArray(dd,prime,array);
 299         if (result == 0) {
 300             Cudd_RecursiveDeref(dd,lb);
 301             Cudd_RecursiveDeref(dd,prime);
 302             FREE(array);
 303             return(0);
 304         }
 305         for (q = 0; q < dd->size; q++) {
 306             switch (array[q]) {
 307             case 0:
 308                 (void) fprintf(dd->out, "0");
 309                 break;
 310             case 1:
 311                 (void) fprintf(dd->out, "1");
 312                 break;
 313             case 2:
 314                 (void) fprintf(dd->out, "-");
 315                 break;
 316             default:
 317                 (void) fprintf(dd->out, "?");
 318             }
 319         }
 320         (void) fprintf(dd->out, " 1\n");
 321 #ifdef DD_DEBUG
 322         tmp = Cudd_bddOr(dd,prime,cover);
 323         if (tmp == NULL) {
 324             Cudd_RecursiveDeref(dd,cover);
 325             Cudd_RecursiveDeref(dd,lb);
 326             Cudd_RecursiveDeref(dd,prime);
 327             FREE(array);
 328             return(0);
 329         }
 330         cuddRef(tmp);
 331         Cudd_RecursiveDeref(dd,cover);
 332         cover = tmp;
 333 #endif
 334         Cudd_RecursiveDeref(dd,prime);
 335     }
 336     (void) fprintf(dd->out, "\n");
 337     Cudd_RecursiveDeref(dd,lb);
 338     FREE(array);
 339 #ifdef DD_DEBUG
 340     if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
 341         Cudd_RecursiveDeref(dd,cover);
 342         return(0);
 343     }
 344     Cudd_RecursiveDeref(dd,cover);
 345 #endif
 346     return(1);
 347
 348 } /* end of Cudd_bddPrintCover */
 349
 350
 351 /**Function********************************************************************
 352
 353   Synopsis    [Prints to the standard output a DD and its statistics.]
 354
 355   Description [Prints to the standard output a DD and its statistics.
 356   The statistics include the number of nodes, the number of leaves, and
 357   the number of minterms. (The number of minterms is the number of
 358   assignments to the variables that cause the function to be different
 359   from the logical zero (for BDDs) and from the background value (for
 360   ADDs.) The statistics are printed if pr &gt; 0. Specifically:
 361   <ul>
 362   <li> pr = 0 : prints nothing
 363   <li> pr = 1 : prints counts of nodes and minterms
 364   <li> pr = 2 : prints counts + disjoint sum of product
 365   <li> pr = 3 : prints counts + list of nodes
 366   <li> pr &gt; 3 : prints counts + disjoint sum of product + list of nodes
 367   </ul>
 368   For the purpose of counting the number of minterms, the function is
 369   supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]
 370
 371   SideEffects [None]
 372
 373   SeeAlso     [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm
 374   Cudd_PrintMinterm]
 375
 376 ******************************************************************************/
 377 int
 378 Cudd_PrintDebug(
 379   DdManager * dd,
 380   DdNode * f,
 381   int  n,
 382   int  pr)
 383 {
 384     DdNode *azero, *bzero;
 385     int    nodes;
 386     int    leaves;
 387     double minterms;
 388     int    retval = 1;
 389
 390     if (f == NULL) {
 391         (void) fprintf(dd->out,": is the NULL DD\n");
 392         (void) fflush(dd->out);
 393         return(0);
 394     }
 395     azero = DD_ZERO(dd);
 396     bzero = Cudd_Not(DD_ONE(dd));
 397     if ((f == azero || f == bzero) && pr > 0){
 398        (void) fprintf(dd->out,": is the zero DD\n");
 399        (void) fflush(dd->out);
 400        return(1);
 401     }
 402     if (pr > 0) {
 403         nodes = Cudd_DagSize(f);
 404         if (nodes == CUDD_OUT_OF_MEM) retval = 0;
 405         leaves = Cudd_CountLeaves(f);
 406         if (leaves == CUDD_OUT_OF_MEM) retval = 0;
 407         minterms = Cudd_CountMinterm(dd, f, n);
 408         if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
 409         (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
 410                        nodes, leaves, minterms);
 411         if (pr > 2) {
 412             if (!cuddP(dd, f)) retval = 0;
 413         }
 414         if (pr == 2 || pr > 3) {
 415             if (!Cudd_PrintMinterm(dd,f)) retval = 0;
 416             (void) fprintf(dd->out,"\n");
 417         }
 418         (void) fflush(dd->out);
 419     }
 420     return(retval);
 421
 422 } /* end of Cudd_PrintDebug */
 423
 424
 425 /**Function********************************************************************
 426
 427   Synopsis    [Counts the number of nodes in a DD.]
 428
 429   Description [Counts the number of nodes in a DD. Returns the number
 430   of nodes in the graph rooted at node.]
 431
 432   SideEffects [None]
 433
 434   SeeAlso     [Cudd_SharingSize Cudd_PrintDebug]
 435
 436 ******************************************************************************/
 437 int
 438 Cudd_DagSize(
 439   DdNode * node)
 440 {
 441     int i;
 442
 443     i = ddDagInt(Cudd_Regular(node));
 444     ddClearFlag(Cudd_Regular(node));
 445
 446     return(i);
 447
 448 } /* end of Cudd_DagSize */
 449
 450
 451 /**Function********************************************************************
 452
 453   Synopsis    [Estimates the number of nodes in a cofactor of a DD.]
 454
 455   Description [Estimates the number of nodes in a cofactor of a DD.
 456   Returns an estimate of the number of nodes in a cofactor of
 457   the graph rooted at node with respect to the variable whose index is i.
 458   In case of failure, returns CUDD_OUT_OF_MEM.
 459   This function uses a refinement of the algorithm of Cabodi et al.
 460   (ICCAD96). The refinement allows the procedure to account for part
 461   of the recombination that may occur in the part of the cofactor above
 462   the cofactoring variable. This procedure does no create any new node.
 463   It does keep a small table of results; therefore it may run out of memory.
 464   If this is a concern, one should use Cudd_EstimateCofactorSimple, which
 465   is faster, does not allocate any memory, but is less accurate.]
 466
 467   SideEffects [None]
 468
 469   SeeAlso     [Cudd_DagSize Cudd_EstimateCofactorSimple]
 470
 471 ******************************************************************************/
 472 int
 473 Cudd_EstimateCofactor(
 474   DdManager *dd /* manager */,
 475   DdNode * f    /* function */,
 476   int i         /* index of variable */,
 477   int phase     /* 1: positive; 0: negative */
 478   )
 479 {
 480     int val;
 481     DdNode *ptr;
 482     st_table *table;
 483
 484     table = st_init_table(st_ptrcmp,st_ptrhash);
 485     if (table == NULL) return(CUDD_OUT_OF_MEM);
 486     val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
 487     ddClearFlag(Cudd_Regular(f));
 488     st_free_table(table);
 489
 490     return(val);
 491
 492 } /* end of Cudd_EstimateCofactor */
 493
 494
 495 /**Function********************************************************************
 496
 497   Synopsis    [Estimates the number of nodes in a cofactor of a DD.]
 498
 499   Description [Estimates the number of nodes in a cofactor of a DD.
 500   Returns an estimate of the number of nodes in the positive cofactor of
 501   the graph rooted at node with respect to the variable whose index is i.
 502   This procedure implements with minor changes the algorithm of Cabodi et al.
 503   (ICCAD96). It does not allocate any memory, it does not change the
 504   state of the manager, and it is fast. However, it has been observed to
 505   overestimate the size of the cofactor by as much as a factor of 2.]
 506
 507   SideEffects [None]
 508
 509   SeeAlso     [Cudd_DagSize]
 510
 511 ******************************************************************************/
 512 int
 513 Cudd_EstimateCofactorSimple(
 514   DdNode * node,
 515   int i)
 516 {
 517     int val;
 518
 519     val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
 520     ddClearFlag(Cudd_Regular(node));
 521
 522     return(val);
 523
 524 } /* end of Cudd_EstimateCofactorSimple */
 525
 526
 527 /**Function********************************************************************
 528
 529   Synopsis    [Counts the number of nodes in an array of DDs.]
 530
 531   Description [Counts the number of nodes in an array of DDs. Shared
 532   nodes are counted only once.  Returns the total number of nodes.]
 533
 534   SideEffects [None]
 535
 536   SeeAlso     [Cudd_DagSize]
 537
 538 ******************************************************************************/
 539 int
 540 Cudd_SharingSize(
 541   DdNode ** nodeArray,
 542   int  n)
 543 {
 544     int i,j;
 545
 546     i = 0;
 547     for (j = 0; j < n; j++) {
 548         i += ddDagInt(Cudd_Regular(nodeArray[j]));
 549     }
 550     for (j = 0; j < n; j++) {
 551         ddClearFlag(Cudd_Regular(nodeArray[j]));
 552     }
 553     return(i);
 554
 555 } /* end of Cudd_SharingSize */
 556
 557
 558 /**Function********************************************************************
 559
 560   Synopsis    [Counts the number of minterms of a DD.]
 561
 562   Description [Counts the number of minterms of a DD. The function is
 563   assumed to depend on nvars variables. The minterm count is
 564   represented as a double, to allow for a larger number of variables.
 565   Returns the number of minterms of the function rooted at node if
 566   successful; (double) CUDD_OUT_OF_MEM otherwise.]
 567
 568   SideEffects [None]
 569
 570   SeeAlso     [Cudd_PrintDebug Cudd_CountPath]
 571
 572 ******************************************************************************/
 573 double
 574 Cudd_CountMinterm(
 575   DdManager * manager,
 576   DdNode * node,
 577   int  nvars)
 578 {
 579     double      max;
 580     DdHashTable *table;
 581     double      res;
 582     CUDD_VALUE_TYPE epsilon;
 583
 584     background = manager->background;
 585     zero = Cudd_Not(manager->one);
 586
 587     max = pow(2.0,(double)nvars);
 588     table = cuddHashTableInit(manager,1,2);
 589     if (table == NULL) {
 590         return((double)CUDD_OUT_OF_MEM);
 591     }
 592     epsilon = Cudd_ReadEpsilon(manager);
 593     Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
 594     res = ddCountMintermAux(node,max,table);
 595     cuddHashTableQuit(table);
 596     Cudd_SetEpsilon(manager,epsilon);
 597
 598     return(res);
 599
 600 } /* end of Cudd_CountMinterm */
 601
 602
 603 /**Function********************************************************************
 604
 605   Synopsis    [Counts the number of paths of a DD.]
 606
 607   Description [Counts the number of paths of a DD.  Paths to all
 608   terminal nodes are counted. The path count is represented as a
 609   double, to allow for a larger number of variables.  Returns the
 610   number of paths of the function rooted at node if successful;
 611   (double) CUDD_OUT_OF_MEM otherwise.]
 612
 613   SideEffects [None]
 614
 615   SeeAlso     [Cudd_CountMinterm]
 616
 617 ******************************************************************************/
 618 double
 619 Cudd_CountPath(
 620   DdNode * node)
 621 {
 622
 623     st_table    *table;
 624     double      i;
 625
 626     table = st_init_table(st_ptrcmp,st_ptrhash);
 627     if (table == NULL) {
 628         return((double)CUDD_OUT_OF_MEM);
 629     }
 630     i = ddCountPathAux(Cudd_Regular(node),table);
 631     st_foreach(table, cuddStCountfree, NULL);
 632     st_free_table(table);
 633     return(i);
 634
 635 } /* end of Cudd_CountPath */
 636
 637
 638 /**Function********************************************************************
 639
 640   Synopsis    [Counts the number of minterms of a DD with extended precision.]
 641
 642   Description [Counts the number of minterms of a DD with extended precision.
 643   The function is assumed to depend on nvars variables. The minterm count is
 644   represented as an EpDouble, to allow any number of variables.
 645   Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]
 646
 647   SideEffects [None]
 648
 649   SeeAlso     [Cudd_PrintDebug Cudd_CountPath]
 650
 651 ******************************************************************************/
 652 int
 653 Cudd_EpdCountMinterm(
 654   DdManager * manager,
 655   DdNode * node,
 656   int  nvars,
 657   EpDouble * epd)
 658 {
 659     EpDouble    max, tmp;
 660     st_table    *table;
 661     int         status;
 662
 663     background = manager->background;
 664     zero = Cudd_Not(manager->one);
 665
 666     EpdPow2(nvars, &max);
 667     table = st_init_table(EpdCmp, st_ptrhash);
 668     if (table == NULL) {
 669         EpdMakeZero(epd, 0);
 670         return(CUDD_OUT_OF_MEM);
 671     }
 672     status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
 673     st_foreach(table, ddEpdFree, NULL);
 674     st_free_table(table);
 675     if (status == CUDD_OUT_OF_MEM) {
 676         EpdMakeZero(epd, 0);
 677         return(CUDD_OUT_OF_MEM);
 678     }
 679     if (Cudd_IsComplement(node)) {
 680         EpdSubtract3(&max, epd, &tmp);
 681         EpdCopy(&tmp, epd);
 682     }
 683     return(0);
 684
 685 } /* end of Cudd_EpdCountMinterm */
 686
 687
 688 /**Function********************************************************************
 689
 690   Synopsis    [Counts the number of paths to a non-zero terminal of a DD.]
 691
 692   Description [Counts the number of paths to a non-zero terminal of a
 693   DD.  The path count is
 694   represented as a double, to allow for a larger number of variables.
 695   Returns the number of paths of the function rooted at node.]
 696
 697   SideEffects [None]
 698
 699   SeeAlso     [Cudd_CountMinterm Cudd_CountPath]
 700
 701 ******************************************************************************/
 702 double
 703 Cudd_CountPathsToNonZero(
 704   DdNode * node)
 705 {
 706
 707     st_table    *table;
 708     double      i;
 709
 710     table = st_init_table(st_ptrcmp,st_ptrhash);
 711     if (table == NULL) {
 712         return((double)CUDD_OUT_OF_MEM);
 713     }
 714     i = ddCountPathsToNonZero(node,table);
 715     st_foreach(table, cuddStCountfree, NULL);
 716     st_free_table(table);
 717     return(i);
 718
 719 } /* end of Cudd_CountPathsToNonZero */
 720
 721
 722 /**Function********************************************************************
 723
 724   Synopsis    [Finds the variables on which a DD depends.]
 725
 726   Description [Finds the variables on which a DD depends.
 727   Returns a BDD consisting of the product of the variables if
 728   successful; NULL otherwise.]
 729
 730   SideEffects [None]
 731
 732   SeeAlso     [Cudd_VectorSupport Cudd_ClassifySupport]
 733
 734 ******************************************************************************/
 735 DdNode *
 736 Cudd_Support(
 737   DdManager * dd /* manager */,
 738   DdNode * f /* DD whose support is sought */)
 739 {
 740     int *support;
 741     DdNode *res, *tmp, *var;
 742     int i,j;
 743     int size;
 744
 745     /* Allocate and initialize support array for ddSupportStep. */
 746     size = ddMax(dd->size, dd->sizeZ);
 747     support = ALLOC(int,size);
 748     if (support == NULL) {
 749         dd->errorCode = CUDD_MEMORY_OUT;
 750         return(NULL);
 751     }
 752     for (i = 0; i < size; i++) {
 753         support[i] = 0;
 754     }
 755
 756     /* Compute support and clean up markers. */
 757     ddSupportStep(Cudd_Regular(f),support);
 758     ddClearFlag(Cudd_Regular(f));
 759
 760     /* Transform support from array to cube. */
 761     do {
 762         dd->reordered = 0;
 763         res = DD_ONE(dd);
 764         cuddRef(res);
 765         for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
 766             i = (j >= dd->size) ? j : dd->invperm[j];
 767             if (support[i] == 1) {
 768                 /* The following call to cuddUniqueInter is guaranteed
 769                 ** not to trigger reordering because the node we look up
 770                 ** already exists. */
 771                 var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
 772                 cuddRef(var);
 773                 tmp = cuddBddAndRecur(dd,res,var);
 774                 if (tmp == NULL) {
 775                     Cudd_RecursiveDeref(dd,res);
 776                     Cudd_RecursiveDeref(dd,var);
 777                     res = NULL;
 778                     break;
 779                 }
 780                 cuddRef(tmp);
 781                 Cudd_RecursiveDeref(dd,res);
 782                 Cudd_RecursiveDeref(dd,var);
 783                 res = tmp;
 784             }
 785         }
 786     } while (dd->reordered == 1);
 787
 788     FREE(support);
 789     if (res != NULL) cuddDeref(res);
 790     return(res);
 791
 792 } /* end of Cudd_Support */
 793
 794
 795 /**Function********************************************************************
 796
 797   Synopsis    [Finds the variables on which a DD depends.]
 798
 799   Description [Finds the variables on which a DD depends.  Returns an
 800   index array of the variables if successful; NULL otherwise.  The
 801   size of the array equals the number of variables in the manager.
 802   Each entry of the array is 1 if the corresponding variable is in the
 803   support of the DD and 0 otherwise.]
 804
 805   SideEffects [None]
 806
 807   SeeAlso     [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]
 808
 809 ******************************************************************************/
 810 int *
 811 Cudd_SupportIndex(
 812   DdManager * dd /* manager */,
 813   DdNode * f /* DD whose support is sought */)
 814 {
 815     int *support;
 816     int i;
 817     int size;
 818
 819     /* Allocate and initialize support array for ddSupportStep. */
 820     size = ddMax(dd->size, dd->sizeZ);
 821     support = ALLOC(int,size);
 822     if (support == NULL) {
 823         dd->errorCode = CUDD_MEMORY_OUT;
 824         return(NULL);
 825     }
 826     for (i = 0; i < size; i++) {
 827         support[i] = 0;
 828     }
 829
 830     /* Compute support and clean up markers. */
 831     ddSupportStep(Cudd_Regular(f),support);
 832     ddClearFlag(Cudd_Regular(f));
 833
 834     return(support);
 835
 836 } /* end of Cudd_SupportIndex */
 837
 838
 839 /**Function********************************************************************
 840
 841   Synopsis    [Counts the variables on which a DD depends.]
 842
 843   Description [Counts the variables on which a DD depends.
 844   Returns the number of the variables if successful; CUDD_OUT_OF_MEM
 845   otherwise.]
 846
 847   SideEffects [None]
 848
 849   SeeAlso     [Cudd_Support]
 850
 851 ******************************************************************************/
 852 int
 853 Cudd_SupportSize(
 854   DdManager * dd /* manager */,
 855   DdNode * f /* DD whose support size is sought */)
 856 {
 857     int *support;
 858     int i;
 859     int size;
 860     int count;
 861
 862     /* Allocate and initialize support array for ddSupportStep. */
 863     size = ddMax(dd->size, dd->sizeZ);
 864     support = ALLOC(int,size);
 865     if (support == NULL) {
 866         dd->errorCode = CUDD_MEMORY_OUT;
 867         return(CUDD_OUT_OF_MEM);
 868     }
 869     for (i = 0; i < size; i++) {
 870         support[i] = 0;
 871     }
 872
 873     /* Compute support and clean up markers. */
 874     ddSupportStep(Cudd_Regular(f),support);
 875     ddClearFlag(Cudd_Regular(f));
 876
 877     /* Count support variables. */
 878     count = 0;
 879     for (i = 0; i < size; i++) {
 880         if (support[i] == 1) count++;
 881     }
 882
 883     FREE(support);
 884     return(count);
 885
 886 } /* end of Cudd_SupportSize */
 887
 888
 889 /**Function********************************************************************
 890
 891   Synopsis    [Finds the variables on which a set of DDs depends.]
 892
 893   Description [Finds the variables on which a set of DDs depends.
 894   The set must contain either BDDs and ADDs, or ZDDs.
 895   Returns a BDD consisting of the product of the variables if
 896   successful; NULL otherwise.]
 897
 898   SideEffects [None]
 899
 900   SeeAlso     [Cudd_Support Cudd_ClassifySupport]
 901
 902 ******************************************************************************/
 903 DdNode *
 904 Cudd_VectorSupport(
 905   DdManager * dd /* manager */,
 906   DdNode ** F /* array of DDs whose support is sought */,
 907   int  n /* size of the array */)
 908 {
 909     int *support;
 910     DdNode *res, *tmp, *var;
 911     int i,j;
 912     int size;
 913
 914     /* Allocate and initialize support array for ddSupportStep. */
 915     size = ddMax(dd->size, dd->sizeZ);
 916     support = ALLOC(int,size);
 917     if (support == NULL) {
 918         dd->errorCode = CUDD_MEMORY_OUT;
 919         return(NULL);
 920     }
 921     for (i = 0; i < size; i++) {
 922         support[i] = 0;
 923     }
 924
 925     /* Compute support and clean up markers. */
 926     for (i = 0; i < n; i++) {
 927         ddSupportStep(Cudd_Regular(F[i]),support);
 928     }
 929     for (i = 0; i < n; i++) {
 930         ddClearFlag(Cudd_Regular(F[i]));
 931     }
 932
 933     /* Transform support from array to cube. */
 934     res = DD_ONE(dd);
 935     cuddRef(res);
 936     for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
 937         i = (j >= dd->size) ? j : dd->invperm[j];
 938         if (support[i] == 1) {
 939             var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
 940             cuddRef(var);
 941             tmp = Cudd_bddAnd(dd,res,var);
 942             if (tmp == NULL) {
 943                 Cudd_RecursiveDeref(dd,res);
 944                 Cudd_RecursiveDeref(dd,var);
 945                 FREE(support);
 946                 return(NULL);
 947             }
 948             cuddRef(tmp);
 949             Cudd_RecursiveDeref(dd,res);
 950             Cudd_RecursiveDeref(dd,var);
 951             res = tmp;
 952         }
 953     }
 954
 955     FREE(support);
 956     cuddDeref(res);
 957     return(res);
 958
 959 } /* end of Cudd_VectorSupport */
 960
 961
 962 /**Function********************************************************************
 963
 964   Synopsis    [Finds the variables on which a set of DDs depends.]
 965
 966   Description [Finds the variables on which a set of DDs depends.
 967   The set must contain either BDDs and ADDs, or ZDDs.
 968   Returns an index array of the variables if successful; NULL otherwise.]
 969
 970   SideEffects [None]
 971
 972   SeeAlso     [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]
 973
 974 ******************************************************************************/
 975 int *
 976 Cudd_VectorSupportIndex(
 977   DdManager * dd /* manager */,
 978   DdNode ** F /* array of DDs whose support is sought */,
 979   int  n /* size of the array */)
 980 {
 981     int *support;
 982     int i;
 983     int size;
 984
 985     /* Allocate and initialize support array for ddSupportStep. */
 986     size = ddMax(dd->size, dd->sizeZ);
 987     support = ALLOC(int,size);
 988     if (support == NULL) {
 989         dd->errorCode = CUDD_MEMORY_OUT;
 990         return(NULL);
 991     }
 992     for (i = 0; i < size; i++) {
 993         support[i] = 0;
 994     }
 995
 996     /* Compute support and clean up markers. */
 997     for (i = 0; i < n; i++) {
 998         ddSupportStep(Cudd_Regular(F[i]),support);
 999     }
1000     for (i = 0; i < n; i++) {
1001         ddClearFlag(Cudd_Regular(F[i]));
1002     }
1003
1004     return(support);
1005
1006 } /* end of Cudd_VectorSupportIndex */
1007
1008
1009 /**Function********************************************************************
1010
1011   Synopsis    [Counts the variables on which a set of DDs depends.]
1012
1013   Description [Counts the variables on which a set of DDs depends.
1014   The set must contain either BDDs and ADDs, or ZDDs.
1015   Returns the number of the variables if successful; CUDD_OUT_OF_MEM
1016   otherwise.]
1017
1018   SideEffects [None]
1019
1020   SeeAlso     [Cudd_VectorSupport Cudd_SupportSize]
1021
1022 ******************************************************************************/
1023 int
1024 Cudd_VectorSupportSize(
1025   DdManager * dd /* manager */,
1026   DdNode ** F /* array of DDs whose support is sought */,
1027   int  n /* size of the array */)
1028 {
1029     int *support;
1030     int i;
1031     int size;
1032     int count;
1033
1034     /* Allocate and initialize support array for ddSupportStep. */
1035     size = ddMax(dd->size, dd->sizeZ);
1036     support = ALLOC(int,size);
1037     if (support == NULL) {
1038         dd->errorCode = CUDD_MEMORY_OUT;
1039         return(CUDD_OUT_OF_MEM);
1040     }
1041     for (i = 0; i < size; i++) {
1042         support[i] = 0;
1043     }
1044
1045     /* Compute support and clean up markers. */
1046     for (i = 0; i < n; i++) {
1047         ddSupportStep(Cudd_Regular(F[i]),support);
1048     }
1049     for (i = 0; i < n; i++) {
1050         ddClearFlag(Cudd_Regular(F[i]));
1051     }
1052
1053     /* Count vriables in support. */
1054     count = 0;
1055     for (i = 0; i < size; i++) {
1056         if (support[i] == 1) count++;
1057     }
1058
1059     FREE(support);
1060     return(count);
1061
1062 } /* end of Cudd_VectorSupportSize */
1063
1064
1065 /**Function********************************************************************
1066
1067   Synopsis    [Classifies the variables in the support of two DDs.]
1068
1069   Description [Classifies the variables in the support of two DDs
1070   <code>f</code> and <code>g</code>, depending on whther they appear
1071   in both DDs, only in <code>f</code>, or only in <code>g</code>.
1072   Returns 1 if successful; 0 otherwise.]
1073
1074   SideEffects [The cubes of the three classes of variables are
1075   returned as side effects.]
1076
1077   SeeAlso     [Cudd_Support Cudd_VectorSupport]
1078
1079 ******************************************************************************/
1080 int
1081 Cudd_ClassifySupport(
1082   DdManager * dd /* manager */,
1083   DdNode * f /* first DD */,
1084   DdNode * g /* second DD */,
1085   DdNode ** common /* cube of shared variables */,
1086   DdNode ** onlyF /* cube of variables only in f */,
1087   DdNode ** onlyG /* cube of variables only in g */)
1088 {
1089     int *supportF, *supportG;
1090     DdNode *tmp, *var;
1091     int i,j;
1092     int size;
1093
1094     /* Allocate and initialize support arrays for ddSupportStep. */
1095     size = ddMax(dd->size, dd->sizeZ);
1096     supportF = ALLOC(int,size);
1097     if (supportF == NULL) {
1098         dd->errorCode = CUDD_MEMORY_OUT;
1099         return(0);
1100     }
1101     supportG = ALLOC(int,size);
1102     if (supportG == NULL) {
1103         dd->errorCode = CUDD_MEMORY_OUT;
1104         FREE(supportF);
1105         return(0);
1106     }
1107     for (i = 0; i < size; i++) {
1108         supportF[i] = 0;
1109         supportG[i] = 0;
1110     }
1111
1112     /* Compute supports and clean up markers. */
1113     ddSupportStep(Cudd_Regular(f),supportF);
1114     ddClearFlag(Cudd_Regular(f));
1115     ddSupportStep(Cudd_Regular(g),supportG);
1116     ddClearFlag(Cudd_Regular(g));
1117
1118     /* Classify variables and create cubes. */
1119     *common = *onlyF = *onlyG = DD_ONE(dd);
1120     cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
1121     for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
1122         i = (j >= dd->size) ? j : dd->invperm[j];
1123         if (supportF[i] == 0 && supportG[i] == 0) continue;
1124         var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
1125         cuddRef(var);
1126         if (supportG[i] == 0) {
1127             tmp = Cudd_bddAnd(dd,*onlyF,var);
1128             if (tmp == NULL) {
1129                 Cudd_RecursiveDeref(dd,*common);
1130                 Cudd_RecursiveDeref(dd,*onlyF);
1131                 Cudd_RecursiveDeref(dd,*onlyG);
1132                 Cudd_RecursiveDeref(dd,var);
1133                 FREE(supportF); FREE(supportG);
1134                 return(0);
1135             }
1136             cuddRef(tmp);
1137             Cudd_RecursiveDeref(dd,*onlyF);
1138             *onlyF = tmp;
1139         } else if (supportF[i] == 0) {
1140             tmp = Cudd_bddAnd(dd,*onlyG,var);
1141             if (tmp == NULL) {
1142                 Cudd_RecursiveDeref(dd,*common);
1143                 Cudd_RecursiveDeref(dd,*onlyF);
1144                 Cudd_RecursiveDeref(dd,*onlyG);
1145                 Cudd_RecursiveDeref(dd,var);
1146                 FREE(supportF); FREE(supportG);
1147                 return(0);
1148             }
1149             cuddRef(tmp);
1150             Cudd_RecursiveDeref(dd,*onlyG);
1151             *onlyG = tmp;
1152         } else {
1153             tmp = Cudd_bddAnd(dd,*common,var);
1154             if (tmp == NULL) {
1155                 Cudd_RecursiveDeref(dd,*common);
1156                 Cudd_RecursiveDeref(dd,*onlyF);
1157                 Cudd_RecursiveDeref(dd,*onlyG);
1158                 Cudd_RecursiveDeref(dd,var);
1159                 FREE(supportF); FREE(supportG);
1160                 return(0);
1161             }
1162             cuddRef(tmp);
1163             Cudd_RecursiveDeref(dd,*common);
1164             *common = tmp;
1165         }
1166         Cudd_RecursiveDeref(dd,var);
1167     }
1168
1169     FREE(supportF); FREE(supportG);
1170     cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
1171     return(1);
1172
1173 } /* end of Cudd_ClassifySupport */
1174
1175
1176 /**Function********************************************************************
1177
1178   Synopsis    [Counts the number of leaves in a DD.]
1179
1180   Description [Counts the number of leaves in a DD. Returns the number
1181   of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM
1182   otherwise.]
1183
1184   SideEffects [None]
1185
1186   SeeAlso     [Cudd_PrintDebug]
1187
1188 ******************************************************************************/
1189 int
1190 Cudd_CountLeaves(
1191   DdNode * node)
1192 {
1193     int i;
1194
1195     i = ddLeavesInt(Cudd_Regular(node));
1196     ddClearFlag(Cudd_Regular(node));
1197     return(i);
1198
1199 } /* end of Cudd_CountLeaves */
1200
1201
1202 /**Function********************************************************************
1203
1204   Synopsis    [Picks one on-set cube randomly from the given DD.]
1205
1206   Description [Picks one on-set cube randomly from the given DD. The
1207   cube is written into an array of characters.  The array must have at
1208   least as many entries as there are variables. Returns 1 if
1209   successful; 0 otherwise.]
1210
1211   SideEffects [None]
1212
1213   SeeAlso     [Cudd_bddPickOneMinterm]
1214
1215 ******************************************************************************/
1216 int
1217 Cudd_bddPickOneCube(
1218   DdManager * ddm,
1219   DdNode * node,
1220   char * string)
1221 {
1222     DdNode *N, *T, *E;
1223     DdNode *one, *bzero;
1224     char   dir;
1225     int    i;
1226
1227     if (string == NULL || node == NULL) return(0);
1228
1229     /* The constant 0 function has no on-set cubes. */
1230     one = DD_ONE(ddm);
1231     bzero = Cudd_Not(one);
1232     if (node == bzero) return(0);
1233
1234     for (i = 0; i < ddm->size; i++) string[i] = 2;
1235
1236     for (;;) {
1237
1238         if (node == one) break;
1239
1240         N = Cudd_Regular(node);
1241
1242         T = cuddT(N); E = cuddE(N);
1243         if (Cudd_IsComplement(node)) {
1244             T = Cudd_Not(T); E = Cudd_Not(E);
1245         }
1246         if (T == bzero) {
1247             string[N->index] = 0;
1248             node = E;
1249         } else if (E == bzero) {
1250             string[N->index] = 1;
1251             node = T;
1252         } else {
1253             dir = (char) ((Cudd_Random() & 0x2000) >> 13);
1254             string[N->index] = dir;
1255             node = dir ? T : E;
1256         }
1257     }
1258     return(1);
1259
1260 } /* end of Cudd_bddPickOneCube */
1261
1262
1263 /**Function********************************************************************
1264
1265   Synopsis    [Picks one on-set minterm randomly from the given DD.]
1266
1267   Description [Picks one on-set minterm randomly from the given
1268   DD. The minterm is in terms of <code>vars</code>. The array
1269   <code>vars</code> should contain at least all variables in the
1270   support of <code>f</code>; if this condition is not met the minterm
1271   built by this procedure may not be contained in
1272   <code>f</code>. Builds a BDD for the minterm and returns a pointer
1273   to it if successful; NULL otherwise. There are three reasons why the
1274   procedure may fail:
1275   <ul>
1276   <li> It may run out of memory;
1277   <li> the function <code>f</code> may be the constant 0;
1278   <li> the minterm may not be contained in <code>f</code>.
1279   </ul>]
1280
1281   SideEffects [None]
1282
1283   SeeAlso     [Cudd_bddPickOneCube]
1284
1285 ******************************************************************************/
1286 DdNode *
1287 Cudd_bddPickOneMinterm(
1288   DdManager * dd /* manager */,
1289   DdNode * f /* function from which to pick one minterm */,
1290   DdNode ** vars /* array of variables */,
1291   int  n /* size of <code>vars</code> */)
1292 {
1293     char *string;
1294     int i, size;
1295     int *indices;
1296     int result;
1297     DdNode *old, *neW;
1298
1299     size = dd->size;
1300     string = ALLOC(char, size);
1301     if (string == NULL) {
1302         dd->errorCode = CUDD_MEMORY_OUT;
1303         return(NULL);
1304     }
1305     indices = ALLOC(int,n);
1306     if (indices == NULL) {
1307         dd->errorCode = CUDD_MEMORY_OUT;
1308         FREE(string);
1309         return(NULL);
1310     }
1311
1312     for (i = 0; i < n; i++) {
1313         indices[i] = vars[i]->index;
1314     }
1315
1316     result = Cudd_bddPickOneCube(dd,f,string);
1317     if (result == 0) {
1318         FREE(string);
1319         FREE(indices);
1320         return(NULL);
1321     }
1322
1323     /* Randomize choice for don't cares. */
1324     for (i = 0; i < n; i++) {
1325         if (string[indices[i]] == 2)
1326             string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
1327     }
1328
1329     /* Build result BDD. */
1330     old = Cudd_ReadOne(dd);
1331     cuddRef(old);
1332
1333     for (i = n-1; i >= 0; i--) {
1334         neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
1335         if (neW == NULL) {
1336             FREE(string);
1337             FREE(indices);
1338             Cudd_RecursiveDeref(dd,old);
1339             return(NULL);
1340         }
1341         cuddRef(neW);
1342         Cudd_RecursiveDeref(dd,old);
1343         old = neW;
1344     }
1345
1346 #ifdef DD_DEBUG
1347     /* Test. */
1348     if (Cudd_bddLeq(dd,old,f)) {
1349         cuddDeref(old);
1350     } else {
1351         Cudd_RecursiveDeref(dd,old);
1352         old = NULL;
1353     }
1354 #else
1355     cuddDeref(old);
1356 #endif
1357
1358     FREE(string);
1359     FREE(indices);
1360     return(old);
1361
1362 }  /* end of Cudd_bddPickOneMinterm */
1363
1364
1365 /**Function********************************************************************
1366
1367   Synopsis    [Picks k on-set minterms evenly distributed from given DD.]
1368
1369   Description [Picks k on-set minterms evenly distributed from given DD.
1370   The minterms are in terms of <code>vars</code>. The array
1371   <code>vars</code> should contain at least all variables in the
1372   support of <code>f</code>; if this condition is not met the minterms
1373   built by this procedure may not be contained in
1374   <code>f</code>. Builds an array of BDDs for the minterms and returns a
1375   pointer to it if successful; NULL otherwise. There are three reasons
1376   why the procedure may fail:
1377   <ul>
1378   <li> It may run out of memory;
1379   <li> the function <code>f</code> may be the constant 0;
1380   <li> the minterms may not be contained in <code>f</code>.
1381   </ul>]
1382
1383   SideEffects [None]
1384
1385   SeeAlso     [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]
1386
1387 ******************************************************************************/
1388 DdNode **
1389 Cudd_bddPickArbitraryMinterms(
1390   DdManager * dd /* manager */,
1391   DdNode * f /* function from which to pick k minterms */,
1392   DdNode ** vars /* array of variables */,
1393   int  n /* size of <code>vars</code> */,
1394   int  k /* number of minterms to find */)
1395 {
1396     char **string;
1397     int i, j, l, size;
1398     int *indices;
1399     int result;
1400     DdNode **old, *neW;
1401     double minterms;
1402     char *saveString;
1403     int saveFlag, savePoint, isSame;
1404
1405     minterms = Cudd_CountMinterm(dd,f,n);
1406     if ((double)k > minterms) {
1407         return(NULL);
1408     }
1409
1410     size = dd->size;
1411     string = ALLOC(char *, k);
1412     if (string == NULL) {
1413         dd->errorCode = CUDD_MEMORY_OUT;
1414         return(NULL);
1415     }
1416     for (i = 0; i < k; i++) {
1417         string[i] = ALLOC(char, size + 1);
1418         if (string[i] == NULL) {
1419             for (j = 0; j < i; j++)
1420                 FREE(string[i]);
1421             FREE(string);
1422             dd->errorCode = CUDD_MEMORY_OUT;
1423             return(NULL);
1424         }
1425         for (j = 0; j < size; j++) string[i][j] = '2';
1426         string[i][size] = '\0';
1427     }
1428     indices = ALLOC(int,n);
1429     if (indices == NULL) {
1430         dd->errorCode = CUDD_MEMORY_OUT;
1431         for (i = 0; i < k; i++)
1432             FREE(string[i]);
1433         FREE(string);
1434         return(NULL);
1435     }
1436
1437     for (i = 0; i < n; i++) {
1438         indices[i] = vars[i]->index;
1439     }
1440
1441     result = ddPickArbitraryMinterms(dd,f,n,k,string);
1442     if (result == 0) {
1443         for (i = 0; i < k; i++)
1444             FREE(string[i]);
1445         FREE(string);
1446         FREE(indices);
1447         return(NULL);
1448     }
1449
1450     old = ALLOC(DdNode *, k);
1451     if (old == NULL) {
1452         dd->errorCode = CUDD_MEMORY_OUT;
1453         for (i = 0; i < k; i++)
1454             FREE(string[i]);
1455         FREE(string);
1456         FREE(indices);
1457         return(NULL);
1458     }
1459     saveString = ALLOC(char, size + 1);
1460     if (saveString == NULL) {
1461         dd->errorCode = CUDD_MEMORY_OUT;
1462         for (i = 0; i < k; i++)
1463             FREE(string[i]);
1464         FREE(string);
1465         FREE(indices);
1466         FREE(old);
1467         return(NULL);
1468     }
1469     saveFlag = 0;
1470
1471     /* Build result BDD array. */
1472     for (i = 0; i < k; i++) {
1473         isSame = 0;
1474         if (!saveFlag) {
1475             for (j = i + 1; j < k; j++) {
1476                 if (strcmp(string[i], string[j]) == 0) {
1477                     savePoint = i;
1478                     strcpy(saveString, string[i]);
1479                     saveFlag = 1;
1480                     break;
1481                 }
1482             }
1483         } else {
1484             if (strcmp(string[i], saveString) == 0) {
1485                 isSame = 1;
1486             } else {
1487                 saveFlag = 0;
1488                 for (j = i + 1; j < k; j++) {
1489                     if (strcmp(string[i], string[j]) == 0) {
1490                         savePoint = i;
1491                         strcpy(saveString, string[i]);
1492                         saveFlag = 1;
1493                         break;
1494                     }
1495                 }
1496             }
1497         }
1498         /* Randomize choice for don't cares. */
1499         for (j = 0; j < n; j++) {
1500             if (string[i][indices[j]] == '2')
1501                 string[i][indices[j]] =
1502                   (char) ((Cudd_Random() & 0x20) ? '1' : '0');
1503         }
1504
1505         while (isSame) {
1506             isSame = 0;
1507             for (j = savePoint; j < i; j++) {
1508                 if (strcmp(string[i], string[j]) == 0) {
1509                     isSame = 1;
1510                     break;
1511                 }
1512             }
1513             if (isSame) {
1514                 strcpy(string[i], saveString);
1515                 /* Randomize choice for don't cares. */
1516                 for (j = 0; j < n; j++) {
1517                     if (string[i][indices[j]] == '2')
1518                         string[i][indices[j]] =
1519                           (char) ((Cudd_Random() & 0x20) ? '1' : '0');
1520                 }
1521             }
1522         }
1523
1524         old[i] = Cudd_ReadOne(dd);
1525         cuddRef(old[i]);
1526
1527         for (j = 0; j < n; j++) {
1528             if (string[i][indices[j]] == '0') {
1529                 neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
1530             } else {
1531                 neW = Cudd_bddAnd(dd,old[i],vars[j]);
1532             }
1533             if (neW == NULL) {
1534                 FREE(saveString);
1535                 for (l = 0; l < k; l++)
1536                     FREE(string[l]);
1537                 FREE(string);
1538                 FREE(indices);
1539                 for (l = 0; l <= i; l++)
1540                     Cudd_RecursiveDeref(dd,old[l]);
1541                 FREE(old);
1542                 return(NULL);
1543             }
1544             cuddRef(neW);
1545             Cudd_RecursiveDeref(dd,old[i]);
1546             old[i] = neW;
1547         }
1548
1549         /* Test. */
1550         if (!Cudd_bddLeq(dd,old[i],f)) {
1551             FREE(saveString);
1552             for (l = 0; l < k; l++)
1553                 FREE(string[l]);
1554             FREE(string);
1555             FREE(indices);
1556             for (l = 0; l <= i; l++)
1557                 Cudd_RecursiveDeref(dd,old[l]);
1558             FREE(old);
1559             return(NULL);
1560         }
1561     }
1562
1563     FREE(saveString);
1564     for (i = 0; i < k; i++) {
1565         cuddDeref(old[i]);
1566         FREE(string[i]);
1567     }
1568     FREE(string);
1569     FREE(indices);
1570     return(old);
1571
1572 }  /* end of Cudd_bddPickArbitraryMinterms */
1573
1574
1575 /**Function********************************************************************
1576
1577   Synopsis    [Extracts a subset from a BDD.]
1578
1579   Description [Extracts a subset from a BDD in the following procedure.
1580   1. Compute the weight for each mask variable by counting the number of
1581      minterms for both positive and negative cofactors of the BDD with
1582      respect to each mask variable. (weight = #positive - #negative)
1583   2. Find a representative cube of the BDD by using the weight. From the
1584      top variable of the BDD, for each variable, if the weight is greater
1585      than 0.0, choose THEN branch, othereise ELSE branch, until meeting
1586      the constant 1.
1587   3. Quantify out the variables not in maskVars from the representative
1588      cube and if a variable in maskVars is don't care, replace the
1589      variable with a constant(1 or 0) depending on the weight.
1590   4. Make a subset of the BDD by multiplying with the modified cube.]
1591
1592   SideEffects [None]
1593
1594   SeeAlso     []
1595
1596 ******************************************************************************/
1597 DdNode *
1598 Cudd_SubsetWithMaskVars(
1599   DdManager * dd /* manager */,
1600   DdNode * f /* function from which to pick a cube */,
1601   DdNode ** vars /* array of variables */,
1602   int  nvars /* size of <code>vars</code> */,
1603   DdNode ** maskVars /* array of variables */,
1604   int  mvars /* size of <code>maskVars</code> */)
1605 {
1606     double      *weight;
1607     char        *string;
1608     int         i, size;
1609     int         *indices, *mask;
1610     int         result;
1611     DdNode      *zero, *cube, *newCube, *subset;
1612     DdNode      *cof;
1613
1614     DdNode      *support;
1615     support = Cudd_Support(dd,f);
1616     cuddRef(support);
1617     Cudd_RecursiveDeref(dd,support);
1618
1619     zero = Cudd_Not(dd->one);
1620     size = dd->size;
1621
1622     weight = ALLOC(double,size);
1623     if (weight == NULL) {
1624         dd->errorCode = CUDD_MEMORY_OUT;
1625         return(NULL);
1626     }
1627     for (i = 0; i < size; i++) {
1628         weight[i] = 0.0;
1629     }
1630     for (i = 0; i < mvars; i++) {
1631         cof = Cudd_Cofactor(dd, f, maskVars[i]);
1632         cuddRef(cof);
1633         weight[i] = Cudd_CountMinterm(dd, cof, nvars);
1634         Cudd_RecursiveDeref(dd,cof);
1635
1636         cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
1637         cuddRef(cof);
1638         weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
1639         Cudd_RecursiveDeref(dd,cof);
1640     }
1641
1642     string = ALLOC(char, size + 1);
1643     if (string == NULL) {
1644         dd->errorCode = CUDD_MEMORY_OUT;
1645         FREE(weight);
1646         return(NULL);
1647     }
1648     mask = ALLOC(int, size);
1649     if (mask == NULL) {
1650         dd->errorCode = CUDD_MEMORY_OUT;
1651         FREE(weight);
1652         FREE(string);
1653         return(NULL);
1654     }
1655     for (i = 0; i < size; i++) {
1656         string[i] = '2';
1657         mask[i] = 0;
1658     }
1659     string[size] = '\0';
1660     indices = ALLOC(int,nvars);
1661     if (indices == NULL) {
1662         dd->errorCode = CUDD_MEMORY_OUT;
1663         FREE(weight);
1664         FREE(string);
1665         FREE(mask);
1666         return(NULL);
1667     }
1668     for (i = 0; i < nvars; i++) {
1669         indices[i] = vars[i]->index;
1670     }
1671
1672     result = ddPickRepresentativeCube(dd,f,weight,string);
1673     if (result == 0) {
1674         FREE(weight);
1675         FREE(string);
1676         FREE(mask);
1677         FREE(indices);
1678         return(NULL);
1679     }
1680
1681     cube = Cudd_ReadOne(dd);
1682     cuddRef(cube);
1683     zero = Cudd_Not(Cudd_ReadOne(dd));
1684     for (i = 0; i < nvars; i++) {
1685         if (string[indices[i]] == '0') {
1686             newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1687         } else if (string[indices[i]] == '1') {
1688             newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1689         } else
1690             continue;
1691         if (newCube == NULL) {
1692             FREE(weight);
1693             FREE(string);
1694             FREE(mask);
1695             FREE(indices);
1696             Cudd_RecursiveDeref(dd,cube);
1697             return(NULL);
1698         }
1699         cuddRef(newCube);
1700         Cudd_RecursiveDeref(dd,cube);
1701         cube = newCube;
1702     }
1703     Cudd_RecursiveDeref(dd,cube);
1704
1705     for (i = 0; i < mvars; i++) {
1706         mask[maskVars[i]->index] = 1;
1707     }
1708     for (i = 0; i < nvars; i++) {
1709         if (mask[indices[i]]) {
1710             if (string[indices[i]] == '2') {
1711                 if (weight[indices[i]] >= 0.0)
1712                     string[indices[i]] = '1';
1713                 else
1714                     string[indices[i]] = '0';
1715             }
1716         } else {
1717             string[indices[i]] = '2';
1718         }
1719     }
1720
1721     cube = Cudd_ReadOne(dd);
1722     cuddRef(cube);
1723     zero = Cudd_Not(Cudd_ReadOne(dd));
1724
1725     /* Build result BDD. */
1726     for (i = 0; i < nvars; i++) {
1727         if (string[indices[i]] == '0') {
1728             newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1729         } else if (string[indices[i]] == '1') {
1730             newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1731         } else
1732             continue;
1733         if (newCube == NULL) {
1734             FREE(weight);
1735             FREE(string);
1736             FREE(mask);
1737             FREE(indices);
1738             Cudd_RecursiveDeref(dd,cube);
1739             return(NULL);
1740         }
1741         cuddRef(newCube);
1742         Cudd_RecursiveDeref(dd,cube);
1743         cube = newCube;
1744     }
1745
1746     subset = Cudd_bddAnd(dd,f,cube);
1747     cuddRef(subset);
1748     Cudd_RecursiveDeref(dd,cube);
1749
1750     /* Test. */
1751     if (Cudd_bddLeq(dd,subset,f)) {
1752         cuddDeref(subset);
1753     } else {
1754         Cudd_RecursiveDeref(dd,subset);
1755         subset = NULL;
1756     }
1757
1758     FREE(weight);
1759     FREE(string);
1760     FREE(mask);
1761     FREE(indices);
1762     return(subset);
1763
1764 } /* end of Cudd_SubsetWithMaskVars */
1765
1766
1767 /**Function********************************************************************
1768
1769   Synopsis    [Finds the first cube of a decision diagram.]
1770
1771   Description [Defines an iterator on the onset of a decision diagram
1772   and finds its first cube. Returns a generator that contains the
1773   information necessary to continue the enumeration if successful; NULL
1774   otherwise.<p>
1775   A cube is represented as an array of literals, which are integers in
1776   {0, 1, 2}; 0 represents a complemented literal, 1 represents an
1777   uncomplemented literal, and 2 stands for don't care. The enumeration
1778   produces a disjoint cover of the function associated with the diagram.
1779   The size of the array equals the number of variables in the manager at
1780   the time Cudd_FirstCube is called.<p>
1781   For each cube, a value is also returned. This value is always 1 for a
1782   BDD, while it may be different from 1 for an ADD.
1783   For BDDs, the offset is the set of cubes whose value is the logical zero.
1784   For ADDs, the offset is the set of cubes whose value is the
1785   background value. The cubes of the offset are not enumerated.]
1786
1787   SideEffects [The first cube and its value are returned as side effects.]
1788
1789   SeeAlso     [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty
1790   Cudd_FirstNode]
1791
1792 ******************************************************************************/
1793 DdGen *
1794 Cudd_FirstCube(
1795   DdManager * dd,
1796   DdNode * f,
1797   int ** cube,
1798   CUDD_VALUE_TYPE * value)
1799 {
1800     DdGen *gen;
1801     DdNode *top, *treg, *next, *nreg, *prev, *preg;
1802     int i;
1803     int nvars;
1804
1805     /* Sanity Check. */
1806     if (dd == NULL || f == NULL) return(NULL);
1807
1808     /* Allocate generator an initialize it. */
1809     gen = ALLOC(DdGen,1);
1810     if (gen == NULL) {
1811         dd->errorCode = CUDD_MEMORY_OUT;
1812         return(NULL);
1813     }
1814
1815     gen->manager = dd;
1816     gen->type = CUDD_GEN_CUBES;
1817     gen->status = CUDD_GEN_EMPTY;
1818     gen->gen.cubes.cube = NULL;
1819     gen->gen.cubes.value = DD_ZERO_VAL;
1820     gen->stack.sp = 0;
1821     gen->stack.stack = NULL;
1822     gen->node = NULL;
1823
1824     nvars = dd->size;
1825     gen->gen.cubes.cube = ALLOC(int,nvars);
1826     if (gen->gen.cubes.cube == NULL) {
1827         dd->errorCode = CUDD_MEMORY_OUT;
1828         FREE(gen);
1829         return(NULL);
1830     }
1831     for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
1832
1833     /* The maximum stack depth is one plus the number of variables.
1834     ** because a path may have nodes at all levels, including the
1835     ** constant level.
1836     */
1837     gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
1838     if (gen->stack.stack == NULL) {
1839         dd->errorCode = CUDD_MEMORY_OUT;
1840         FREE(gen->gen.cubes.cube);
1841         FREE(gen);
1842         return(NULL);
1843     }
1844     for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
1845
1846     /* Find the first cube of the onset. */
1847     gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
1848
1849     while (1) {
1850         top = gen->stack.stack[gen->stack.sp-1];
1851         treg = Cudd_Regular(top);
1852         if (!cuddIsConstant(treg)) {
1853             /* Take the else branch first. */
1854             gen->gen.cubes.cube[treg->index] = 0;
1855             next = cuddE(treg);
1856             if (top != treg) next = Cudd_Not(next);
1857             gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1858         } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
1859             /* Backtrack */
1860             while (1) {
1861                 if (gen->stack.sp == 1) {
1862                     /* The current node has no predecessor. */
1863                     gen->status = CUDD_GEN_EMPTY;
1864                     gen->stack.sp--;
1865                     goto done;
1866                 }
1867                 prev = gen->stack.stack[gen->stack.sp-2];
1868                 preg = Cudd_Regular(prev);
1869                 nreg = cuddT(preg);
1870                 if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1871                 if (next != top) { /* follow the then branch next */
1872                     gen->gen.cubes.cube[preg->index] = 1;
1873                     gen->stack.stack[gen->stack.sp-1] = next;
1874                     break;
1875                 }
1876                 /* Pop the stack and try again. */
1877                 gen->gen.cubes.cube[preg->index] = 2;
1878                 gen->stack.sp--;
1879                 top = gen->stack.stack[gen->stack.sp-1];
1880                 treg = Cudd_Regular(top);
1881             }
1882         } else {
1883             gen->status = CUDD_GEN_NONEMPTY;
1884             gen->gen.cubes.value = cuddV(top);
1885             goto done;
1886         }
1887     }
1888
1889 done:
1890     *cube = gen->gen.cubes.cube;
1891     *value = gen->gen.cubes.value;
1892     return(gen);
1893
1894 } /* end of Cudd_FirstCube */
1895
1896
1897 /**Function********************************************************************
1898
1899   Synopsis    [Generates the next cube of a decision diagram onset.]
1900
1901   Description [Generates the next cube of a decision diagram onset,
1902   using generator gen. Returns 0 if the enumeration is completed; 1
1903   otherwise.]
1904
1905   SideEffects [The cube and its value are returned as side effects. The
1906   generator is modified.]
1907
1908   SeeAlso     [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty
1909   Cudd_NextNode]
1910
1911 ******************************************************************************/
1912 int
1913 Cudd_NextCube(
1914   DdGen * gen,
1915   int ** cube,
1916   CUDD_VALUE_TYPE * value)
1917 {
1918     DdNode *top, *treg, *next, *nreg, *prev, *preg;
1919     DdManager *dd = gen->manager;
1920
1921     /* Backtrack from previously reached terminal node. */
1922     while (1) {
1923         if (gen->stack.sp == 1) {
1924             /* The current node has no predecessor. */
1925             gen->status = CUDD_GEN_EMPTY;
1926             gen->stack.sp--;
1927             goto done;
1928         }
1929         top = gen->stack.stack[gen->stack.sp-1];
1930         treg = Cudd_Regular(top);
1931         prev = gen->stack.stack[gen->stack.sp-2];
1932         preg = Cudd_Regular(prev);
1933         nreg = cuddT(preg);
1934         if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1935         if (next != top) { /* follow the then branch next */
1936             gen->gen.cubes.cube[preg->index] = 1;
1937             gen->stack.stack[gen->stack.sp-1] = next;
1938             break;
1939         }
1940         /* Pop the stack and try again. */
1941         gen->gen.cubes.cube[preg->index] = 2;
1942         gen->stack.sp--;
1943     }
1944
1945     while (1) {
1946         top = gen->stack.stack[gen->stack.sp-1];
1947         treg = Cudd_Regular(top);
1948         if (!cuddIsConstant(treg)) {
1949             /* Take the else branch first. */
1950             gen->gen.cubes.cube[treg->index] = 0;
1951             next = cuddE(treg);
1952             if (top != treg) next = Cudd_Not(next);
1953             gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1954         } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
1955             /* Backtrack */
1956             while (1) {
1957                 if (gen->stack.sp == 1) {
1958                     /* The current node has no predecessor. */
1959                     gen->status = CUDD_GEN_EMPTY;
1960                     gen->stack.sp--;
1961                     goto done;
1962                 }
1963                 prev = gen->stack.stack[gen->stack.sp-2];
1964                 preg = Cudd_Regular(prev);
1965                 nreg = cuddT(preg);
1966                 if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1967                 if (next != top) { /* follow the then branch next */
1968                     gen->gen.cubes.cube[preg->index] = 1;
1969                     gen->stack.stack[gen->stack.sp-1] = next;
1970                     break;
1971                 }
1972                 /* Pop the stack and try again. */
1973                 gen->gen.cubes.cube[preg->index] = 2;
1974                 gen->stack.sp--;
1975                 top = gen->stack.stack[gen->stack.sp-1];
1976                 treg = Cudd_Regular(top);
1977             }
1978         } else {
1979             gen->status = CUDD_GEN_NONEMPTY;
1980             gen->gen.cubes.value = cuddV(top);
1981             goto done;
1982         }
1983     }
1984
1985 done:
1986     if (gen->status == CUDD_GEN_EMPTY) return(0);
1987     *cube = gen->gen.cubes.cube;
1988     *value = gen->gen.cubes.value;
1989     return(1);
1990
1991 } /* end of Cudd_NextCube */
1992
1993
1994 /**Function********************************************************************
1995
1996   Synopsis    [Finds the first prime of a Boolean function.]
1997
1998   Description [Defines an iterator on a pair of BDDs describing a
1999   (possibly incompletely specified) Boolean functions and finds the
2000   first cube of a cover of the function.  Returns a generator
2001   that contains the information necessary to continue the enumeration
2002   if successful; NULL otherwise.<p>
2003
2004   The two argument BDDs are the lower and upper bounds of an interval.
2005   It is a mistake to call this function with a lower bound that is not
2006   less than or equal to the upper bound.<p>
2007
2008   A cube is represented as an array of literals, which are integers in
2009   {0, 1, 2}; 0 represents a complemented literal, 1 represents an
2010   uncomplemented literal, and 2 stands for don't care. The enumeration
2011   produces a prime and irredundant cover of the function associated
2012   with the two BDDs.  The size of the array equals the number of
2013   variables in the manager at the time Cudd_FirstCube is called.<p>
2014
2015   This iterator can only be used on BDDs.]
2016
2017   SideEffects [The first cube is returned as side effect.]
2018
2019   SeeAlso     [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty
2020   Cudd_FirstCube Cudd_FirstNode]
2021
2022 ******************************************************************************/
2023 DdGen *
2024 Cudd_FirstPrime(
2025   DdManager *dd,
2026   DdNode *l,
2027   DdNode *u,
2028   int **cube)
2029 {
2030     DdGen *gen;
2031     DdNode *implicant, *prime, *tmp;
2032     int length, result;
2033
2034     /* Sanity Check. */
2035     if (dd == NULL || l == NULL || u == NULL) return(NULL);
2036
2037     /* Allocate generator an initialize it. */
2038     gen = ALLOC(DdGen,1);
2039     if (gen == NULL) {
2040         dd->errorCode = CUDD_MEMORY_OUT;
2041         return(NULL);
2042     }
2043
2044     gen->manager = dd;
2045     gen->type = CUDD_GEN_PRIMES;
2046     gen->status = CUDD_GEN_EMPTY;
2047     gen->gen.primes.cube = NULL;
2048     gen->gen.primes.ub = u;
2049     gen->stack.sp = 0;
2050     gen->stack.stack = NULL;
2051     gen->node = l;
2052     cuddRef(l);
2053
2054     gen->gen.primes.cube = ALLOC(int,dd->size);
2055     if (gen->gen.primes.cube == NULL) {
2056         dd->errorCode = CUDD_MEMORY_OUT;
2057         FREE(gen);
2058         return(NULL);
2059     }
2060
2061     if (gen->node == Cudd_ReadLogicZero(dd)) {
2062         gen->status = CUDD_GEN_EMPTY;
2063     } else {
2064         implicant = Cudd_LargestCube(dd,gen->node,&length);
2065         if (implicant == NULL) {
2066             Cudd_RecursiveDeref(dd,gen->node);
2067             FREE(gen->gen.primes.cube);
2068             FREE(gen);
2069             return(NULL);
2070         }
2071         cuddRef(implicant);
2072         prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2073         if (prime == NULL) {
2074             Cudd_RecursiveDeref(dd,gen->node);
2075             Cudd_RecursiveDeref(dd,implicant);
2076             FREE(gen->gen.primes.cube);
2077             FREE(gen);
2078             return(NULL);
2079         }
2080         cuddRef(prime);
2081         Cudd_RecursiveDeref(dd,implicant);
2082         tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2083         if (tmp == NULL) {
2084             Cudd_RecursiveDeref(dd,gen->node);
2085             Cudd_RecursiveDeref(dd,prime);
2086             FREE(gen->gen.primes.cube);
2087             FREE(gen);
2088             return(NULL);
2089         }
2090         cuddRef(tmp);
2091         Cudd_RecursiveDeref(dd,gen->node);
2092         gen->node = tmp;
2093         result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2094         if (result == 0) {
2095             Cudd_RecursiveDeref(dd,gen->node);
2096             Cudd_RecursiveDeref(dd,prime);
2097             FREE(gen->gen.primes.cube);
2098             FREE(gen);
2099             return(NULL);
2100         }
2101         Cudd_RecursiveDeref(dd,prime);
2102         gen->status = CUDD_GEN_NONEMPTY;
2103     }
2104     *cube = gen->gen.primes.cube;
2105     return(gen);
2106
2107 } /* end of Cudd_FirstPrime */
2108
2109
2110 /**Function********************************************************************
2111
2112   Synopsis    [Generates the next prime of a Boolean function.]
2113
2114   Description [Generates the next cube of a Boolean function,
2115   using generator gen. Returns 0 if the enumeration is completed; 1
2116   otherwise.]
2117
2118   SideEffects [The cube and is returned as side effects. The
2119   generator is modified.]
2120
2121   SeeAlso     [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty
2122   Cudd_NextCube Cudd_NextNode]
2123
2124 ******************************************************************************/
2125 int
2126 Cudd_NextPrime(
2127   DdGen *gen,
2128   int **cube)
2129 {
2130     DdNode *implicant, *prime, *tmp;
2131     DdManager *dd = gen->manager;
2132     int length, result;
2133
2134     if (gen->node == Cudd_ReadLogicZero(dd)) {
2135         gen->status = CUDD_GEN_EMPTY;
2136     } else {
2137         implicant = Cudd_LargestCube(dd,gen->node,&length);
2138         if (implicant == NULL) {
2139             gen->status = CUDD_GEN_EMPTY;
2140             return(0);
2141         }
2142         cuddRef(implicant);
2143         prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2144         if (prime == NULL) {
2145             Cudd_RecursiveDeref(dd,implicant);
2146             gen->status = CUDD_GEN_EMPTY;
2147             return(0);
2148         }
2149         cuddRef(prime);
2150         Cudd_RecursiveDeref(dd,implicant);
2151         tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2152         if (tmp == NULL) {
2153             Cudd_RecursiveDeref(dd,prime);
2154             gen->status = CUDD_GEN_EMPTY;
2155             return(0);
2156         }
2157         cuddRef(tmp);
2158         Cudd_RecursiveDeref(dd,gen->node);
2159         gen->node = tmp;
2160         result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2161         if (result == 0) {
2162             Cudd_RecursiveDeref(dd,prime);
2163             gen->status = CUDD_GEN_EMPTY;
2164             return(0);
2165         }
2166         Cudd_RecursiveDeref(dd,prime);
2167         gen->status = CUDD_GEN_NONEMPTY;
2168     }
2169     if (gen->status == CUDD_GEN_EMPTY) return(0);
2170     *cube = gen->gen.primes.cube;
2171     return(1);
2172
2173 } /* end of Cudd_NextPrime */
2174
2175
2176 /**Function********************************************************************
2177
2178   Synopsis    [Computes the cube of an array of BDD variables.]
2179
2180   Description [Computes the cube of an array of BDD variables. If
2181   non-null, the phase argument indicates which literal of each
2182   variable should appear in the cube. If phase\[i\] is nonzero, then the
2183   positive literal is used. If phase is NULL, the cube is positive unate.
2184   Returns a pointer to the result if successful; NULL otherwise.]
2185
2186   SideEffects [None]
2187
2188   SeeAlso     [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]
2189
2190 ******************************************************************************/
2191 DdNode *
2192 Cudd_bddComputeCube(
2193   DdManager * dd,
2194   DdNode ** vars,
2195   int * phase,
2196   int  n)
2197 {
2198     DdNode      *cube;
2199     DdNode      *fn;
2200     int         i;
2201
2202     cube = DD_ONE(dd);
2203     cuddRef(cube);
2204
2205     for (i = n - 1; i >= 0; i--) {
2206         if (phase == NULL || phase[i] != 0) {
2207             fn = Cudd_bddAnd(dd,vars[i],cube);
2208         } else {
2209             fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
2210         }
2211         if (fn == NULL) {
2212             Cudd_RecursiveDeref(dd,cube);
2213             return(NULL);
2214         }
2215         cuddRef(fn);
2216         Cudd_RecursiveDeref(dd,cube);
2217         cube = fn;
2218     }
2219     cuddDeref(cube);
2220
2221     return(cube);
2222
2223 }  /* end of Cudd_bddComputeCube */
2224
2225
2226 /**Function********************************************************************
2227
2228   Synopsis    [Computes the cube of an array of ADD variables.]
2229
2230   Description [Computes the cube of an array of ADD variables.  If
2231   non-null, the phase argument indicates which literal of each
2232   variable should appear in the cube. If phase\[i\] is nonzero, then the
2233   positive literal is used. If phase is NULL, the cube is positive unate.
2234   Returns a pointer to the result if successful; NULL otherwise.]
2235
2236   SideEffects [none]
2237
2238   SeeAlso     [Cudd_bddComputeCube]
2239
2240 ******************************************************************************/
2241 DdNode *
2242 Cudd_addComputeCube(
2243   DdManager * dd,
2244   DdNode ** vars,
2245   int * phase,
2246   int  n)
2247 {
2248     DdNode      *cube, *zero;
2249     DdNode      *fn;
2250     int         i;
2251
2252     cube = DD_ONE(dd);
2253     cuddRef(cube);
2254     zero = DD_ZERO(dd);
2255
2256     for (i = n - 1; i >= 0; i--) {
2257         if (phase == NULL || phase[i] != 0) {
2258             fn = Cudd_addIte(dd,vars[i],cube,zero);
2259         } else {
2260             fn = Cudd_addIte(dd,vars[i],zero,cube);
2261         }
2262         if (fn == NULL) {
2263             Cudd_RecursiveDeref(dd,cube);
2264             return(NULL);
2265         }
2266         cuddRef(fn);
2267         Cudd_RecursiveDeref(dd,cube);
2268         cube = fn;
2269     }
2270     cuddDeref(cube);
2271
2272     return(cube);
2273
2274 } /* end of Cudd_addComputeCube */
2275
2276
2277 /**Function********************************************************************
2278
2279   Synopsis    [Builds the BDD of a cube from a positional array.]
2280
2281   Description [Builds a cube from a positional array.  The array must
2282   have one integer entry for each BDD variable.  If the i-th entry is
2283   1, the variable of index i appears in true form in the cube; If the
2284   i-th entry is 0, the variable of index i appears complemented in the
2285   cube; otherwise the variable does not appear in the cube.  Returns a
2286   pointer to the BDD for the cube if successful; NULL otherwise.]
2287
2288   SideEffects [None]
2289
2290   SeeAlso     [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]
2291
2292 ******************************************************************************/
2293 DdNode *
2294 Cudd_CubeArrayToBdd(
2295   DdManager *dd,
2296   int *array)
2297 {
2298     DdNode *cube, *var, *tmp;
2299     int i;
2300     int size = Cudd_ReadSize(dd);
2301
2302     cube = DD_ONE(dd);
2303     cuddRef(cube);
2304     for (i = size - 1; i >= 0; i--) {
2305         if ((array[i] & ~1) == 0) {
2306             var = Cudd_bddIthVar(dd,i);
2307             tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
2308             if (tmp == NULL) {
2309                 Cudd_RecursiveDeref(dd,cube);
2310                 return(NULL);
2311             }
2312             cuddRef(tmp);
2313             Cudd_RecursiveDeref(dd,cube);
2314             cube = tmp;
2315         }
2316     }
2317     cuddDeref(cube);
2318     return(cube);
2319
2320 } /* end of Cudd_CubeArrayToBdd */
2321
2322
2323 /**Function********************************************************************
2324
2325   Synopsis    [Builds a positional array from the BDD of a cube.]
2326
2327   Description [Builds a positional array from the BDD of a cube.
2328   Array must have one entry for each BDD variable.  The positional
2329   array has 1 in i-th position if the variable of index i appears in
2330   true form in the cube; it has 0 in i-th position if the variable of
2331   index i appears in complemented form in the cube; finally, it has 2
2332   in i-th position if the variable of index i does not appear in the
2333   cube.  Returns 1 if successful (the BDD is indeed a cube); 0
2334   otherwise.]
2335
2336   SideEffects [The result is in the array passed by reference.]
2337
2338   SeeAlso     [Cudd_CubeArrayToBdd]
2339
2340 ******************************************************************************/
2341 int
2342 Cudd_BddToCubeArray(
2343   DdManager *dd,
2344   DdNode *cube,
2345   int *array)
2346 {
2347     DdNode *scan, *t, *e;
2348     int i;
2349     int size = Cudd_ReadSize(dd);
2350     DdNode *zero = Cudd_Not(DD_ONE(dd));
2351
2352     for (i = size-1; i >= 0; i--) {
2353         array[i] = 2;
2354     }
2355     scan = cube;
2356     while (!Cudd_IsConstant(scan)) {
2357         int index = Cudd_Regular(scan)->index;
2358         cuddGetBranches(scan,&t,&e);
2359         if (t == zero) {
2360             array[index] = 0;
2361             scan = e;
2362         } else if (e == zero) {
2363             array[index] = 1;
2364             scan = t;
2365         } else {
2366             return(0);  /* cube is not a cube */
2367         }
2368     }
2369     if (scan == zero) {
2370         return(0);
2371     } else {
2372         return(1);
2373     }
2374
2375 } /* end of Cudd_BddToCubeArray */
2376
2377
2378 /**Function********************************************************************
2379
2380   Synopsis    [Finds the first node of a decision diagram.]
2381
2382   Description [Defines an iterator on the nodes of a decision diagram
2383   and finds its first node. Returns a generator that contains the
2384   information necessary to continue the enumeration if successful;
2385   NULL otherwise.  The nodes are enumerated in a reverse topological
2386   order, so that a node is always preceded in the enumeration by its
2387   descendants.]
2388
2389   SideEffects [The first node is returned as a side effect.]
2390
2391   SeeAlso     [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty
2392   Cudd_FirstCube]
2393
2394 ******************************************************************************/
2395 DdGen *
2396 Cudd_FirstNode(
2397   DdManager * dd,
2398   DdNode * f,
2399   DdNode ** node)
2400 {
2401     DdGen *gen;
2402     int size;
2403
2404     /* Sanity Check. */
2405     if (dd == NULL || f == NULL) return(NULL);
2406
2407     /* Allocate generator an initialize it. */
2408     gen = ALLOC(DdGen,1);
2409     if (gen == NULL) {
2410         dd->errorCode = CUDD_MEMORY_OUT;
2411         return(NULL);
2412     }
2413
2414     gen->manager = dd;
2415     gen->type = CUDD_GEN_NODES;
2416     gen->status = CUDD_GEN_EMPTY;
2417     gen->stack.sp = 0;
2418     gen->node = NULL;
2419
2420     /* Collect all the nodes on the generator stack for later perusal. */
2421     gen->stack.stack = cuddNodeArray(Cudd_Regular(f), &size);
2422     if (gen->stack.stack == NULL) {
2423         FREE(gen);
2424         dd->errorCode = CUDD_MEMORY_OUT;
2425         return(NULL);
2426     }
2427     gen->gen.nodes.size = size;
2428
2429     /* Find the first node. */
2430     if (gen->stack.sp < gen->gen.nodes.size) {
2431         gen->status = CUDD_GEN_NONEMPTY;
2432         gen->node = gen->stack.stack[gen->stack.sp];
2433         *node = gen->node;
2434     }
2435
2436     return(gen);
2437
2438 } /* end of Cudd_FirstNode */
2439
2440
2441 /**Function********************************************************************
2442
2443   Synopsis    [Finds the next node of a decision diagram.]
2444
2445   Description [Finds the node of a decision diagram, using generator
2446   gen. Returns 0 if the enumeration is completed; 1 otherwise.]
2447
2448   SideEffects [The next node is returned as a side effect.]
2449
2450   SeeAlso     [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty
2451   Cudd_NextCube]
2452
2453 ******************************************************************************/
2454 int
2455 Cudd_NextNode(
2456   DdGen * gen,
2457   DdNode ** node)
2458 {
2459     /* Find the next node. */
2460     gen->stack.sp++;
2461     if (gen->stack.sp < gen->gen.nodes.size) {
2462         gen->node = gen->stack.stack[gen->stack.sp];
2463         *node = gen->node;
2464         return(1);
2465     } else {
2466         gen->status = CUDD_GEN_EMPTY;
2467         return(0);
2468     }
2469
2470 } /* end of Cudd_NextNode */
2471
2472
2473 /**Function********************************************************************
2474
2475   Synopsis    [Frees a CUDD generator.]
2476
2477   Description [Frees a CUDD generator. Always returns 0, so that it can
2478   be used in mis-like foreach constructs.]
2479
2480   SideEffects [None]
2481
2482   SeeAlso     [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2483   Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]
2484
2485 ******************************************************************************/
2486 int
2487 Cudd_GenFree(
2488   DdGen * gen)
2489 {
2490     if (gen == NULL) return(0);
2491     switch (gen->type) {
2492     case CUDD_GEN_CUBES:
2493     case CUDD_GEN_ZDD_PATHS:
2494         FREE(gen->gen.cubes.cube);
2495         FREE(gen->stack.stack);
2496         break;
2497     case CUDD_GEN_PRIMES:
2498         FREE(gen->gen.primes.cube);
2499         Cudd_RecursiveDeref(gen->manager,gen->node);
2500         break;
2501     case CUDD_GEN_NODES:
2502         FREE(gen->stack.stack);
2503         break;
2504     default:
2505         return(0);
2506     }
2507     FREE(gen);
2508     return(0);
2509
2510 } /* end of Cudd_GenFree */
2511
2512
2513 /**Function********************************************************************
2514
2515   Synopsis    [Queries the status of a generator.]
2516
2517   Description [Queries the status of a generator. Returns 1 if the
2518   generator is empty or NULL; 0 otherswise.]
2519
2520   SideEffects [None]
2521
2522   SeeAlso     [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2523   Cudd_FirstNode Cudd_NextNode Cudd_GenFree]
2524
2525 ******************************************************************************/
2526 int
2527 Cudd_IsGenEmpty(
2528   DdGen * gen)
2529 {
2530     if (gen == NULL) return(1);
2531     return(gen->status == CUDD_GEN_EMPTY);
2532
2533 } /* end of Cudd_IsGenEmpty */
2534
2535
2536 /**Function********************************************************************
2537
2538   Synopsis    [Builds a cube of BDD variables from an array of indices.]
2539
2540   Description [Builds a cube of BDD variables from an array of indices.
2541   Returns a pointer to the result if successful; NULL otherwise.]
2542
2543   SideEffects [None]
2544
2545   SeeAlso     [Cudd_bddComputeCube Cudd_CubeArrayToBdd]
2546
2547 ******************************************************************************/
2548 DdNode *
2549 Cudd_IndicesToCube(
2550   DdManager * dd,
2551   int * array,
2552   int  n)
2553 {
2554     DdNode *cube, *tmp;
2555     int i;
2556
2557     cube = DD_ONE(dd);
2558     cuddRef(cube);
2559     for (i = n - 1; i >= 0; i--) {
2560         tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
2561         if (tmp == NULL) {
2562             Cudd_RecursiveDeref(dd,cube);
2563             return(NULL);
2564         }
2565         cuddRef(tmp);
2566         Cudd_RecursiveDeref(dd,cube);
2567         cube = tmp;
2568     }
2569
2570     cuddDeref(cube);
2571     return(cube);
2572
2573 } /* end of Cudd_IndicesToCube */
2574
2575
2576 /**Function********************************************************************
2577
2578   Synopsis    [Prints the package version number.]
2579
2580   Description []
2581
2582   SideEffects [None]
2583
2584   SeeAlso     []
2585
2586 ******************************************************************************/
2587 void
2588 Cudd_PrintVersion(
2589   FILE * fp)
2590 {
2591     (void) fprintf(fp, "%s\n", CUDD_VERSION);
2592
2593 } /* end of Cudd_PrintVersion */
2594
2595
2596 /**Function********************************************************************
2597
2598   Synopsis    [Computes the average distance between adjacent nodes.]
2599
2600   Description [Computes the average distance between adjacent nodes in
2601   the manager. Adjacent nodes are node pairs such that the second node
2602   is the then child, else child, or next node in the collision list.]
2603
2604   SideEffects [None]
2605
2606   SeeAlso     []
2607
2608 ******************************************************************************/
2609 double
2610 Cudd_AverageDistance(
2611   DdManager * dd)
2612 {
2613     double tetotal, nexttotal;
2614     double tesubtotal, nextsubtotal;
2615     double temeasured, nextmeasured;
2616     int i, j;
2617     int slots, nvars;
2618     long diff;
2619     DdNode *scan;
2620     DdNodePtr *nodelist;
2621     DdNode *sentinel = &(dd->sentinel);
2622
2623     nvars = dd->size;
2624     if (nvars == 0) return(0.0);
2625
2626     /* Initialize totals. */
2627     tetotal = 0.0;
2628     nexttotal = 0.0;
2629     temeasured = 0.0;
2630     nextmeasured = 0.0;
2631
2632     /* Scan the variable subtables. */
2633     for (i = 0; i < nvars; i++) {
2634         nodelist = dd->subtables[i].nodelist;
2635         tesubtotal = 0.0;
2636         nextsubtotal = 0.0;
2637         slots = dd->subtables[i].slots;
2638         for (j = 0; j < slots; j++) {
2639             scan = nodelist[j];
2640             while (scan != sentinel) {
2641                 diff = (long) scan - (long) cuddT(scan);
2642                 tesubtotal += (double) ddAbs(diff);
2643                 diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
2644                 tesubtotal += (double) ddAbs(diff);
2645                 temeasured += 2.0;
2646                 if (scan->next != sentinel) {
2647                     diff = (long) scan - (long) scan->next;
2648                     nextsubtotal += (double) ddAbs(diff);
2649                     nextmeasured += 1.0;
2650                 }
2651                 scan = scan->next;
2652             }
2653         }
2654         tetotal += tesubtotal;
2655         nexttotal += nextsubtotal;
2656     }
2657
2658     /* Scan the constant table. */
2659     nodelist = dd->constants.nodelist;
2660     nextsubtotal = 0.0;
2661     slots = dd->constants.slots;
2662     for (j = 0; j < slots; j++) {
2663         scan = nodelist[j];
2664         while (scan != NULL) {
2665             if (scan->next != NULL) {
2666                 diff = (long) scan - (long) scan->next;
2667                 nextsubtotal += (double) ddAbs(diff);
2668                 nextmeasured += 1.0;
2669             }
2670             scan = scan->next;
2671         }
2672     }
2673     nexttotal += nextsubtotal;
2674
2675     return((tetotal + nexttotal) / (temeasured + nextmeasured));
2676
2677 } /* end of Cudd_AverageDistance */
2678
2679
2680 /**Function********************************************************************
2681
2682   Synopsis    [Portable random number generator.]
2683
2684   Description [Portable number generator based on ran2 from "Numerical
2685   Recipes in C." It is a long period (> 2 * 10^18) random number generator
2686   of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
2687   distributed between 0 and 2147483561 (inclusive of the endpoint values).
2688   The random generator can be explicitly initialized by calling
2689   Cudd_Srandom. If no explicit initialization is performed, then the
2690   seed 1 is assumed.]
2691
2692   SideEffects [None]
2693
2694   SeeAlso     [Cudd_Srandom]
2695
2696 ******************************************************************************/
2697 long
2698 Cudd_Random(void)
2699 {
2700     int i;      /* index in the shuffle table */
2701     long int w; /* work variable */
2702
2703     /* cuddRand == 0 if the geneartor has not been initialized yet. */
2704     if (cuddRand == 0) Cudd_Srandom(1);
2705
2706     /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
2707     ** overflows by Schrage's method.
2708     */
2709     w          = cuddRand / LEQQ1;
2710     cuddRand   = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2711     cuddRand  += (cuddRand < 0) * MODULUS1;
2712
2713     /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
2714     ** overflows by Schrage's method.
2715     */
2716     w          = cuddRand2 / LEQQ2;
2717     cuddRand2  = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
2718     cuddRand2 += (cuddRand2 < 0) * MODULUS2;
2719
2720     /* cuddRand is shuffled with the Bays-Durham algorithm.
2721     ** shuffleSelect and cuddRand2 are combined to generate the output.
2722     */
2723
2724     /* Pick one element from the shuffle table; "i" will be in the range
2725     ** from 0 to STAB_SIZE-1.
2726     */
2727     i = (int) (shuffleSelect / STAB_DIV);
2728     /* Mix the element of the shuffle table with the current iterate of
2729     ** the second sub-generator, and replace the chosen element of the
2730     ** shuffle table with the current iterate of the first sub-generator.
2731     */
2732     shuffleSelect   = shuffleTable[i] - cuddRand2;
2733     shuffleTable[i] = cuddRand;
2734     shuffleSelect  += (shuffleSelect < 1) * (MODULUS1 - 1);
2735     /* Since shuffleSelect != 0, and we want to be able to return 0,
2736     ** here we subtract 1 before returning.
2737     */
2738     return(shuffleSelect - 1);
2739
2740 } /* end of Cudd_Random */
2741
2742
2743 /**Function********************************************************************
2744
2745   Synopsis    [Initializer for the portable random number generator.]
2746
2747   Description [Initializer for the portable number generator based on
2748   ran2 in "Numerical Recipes in C." The input is the seed for the
2749   generator. If it is negative, its absolute value is taken as seed.
2750   If it is 0, then 1 is taken as seed. The initialized sets up the two
2751   recurrences used to generate a long-period stream, and sets up the
2752   shuffle table.]
2753
2754   SideEffects [None]
2755
2756   SeeAlso     [Cudd_Random]
2757
2758 ******************************************************************************/
2759 void
2760 Cudd_Srandom(
2761   long  seed)
2762 {
2763     int i;
2764
2765     if (seed < 0)       cuddRand = -seed;
2766     else if (seed == 0) cuddRand = 1;
2767     else                cuddRand = seed;
2768     cuddRand2 = cuddRand;
2769     /* Load the shuffle table (after 11 warm-ups). */
2770     for (i = 0; i < STAB_SIZE + 11; i++) {
2771         long int w;
2772         w = cuddRand / LEQQ1;
2773         cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2774         cuddRand += (cuddRand < 0) * MODULUS1;
2775         shuffleTable[i % STAB_SIZE] = cuddRand;
2776     }
2777     shuffleSelect = shuffleTable[1 % STAB_SIZE];
2778
2779 } /* end of Cudd_Srandom */
2780
2781
2782 /**Function********************************************************************
2783
2784   Synopsis    [Computes the density of a BDD or ADD.]
2785
2786   Description [Computes the density of a BDD or ADD. The density is
2787   the ratio of the number of minterms to the number of nodes. If 0 is
2788   passed as number of variables, the number of variables existing in
2789   the manager is used. Returns the density if successful; (double)
2790   CUDD_OUT_OF_MEM otherwise.]
2791
2792   SideEffects [None]
2793
2794   SeeAlso     [Cudd_CountMinterm Cudd_DagSize]
2795
2796 ******************************************************************************/
2797 double
2798 Cudd_Density(
2799   DdManager * dd /* manager */,
2800   DdNode * f /* function whose density is sought */,
2801   int  nvars /* size of the support of f */)
2802 {
2803     double minterms;
2804     int nodes;
2805     double density;
2806
2807     if (nvars == 0) nvars = dd->size;
2808     minterms = Cudd_CountMinterm(dd,f,nvars);
2809     if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
2810     nodes = Cudd_DagSize(f);
2811     density = minterms / (double) nodes;
2812     return(density);
2813
2814 } /* end of Cudd_Density */
2815
2816
2817 /**Function********************************************************************
2818
2819   Synopsis    [Warns that a memory allocation failed.]
2820
2821   Description [Warns that a memory allocation failed.
2822   This function can be used as replacement of MMout_of_memory to prevent
2823   the safe_mem functions of the util package from exiting when malloc
2824   returns NULL. One possible use is in case of discretionary allocations;
2825   for instance, the allocation of memory to enlarge the computed table.]
2826
2827   SideEffects [None]
2828
2829   SeeAlso     []
2830
2831 ******************************************************************************/
2832 void
2833 Cudd_OutOfMem(
2834   long size /* size of the allocation that failed */)
2835 {
2836     (void) fflush(stdout);
2837     (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
2838     return;
2839
2840 } /* end of Cudd_OutOfMem */
2841
2842
2843 /*---------------------------------------------------------------------------*/
2844 /* Definition of internal functions                                          */
2845 /*---------------------------------------------------------------------------*/
2846
2847
2848 /**Function********************************************************************
2849
2850   Synopsis    [Prints a DD to the standard output. One line per node is
2851   printed.]
2852
2853   Description [Prints a DD to the standard output. One line per node is
2854   printed. Returns 1 if successful; 0 otherwise.]
2855
2856   SideEffects [None]
2857
2858   SeeAlso     [Cudd_PrintDebug]
2859
2860 ******************************************************************************/
2861 int
2862 cuddP(
2863   DdManager * dd,
2864   DdNode * f)
2865 {
2866     int retval;
2867     st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
2868
2869     if (table == NULL) return(0);
2870
2871     retval = dp2(dd,f,table);
2872     st_free_table(table);
2873     (void) fputc('\n',dd->out);
2874     return(retval);
2875
2876 } /* end of cuddP */
2877
2878
2879 /**Function********************************************************************
2880
2881   Synopsis [Frees the memory used to store the minterm counts recorded
2882   in the visited table.]
2883
2884   Description [Frees the memory used to store the minterm counts
2885   recorded in the visited table. Returns ST_CONTINUE.]
2886
2887   SideEffects [None]
2888
2889 ******************************************************************************/
2890 enum st_retval
2891 cuddStCountfree(
2892   char * key,
2893   char * value,
2894   char * arg)
2895 {
2896     double      *d;
2897
2898     d = (double *)value;
2899     FREE(d);
2900     return(ST_CONTINUE);
2901
2902 } /* end of cuddStCountfree */
2903
2904
2905 /**Function********************************************************************
2906
2907   Synopsis    [Recursively collects all the nodes of a DD in a symbol
2908   table.]
2909
2910   Description [Traverses the DD f and collects all its nodes in a
2911   symbol table.  f is assumed to be a regular pointer and
2912   cuddCollectNodes guarantees this assumption in the recursive calls.
2913   Returns 1 in case of success; 0 otherwise.]
2914
2915   SideEffects [None]
2916
2917   SeeAlso     []
2918
2919 ******************************************************************************/
2920 int
2921 cuddCollectNodes(
2922   DdNode * f,
2923   st_table * visited)
2924 {
2925     DdNode      *T, *E;
2926     int         retval;
2927
2928 #ifdef DD_DEBUG
2929     assert(!Cudd_IsComplement(f));
2930 #endif
2931
2932     /* If already visited, nothing to do. */
2933     if (st_is_member(visited, (char *) f) == 1)
2934         return(1);
2935
2936     /* Check for abnormal condition that should never happen. */
2937     if (f == NULL)
2938         return(0);
2939
2940     /* Mark node as visited. */
2941     if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
2942         return(0);
2943
2944     /* Check terminal case. */
2945     if (cuddIsConstant(f))
2946         return(1);
2947
2948     /* Recursive calls. */
2949     T = cuddT(f);
2950     retval = cuddCollectNodes(T,visited);
2951     if (retval != 1) return(retval);
2952     E = Cudd_Regular(cuddE(f));
2953     retval = cuddCollectNodes(E,visited);
2954     return(retval);
2955
2956 } /* end of cuddCollectNodes */
2957
2958
2959 /**Function********************************************************************
2960
2961   Synopsis    [Recursively collects all the nodes of a DD in an array.]
2962
2963   Description [Traverses the DD f and collects all its nodes in an array.
2964   The caller should free the array returned by cuddNodeArray.
2965   Returns a pointer to the array of nodes in case of success; NULL
2966   otherwise.  The nodes are collected in reverse topological order, so
2967   that a node is always preceded in the array by all its descendants.]
2968
2969   SideEffects [The number of nodes is returned as a side effect.]
2970
2971   SeeAlso     [Cudd_FirstNode]
2972
2973 ******************************************************************************/
2974 DdNodePtr *
2975 cuddNodeArray(
2976   DdNode *f,
2977   int *n)
2978 {
2979     DdNodePtr *table;
2980     int size, retval;
2981
2982     size = ddDagInt(Cudd_Regular(f));
2983     table = ALLOC(DdNodePtr, size);
2984     if (table == NULL) {
2985         ddClearFlag(Cudd_Regular(f));
2986         return(NULL);
2987     }
2988
2989     retval = cuddNodeArrayRecur(f, table, 0);
2990     assert(retval == size);
2991
2992     *n = size;
2993     return(table);
2994
2995 } /* cuddNodeArray */
2996
2997
2998 /*---------------------------------------------------------------------------*/
2999 /* Definition of static functions                                            */
3000 /*---------------------------------------------------------------------------*/
3001
3002
3003 /**Function********************************************************************
3004
3005   Synopsis    [Performs the recursive step of cuddP.]
3006
3007   Description [Performs the recursive step of cuddP. Returns 1 in case
3008   of success; 0 otherwise.]
3009
3010   SideEffects [None]
3011
3012 ******************************************************************************/
3013 static int
3014 dp2(
3015   DdManager *dd,
3016   DdNode * f,
3017   st_table * t)
3018 {
3019     DdNode *g, *n, *N;
3020     int T,E;
3021
3022     if (f == NULL) {
3023         return(0);
3024     }
3025     g = Cudd_Regular(f);
3026     if (cuddIsConstant(g)) {
3027 #if SIZEOF_VOID_P == 8
3028         (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
3029                 (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3030 #else
3031         (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
3032                 (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3033 #endif
3034         return(1);
3035     }
3036     if (st_is_member(t,(char *) g) == 1) {
3037         return(1);
3038     }
3039     if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
3040         return(0);
3041 #ifdef DD_STATS
3042 #if SIZEOF_VOID_P == 8
3043     (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
3044                 (ptruint) g / (ptruint) sizeof(DdNode), g->index, g->ref);
3045 #else
3046     (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
3047                 (ptruint) g / (ptruint) sizeof(DdNode),g->index,g->ref);
3048 #endif
3049 #else
3050 #if SIZEOF_VOID_P == 8
3051     (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %u\t", bang(f),
3052                 (ptruint) g / (ptruint) sizeof(DdNode),g->index);
3053 #else
3054     (void) fprintf(dd->out,"ID = %c0x%x\tindex = %hu\t", bang(f),
3055                 (ptruint) g / (ptruint) sizeof(DdNode),g->index);
3056 #endif
3057 #endif
3058     n = cuddT(g);
3059     if (cuddIsConstant(n)) {
3060         (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
3061         T = 1;
3062     } else {
3063 #if SIZEOF_VOID_P == 8
3064         (void) fprintf(dd->out,"T = 0x%lx\t",(ptruint) n / (ptruint) sizeof(DdNode));
3065 #else
3066         (void) fprintf(dd->out,"T = 0x%x\t",(ptruint) n / (ptruint) sizeof(DdNode));
3067 #endif
3068         T = 0;
3069     }
3070
3071     n = cuddE(g);
3072     N = Cudd_Regular(n);
3073     if (cuddIsConstant(N)) {
3074         (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
3075         E = 1;
3076     } else {
3077 #if SIZEOF_VOID_P == 8
3078         (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3079 #else
3080         (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3081 #endif
3082         E = 0;
3083     }
3084     if (E == 0) {
3085         if (dp2(dd,N,t) == 0)
3086             return(0);
3087     }
3088     if (T == 0) {
3089         if (dp2(dd,cuddT(g),t) == 0)
3090             return(0);
3091     }
3092     return(1);
3093
3094 } /* end of dp2 */
3095
3096
3097 /**Function********************************************************************
3098
3099   Synopsis    [Performs the recursive step of Cudd_PrintMinterm.]
3100
3101   Description []
3102
3103   SideEffects [None]
3104
3105 ******************************************************************************/
3106 static void
3107 ddPrintMintermAux(
3108   DdManager * dd /* manager */,
3109   DdNode * node /* current node */,
3110   int * list /* current recursion path */)
3111 {
3112     DdNode      *N,*Nv,*Nnv;
3113     int         i,v,index;
3114
3115     N = Cudd_Regular(node);
3116
3117     if (cuddIsConstant(N)) {
3118         /* Terminal case: Print one cube based on the current recursion
3119         ** path, unless we have reached the background value (ADDs) or
3120         ** the logical zero (BDDs).
3121         */
3122         if (node != background && node != zero) {
3123             for (i = 0; i < dd->size; i++) {
3124                 v = list[i];
3125                 if (v == 0) (void) fprintf(dd->out,"0");
3126                 else if (v == 1) (void) fprintf(dd->out,"1");
3127                 else (void) fprintf(dd->out,"-");
3128             }
3129             (void) fprintf(dd->out," % g\n", cuddV(node));
3130         }
3131     } else {
3132         Nv  = cuddT(N);
3133         Nnv = cuddE(N);
3134         if (Cudd_IsComplement(node)) {
3135             Nv  = Cudd_Not(Nv);
3136             Nnv = Cudd_Not(Nnv);
3137         }
3138         index = N->index;
3139         list[index] = 0;
3140         ddPrintMintermAux(dd,Nnv,list);
3141         list[index] = 1;
3142         ddPrintMintermAux(dd,Nv,list);
3143         list[index] = 2;
3144     }
3145     return;
3146
3147 } /* end of ddPrintMintermAux */
3148
3149
3150 /**Function********************************************************************
3151
3152   Synopsis    [Performs the recursive step of Cudd_DagSize.]
3153
3154   Description [Performs the recursive step of Cudd_DagSize. Returns the
3155   number of nodes in the graph rooted at n.]
3156
3157   SideEffects [None]
3158
3159 ******************************************************************************/
3160 static int
3161 ddDagInt(
3162   DdNode * n)
3163 {
3164     int tval, eval;
3165
3166     if (Cudd_IsComplement(n->next)) {
3167         return(0);
3168     }
3169     n->next = Cudd_Not(n->next);
3170     if (cuddIsConstant(n)) {
3171         return(1);
3172     }
3173     tval = ddDagInt(cuddT(n));
3174     eval = ddDagInt(Cudd_Regular(cuddE(n)));
3175     return(1 + tval + eval);
3176
3177 } /* end of ddDagInt */
3178
3179
3180 /**Function********************************************************************
3181
3182   Synopsis    [Performs the recursive step of cuddNodeArray.]
3183
3184   Description [Performs the recursive step of cuddNodeArray.  Returns
3185   an the number of nodes in the DD.  Clear the least significant bit
3186   of the next field that was used as visited flag by
3187   cuddNodeArrayRecur when counting the nodes.  node is supposed to be
3188   regular; the invariant is maintained by this procedure.]
3189
3190   SideEffects [None]
3191
3192   SeeAlso     []
3193
3194 ******************************************************************************/
3195 static int
3196 cuddNodeArrayRecur(
3197   DdNode *f,
3198   DdNodePtr *table,
3199   int index)
3200 {
3201     int tindex, eindex;
3202
3203     if (!Cudd_IsComplement(f->next)) {
3204         return(index);
3205     }
3206     /* Clear visited flag. */
3207     f->next = Cudd_Regular(f->next);
3208     if (cuddIsConstant(f)) {
3209         table[index] = f;
3210         return(index + 1);
3211     }
3212     tindex = cuddNodeArrayRecur(cuddT(f), table, index);
3213     eindex = cuddNodeArrayRecur(Cudd_Regular(cuddE(f)), table, tindex);
3214     table[eindex] = f;
3215     return(eindex + 1);
3216
3217 } /* end of cuddNodeArrayRecur */
3218
3219
3220 /**Function********************************************************************
3221
3222   Synopsis    [Performs the recursive step of Cudd_CofactorEstimate.]
3223
3224   Description [Performs the recursive step of Cudd_CofactorEstimate.
3225   Returns an estimate of the number of nodes in the DD of a
3226   cofactor of node. Uses the least significant bit of the next field as
3227   visited flag. node is supposed to be regular; the invariant is maintained
3228   by this procedure.]
3229
3230   SideEffects [None]
3231
3232   SeeAlso     []
3233
3234 ******************************************************************************/
3235 static int
3236 cuddEstimateCofactor(
3237   DdManager *dd,
3238   st_table *table,
3239   DdNode * node,
3240   int i,
3241   int phase,
3242   DdNode ** ptr)
3243 {
3244     int tval, eval, val;
3245     DdNode *ptrT, *ptrE;
3246
3247     if (Cudd_IsComplement(node->next)) {
3248         if (!st_lookup(table,(char *)node,(char **)ptr)) {
3249             if (st_add_direct(table,(char *)node,(char *)node) ==
3250                 ST_OUT_OF_MEM)
3251                 return(CUDD_OUT_OF_MEM);
3252             *ptr = node;
3253         }
3254         return(0);
3255     }
3256     node->next = Cudd_Not(node->next);
3257     if (cuddIsConstant(node)) {
3258         *ptr = node;
3259         if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM)
3260             return(CUDD_OUT_OF_MEM);
3261         return(1);
3262     }
3263     if ((int) node->index == i) {
3264         if (phase == 1) {
3265             *ptr = cuddT(node);
3266             val = ddDagInt(cuddT(node));
3267         } else {
3268             *ptr = cuddE(node);
3269             val = ddDagInt(Cudd_Regular(cuddE(node)));
3270         }
3271         if (node->ref > 1) {
3272             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
3273                 ST_OUT_OF_MEM)
3274                 return(CUDD_OUT_OF_MEM);
3275         }
3276         return(val);
3277     }
3278     if (dd->perm[node->index] > dd->perm[i]) {
3279         *ptr = node;
3280         tval = ddDagInt(cuddT(node));
3281         eval = ddDagInt(Cudd_Regular(cuddE(node)));
3282         if (node->ref > 1) {
3283             if (st_add_direct(table,(char *)node,(char *)node) ==
3284                 ST_OUT_OF_MEM)
3285                 return(CUDD_OUT_OF_MEM);
3286         }
3287         val = 1 + tval + eval;
3288         return(val);
3289     }
3290     tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
3291     eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
3292                                 phase,&ptrE);
3293     ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
3294     if (ptrT == ptrE) {         /* recombination */
3295         *ptr = ptrT;
3296         val = tval;
3297         if (node->ref > 1) {
3298             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
3299                     ST_OUT_OF_MEM)
3300                 return(CUDD_OUT_OF_MEM);
3301         }
3302     } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
3303                (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
3304         if (Cudd_IsComplement((*ptr)->next)) {
3305             val = 0;
3306         } else {
3307             val = 1 + tval + eval;
3308         }
3309         if (node->ref > 1) {
3310             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
3311                     ST_OUT_OF_MEM)
3312                 return(CUDD_OUT_OF_MEM);
3313         }
3314     } else {
3315         *ptr = node;
3316         val = 1 + tval + eval;
3317     }
3318     return(val);
3319
3320 } /* end of cuddEstimateCofactor */
3321
3322
3323 /**Function********************************************************************
3324
3325   Synopsis    [Checks the unique table for the existence of an internal node.]
3326
3327   Description [Checks the unique table for the existence of an internal
3328   node. Returns a pointer to the node if it is in the table; NULL otherwise.]
3329
3330   SideEffects [None]
3331
3332   SeeAlso     [cuddUniqueInter]
3333
3334 ******************************************************************************/
3335 static DdNode *
3336 cuddUniqueLookup(
3337   DdManager * unique,
3338   int  index,
3339   DdNode * T,
3340   DdNode * E)
3341 {
3342     int posn;
3343     unsigned int level;
3344     DdNodePtr *nodelist;
3345     DdNode *looking;
3346     DdSubtable *subtable;
3347
3348     if (index >= unique->size) {
3349         return(NULL);
3350     }
3351
3352     level = unique->perm[index];
3353     subtable = &(unique->subtables[level]);
3354
3355 #ifdef DD_DEBUG
3356     assert(level < (unsigned) cuddI(unique,T->index));
3357     assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
3358 #endif
3359
3360     posn = ddHash(T, E, subtable->shift);
3361     nodelist = subtable->nodelist;
3362     looking = nodelist[posn];
3363
3364     while (T < cuddT(looking)) {
3365         looking = Cudd_Regular(looking->next);
3366     }
3367     while (T == cuddT(looking) && E < cuddE(looking)) {
3368         looking = Cudd_Regular(looking->next);
3369     }
3370     if (cuddT(looking) == T && cuddE(looking) == E) {
3371         return(looking);
3372     }
3373
3374     return(NULL);
3375
3376 } /* end of cuddUniqueLookup */
3377
3378
3379 /**Function********************************************************************
3380
3381   Synopsis    [Performs the recursive step of Cudd_CofactorEstimateSimple.]
3382
3383   Description [Performs the recursive step of Cudd_CofactorEstimateSimple.
3384   Returns an estimate of the number of nodes in the DD of the positive
3385   cofactor of node. Uses the least significant bit of the next field as
3386   visited flag. node is supposed to be regular; the invariant is maintained
3387   by this procedure.]
3388
3389   SideEffects [None]
3390
3391   SeeAlso     []
3392
3393 ******************************************************************************/
3394 static int
3395 cuddEstimateCofactorSimple(
3396   DdNode * node,
3397   int i)
3398 {
3399     int tval, eval;
3400
3401     if (Cudd_IsComplement(node->next)) {
3402         return(0);
3403     }
3404     node->next = Cudd_Not(node->next);
3405     if (cuddIsConstant(node)) {
3406         return(1);
3407     }
3408     tval = cuddEstimateCofactorSimple(cuddT(node),i);
3409     if ((int) node->index == i) return(tval);
3410     eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
3411     return(1 + tval + eval);
3412
3413 } /* end of cuddEstimateCofactorSimple */
3414
3415
3416 /**Function********************************************************************
3417
3418   Synopsis    [Performs the recursive step of Cudd_CountMinterm.]
3419
3420   Description [Performs the recursive step of Cudd_CountMinterm.
3421   It is based on the following identity. Let |f| be the
3422   number of minterms of f. Then:
3423   <xmp>
3424     |f| = (|f0|+|f1|)/2
3425   </xmp>
3426   where f0 and f1 are the two cofactors of f.  Does not use the
3427   identity |f'| = max - |f|, to minimize loss of accuracy due to
3428   roundoff.  Returns the number of minterms of the function rooted at
3429   node.]
3430
3431   SideEffects [None]
3432
3433 ******************************************************************************/
3434 static double
3435 ddCountMintermAux(
3436   DdNode * node,
3437   double  max,
3438   DdHashTable * table)
3439 {
3440     DdNode      *N, *Nt, *Ne;
3441     double      min, minT, minE;
3442     DdNode      *res;
3443
3444     N = Cudd_Regular(node);
3445
3446     if (cuddIsConstant(N)) {
3447         if (node == background || node == zero) {
3448             return(0.0);
3449         } else {
3450             return(max);
3451         }
3452     }
3453     if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
3454         min = cuddV(res);
3455         if (res->ref == 0) {
3456             table->manager->dead++;
3457             table->manager->constants.dead++;
3458         }
3459         return(min);
3460     }
3461
3462     Nt = cuddT(N); Ne = cuddE(N);
3463     if (Cudd_IsComplement(node)) {
3464         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3465     }
3466
3467     minT = ddCountMintermAux(Nt,max,table);
3468     if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3469     minT *= 0.5;
3470     minE = ddCountMintermAux(Ne,max,table);
3471     if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3472     minE *= 0.5;
3473     min = minT + minE;
3474
3475     if (N->ref != 1) {
3476         ptrint fanout = (ptrint) N->ref;
3477         cuddSatDec(fanout);
3478         res = cuddUniqueConst(table->manager,min);
3479         if (!cuddHashTableInsert1(table,node,res,fanout)) {
3480             cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
3481             return((double)CUDD_OUT_OF_MEM);
3482         }
3483     }
3484
3485     return(min);
3486
3487 } /* end of ddCountMintermAux */
3488
3489
3490 /**Function********************************************************************
3491
3492   Synopsis    [Performs the recursive step of Cudd_CountPath.]
3493
3494   Description [Performs the recursive step of Cudd_CountPath.
3495   It is based on the following identity. Let |f| be the
3496   number of paths of f. Then:
3497   <xmp>
3498     |f| = |f0|+|f1|
3499   </xmp>
3500   where f0 and f1 are the two cofactors of f.  Uses the
3501   identity |f'| = |f|, to improve the utilization of the (local) cache.
3502   Returns the number of paths of the function rooted at node.]
3503
3504   SideEffects [None]
3505
3506 ******************************************************************************/
3507 static double
3508 ddCountPathAux(
3509   DdNode * node,
3510   st_table * table)
3511 {
3512
3513     DdNode      *Nv, *Nnv;
3514     double      paths, *ppaths, paths1, paths2;
3515     double      *dummy;
3516
3517
3518     if (cuddIsConstant(node)) {
3519         return(1.0);
3520     }
3521     if (st_lookup(table, node, &dummy)) {
3522         paths = *dummy;
3523         return(paths);
3524     }
3525
3526     Nv = cuddT(node); Nnv = cuddE(node);
3527
3528     paths1 = ddCountPathAux(Nv,table);
3529     if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3530     paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
3531     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3532     paths = paths1 + paths2;
3533
3534     ppaths = ALLOC(double,1);
3535     if (ppaths == NULL) {
3536         return((double)CUDD_OUT_OF_MEM);
3537     }
3538
3539     *ppaths = paths;
3540
3541     if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
3542         FREE(ppaths);
3543         return((double)CUDD_OUT_OF_MEM);
3544     }
3545     return(paths);
3546
3547 } /* end of ddCountPathAux */
3548
3549
3550 /**Function********************************************************************
3551
3552   Synopsis    [Performs the recursive step of Cudd_EpdCountMinterm.]
3553
3554   Description [Performs the recursive step of Cudd_EpdCountMinterm.
3555   It is based on the following identity. Let |f| be the
3556   number of minterms of f. Then:
3557   <xmp>
3558     |f| = (|f0|+|f1|)/2
3559   </xmp>
3560   where f0 and f1 are the two cofactors of f.  Does not use the
3561   identity |f'| = max - |f|, to minimize loss of accuracy due to
3562   roundoff.  Returns the number of minterms of the function rooted at
3563   node.]
3564
3565   SideEffects [None]
3566
3567 ******************************************************************************/
3568 static int
3569 ddEpdCountMintermAux(
3570   DdNode * node,
3571   EpDouble * max,
3572   EpDouble * epd,
3573   st_table * table)
3574 {
3575     DdNode      *Nt, *Ne;
3576     EpDouble    *min, minT, minE;
3577     EpDouble    *res;
3578     int         status;
3579
3580     /* node is assumed to be regular */
3581     if (cuddIsConstant(node)) {
3582         if (node == background || node == zero) {
3583             EpdMakeZero(epd, 0);
3584         } else {
3585             EpdCopy(max, epd);
3586         }
3587         return(0);
3588     }
3589     if (node->ref != 1 && st_lookup(table, node, &res)) {
3590         EpdCopy(res, epd);
3591         return(0);
3592     }
3593
3594     Nt = cuddT(node); Ne = cuddE(node);
3595
3596     status = ddEpdCountMintermAux(Nt,max,&minT,table);
3597     if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3598     EpdMultiply(&minT, (double)0.5);
3599     status = ddEpdCountMintermAux(Cudd_Regular(Ne),max,&minE,table);
3600     if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3601     if (Cudd_IsComplement(Ne)) {
3602         EpdSubtract3(max, &minE, epd);
3603         EpdCopy(epd, &minE);
3604     }
3605     EpdMultiply(&minE, (double)0.5);
3606     EpdAdd3(&minT, &minE, epd);
3607
3608     if (node->ref > 1) {
3609         min = EpdAlloc();
3610         if (!min)
3611             return(CUDD_OUT_OF_MEM);
3612         EpdCopy(epd, min);
3613         if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) {
3614             EpdFree(min);
3615             return(CUDD_OUT_OF_MEM);
3616         }
3617     }
3618
3619     return(0);
3620
3621 } /* end of ddEpdCountMintermAux */
3622
3623
3624 /**Function********************************************************************
3625
3626   Synopsis    [Performs the recursive step of Cudd_CountPathsToNonZero.]
3627
3628   Description [Performs the recursive step of Cudd_CountPathsToNonZero.
3629   It is based on the following identity. Let |f| be the
3630   number of paths of f. Then:
3631   <xmp>
3632     |f| = |f0|+|f1|
3633   </xmp>
3634   where f0 and f1 are the two cofactors of f.  Returns the number of
3635   paths of the function rooted at node.]
3636
3637   SideEffects [None]
3638
3639 ******************************************************************************/
3640 static double
3641 ddCountPathsToNonZero(
3642   DdNode * N,
3643   st_table * table)
3644 {
3645
3646     DdNode      *node, *Nt, *Ne;
3647     double      paths, *ppaths, paths1, paths2;
3648     double      *dummy;
3649
3650     node = Cudd_Regular(N);
3651     if (cuddIsConstant(node)) {
3652         return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
3653     }
3654     if (st_lookup(table, N, &dummy)) {
3655         paths = *dummy;
3656         return(paths);
3657     }
3658
3659     Nt = cuddT(node); Ne = cuddE(node);
3660     if (node != N) {
3661         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3662     }
3663
3664     paths1 = ddCountPathsToNonZero(Nt,table);
3665     if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3666     paths2 = ddCountPathsToNonZero(Ne,table);
3667     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3668     paths = paths1 + paths2;
3669
3670     ppaths = ALLOC(double,1);
3671     if (ppaths == NULL) {
3672         return((double)CUDD_OUT_OF_MEM);
3673     }
3674
3675     *ppaths = paths;
3676
3677     if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
3678         FREE(ppaths);
3679         return((double)CUDD_OUT_OF_MEM);
3680     }
3681     return(paths);
3682
3683 } /* end of ddCountPathsToNonZero */
3684
3685
3686 /**Function********************************************************************
3687
3688   Synopsis    [Performs the recursive step of Cudd_Support.]
3689
3690   Description [Performs the recursive step of Cudd_Support. Performs a
3691   DFS from f. The support is accumulated in supp as a side effect. Uses
3692   the LSB of the then pointer as visited flag.]
3693
3694   SideEffects [None]
3695
3696   SeeAlso     [ddClearFlag]
3697
3698 ******************************************************************************/
3699 static void
3700 ddSupportStep(
3701   DdNode * f,
3702   int * support)
3703 {
3704     if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
3705         return;
3706     }
3707
3708     support[f->index] = 1;
3709     ddSupportStep(cuddT(f),support);
3710     ddSupportStep(Cudd_Regular(cuddE(f)),support);
3711     /* Mark as visited. */
3712     f->next = Cudd_Not(f->next);
3713     return;
3714
3715 } /* end of ddSupportStep */
3716
3717
3718 /**Function********************************************************************
3719
3720   Synopsis    [Performs a DFS from f, clearing the LSB of the next
3721   pointers.]
3722
3723   Description []
3724
3725   SideEffects [None]
3726
3727   SeeAlso     [ddSupportStep ddDagInt]
3728
3729 ******************************************************************************/
3730 static void
3731 ddClearFlag(
3732   DdNode * f)
3733 {
3734     if (!Cudd_IsComplement(f->next)) {
3735         return;
3736     }
3737     /* Clear visited flag. */
3738     f->next = Cudd_Regular(f->next);
3739     if (cuddIsConstant(f)) {
3740         return;
3741     }
3742     ddClearFlag(cuddT(f));
3743     ddClearFlag(Cudd_Regular(cuddE(f)));
3744     return;
3745
3746 } /* end of ddClearFlag */
3747
3748
3749 /**Function********************************************************************
3750
3751   Synopsis    [Performs the recursive step of Cudd_CountLeaves.]
3752
3753   Description [Performs the recursive step of Cudd_CountLeaves. Returns
3754   the number of leaves in the DD rooted at n.]
3755
3756   SideEffects [None]
3757
3758   SeeAlso     [Cudd_CountLeaves]
3759
3760 ******************************************************************************/
3761 static int
3762 ddLeavesInt(
3763   DdNode * n)
3764 {
3765     int tval, eval;
3766
3767     if (Cudd_IsComplement(n->next)) {
3768         return(0);
3769     }
3770     n->next = Cudd_Not(n->next);
3771     if (cuddIsConstant(n)) {
3772         return(1);
3773     }
3774     tval = ddLeavesInt(cuddT(n));
3775     eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
3776     return(tval + eval);
3777
3778 } /* end of ddLeavesInt */
3779
3780
3781 /**Function********************************************************************
3782
3783   Synopsis    [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]
3784
3785   Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms.
3786   Returns 1 if successful; 0 otherwise.]
3787
3788   SideEffects [none]
3789
3790   SeeAlso [Cudd_bddPickArbitraryMinterms]
3791
3792 ******************************************************************************/
3793 static int
3794 ddPickArbitraryMinterms(
3795   DdManager *dd,
3796   DdNode *node,
3797   int nvars,
3798   int nminterms,
3799   char **string)
3800 {
3801     DdNode *N, *T, *E;
3802     DdNode *one, *bzero;
3803     int    i, t, result;
3804     double min1, min2;
3805
3806     if (string == NULL || node == NULL) return(0);
3807
3808     /* The constant 0 function has no on-set cubes. */
3809     one = DD_ONE(dd);
3810     bzero = Cudd_Not(one);
3811     if (nminterms == 0 || node == bzero) return(1);
3812     if (node == one) {
3813         return(1);
3814     }
3815
3816     N = Cudd_Regular(node);
3817     T = cuddT(N); E = cuddE(N);
3818     if (Cudd_IsComplement(node)) {
3819         T = Cudd_Not(T); E = Cudd_Not(E);
3820     }
3821
3822     min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
3823     if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
3824     min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
3825     if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
3826
3827     t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
3828     for (i = 0; i < t; i++)
3829         string[i][N->index] = '1';
3830     for (i = t; i < nminterms; i++)
3831         string[i][N->index] = '0';
3832
3833     result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
3834     if (result == 0)
3835         return(0);
3836     result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
3837     return(result);
3838
3839 } /* end of ddPickArbitraryMinterms */
3840
3841
3842 /**Function********************************************************************
3843
3844   Synopsis    [Finds a representative cube of a BDD.]
3845
3846   Description [Finds a representative cube of a BDD with the weight of
3847   each variable. From the top variable, if the weight is greater than or
3848   equal to 0.0, choose THEN branch unless the child is the constant 0.
3849   Otherwise, choose ELSE branch unless the child is the constant 0.]
3850
3851   SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube]
3852
3853 ******************************************************************************/
3854 static int
3855 ddPickRepresentativeCube(
3856   DdManager *dd,
3857   DdNode *node,
3858   double *weight,
3859   char *string)
3860 {
3861     DdNode *N, *T, *E;
3862     DdNode *one, *bzero;
3863
3864     if (string == NULL || node == NULL) return(0);
3865
3866     /* The constant 0 function has no on-set cubes. */
3867     one = DD_ONE(dd);
3868     bzero = Cudd_Not(one);
3869     if (node == bzero) return(0);
3870
3871     if (node == DD_ONE(dd)) return(1);
3872
3873     for (;;) {
3874         N = Cudd_Regular(node);
3875         if (N == one)
3876             break;
3877         T = cuddT(N);
3878         E = cuddE(N);
3879         if (Cudd_IsComplement(node)) {
3880             T = Cudd_Not(T);
3881             E = Cudd_Not(E);
3882         }
3883         if (weight[N->index] >= 0.0) {
3884             if (T == bzero) {
3885                 node = E;
3886                 string[N->index] = '0';
3887             } else {
3888                 node = T;
3889                 string[N->index] = '1';
3890             }
3891         } else {
3892             if (E == bzero) {
3893                 node = T;
3894                 string[N->index] = '1';
3895             } else {
3896                 node = E;
3897                 string[N->index] = '0';
3898             }
3899         }
3900     }
3901     return(1);
3902
3903 } /* end of ddPickRepresentativeCube */
3904
3905
3906 /**Function********************************************************************
3907
3908   Synopsis [Frees the memory used to store the minterm counts recorded
3909   in the visited table.]
3910
3911   Description [Frees the memory used to store the minterm counts
3912   recorded in the visited table. Returns ST_CONTINUE.]
3913
3914   SideEffects [None]
3915
3916 ******************************************************************************/
3917 static enum st_retval
3918 ddEpdFree(
3919   char * key,
3920   char * value,
3921   char * arg)
3922 {
3923     EpDouble    *epd;
3924
3925     epd = (EpDouble *) value;
3926     EpdFree(epd);
3927     return(ST_CONTINUE);
3928
3929 } /* end of ddEpdFree */