src/bdd/cudd/cuddSubsetHB.c

Go to the documentation of this file.

#ifdef __STDC__
#include <float.h>
#else
#define DBL_MAX_EXP 1024
#endif
#include "util_hack.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define DEFAULT_PAGE_SIZE 2048
#define DEFAULT_NODE_DATA_PAGE_SIZE 1024
#define INITIAL_PAGES 128


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/* data structure to store the information on each node. It keeps
 * the number of minterms represented by the DAG rooted at this node
 * in terms of the number of variables specified by the user, number
 * of nodes in this DAG and the number of nodes of its child with
 * lesser number of minterms that are not shared by the child with
 * more minterms
 */
struct NodeData {
    double *mintermPointer;
    int *nodesPointer;
    int *lightChildNodesPointer;
};

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct NodeData NodeData_t;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddSubsetHB.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
#endif

static int memOut;
#ifdef DEBUG
static  int             num_calls;
#endif

static  DdNode          *zero, *one; /* constant functions */
static  double          **mintermPages; /* pointers to the pages */
static  int             **nodePages; /* pointers to the pages */
static  int             **lightNodePages; /* pointers to the pages */
static  double          *currentMintermPage; /* pointer to the current
                                                   page */
static  double          max; /* to store the 2^n value of the number
                              * of variables */

static  int             *currentNodePage; /* pointer to the current
                                                   page */
static  int             *currentLightNodePage; /* pointer to the
                                                *  current page */
static  int             pageIndex; /* index to next element */
static  int             page; /* index to current page */
static  int             pageSize = DEFAULT_PAGE_SIZE; /* page size */
static  int             maxPages; /* number of page pointers */

static  NodeData_t      *currentNodeDataPage; /* pointer to the current
                                                 page */
static  int             nodeDataPage; /* index to next element */
static  int             nodeDataPageIndex; /* index to next element */
static  NodeData_t      **nodeDataPages; /* index to current page */
static  int             nodeDataPageSize = DEFAULT_NODE_DATA_PAGE_SIZE;
                                                     /* page size */
static  int             maxNodeDataPages; /* number of page pointers */


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void ResizeNodeDataPages ARGS(());
static void ResizeCountMintermPages ARGS(());
static void ResizeCountNodePages ARGS(());
static double SubsetCountMintermAux ARGS((DdNode *node, double max, st_table *table));
static st_table * SubsetCountMinterm ARGS((DdNode *node, int nvars));
static int SubsetCountNodesAux ARGS((DdNode *node, st_table *table, double max));
static int SubsetCountNodes ARGS((DdNode *node, st_table *table, int nvars));
static void StoreNodes ARGS((st_table *storeTable, DdManager *dd, DdNode *node));
static DdNode * BuildSubsetBdd ARGS((DdManager *dd, DdNode *node, int *size, st_table *visitedTable, int threshold, st_table *storeTable, st_table *approxTable));

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

DdNode *
Cudd_SubsetHeavyBranch(
  DdManager * dd /* manager */,
  DdNode * f /* function to be subset */,
  int  numVars /* number of variables in the support of f */,
  int  threshold /* maximum number of nodes in the subset */)
{
    DdNode *subset;

    memOut = 0;
    do {
        dd->reordered = 0;
        subset = cuddSubsetHeavyBranch(dd, f, numVars, threshold);
    } while ((dd->reordered == 1) && (!memOut));

    return(subset);

} /* end of Cudd_SubsetHeavyBranch */


