distr/cudd/cuddSubsetHB.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddSubsetHB.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Procedure to subset the given BDD by choosing the heavier
   8                branches.]
   9
  10
  11   Description [External procedures provided by this module:
  12                 <ul>
  13                 <li> Cudd_SubsetHeavyBranch()
  14                 <li> Cudd_SupersetHeavyBranch()
  15                 </ul>
  16                Internal procedures included in this module:
  17                 <ul>
  18                 <li> cuddSubsetHeavyBranch()
  19                 </ul>
  20                Static procedures included in this module:
  21                 <ul>
  22                 <li> ResizeCountMintermPages();
  23                 <li> ResizeNodeDataPages()
  24                 <li> ResizeCountNodePages()
  25                 <li> SubsetCountMintermAux()
  26                 <li> SubsetCountMinterm()
  27                 <li> SubsetCountNodesAux()
  28                 <li> SubsetCountNodes()
  29                 <li> BuildSubsetBdd()
  30                 </ul>
  31                 ]
  32
  33   SeeAlso     [cuddSubsetSP.c]
  34
  35   Author      [Kavita Ravi]
  36
  37   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  38
  39   All rights reserved.
  40
  41   Redistribution and use in source and binary forms, with or without
  42   modification, are permitted provided that the following conditions
  43   are met:
  44
  45   Redistributions of source code must retain the above copyright
  46   notice, this list of conditions and the following disclaimer.
  47
  48   Redistributions in binary form must reproduce the above copyright
  49   notice, this list of conditions and the following disclaimer in the
  50   documentation and/or other materials provided with the distribution.
  51
  52   Neither the name of the University of Colorado nor the names of its
  53   contributors may be used to endorse or promote products derived from
  54   this software without specific prior written permission.
  55
  56   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  57   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  58   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  59   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  60   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  61   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  62   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  63   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  64   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  65   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  66   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  67   POSSIBILITY OF SUCH DAMAGE.]
  68
  69 ******************************************************************************/
  70
  71 #ifdef __STDC__
  72 #include <float.h>
  73 #else
  74 #define DBL_MAX_EXP 1024
  75 #endif
  76 #include "util.h"
  77 #include "cuddInt.h"
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Constant declarations                                                     */
  81 /*---------------------------------------------------------------------------*/
  82
  83 #define DEFAULT_PAGE_SIZE 2048
  84 #define DEFAULT_NODE_DATA_PAGE_SIZE 1024
  85 #define INITIAL_PAGES 128
  86
  87
  88 /*---------------------------------------------------------------------------*/
  89 /* Stucture declarations                                                     */
  90 /*---------------------------------------------------------------------------*/
  91
  92 /* data structure to store the information on each node. It keeps
  93  * the number of minterms represented by the DAG rooted at this node
  94  * in terms of the number of variables specified by the user, number
  95  * of nodes in this DAG and the number of nodes of its child with
  96  * lesser number of minterms that are not shared by the child with
  97  * more minterms
  98  */
  99 struct NodeData {
 100     double *mintermPointer;
 101     int *nodesPointer;
 102     int *lightChildNodesPointer;
 103 };
 104
 105 /*---------------------------------------------------------------------------*/
 106 /* Type declarations                                                         */
 107 /*---------------------------------------------------------------------------*/
 108
 109 typedef struct NodeData NodeData_t;
 110
 111 /*---------------------------------------------------------------------------*/
 112 /* Variable declarations                                                     */
 113 /*---------------------------------------------------------------------------*/
 114
 115 #ifndef lint
 116 static char rcsid[] DD_UNUSED = "$Id: cuddSubsetHB.c,v 1.37 2009/02/20 02:14:58 fabio Exp $";
 117 #endif
 118
 119 static int memOut;
 120 #ifdef DEBUG
 121 static  int             num_calls;
 122 #endif
 123
 124 static  DdNode          *zero, *one; /* constant functions */
 125 static  double          **mintermPages; /* pointers to the pages */
 126 static  int             **nodePages; /* pointers to the pages */
 127 static  int             **lightNodePages; /* pointers to the pages */
 128 static  double          *currentMintermPage; /* pointer to the current
 129                                                    page */
 130 static  double          max; /* to store the 2^n value of the number
 131                               * of variables */
 132
 133 static  int             *currentNodePage; /* pointer to the current
 134                                                    page */
 135 static  int             *currentLightNodePage; /* pointer to the
 136                                                 *  current page */
 137 static  int             pageIndex; /* index to next element */
 138 static  int             page; /* index to current page */
 139 static  int             pageSize = DEFAULT_PAGE_SIZE; /* page size */
 140 static  int             maxPages; /* number of page pointers */
 141
 142 static  NodeData_t      *currentNodeDataPage; /* pointer to the current
 143                                                  page */
 144 static  int             nodeDataPage; /* index to next element */
 145 static  int             nodeDataPageIndex; /* index to next element */
 146 static  NodeData_t      **nodeDataPages; /* index to current page */
 147 static  int             nodeDataPageSize = DEFAULT_NODE_DATA_PAGE_SIZE;
 148                                                      /* page size */
 149 static  int             maxNodeDataPages; /* number of page pointers */
 150
 151
 152 /*---------------------------------------------------------------------------*/
 153 /* Macro declarations                                                        */
 154 /*---------------------------------------------------------------------------*/
 155
 156 /**AutomaticStart*************************************************************/
 157
 158 /*---------------------------------------------------------------------------*/
 159 /* Static function prototypes                                                */
 160 /*---------------------------------------------------------------------------*/
 161
 162 static void ResizeNodeDataPages (void);
 163 static void ResizeCountMintermPages (void);
 164 static void ResizeCountNodePages (void);
 165 static double SubsetCountMintermAux (DdNode *node, double max, st_table *table);
 166 static st_table * SubsetCountMinterm (DdNode *node, int nvars);
 167 static int SubsetCountNodesAux (DdNode *node, st_table *table, double max);
 168 static int SubsetCountNodes (DdNode *node, st_table *table, int nvars);
 169 static void StoreNodes (st_table *storeTable, DdManager *dd, DdNode *node);
 170 static DdNode * BuildSubsetBdd (DdManager *dd, DdNode *node, int *size, st_table *visitedTable, int threshold, st_table *storeTable, st_table *approxTable);
 171
 172 /**AutomaticEnd***************************************************************/
 173
 174
 175 /*---------------------------------------------------------------------------*/
 176 /* Definition of exported functions                                          */
 177 /*---------------------------------------------------------------------------*/
 178
 179 /**Function********************************************************************
 180
 181   Synopsis    [Extracts a dense subset from a BDD with the heavy branch
 182   heuristic.]
 183
 184   Description [Extracts a dense subset from a BDD. This procedure
 185   builds a subset by throwing away one of the children of each node,
 186   starting from the root, until the result is small enough. The child
 187   that is eliminated from the result is the one that contributes the
 188   fewer minterms.  Returns a pointer to the BDD of the subset if
 189   successful. NULL if the procedure runs out of memory. The parameter
 190   numVars is the maximum number of variables to be used in minterm
 191   calculation and node count calculation.  The optimal number should
 192   be as close as possible to the size of the support of f.  However,
 193   it is safe to pass the value returned by Cudd_ReadSize for numVars
 194   when the number of variables is under 1023.  If numVars is larger
 195   than 1023, it will overflow. If a 0 parameter is passed then the
 196   procedure will compute a value which will avoid overflow but will
 197   cause underflow with 2046 variables or more.]
 198
 199   SideEffects [None]
 200
 201   SeeAlso     [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize]
 202
 203 ******************************************************************************/
 204 DdNode *
 205 Cudd_SubsetHeavyBranch(
 206   DdManager * dd /* manager */,
 207   DdNode * f /* function to be subset */,
 208   int  numVars /* number of variables in the support of f */,
 209   int  threshold /* maximum number of nodes in the subset */)
 210 {
 211     DdNode *subset;
 212
 213     memOut = 0;
 214     do {
 215         dd->reordered = 0;
 216         subset = cuddSubsetHeavyBranch(dd, f, numVars, threshold);
 217     } while ((dd->reordered == 1) && (!memOut));
 218
 219     return(subset);
 220
 221 } /* end of Cudd_SubsetHeavyBranch */
 222
 223
 224 /**Function********************************************************************
 225
 226   Synopsis    [Extracts a dense superset from a BDD with the heavy branch
 227   heuristic.]
 228
 229   Description [Extracts a dense superset from a BDD. The procedure is
 230   identical to the subset procedure except for the fact that it
 231   receives the complement of the given function. Extracting the subset
 232   of the complement function is equivalent to extracting the superset
 233   of the function. This procedure builds a superset by throwing away
 234   one of the children of each node starting from the root of the
 235   complement function, until the result is small enough. The child
 236   that is eliminated from the result is the one that contributes the
 237   fewer minterms.
 238   Returns a pointer to the BDD of the superset if successful. NULL if
 239   intermediate result causes the procedure to run out of memory. The
 240   parameter numVars is the maximum number of variables to be used in
 241   minterm calculation and node count calculation.  The optimal number
 242   should be as close as possible to the size of the support of f.
 243   However, it is safe to pass the value returned by Cudd_ReadSize for
 244   numVars when the number of variables is under 1023.  If numVars is
 245   larger than 1023, it will overflow. If a 0 parameter is passed then
 246   the procedure will compute a value which will avoid overflow but
 247   will cause underflow with 2046 variables or more.]
 248
 249   SideEffects [None]
 250
 251   SeeAlso     [Cudd_SubsetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
 252
 253 ******************************************************************************/
 254 DdNode *
 255 Cudd_SupersetHeavyBranch(
 256   DdManager * dd /* manager */,
 257   DdNode * f /* function to be superset */,
 258   int  numVars /* number of variables in the support of f */,
 259   int  threshold /* maximum number of nodes in the superset */)
 260 {
 261     DdNode *subset, *g;
 262
 263     g = Cudd_Not(f);
 264     memOut = 0;
 265     do {
 266         dd->reordered = 0;
 267         subset = cuddSubsetHeavyBranch(dd, g, numVars, threshold);
 268     } while ((dd->reordered == 1) && (!memOut));
 269
 270     return(Cudd_NotCond(subset, (subset != NULL)));
 271
 272 } /* end of Cudd_SupersetHeavyBranch */
 273
 274
 275 /*---------------------------------------------------------------------------*/
 276 /* Definition of internal functions                                          */
 277 /*---------------------------------------------------------------------------*/
 278
 279
 280 /**Function********************************************************************
 281
 282   Synopsis    [The main procedure that returns a subset by choosing the heavier
 283   branch in the BDD.]
 284
 285   Description [Here a subset BDD is built by throwing away one of the
 286   children. Starting at root, annotate each node with the number of
 287   minterms (in terms of the total number of variables specified -
 288   numVars), number of nodes taken by the DAG rooted at this node and
 289   number of additional nodes taken by the child that has the lesser
 290   minterms. The child with the lower number of minterms is thrown away
 291   and a dyanmic count of the nodes of the subset is kept. Once the
 292   threshold is reached the subset is returned to the calling
 293   procedure.]
 294
 295   SideEffects [None]
 296
 297   SeeAlso     [Cudd_SubsetHeavyBranch]
 298
 299 ******************************************************************************/
 300 DdNode *
 301 cuddSubsetHeavyBranch(
 302   DdManager * dd /* DD manager */,
 303   DdNode * f /* current DD */,
 304   int  numVars /* maximum number of variables */,
 305   int  threshold /* threshold size for the subset */)
 306 {
 307
 308     int i, *size;
 309     st_table *visitedTable;
 310     int numNodes;
 311     NodeData_t *currNodeQual;
 312     DdNode *subset;
 313     st_table *storeTable, *approxTable;
 314     char *key, *value;
 315     st_generator *stGen;
 316
 317     if (f == NULL) {
 318         fprintf(dd->err, "Cannot subset, nil object\n");
 319         dd->errorCode = CUDD_INVALID_ARG;
 320         return(NULL);
 321     }
 322
 323     one  = Cudd_ReadOne(dd);
 324     zero = Cudd_Not(one);
 325
 326     /* If user does not know numVars value, set it to the maximum
 327      * exponent that the pow function can take. The -1 is due to the
 328      * discrepancy in the value that pow takes and the value that
 329      * log gives.
 330      */
 331     if (numVars == 0) {
 332         /* set default value */
 333         numVars = DBL_MAX_EXP - 1;
 334     }
 335
 336     if (Cudd_IsConstant(f)) {
 337         return(f);
 338     }
 339
 340     max = pow(2.0, (double)numVars);
 341
 342     /* Create visited table where structures for node data are allocated and
 343        stored in a st_table */
 344     visitedTable = SubsetCountMinterm(f, numVars);
 345     if ((visitedTable == NULL) || memOut) {
 346         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
 347         dd->errorCode = CUDD_MEMORY_OUT;
 348         return(0);
 349     }
 350     numNodes = SubsetCountNodes(f, visitedTable, numVars);
 351     if (memOut) {
 352         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
 353         dd->errorCode = CUDD_MEMORY_OUT;
 354         return(0);
 355     }
 356
 357     if (st_lookup(visitedTable, f, &currNodeQual) == 0) {
 358         fprintf(dd->err,
 359                 "Something is wrong, ought to be node quality table\n");
 360         dd->errorCode = CUDD_INTERNAL_ERROR;
 361     }
 362
 363     size = ALLOC(int, 1);
 364     if (size == NULL) {
 365         dd->errorCode = CUDD_MEMORY_OUT;
 366         return(NULL);
 367     }
 368     *size = numNodes;
 369
 370 #ifdef DEBUG
 371     num_calls = 0;
 372 #endif
 373     /* table to store nodes being created. */
 374     storeTable = st_init_table(st_ptrcmp, st_ptrhash);
 375     /* insert the constant */
 376     cuddRef(one);
 377     if (st_insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
 378         ST_OUT_OF_MEM) {
 379         fprintf(dd->out, "Something wrong, st_table insert failed\n");
 380     }
 381     /* table to store approximations of nodes */
 382     approxTable = st_init_table(st_ptrcmp, st_ptrhash);
 383     subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
 384                                       storeTable, approxTable);
 385     if (subset != NULL) {
 386         cuddRef(subset);
 387     }
 388
 389     stGen = st_init_gen(approxTable);
 390     if (stGen == NULL) {
 391         st_free_table(approxTable);
 392         return(NULL);
 393     }
 394     while(st_gen(stGen, (char **)&key, (char **)&value)) {
 395         Cudd_RecursiveDeref(dd, (DdNode *)value);
 396     }
 397     st_free_gen(stGen); stGen = NULL;
 398     st_free_table(approxTable);
 399
 400     stGen = st_init_gen(storeTable);
 401     if (stGen == NULL) {
 402         st_free_table(storeTable);
 403         return(NULL);
 404     }
 405     while(st_gen(stGen, (char **)&key, (char **)&value)) {
 406         Cudd_RecursiveDeref(dd, (DdNode *)key);
 407     }
 408     st_free_gen(stGen); stGen = NULL;
 409     st_free_table(storeTable);
 410
 411     for (i = 0; i <= page; i++) {
 412         FREE(mintermPages[i]);
 413     }
 414     FREE(mintermPages);
 415     for (i = 0; i <= page; i++) {
 416         FREE(nodePages[i]);
 417     }
 418     FREE(nodePages);
 419     for (i = 0; i <= page; i++) {
 420         FREE(lightNodePages[i]);
 421     }
 422     FREE(lightNodePages);
 423     for (i = 0; i <= nodeDataPage; i++) {
 424         FREE(nodeDataPages[i]);
 425     }
 426     FREE(nodeDataPages);
 427     st_free_table(visitedTable);
 428     FREE(size);
 429 #if 0
 430     (void) Cudd_DebugCheck(dd);
 431     (void) Cudd_CheckKeys(dd);
 432 #endif
 433
 434     if (subset != NULL) {
 435 #ifdef DD_DEBUG
 436       if (!Cudd_bddLeq(dd, subset, f)) {
 437             fprintf(dd->err, "Wrong subset\n");
 438             dd->errorCode = CUDD_INTERNAL_ERROR;
 439             return(NULL);
 440       }
 441 #endif
 442         cuddDeref(subset);
 443         return(subset);
 444     } else {
 445         return(NULL);
 446     }
 447 } /* end of cuddSubsetHeavyBranch */
 448
 449
 450 /*---------------------------------------------------------------------------*/
 451 /* Definition of static functions                                            */
 452 /*---------------------------------------------------------------------------*/
 453
 454
 455 /**Function********************************************************************
 456
 457   Synopsis    [Resize the number of pages allocated to store the node data.]
 458
 459   Description [Resize the number of pages allocated to store the node data
 460   The procedure  moves the counter to the next page when the end of
 461   the page is reached and allocates new pages when necessary.]
 462
 463   SideEffects [Changes the size of pages, page, page index, maximum
 464   number of pages freeing stuff in case of memory out. ]
 465
 466   SeeAlso     []
 467
 468 ******************************************************************************/
 469 static void
 470 ResizeNodeDataPages(void)
 471 {
 472     int i;
 473     NodeData_t **newNodeDataPages;
 474
 475     nodeDataPage++;
 476     /* If the current page index is larger than the number of pages
 477      * allocated, allocate a new page array. Page numbers are incremented by
 478      * INITIAL_PAGES
 479      */
 480     if (nodeDataPage == maxNodeDataPages) {
 481         newNodeDataPages = ALLOC(NodeData_t *,maxNodeDataPages + INITIAL_PAGES);
 482         if (newNodeDataPages == NULL) {
 483             for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
 484             FREE(nodeDataPages);
 485             memOut = 1;
 486             return;
 487         } else {
 488             for (i = 0; i < maxNodeDataPages; i++) {
 489                 newNodeDataPages[i] = nodeDataPages[i];
 490             }
 491             /* Increase total page count */
 492             maxNodeDataPages += INITIAL_PAGES;
 493             FREE(nodeDataPages);
 494             nodeDataPages = newNodeDataPages;
 495         }
 496     }
 497     /* Allocate a new page */
 498     currentNodeDataPage = nodeDataPages[nodeDataPage] =
 499         ALLOC(NodeData_t ,nodeDataPageSize);
 500     if (currentNodeDataPage == NULL) {
 501         for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
 502         FREE(nodeDataPages);
 503         memOut = 1;
 504         return;
 505     }
 506     /* reset page index */
 507     nodeDataPageIndex = 0;
 508     return;
 509
 510 } /* end of ResizeNodeDataPages */
 511
 512
 513 /**Function********************************************************************
 514
 515   Synopsis    [Resize the number of pages allocated to store the minterm
 516   counts. ]
 517
 518   Description [Resize the number of pages allocated to store the minterm
 519   counts.  The procedure  moves the counter to the next page when the
 520   end of the page is reached and allocates new pages when necessary.]
 521
 522   SideEffects [Changes the size of minterm pages, page, page index, maximum
 523   number of pages freeing stuff in case of memory out. ]
 524
 525   SeeAlso     []
 526
 527 ******************************************************************************/
 528 static void
 529 ResizeCountMintermPages(void)
 530 {
 531     int i;
 532     double **newMintermPages;
 533
 534     page++;
 535     /* If the current page index is larger than the number of pages
 536      * allocated, allocate a new page array. Page numbers are incremented by
 537      * INITIAL_PAGES
 538      */
 539     if (page == maxPages) {
 540         newMintermPages = ALLOC(double *,maxPages + INITIAL_PAGES);
 541         if (newMintermPages == NULL) {
 542             for (i = 0; i < page; i++) FREE(mintermPages[i]);
 543             FREE(mintermPages);
 544             memOut = 1;
 545             return;
 546         } else {
 547             for (i = 0; i < maxPages; i++) {
 548                 newMintermPages[i] = mintermPages[i];
 549             }
 550             /* Increase total page count */
 551             maxPages += INITIAL_PAGES;
 552             FREE(mintermPages);
 553             mintermPages = newMintermPages;
 554         }
 555     }
 556     /* Allocate a new page */
 557     currentMintermPage = mintermPages[page] = ALLOC(double,pageSize);
 558     if (currentMintermPage == NULL) {
 559         for (i = 0; i < page; i++) FREE(mintermPages[i]);
 560         FREE(mintermPages);
 561         memOut = 1;
 562         return;
 563     }
 564     /* reset page index */
 565     pageIndex = 0;
 566     return;
 567
 568 } /* end of ResizeCountMintermPages */
 569
 570
 571 /**Function********************************************************************
 572
 573   Synopsis    [Resize the number of pages allocated to store the node counts.]
 574
 575   Description [Resize the number of pages allocated to store the node counts.
 576   The procedure  moves the counter to the next page when the end of
 577   the page is reached and allocates new pages when necessary.]
 578
 579   SideEffects [Changes the size of pages, page, page index, maximum
 580   number of pages freeing stuff in case of memory out.]
 581
 582   SeeAlso     []
 583
 584 ******************************************************************************/
 585 static void
 586 ResizeCountNodePages(void)
 587 {
 588     int i;
 589     int **newNodePages;
 590
 591     page++;
 592
 593     /* If the current page index is larger than the number of pages
 594      * allocated, allocate a new page array. The number of pages is incremented
 595      * by INITIAL_PAGES.
 596      */
 597     if (page == maxPages) {
 598         newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
 599         if (newNodePages == NULL) {
 600             for (i = 0; i < page; i++) FREE(nodePages[i]);
 601             FREE(nodePages);
 602             for (i = 0; i < page; i++) FREE(lightNodePages[i]);
 603             FREE(lightNodePages);
 604             memOut = 1;
 605             return;
 606         } else {
 607             for (i = 0; i < maxPages; i++) {
 608                 newNodePages[i] = nodePages[i];
 609             }
 610             FREE(nodePages);
 611             nodePages = newNodePages;
 612         }
 613
 614         newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
 615         if (newNodePages == NULL) {
 616             for (i = 0; i < page; i++) FREE(nodePages[i]);
 617             FREE(nodePages);
 618             for (i = 0; i < page; i++) FREE(lightNodePages[i]);
 619             FREE(lightNodePages);
 620             memOut = 1;
 621             return;
 622         } else {
 623             for (i = 0; i < maxPages; i++) {
 624                 newNodePages[i] = lightNodePages[i];
 625             }
 626             FREE(lightNodePages);
 627             lightNodePages = newNodePages;
 628         }
 629         /* Increase total page count */
 630         maxPages += INITIAL_PAGES;
 631     }
 632     /* Allocate a new page */
 633     currentNodePage = nodePages[page] = ALLOC(int,pageSize);
 634     if (currentNodePage == NULL) {
 635         for (i = 0; i < page; i++) FREE(nodePages[i]);
 636         FREE(nodePages);
 637         for (i = 0; i < page; i++) FREE(lightNodePages[i]);
 638         FREE(lightNodePages);
 639         memOut = 1;
 640         return;
 641     }
 642     /* Allocate a new page */
 643     currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
 644     if (currentLightNodePage == NULL) {
 645         for (i = 0; i <= page; i++) FREE(nodePages[i]);
 646         FREE(nodePages);
 647         for (i = 0; i < page; i++) FREE(lightNodePages[i]);
 648         FREE(lightNodePages);
 649         memOut = 1;
 650         return;
 651     }
 652     /* reset page index */
 653     pageIndex = 0;
 654     return;
 655
 656 } /* end of ResizeCountNodePages */
 657
 658
 659 /**Function********************************************************************
 660
 661   Synopsis    [Recursively counts minterms of each node in the DAG.]
 662
 663   Description [Recursively counts minterms of each node in the DAG.
 664   Similar to the cuddCountMintermAux which recursively counts the
 665   number of minterms for the dag rooted at each node in terms of the
 666   total number of variables (max). This procedure creates the node
 667   data structure and stores the minterm count as part of the node
 668   data structure. ]
 669
 670   SideEffects [Creates structures of type node quality and fills the st_table]
 671
 672   SeeAlso     [SubsetCountMinterm]
 673
 674 ******************************************************************************/
 675 static double
 676 SubsetCountMintermAux(
 677   DdNode * node /* function to analyze */,
 678   double  max /* number of minterms of constant 1 */,
 679   st_table * table /* visitedTable table */)
 680 {
 681
 682     DdNode      *N,*Nv,*Nnv; /* nodes to store cofactors  */
 683     double      min,*pmin; /* minterm count */
 684     double      min1, min2; /* minterm count */
 685     NodeData_t *dummy;
 686     NodeData_t *newEntry;
 687     int i;
 688
 689 #ifdef DEBUG
 690     num_calls++;
 691 #endif
 692
 693     /* Constant case */
 694     if (Cudd_IsConstant(node)) {
 695         if (node == zero) {
 696             return(0.0);
 697         } else {
 698             return(max);
 699         }
 700     } else {
 701
 702         /* check if entry for this node exists */
 703         if (st_lookup(table, node, &dummy)) {
 704             min = *(dummy->mintermPointer);
 705             return(min);
 706         }
 707
 708         /* Make the node regular to extract cofactors */
 709         N = Cudd_Regular(node);
 710
 711         /* store the cofactors */
 712         Nv = Cudd_T(N);
 713         Nnv = Cudd_E(N);
 714
 715         Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
 716         Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
 717
 718         min1 =  SubsetCountMintermAux(Nv, max,table)/2.0;
 719         if (memOut) return(0.0);
 720         min2 =  SubsetCountMintermAux(Nnv,max,table)/2.0;
 721         if (memOut) return(0.0);
 722         min = (min1+min2);
 723
 724         /* if page index is at the bottom, then create a new page */
 725         if (pageIndex == pageSize) ResizeCountMintermPages();
 726         if (memOut) {
 727             for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
 728             FREE(nodeDataPages);
 729             st_free_table(table);
 730             return(0.0);
 731         }
 732
 733         /* point to the correct location in the page */
 734         pmin = currentMintermPage+pageIndex;
 735         pageIndex++;
 736
 737         /* store the minterm count of this node in the page */
 738         *pmin = min;
 739
 740         /* Note I allocate the struct here. Freeing taken care of later */
 741         if (nodeDataPageIndex == nodeDataPageSize) ResizeNodeDataPages();
 742         if (memOut) {
 743             for (i = 0; i <= page; i++) FREE(mintermPages[i]);
 744             FREE(mintermPages);
 745             st_free_table(table);
 746             return(0.0);
 747         }
 748
 749         newEntry = currentNodeDataPage + nodeDataPageIndex;
 750         nodeDataPageIndex++;
 751
 752         /* points to the correct location in the page */
 753         newEntry->mintermPointer = pmin;
 754         /* initialize this field of the Node Quality structure */
 755         newEntry->nodesPointer = NULL;
 756
 757         /* insert entry for the node in the table */
 758         if (st_insert(table,(char *)node, (char *)newEntry) == ST_OUT_OF_MEM) {
 759             memOut = 1;
 760             for (i = 0; i <= page; i++) FREE(mintermPages[i]);
 761             FREE(mintermPages);
 762             for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
 763             FREE(nodeDataPages);
 764             st_free_table(table);
 765             return(0.0);
 766         }
 767         return(min);
 768     }
 769
 770 } /* end of SubsetCountMintermAux */
 771
 772
 773 /**Function********************************************************************
 774
 775   Synopsis    [Counts minterms of each node in the DAG]
 776
 777   Description [Counts minterms of each node in the DAG. Similar to the
 778   Cudd_CountMinterm procedure except this returns the minterm count for
 779   all the nodes in the bdd in an st_table.]
 780
 781   SideEffects [none]
 782
 783   SeeAlso     [SubsetCountMintermAux]
 784
 785 ******************************************************************************/
 786 static st_table *
 787 SubsetCountMinterm(
 788   DdNode * node /* function to be analyzed */,
 789   int nvars /* number of variables node depends on */)
 790 {
 791     st_table    *table;
 792     int i;
 793
 794
 795 #ifdef DEBUG
 796     num_calls = 0;
 797 #endif
 798
 799     max = pow(2.0,(double) nvars);
 800     table = st_init_table(st_ptrcmp,st_ptrhash);
 801     if (table == NULL) goto OUT_OF_MEM;
 802     maxPages = INITIAL_PAGES;
 803     mintermPages = ALLOC(double *,maxPages);
 804     if (mintermPages == NULL) {
 805         st_free_table(table);
 806         goto OUT_OF_MEM;
 807     }
 808     page = 0;
 809     currentMintermPage = ALLOC(double,pageSize);
 810     mintermPages[page] = currentMintermPage;
 811     if (currentMintermPage == NULL) {
 812         FREE(mintermPages);
 813         st_free_table(table);
 814         goto OUT_OF_MEM;
 815     }
 816     pageIndex = 0;
 817     maxNodeDataPages = INITIAL_PAGES;
 818     nodeDataPages = ALLOC(NodeData_t *, maxNodeDataPages);
 819     if (nodeDataPages == NULL) {
 820         for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
 821         FREE(mintermPages);
 822         st_free_table(table);
 823         goto OUT_OF_MEM;
 824     }
 825     nodeDataPage = 0;
 826     currentNodeDataPage = ALLOC(NodeData_t ,nodeDataPageSize);
 827     nodeDataPages[nodeDataPage] = currentNodeDataPage;
 828     if (currentNodeDataPage == NULL) {
 829         for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
 830         FREE(mintermPages);
 831         FREE(nodeDataPages);
 832         st_free_table(table);
 833         goto OUT_OF_MEM;
 834     }
 835     nodeDataPageIndex = 0;
 836
 837     (void) SubsetCountMintermAux(node,max,table);
 838     if (memOut) goto OUT_OF_MEM;
 839     return(table);
 840
 841 OUT_OF_MEM:
 842     memOut = 1;
 843     return(NULL);
 844
 845 } /* end of SubsetCountMinterm */
 846
 847
 848 /**Function********************************************************************
 849
 850   Synopsis    [Recursively counts the number of nodes under the dag.
 851   Also counts the number of nodes under the lighter child of
 852   this node.]
 853
 854   Description [Recursively counts the number of nodes under the dag.
 855   Also counts the number of nodes under the lighter child of
 856   this node. . Note that the same dag may be the lighter child of two
 857   different nodes and have different counts. As with the minterm counts,
 858   the node counts are stored in pages to be space efficient and the
 859   address for these node counts are stored in an st_table associated
 860   to each node. ]
 861
 862   SideEffects [Updates the node data table with node counts]
 863
 864   SeeAlso     [SubsetCountNodes]
 865
 866 ******************************************************************************/
 867 static int
 868 SubsetCountNodesAux(
 869   DdNode * node /* current node */,
 870   st_table * table /* table to update node count, also serves as visited table. */,
 871   double  max /* maximum number of variables */)
 872 {
 873     int tval, eval, i;
 874     DdNode *N, *Nv, *Nnv;
 875     double minNv, minNnv;
 876     NodeData_t *dummyN, *dummyNv, *dummyNnv, *dummyNBar;
 877     int *pmin, *pminBar, *val;
 878
 879     if ((node == NULL) || Cudd_IsConstant(node))
 880         return(0);
 881
 882     /* if this node has been processed do nothing */
 883     if (st_lookup(table, node, &dummyN) == 1) {
 884         val = dummyN->nodesPointer;
 885         if (val != NULL)
 886             return(0);
 887     } else {
 888         return(0);
 889     }
 890
 891     N  = Cudd_Regular(node);
 892     Nv = Cudd_T(N);
 893     Nnv = Cudd_E(N);
 894
 895     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
 896     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
 897
 898     /* find the minterm counts for the THEN and ELSE branches */
 899     if (Cudd_IsConstant(Nv)) {
 900         if (Nv == zero) {
 901             minNv = 0.0;
 902         } else {
 903             minNv = max;
 904         }
 905     } else {
 906         if (st_lookup(table, Nv, &dummyNv) == 1)
 907             minNv = *(dummyNv->mintermPointer);
 908         else {
 909             return(0);
 910         }
 911     }
 912     if (Cudd_IsConstant(Nnv)) {
 913         if (Nnv == zero) {
 914             minNnv = 0.0;
 915         } else {
 916             minNnv = max;
 917         }
 918     } else {
 919         if (st_lookup(table, Nnv, &dummyNnv) == 1) {
 920             minNnv = *(dummyNnv->mintermPointer);
 921         }
 922         else {
 923             return(0);
 924         }
 925     }
 926
 927
 928     /* recur based on which has larger minterm, */
 929     if (minNv >= minNnv) {
 930         tval = SubsetCountNodesAux(Nv, table, max);
 931         if (memOut) return(0);
 932         eval = SubsetCountNodesAux(Nnv, table, max);
 933         if (memOut) return(0);
 934
 935         /* store the node count of the lighter child. */
 936         if (pageIndex == pageSize) ResizeCountNodePages();
 937         if (memOut) {
 938             for (i = 0; i <= page; i++) FREE(mintermPages[i]);
 939             FREE(mintermPages);
 940             for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
 941             FREE(nodeDataPages);
 942             st_free_table(table);
 943             return(0);
 944         }
 945         pmin = currentLightNodePage + pageIndex;
 946         *pmin = eval; /* Here the ELSE child is lighter */
 947         dummyN->lightChildNodesPointer = pmin;
 948
 949     } else {
 950         eval = SubsetCountNodesAux(Nnv, table, max);
 951         if (memOut) return(0);
 952         tval = SubsetCountNodesAux(Nv, table, max);
 953         if (memOut) return(0);
 954
 955         /* store the node count of the lighter child. */
 956         if (pageIndex == pageSize) ResizeCountNodePages();
 957         if (memOut) {
 958             for (i = 0; i <= page; i++) FREE(mintermPages[i]);
 959             FREE(mintermPages);
 960             for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
 961             FREE(nodeDataPages);
 962             st_free_table(table);
 963             return(0);
 964         }
 965         pmin = currentLightNodePage + pageIndex;
 966         *pmin = tval; /* Here the THEN child is lighter */
 967         dummyN->lightChildNodesPointer = pmin;
 968
 969     }
 970     /* updating the page index for node count storage. */
 971     pmin = currentNodePage + pageIndex;
 972     *pmin = tval + eval + 1;
 973     dummyN->nodesPointer = pmin;
 974
 975     /* pageIndex is parallel page index for count_nodes and count_lightNodes */
 976     pageIndex++;
 977
 978     /* if this node has been reached first, it belongs to a heavier
 979        branch. Its complement will be reached later on a lighter branch.
 980        Hence the complement has zero node count. */
 981
 982     if (st_lookup(table, Cudd_Not(node), &dummyNBar) == 1)  {
 983         if (pageIndex == pageSize) ResizeCountNodePages();
 984         if (memOut) {
 985             for (i = 0; i < page; i++) FREE(mintermPages[i]);
 986             FREE(mintermPages);
 987             for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
 988             FREE(nodeDataPages);
 989             st_free_table(table);
 990             return(0);
 991         }
 992         pminBar = currentLightNodePage + pageIndex;
 993         *pminBar = 0;
 994         dummyNBar->lightChildNodesPointer = pminBar;
 995         /* The lighter child has less nodes than the parent.
 996          * So if parent 0 then lighter child zero
 997          */
 998         if (pageIndex == pageSize) ResizeCountNodePages();
 999         if (memOut) {
1000             for (i = 0; i < page; i++) FREE(mintermPages[i]);
1001             FREE(mintermPages);
1002             for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
1003             FREE(nodeDataPages);
1004             st_free_table(table);
1005             return(0);
1006         }
1007         pminBar = currentNodePage + pageIndex;
1008         *pminBar = 0;
1009         dummyNBar->nodesPointer = pminBar ; /* maybe should point to zero */
1010
1011         pageIndex++;
1012     }
1013     return(*pmin);
1014 } /*end of SubsetCountNodesAux */
1015
1016
1017 /**Function********************************************************************
1018
1019   Synopsis    [Counts the nodes under the current node and its lighter child]
1020
1021   Description [Counts the nodes under the current node and its lighter
1022   child. Calls a recursive procedure to count the number of nodes of
1023   a DAG rooted at a particular node and the number of nodes taken by its
1024   lighter child.]
1025
1026   SideEffects [None]
1027
1028   SeeAlso     [SubsetCountNodesAux]
1029
1030 ******************************************************************************/
1031 static int
1032 SubsetCountNodes(
1033   DdNode * node /* function to be analyzed */,
1034   st_table * table /* node quality table */,
1035   int  nvars /* number of variables node depends on */)
1036 {
1037     int num;
1038     int i;
1039
1040 #ifdef DEBUG
1041     num_calls = 0;
1042 #endif
1043
1044     max = pow(2.0,(double) nvars);
1045     maxPages = INITIAL_PAGES;
1046     nodePages = ALLOC(int *,maxPages);
1047     if (nodePages == NULL)  {
1048         goto OUT_OF_MEM;
1049     }
1050
1051     lightNodePages = ALLOC(int *,maxPages);
1052     if (lightNodePages == NULL) {
1053         for (i = 0; i <= page; i++) FREE(mintermPages[i]);
1054         FREE(mintermPages);
1055         for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
1056         FREE(nodeDataPages);
1057         FREE(nodePages);
1058         goto OUT_OF_MEM;
1059     }
1060
1061     page = 0;
1062     currentNodePage = nodePages[page] = ALLOC(int,pageSize);
1063     if (currentNodePage == NULL) {
1064         for (i = 0; i <= page; i++) FREE(mintermPages[i]);
1065         FREE(mintermPages);
1066         for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
1067         FREE(nodeDataPages);
1068         FREE(lightNodePages);
1069         FREE(nodePages);
1070         goto OUT_OF_MEM;
1071     }
1072
1073     currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
1074     if (currentLightNodePage == NULL) {
1075         for (i = 0; i <= page; i++) FREE(mintermPages[i]);
1076         FREE(mintermPages);
1077         for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
1078         FREE(nodeDataPages);
1079         FREE(currentNodePage);
1080         FREE(lightNodePages);
1081         FREE(nodePages);
1082         goto OUT_OF_MEM;
1083     }
1084
1085     pageIndex = 0;
1086     num = SubsetCountNodesAux(node,table,max);
1087     if (memOut) goto OUT_OF_MEM;
1088     return(num);
1089
1090 OUT_OF_MEM:
1091     memOut = 1;
1092     return(0);
1093
1094 } /* end of SubsetCountNodes */
1095
1096
1097 /**Function********************************************************************
1098
1099   Synopsis    [Procedure to recursively store nodes that are retained in the subset.]
1100
1101   Description [rocedure to recursively store nodes that are retained in the subset.]
1102
1103   SideEffects [None]
1104
1105   SeeAlso     [StoreNodes]
1106
1107 ******************************************************************************/
1108 static void
1109 StoreNodes(
1110   st_table * storeTable,
1111   DdManager * dd,
1112   DdNode * node)
1113 {
1114     DdNode *N, *Nt, *Ne;
1115     if (Cudd_IsConstant(dd)) {
1116         return;
1117     }
1118     N = Cudd_Regular(node);
1119     if (st_lookup(storeTable, (char *)N, NIL(char *))) {
1120         return;
1121     }
1122     cuddRef(N);
1123     if (st_insert(storeTable, (char *)N, NIL(char)) == ST_OUT_OF_MEM) {
1124         fprintf(dd->err,"Something wrong, st_table insert failed\n");
1125     }
1126
1127     Nt = Cudd_T(N);
1128     Ne = Cudd_E(N);
1129
1130     StoreNodes(storeTable, dd, Nt);
1131     StoreNodes(storeTable, dd, Ne);
1132     return;
1133
1134 }
1135
1136
1137 /**Function********************************************************************
1138
1139   Synopsis    [Builds the subset BDD using the heavy branch method.]
1140
1141   Description [The procedure carries out the building of the subset BDD
1142   starting at the root. Using the three different counts labelling each node,
1143   the procedure chooses the heavier branch starting from the root and keeps
1144   track of the number of nodes it discards at each step, thus keeping count
1145   of the size of the subset BDD dynamically. Once the threshold is satisfied,
1146   the procedure then calls ITE to build the BDD.]
1147
1148   SideEffects [None]
1149
1150   SeeAlso     []
1151
1152 ******************************************************************************/
1153 static DdNode *
1154 BuildSubsetBdd(
1155   DdManager * dd /* DD manager */,
1156   DdNode * node /* current node */,
1157   int * size /* current size of the subset */,
1158   st_table * visitedTable /* visited table storing all node data */,
1159   int  threshold,
1160   st_table * storeTable,
1161   st_table * approxTable)
1162 {
1163
1164     DdNode *Nv, *Nnv, *N, *topv, *neW;
1165     double minNv, minNnv;
1166     NodeData_t *currNodeQual;
1167     NodeData_t *currNodeQualT;
1168     NodeData_t *currNodeQualE;
1169     DdNode *ThenBranch, *ElseBranch;
1170     unsigned int topid;
1171     char *dummy;
1172
1173 #ifdef DEBUG
1174     num_calls++;
1175 #endif
1176     /*If the size of the subset is below the threshold, dont do
1177       anything. */
1178     if ((*size) <= threshold) {
1179       /* store nodes below this, so we can recombine if possible */
1180       StoreNodes(storeTable, dd, node);
1181       return(node);
1182     }
1183
1184     if (Cudd_IsConstant(node))
1185         return(node);
1186
1187     /* Look up minterm count for this node. */
1188     if (!st_lookup(visitedTable, node, &currNodeQual)) {
1189         fprintf(dd->err,
1190                 "Something is wrong, ought to be in node quality table\n");
1191     }
1192
1193     /* Get children. */
1194     N = Cudd_Regular(node);
1195     Nv = Cudd_T(N);
1196     Nnv = Cudd_E(N);
1197
1198     /* complement if necessary */
1199     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1200     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1201
1202     if (!Cudd_IsConstant(Nv)) {
1203         /* find out minterms and nodes contributed by then child */
1204         if (!st_lookup(visitedTable, Nv, &currNodeQualT)) {
1205                 fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
1206                 dd->errorCode = CUDD_INTERNAL_ERROR;
1207                 return(NULL);
1208             }
1209         else {
1210             minNv = *(((NodeData_t *)currNodeQualT)->mintermPointer);
1211         }
1212     } else {
1213         if (Nv == zero) {
1214             minNv = 0;
1215         } else  {
1216             minNv = max;
1217         }
1218     }
1219     if (!Cudd_IsConstant(Nnv)) {
1220         /* find out minterms and nodes contributed by else child */
1221         if (!st_lookup(visitedTable, Nnv, &currNodeQualE)) {
1222             fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
1223             dd->errorCode = CUDD_INTERNAL_ERROR;
1224             return(NULL);
1225         } else {
1226             minNnv = *(((NodeData_t *)currNodeQualE)->mintermPointer);
1227         }
1228     } else {
1229         if (Nnv == zero) {
1230             minNnv = 0;
1231         } else {
1232             minNnv = max;
1233         }
1234     }
1235
1236     /* keep track of size of subset by subtracting the number of
1237      * differential nodes contributed by lighter child
1238      */
1239     *size = (*(size)) - (int)*(currNodeQual->lightChildNodesPointer);
1240     if (minNv >= minNnv) { /*SubsetCountNodesAux procedure takes
1241                              the Then branch in case of a tie */
1242
1243         /* recur with the Then branch */
1244         ThenBranch = (DdNode *)BuildSubsetBdd(dd, Nv, size,
1245               visitedTable, threshold, storeTable, approxTable);
1246         if (ThenBranch == NULL) {
1247             return(NULL);
1248         }
1249         cuddRef(ThenBranch);
1250         /* The Else branch is either a node that already exists in the
1251          * subset, or one whose approximation has been computed, or
1252          * Zero.
1253          */
1254         if (st_lookup(storeTable, (char *)Cudd_Regular(Nnv), &dummy)) {
1255           ElseBranch = Nnv;
1256           cuddRef(ElseBranch);
1257         } else {
1258           if (st_lookup(approxTable, (char *)Nnv, &dummy)) {
1259             ElseBranch = (DdNode *)dummy;
1260             cuddRef(ElseBranch);
1261           } else {
1262             ElseBranch = zero;
1263             cuddRef(ElseBranch);
1264           }
1265         }
1266
1267     }
1268     else {
1269         /* recur with the Else branch */
1270         ElseBranch = (DdNode *)BuildSubsetBdd(dd, Nnv, size,
1271                       visitedTable, threshold, storeTable, approxTable);
1272         if (ElseBranch == NULL) {
1273             return(NULL);
1274         }
1275         cuddRef(ElseBranch);
1276         /* The Then branch is either a node that already exists in the
1277          * subset, or one whose approximation has been computed, or
1278          * Zero.
1279          */
1280         if (st_lookup(storeTable, (char *)Cudd_Regular(Nv), &dummy)) {
1281           ThenBranch = Nv;
1282           cuddRef(ThenBranch);
1283         } else {
1284           if (st_lookup(approxTable, (char *)Nv, &dummy)) {
1285             ThenBranch = (DdNode *)dummy;
1286             cuddRef(ThenBranch);
1287           } else {
1288             ThenBranch = zero;
1289             cuddRef(ThenBranch);
1290           }
1291         }
1292     }
1293
1294     /* construct the Bdd with the top variable and the two children */
1295     topid = Cudd_NodeReadIndex(N);
1296     topv = Cudd_ReadVars(dd, topid);
1297     cuddRef(topv);
1298     neW =  cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
1299     if (neW != NULL) {
1300       cuddRef(neW);
1301     }
1302     Cudd_RecursiveDeref(dd, topv);
1303     Cudd_RecursiveDeref(dd, ThenBranch);
1304     Cudd_RecursiveDeref(dd, ElseBranch);
1305
1306
1307     if (neW == NULL)
1308         return(NULL);
1309     else {
1310         /* store this node in the store table */
1311         if (!st_lookup(storeTable, (char *)Cudd_Regular(neW), &dummy)) {
1312           cuddRef(neW);
1313           if (!st_insert(storeTable, (char *)Cudd_Regular(neW), NIL(char)))
1314               return (NULL);
1315         }
1316         /* store the approximation for this node */
1317         if (N !=  Cudd_Regular(neW)) {
1318             if (st_lookup(approxTable, (char *)node, &dummy)) {
1319                 fprintf(dd->err, "This node should not be in the approximated table\n");
1320             } else {
1321                 cuddRef(neW);
1322                 if (!st_insert(approxTable, (char *)node, (char *)neW))
1323                     return(NULL);
1324             }
1325         }
1326         cuddDeref(neW);
1327         return(neW);
1328     }
1329 } /* end of BuildSubsetBdd */