DdNode *
Cudd_SupersetHeavyBranch(
  DdManager * dd /* manager */,
  DdNode * f /* function to be superset */,
  int  numVars /* number of variables in the support of f */,
  int  threshold /* maximum number of nodes in the superset */)
{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    memOut = 0;
    do {
        dd->reordered = 0;
        subset = cuddSubsetHeavyBranch(dd, g, numVars, threshold);
    } while ((dd->reordered == 1) && (!memOut));
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_SupersetHeavyBranch */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


DdNode *
cuddSubsetHeavyBranch(
  DdManager * dd /* DD manager */,
  DdNode * f /* current DD */,
  int  numVars /* maximum number of variables */,
  int  threshold /* threshold size for the subset */)
{

    int i, *size;
    st_table *visitedTable;
    int numNodes;
    NodeData_t *currNodeQual;
    DdNode *subset;
    double minN;
    st_table *storeTable, *approxTable;
    char *key, *value;
    st_generator *stGen;
    
    if (f == NULL) {
        fprintf(dd->err, "Cannot subset, nil object\n");
        dd->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

    one  = Cudd_ReadOne(dd);
    zero = Cudd_Not(one);

    /* If user does not know numVars value, set it to the maximum
     * exponent that the pow function can take. The -1 is due to the
     * discrepancy in the value that pow takes and the value that
     * log gives.
     */
    if (numVars == 0) {
        /* set default value */
        numVars = DBL_MAX_EXP - 1;
    }

    if (Cudd_IsConstant(f)) {
        return(f);
    }

    max = pow(2.0, (double)numVars);

    /* Create visited table where structures for node data are allocated and
       stored in a st_table */
    visitedTable = SubsetCountMinterm(f, numVars);
    if ((visitedTable == NULL) || memOut) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    numNodes = SubsetCountNodes(f, visitedTable, numVars);
    if (memOut) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }

    if (st_lookup(visitedTable, (char *)f, (char **)&currNodeQual)) {
        minN = *(((NodeData_t *)currNodeQual)->mintermPointer);
    } else {
        fprintf(dd->err,
                "Something is wrong, ought to be node quality table\n");
        dd->errorCode = CUDD_INTERNAL_ERROR;
    }

    size = ALLOC(int, 1);
    if (size == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    *size = numNodes;

#ifdef DEBUG
    num_calls = 0;
#endif
    /* table to store nodes being created. */
    storeTable = st_init_table(st_ptrcmp, st_ptrhash);
    /* insert the constant */
    cuddRef(one);
    if (st_insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
        ST_OUT_OF_MEM) {
        fprintf(dd->out, "Something wrong, st_table insert failed\n");
    }
    /* table to store approximations of nodes */
    approxTable = st_init_table(st_ptrcmp, st_ptrhash);
    subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
                                      storeTable, approxTable);
    if (subset != NULL) {
        cuddRef(subset);
    }

    stGen = st_init_gen(approxTable);
    if (stGen == NULL) {
        st_free_table(approxTable);
        return(NULL);
    }
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
        Cudd_RecursiveDeref(dd, (DdNode *)value);
    }
    st_free_gen(stGen); stGen = NULL;
    st_free_table(approxTable);

    stGen = st_init_gen(storeTable);
    if (stGen == NULL) {
        st_free_table(storeTable);
        return(NULL);
    }
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
        Cudd_RecursiveDeref(dd, (DdNode *)key);
    }
    st_free_gen(stGen); stGen = NULL;
    st_free_table(storeTable);

    for (i = 0; i <= page; i++) {
        FREE(mintermPages[i]);
    }
    FREE(mintermPages);
    for (i = 0; i <= page; i++) {
        FREE(nodePages[i]);
    }
    FREE(nodePages);
    for (i = 0; i <= page; i++) {
        FREE(lightNodePages[i]);
    }
    FREE(lightNodePages);
    for (i = 0; i <= nodeDataPage; i++) {
        FREE(nodeDataPages[i]);
    }
    FREE(nodeDataPages);
    st_free_table(visitedTable);
    FREE(size);
#if 0
    (void) Cudd_DebugCheck(dd);
    (void) Cudd_CheckKeys(dd);
#endif

    if (subset != NULL) {
#ifdef DD_DEBUG
      if (!Cudd_bddLeq(dd, subset, f)) {
            fprintf(dd->err, "Wrong subset\n");
            dd->errorCode = CUDD_INTERNAL_ERROR;
            return(NULL);
      }
#endif
        cuddDeref(subset);
        return(subset);
    } else {
        return(NULL);
    }
} /* end of cuddSubsetHeavyBranch */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static void
ResizeNodeDataPages(
   )
{
    int i;
    NodeData_t **newNodeDataPages;

    nodeDataPage++;
    /* If the current page index is larger than the number of pages
     * allocated, allocate a new page array. Page numbers are incremented by
     * INITIAL_PAGES
     */
    if (nodeDataPage == maxNodeDataPages) {
        newNodeDataPages = ALLOC(NodeData_t *,maxNodeDataPages + INITIAL_PAGES);
        if (newNodeDataPages == NULL) {
            for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            memOut = 1;
            return;
        } else {
            for (i = 0; i < maxNodeDataPages; i++) {
                newNodeDataPages[i] = nodeDataPages[i];
            }
            /* Increase total page count */
            maxNodeDataPages += INITIAL_PAGES;
            FREE(nodeDataPages);
            nodeDataPages = newNodeDataPages;
        }
    }
    /* Allocate a new page */
    currentNodeDataPage = nodeDataPages[nodeDataPage] =
        ALLOC(NodeData_t ,nodeDataPageSize);
    if (currentNodeDataPage == NULL) {
        for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
        FREE(nodeDataPages);
        memOut = 1;
        return;
    }
    /* reset page index */
    nodeDataPageIndex = 0;
    return;

} /* end of ResizeNodeDataPages */


static void
ResizeCountMintermPages(
   )
{
    int i;
    double **newMintermPages;

    page++;
    /* If the current page index is larger than the number of pages
     * allocated, allocate a new page array. Page numbers are incremented by
     * INITIAL_PAGES
     */
    if (page == maxPages) {
        newMintermPages = ALLOC(double *,maxPages + INITIAL_PAGES);
        if (newMintermPages == NULL) {
            for (i = 0; i < page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            memOut = 1;
            return;
        } else {
            for (i = 0; i < maxPages; i++) {
                newMintermPages[i] = mintermPages[i];
            }
            /* Increase total page count */
            maxPages += INITIAL_PAGES;
            FREE(mintermPages);
            mintermPages = newMintermPages;
        }
    }
    /* Allocate a new page */
    currentMintermPage = mintermPages[page] = ALLOC(double,pageSize);
    if (currentMintermPage == NULL) {
        for (i = 0; i < page; i++) FREE(mintermPages[i]);
        FREE(mintermPages);
        memOut = 1;
        return;
    }
    /* reset page index */
    pageIndex = 0;
    return;

} /* end of ResizeCountMintermPages */


static void
ResizeCountNodePages(
   )
{
    int i;
    int **newNodePages;

    page++;

    /* If the current page index is larger than the number of pages
     * allocated, allocate a new page array. The number of pages is incremented
     * by INITIAL_PAGES.
     */
    if (page == maxPages) {
        newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
        if (newNodePages == NULL) {
            for (i = 0; i < page; i++) FREE(nodePages[i]);
            FREE(nodePages);
            for (i = 0; i < page; i++) FREE(lightNodePages[i]);
            FREE(lightNodePages);
            memOut = 1;
            return;
        } else {
            for (i = 0; i < maxPages; i++) {
                newNodePages[i] = nodePages[i];
            }
            FREE(nodePages);
            nodePages = newNodePages;
        }

        newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
        if (newNodePages == NULL) {
            for (i = 0; i < page; i++) FREE(nodePages[i]);
            FREE(nodePages);
            for (i = 0; i < page; i++) FREE(lightNodePages[i]);
            FREE(lightNodePages);
            memOut = 1;
            return;
        } else {
            for (i = 0; i < maxPages; i++) {
                newNodePages[i] = lightNodePages[i];
            }
            FREE(lightNodePages);
            lightNodePages = newNodePages;
        }
        /* Increase total page count */
        maxPages += INITIAL_PAGES;
    }
    /* Allocate a new page */
    currentNodePage = nodePages[page] = ALLOC(int,pageSize);
    if (currentNodePage == NULL) {
        for (i = 0; i < page; i++) FREE(nodePages[i]);
        FREE(nodePages);
        for (i = 0; i < page; i++) FREE(lightNodePages[i]);
        FREE(lightNodePages);
        memOut = 1;
        return;
    }
    /* Allocate a new page */
    currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
    if (currentLightNodePage == NULL) {
        for (i = 0; i <= page; i++) FREE(nodePages[i]);
        FREE(nodePages);
        for (i = 0; i < page; i++) FREE(lightNodePages[i]);
        FREE(lightNodePages);
        memOut = 1;
        return;
    }
    /* reset page index */
    pageIndex = 0;
    return;

} /* end of ResizeCountNodePages */


static double
SubsetCountMintermAux(
  DdNode * node /* function to analyze */,
  double  max /* number of minterms of constant 1 */,
  st_table * table /* visitedTable table */)
{

    DdNode      *N,*Nv,*Nnv; /* nodes to store cofactors  */
    double      min,*pmin; /* minterm count */
    double      min1, min2; /* minterm count */
    NodeData_t *dummy;
    NodeData_t *newEntry;
    int i;

#ifdef DEBUG
    num_calls++;
#endif

    /* Constant case */
    if (Cudd_IsConstant(node)) {
        if (node == zero) {
            return(0.0);
        } else {
            return(max);
        }
    } else {

        /* check if entry for this node exists */
        if (st_lookup(table,(char *)node, (char **)&dummy)) {
            min = *(dummy->mintermPointer);
            return(min);
        }

        /* Make the node regular to extract cofactors */
        N = Cudd_Regular(node);

        /* store the cofactors */
        Nv = Cudd_T(N);
        Nnv = Cudd_E(N);
        
        Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
        Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

        min1 =  SubsetCountMintermAux(Nv, max,table)/2.0;
        if (memOut) return(0.0);
        min2 =  SubsetCountMintermAux(Nnv,max,table)/2.0;
        if (memOut) return(0.0);
        min = (min1+min2);

        /* if page index is at the bottom, then create a new page */
        if (pageIndex == pageSize) ResizeCountMintermPages();
        if (memOut) {
            for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            st_free_table(table);
            return(0.0);
        }

        /* point to the correct location in the page */
        pmin = currentMintermPage+pageIndex;
        pageIndex++;

        /* store the minterm count of this node in the page */
        *pmin = min;

        /* Note I allocate the struct here. Freeing taken care of later */
        if (nodeDataPageIndex == nodeDataPageSize) ResizeNodeDataPages();
        if (memOut) {
            for (i = 0; i <= page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            st_free_table(table);
            return(0.0);
        }

        newEntry = currentNodeDataPage + nodeDataPageIndex;
        nodeDataPageIndex++;

        /* points to the correct location in the page */
        newEntry->mintermPointer = pmin;
        /* initialize this field of the Node Quality structure */
        newEntry->nodesPointer = NULL;

        /* insert entry for the node in the table */
        if (st_insert(table,(char *)node, (char *)newEntry) == ST_OUT_OF_MEM) {
            memOut = 1;
            for (i = 0; i <= page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            st_free_table(table);
            return(0.0);
        }
        return(min);
    }

} /* end of SubsetCountMintermAux */


static st_table *
SubsetCountMinterm(
  DdNode * node /* function to be analyzed */,
  int nvars /* number of variables node depends on */)
{
    st_table    *table;
    double      num;
    int i;


#ifdef DEBUG
    num_calls = 0;
#endif

    max = pow(2.0,(double) nvars);
    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) goto OUT_OF_MEM;
    maxPages = INITIAL_PAGES;
    mintermPages = ALLOC(double *,maxPages);
    if (mintermPages == NULL) {
        st_free_table(table);
        goto OUT_OF_MEM;
    }
    page = 0;
    currentMintermPage = ALLOC(double,pageSize);
    mintermPages[page] = currentMintermPage;
    if (currentMintermPage == NULL) {
        FREE(mintermPages);
        st_free_table(table);
        goto OUT_OF_MEM;
    }
    pageIndex = 0;
    maxNodeDataPages = INITIAL_PAGES;
    nodeDataPages = ALLOC(NodeData_t *, maxNodeDataPages);
    if (nodeDataPages == NULL) {
        for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
        FREE(mintermPages);
        st_free_table(table);
        goto OUT_OF_MEM;
    }
    nodeDataPage = 0;
    currentNodeDataPage = ALLOC(NodeData_t ,nodeDataPageSize);
    nodeDataPages[nodeDataPage] = currentNodeDataPage;
    if (currentNodeDataPage == NULL) {
        for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
        FREE(mintermPages);
        FREE(nodeDataPages);
        st_free_table(table);
        goto OUT_OF_MEM;
    }
    nodeDataPageIndex = 0;

    num = SubsetCountMintermAux(node,max,table);
    if (memOut) goto OUT_OF_MEM;
    return(table);

OUT_OF_MEM:
    memOut = 1;
    return(NULL);

} /* end of SubsetCountMinterm */


static int
SubsetCountNodesAux(
  DdNode * node /* current node */,
  st_table * table /* table to update node count, also serves as visited table. */,
  double  max /* maximum number of variables */)
{
    int tval, eval, i;
    DdNode *N, *Nv, *Nnv;
    double minNv, minNnv;
    NodeData_t *dummyN, *dummyNv, *dummyNnv, *dummyNBar;
    int *pmin, *pminBar, *val;

    if ((node == NULL) || Cudd_IsConstant(node))
        return(0);

    /* if this node has been processed do nothing */
    if (st_lookup(table, (char *)node, (char **)&dummyN) == 1) {
        val = dummyN->nodesPointer;
        if (val != NULL)
            return(0);
    } else {
        return(0);
    }

    N  = Cudd_Regular(node);
    Nv = Cudd_T(N);
    Nnv = Cudd_E(N);
    
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

    /* find the minterm counts for the THEN and ELSE branches */
    if (Cudd_IsConstant(Nv)) {
        if (Nv == zero) {
            minNv = 0.0;
        } else {
            minNv = max;
        }
    } else {
        if (st_lookup(table, (char *)Nv, (char **)&dummyNv) == 1)
            minNv = *(dummyNv->mintermPointer);
        else {
            return(0);
        }
    }
    if (Cudd_IsConstant(Nnv)) {
        if (Nnv == zero) {
            minNnv = 0.0;
        } else {
            minNnv = max;
        }
    } else {
        if (st_lookup(table, (char *)Nnv, (char **)&dummyNnv) == 1) {
            minNnv = *(dummyNnv->mintermPointer);
        }
        else {
            return(0);
        }
    }


    /* recur based on which has larger minterm, */
    if (minNv >= minNnv) {
        tval = SubsetCountNodesAux(Nv, table, max);
        if (memOut) return(0);
        eval = SubsetCountNodesAux(Nnv, table, max);
        if (memOut) return(0);

        /* store the node count of the lighter child. */
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i <= page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            st_free_table(table);
            return(0);
        }
        pmin = currentLightNodePage + pageIndex;
        *pmin = eval; /* Here the ELSE child is lighter */
        dummyN->lightChildNodesPointer = pmin;

    } else {
        eval = SubsetCountNodesAux(Nnv, table, max);
        if (memOut) return(0);
        tval = SubsetCountNodesAux(Nv, table, max);
        if (memOut) return(0);

        /* store the node count of the lighter child. */
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i <= page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            st_free_table(table);
            return(0);
        }
        pmin = currentLightNodePage + pageIndex;
        *pmin = tval; /* Here the THEN child is lighter */
        dummyN->lightChildNodesPointer = pmin;

    }
    /* updating the page index for node count storage. */
    pmin = currentNodePage + pageIndex;
    *pmin = tval + eval + 1;
    dummyN->nodesPointer = pmin;

    /* pageIndex is parallel page index for count_nodes and count_lightNodes */
    pageIndex++;

    /* if this node has been reached first, it belongs to a heavier
       branch. Its complement will be reached later on a lighter branch.
       Hence the complement has zero node count. */

    if (st_lookup(table, (char *)Cudd_Not(node), (char **)&dummyNBar) == 1)  {
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i < page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            st_free_table(table);
            return(0);
        }
        pminBar = currentLightNodePage + pageIndex;
        *pminBar = 0;
        dummyNBar->lightChildNodesPointer = pminBar;
        /* The lighter child has less nodes than the parent.
         * So if parent 0 then lighter child zero
         */
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i < page; i++) FREE(mintermPages[i]);
            FREE(mintermPages);
            for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
            FREE(nodeDataPages);
            st_free_table(table);
            return(0);
        }
        pminBar = currentNodePage + pageIndex;
        *pminBar = 0;
        dummyNBar->nodesPointer = pminBar ; /* maybe should point to zero */

        pageIndex++;
    }
    return(*pmin);
} /*end of SubsetCountNodesAux */


static int
SubsetCountNodes(
  DdNode * node /* function to be analyzed */,
  st_table * table /* node quality table */,
  int  nvars /* number of variables node depends on */)
{
    int num;
    int i;

#ifdef DEBUG
    num_calls = 0;
#endif

    max = pow(2.0,(double) nvars);
    maxPages = INITIAL_PAGES;
    nodePages = ALLOC(int *,maxPages);
    if (nodePages == NULL)  {
        goto OUT_OF_MEM;
    }

    lightNodePages = ALLOC(int *,maxPages);
    if (lightNodePages == NULL) {
        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
        FREE(mintermPages);
        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
        FREE(nodeDataPages);
        FREE(nodePages);
        goto OUT_OF_MEM;
    }

    page = 0;
    currentNodePage = nodePages[page] = ALLOC(int,pageSize);
    if (currentNodePage == NULL) {
        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
        FREE(mintermPages);
        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
        FREE(nodeDataPages);
        FREE(lightNodePages);
        FREE(nodePages);
        goto OUT_OF_MEM;
    }

    currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
    if (currentLightNodePage == NULL) {
        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
        FREE(mintermPages);
        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
        FREE(nodeDataPages);
        FREE(currentNodePage);
        FREE(lightNodePages);
        FREE(nodePages);
        goto OUT_OF_MEM;
    }

    pageIndex = 0;
    num = SubsetCountNodesAux(node,table,max);
    if (memOut) goto OUT_OF_MEM;
    return(num);

OUT_OF_MEM:
    memOut = 1;
    return(0);

} /* end of SubsetCountNodes */


static void
StoreNodes(
  st_table * storeTable,
  DdManager * dd,
  DdNode * node)
{
    char *dummy;
    DdNode *N, *Nt, *Ne;
    if (Cudd_IsConstant(dd)) {
        return;
    }
    N = Cudd_Regular(node);
    if (st_lookup(storeTable, (char *)N, (char **)&dummy)) {
        return;
    }
    cuddRef(N);
    if (st_insert(storeTable, (char *)N, NIL(char)) == ST_OUT_OF_MEM) {
        fprintf(dd->err,"Something wrong, st_table insert failed\n");
    }

    Nt = Cudd_T(N);
    Ne = Cudd_E(N);

    StoreNodes(storeTable, dd, Nt);
    StoreNodes(storeTable, dd, Ne);
    return;

}


static DdNode *
BuildSubsetBdd(
  DdManager * dd /* DD manager */,
  DdNode * node /* current node */,
  int * size /* current size of the subset */,
  st_table * visitedTable /* visited table storing all node data */,
  int  threshold,
  st_table * storeTable,
  st_table * approxTable)
{

    DdNode *Nv, *Nnv, *N, *topv, *neW;
    double minNv, minNnv;
    NodeData_t *currNodeQual;
    NodeData_t *currNodeQualT;
    NodeData_t *currNodeQualE;
    DdNode *ThenBranch, *ElseBranch;
    unsigned int topid;
    char *dummy;

#ifdef DEBUG
    num_calls++;
#endif
    /*If the size of the subset is below the threshold, dont do
      anything. */
    if ((*size) <= threshold) {
      /* store nodes below this, so we can recombine if possible */
      StoreNodes(storeTable, dd, node);
      return(node);
    }

    if (Cudd_IsConstant(node))
        return(node);

    /* Look up minterm count for this node. */
    if (!st_lookup(visitedTable, (char *)node, (char **)&currNodeQual)) {
        fprintf(dd->err,
                "Something is wrong, ought to be in node quality table\n");
    }

    /* Get children. */
    N = Cudd_Regular(node);
    Nv = Cudd_T(N);
    Nnv = Cudd_E(N);

    /* complement if necessary */
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

    if (!Cudd_IsConstant(Nv)) {
        /* find out minterms and nodes contributed by then child */
        if (!st_lookup(visitedTable, (char *)Nv,
                       (char **)&currNodeQualT)) {
                fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
                dd->errorCode = CUDD_INTERNAL_ERROR;
                return(NULL);
            }
        else {
            minNv = *(((NodeData_t *)currNodeQualT)->mintermPointer);
        }
    } else {
        if (Nv == zero) {
            minNv = 0;
        } else  {
            minNv = max;
        }
    }
    if (!Cudd_IsConstant(Nnv)) {
        /* find out minterms and nodes contributed by else child */
        if (!st_lookup(visitedTable, (char *)Nnv, (char **)&currNodeQualE)) {
            fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
            dd->errorCode = CUDD_INTERNAL_ERROR;
            return(NULL);
        } else {
            minNnv = *(((NodeData_t *)currNodeQualE)->mintermPointer);
        }
    } else {
        if (Nnv == zero) {
            minNnv = 0;
        } else {
            minNnv = max;
        }
    }

    /* keep track of size of subset by subtracting the number of
     * differential nodes contributed by lighter child
     */
    *size = (*(size)) - (int)*(currNodeQual->lightChildNodesPointer);
    if (minNv >= minNnv) { /*SubsetCountNodesAux procedure takes
                             the Then branch in case of a tie */

        /* recur with the Then branch */
        ThenBranch = (DdNode *)BuildSubsetBdd(dd, Nv, size,
              visitedTable, threshold, storeTable, approxTable);
        if (ThenBranch == NULL) {
            return(NULL);
        }
        cuddRef(ThenBranch);
        /* The Else branch is either a node that already exists in the
         * subset, or one whose approximation has been computed, or
         * Zero.
         */
        if (st_lookup(storeTable, (char *)Cudd_Regular(Nnv), (char **)&dummy)) {
          ElseBranch = Nnv;
          cuddRef(ElseBranch);
        } else {
          if (st_lookup(approxTable, (char *)Nnv, (char **)&dummy)) {
            ElseBranch = (DdNode *)dummy;
            cuddRef(ElseBranch);
          } else {
            ElseBranch = zero;
            cuddRef(ElseBranch);
          }
        }
        
    }
    else {
        /* recur with the Else branch */
        ElseBranch = (DdNode *)BuildSubsetBdd(dd, Nnv, size,
                      visitedTable, threshold, storeTable, approxTable);
        if (ElseBranch == NULL) {
            return(NULL);
        }
        cuddRef(ElseBranch);
        /* The Then branch is either a node that already exists in the
         * subset, or one whose approximation has been computed, or
         * Zero.
         */
        if (st_lookup(storeTable, (char *)Cudd_Regular(Nv), (char **)&dummy)) {
          ThenBranch = Nv;
          cuddRef(ThenBranch);
        } else {
          if (st_lookup(approxTable, (char *)Nv, (char **)&dummy)) {
            ThenBranch = (DdNode *)dummy;
            cuddRef(ThenBranch);
          } else {
            ThenBranch = zero;
            cuddRef(ThenBranch);
          }
        }
    }

    /* construct the Bdd with the top variable and the two children */
    topid = Cudd_NodeReadIndex(N);
    topv = Cudd_ReadVars(dd, topid);
    cuddRef(topv);
    neW =  cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
    if (neW != NULL) {
      cuddRef(neW);
    }
    Cudd_RecursiveDeref(dd, topv);
    Cudd_RecursiveDeref(dd, ThenBranch);
    Cudd_RecursiveDeref(dd, ElseBranch);

      
    if (neW == NULL)
        return(NULL);
    else {
        /* store this node in the store table */
        if (!st_lookup(storeTable, (char *)Cudd_Regular(neW), (char **)&dummy)) {
          cuddRef(neW);
          st_insert(storeTable, (char *)Cudd_Regular(neW), (char *)NIL(char));
          
        }
        /* store the approximation for this node */
        if (N !=  Cudd_Regular(neW)) {
            if (st_lookup(approxTable, (char *)node, (char **)&dummy)) {
                fprintf(dd->err, "This node should not be in the approximated table\n");
            } else {
                cuddRef(neW);
                st_insert(approxTable, (char *)node, (char *)neW);
            }
        }
        cuddDeref(neW);
        return(neW);
    }
} /* end of BuildSubsetBdd */

---