src/bdd/cudd/cuddApprox.c File Reference

#include "util_hack.h"
#include "cuddInt.h"

Include dependency graph for cuddApprox.c:

Go to the source code of this file.

Data Structures
struct	NodeData
struct	ApproxInfo
struct	GlobalQueueItem
struct	LocalQueueItem
Defines
#define	DBL_MAX_EXP   1024
#define	NOTHING   0
#define	REPLACE_T   1
#define	REPLACE_E   2
#define	REPLACE_N   3
#define	REPLACE_TT   4
#define	REPLACE_TE   5
#define	DONT_CARE   0
#define	CARE   1
#define	TOTAL_CARE   2
#define	CARE_ERROR   3
Functions
static void updateParity	ARGS ((DdNode *node, ApproxInfo *info, int newparity))
static NodeData *gatherInfoAux	ARGS ((DdNode *node, ApproxInfo *info, int parity))
static ApproxInfo *gatherInfo	ARGS ((DdManager *dd, DdNode *node, int numVars, int parity))
static int computeSavings	ARGS ((DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue))
static int UAmarkNodes	ARGS ((DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality))
static DdNode *UAbuildSubset	ARGS ((DdManager *dd, DdNode *node, ApproxInfo *info))
static int RAmarkNodes	ARGS ((DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality))
static int BAmarkNodes	ARGS ((DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0))
static int BAapplyBias	ARGS ((DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache))
DdNode *	Cudd_UnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
DdNode *	Cudd_OverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
DdNode *	Cudd_RemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
DdNode *	Cudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
DdNode *	Cudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
DdNode *	Cudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
DdNode *	cuddUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
DdNode *	cuddRemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
DdNode *	cuddBiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
static void	updateParity (DdNode *node, ApproxInfo *info, int newparity)
static NodeData *	gatherInfoAux (DdNode *node, ApproxInfo *info, int parity)
static ApproxInfo *	gatherInfo (DdManager *dd, DdNode *node, int numVars, int parity)
static int	computeSavings (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
static int	updateRefs (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
static int	UAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality)
static DdNode *	UAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info)
static int	RAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality)
static int	BAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0)
static DdNode *	RAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info)
static int	BAapplyBias (DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddApprox.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"

---

Define Documentation

#define CARE   1

Definition at line 69 of file cuddApprox.c.

#define CARE_ERROR   3

Definition at line 71 of file cuddApprox.c.

#define DBL_MAX_EXP   1024

CFile***********************************************************************

FileName [cuddApprox.c]

PackageName [cudd]

Synopsis [Procedures to approximate a given BDD.]

Description [External procedures provided by this module:

• Cudd_UnderApprox()
• Cudd_OverApprox()
• Cudd_RemapUnderApprox()
• Cudd_RemapOverApprox()
• Cudd_BiasedUnderApprox()
• Cudd_BiasedOverApprox()

Internal procedures included in this module:

• cuddUnderApprox()
• cuddRemapUnderApprox()
• cuddBiasedUnderApprox()

Static procedures included in this module:

• gatherInfoAux()
• gatherInfo()
• computeSavings()
• UAmarkNodes()
• UAbuildSubset()
• updateRefs()
• RAmarkNodes()
• BAmarkNodes()
• RAbuildSubset()

]

SeeAlso [cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 52 of file cuddApprox.c.

#define DONT_CARE   0

Definition at line 68 of file cuddApprox.c.

#define NOTHING   0

Definition at line 61 of file cuddApprox.c.

#define REPLACE_E   2

Definition at line 63 of file cuddApprox.c.

#define REPLACE_N   3

Definition at line 64 of file cuddApprox.c.

#define REPLACE_T   1

Definition at line 62 of file cuddApprox.c.

#define REPLACE_TE   5

Definition at line 66 of file cuddApprox.c.

#define REPLACE_TT   4

Definition at line 65 of file cuddApprox.c.

#define TOTAL_CARE   2

Definition at line 70 of file cuddApprox.c.

---

Function Documentation

static int BAapplyBias ARGS

(

(DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)

)

[static]

static int BAmarkNodes ARGS

(

(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0)

)

[static]

static int RAmarkNodes ARGS

(

(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality)

)

[static]

static DdNode *RAbuildSubset ARGS

(

(DdManager *dd, DdNode *node, ApproxInfo *info)

)

[static]

static int UAmarkNodes ARGS

(

(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality)

)

[static]

static int updateRefs ARGS

(

(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)

)

[static]

static ApproxInfo* gatherInfo ARGS

(

(DdManager *dd, DdNode *node, int numVars, int parity)

)

[static]

static NodeData* gatherInfoAux ARGS

(

(DdNode *node, ApproxInfo *info, int parity)

)

[static]

static void updateParity ARGS

(

(DdNode *node, ApproxInfo *info, int newparity)

)

[static]

AutomaticStart

static int BAapplyBias	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		ApproxInfo *	info,
		DdHashTable *	cache
	)			[static]

Function********************************************************************

Synopsis [Finds don't care nodes.]

Description [Finds don't care nodes by traversing f and b in parallel. Returns the care status of the visited f node if successful; CARE_ERROR otherwise.]

SideEffects [None]

SeeAlso [cuddBiasedUnderApprox]

Definition at line 2121 of file cuddApprox.c.

{
    DdNode *one, *zero, *res;
    DdNode *Ft, *Fe, *B, *Bt, *Be;
    unsigned int topf, topb;
    NodeData *infoF;
    int careT, careE;

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

    if (!st_lookup(info->table, (char *) f, (char **)&infoF))
        return(CARE_ERROR);
    if (f == one) return(TOTAL_CARE);
    if (b == zero) return(infoF->care);
    if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);

    if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
        (res = cuddHashTableLookup2(cache,f,b)) != NULL) {
        if (res->ref == 0) {
            cache->manager->dead++;
            cache->manager->constants.dead++;
        }
        return(infoF->care);
    }

    topf = dd->perm[f->index];
    B = Cudd_Regular(b);
    topb = cuddI(dd,B->index);
    if (topf <= topb) {
        Ft = cuddT(f); Fe = cuddE(f);
    } else {
        Ft = Fe = f;
    }
    if (topb <= topf) {
        /* We know that b is not constant because f is not. */
        Bt = cuddT(B); Be = cuddE(B);
        if (Cudd_IsComplement(b)) {
            Bt = Cudd_Not(Bt);
            Be = Cudd_Not(Be);
        }
    } else {
        Bt = Be = b;
    }

    careT = BAapplyBias(dd, Ft, Bt, info, cache);
    if (careT == CARE_ERROR)
        return(CARE_ERROR);
    careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
    if (careE == CARE_ERROR)
        return(CARE_ERROR);
    if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
        infoF->care = TOTAL_CARE;
    } else {
        infoF->care = CARE;
    }

    if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
        ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
            return(CARE_ERROR);
        }
    }
    return(infoF->care);

} /* end of BAapplyBias */

static int BAmarkNodes	(	DdManager *	dd,
		DdNode *	f,
		ApproxInfo *	info,
		int	threshold,
		double	quality1,
		double	quality0
	)			[static]

Function********************************************************************

Synopsis [Marks nodes for remapping.]

Description [Marks nodes for remapping. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddRemapUnderApprox]

Definition at line 1655 of file cuddApprox.c.

{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN, *infoT, *infoE;
    GlobalQueueItem *item;
    DdNode *node, *T, *E;
    DdNode *shared; /* grandchild shared by the two children of node */
    double numOnset;
    double impact, impactP, impactN;
    double minterms;
    double quality;
    int savings;
    int replace;

#if 0
    (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
                  info->size, info->minterms);
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
        return(0);
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
                                    dd->initSlots);
    if (localQueue == NULL) {
        cuddLevelQueueQuit(queue);
        return(0);
    }
    /* Enqueue regular pointer to root and initialize impact. */
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *)
        cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL) {
        cuddLevelQueueQuit(queue);
        cuddLevelQueueQuit(localQueue);
        return(0);
    }
    if (Cudd_IsComplement(f)) {
        item->impactP = 0.0;
        item->impactN = 1.0;
    } else {
        item->impactP = 1.0;
        item->impactN = 0.0;
    }
    /* The nodes retrieved here are guaranteed to be non-terminal.
    ** The initial node is not terminal because constant nodes are
    ** dealt with in the calling procedure. Subsequent nodes are inserted
    ** only if they are not terminal. */
    while (queue->first != NULL) {
        /* If the size of the subset is below the threshold, quit. */
        if (info->size <= threshold)
            break;
        item = (GlobalQueueItem *) queue->first;
        node = item->node;
#ifdef DD_DEBUG
        assert(item->impactP >= 0 && item->impactP <= 1.0);
        assert(item->impactN >= 0 && item->impactN <= 1.0);
        assert(!Cudd_IsComplement(node));
        assert(!Cudd_IsConstant(node));
#endif
        if (!st_lookup(info->table, (char *)node, (char **)&infoN)) {
            cuddLevelQueueQuit(queue);
            cuddLevelQueueQuit(localQueue);
            return(0);
        }
        quality = infoN->care ? quality1 : quality0;
#ifdef DD_DEBUG
        assert(infoN->parity >= 1 && infoN->parity <= 3);
#endif
        if (infoN->parity == 3) {
            /* This node can be reached through paths of different parity.
            ** It is not safe to replace it, because remapping will give
            ** an incorrect result, while replacement by 0 may cause node
            ** splitting. */
            cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
            continue;
        }
        T = cuddT(node);
        E = cuddE(node);
        shared = NULL;
        impactP = item->impactP;
        impactN = item->impactN;
        if (Cudd_bddLeq(dd,T,E)) {
            /* Here we know that E is regular. */
#ifdef DD_DEBUG
            assert(!Cudd_IsComplement(E));
#endif
            (void) st_lookup(info->table, (char *)T, (char **)&infoT);
            (void) st_lookup(info->table, (char *)E, (char **)&infoE);
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
            } else {
#ifdef DD_DEBUG
                assert(infoN->parity == 2);
#endif
                impact = impactN;
                minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
            }
            numOnset = impact * minterms;
        } else if (Cudd_bddLeq(dd,E,T)) {
            /* Here E may be complemented. */
            DdNode *Ereg = Cudd_Regular(E);
            (void) st_lookup(info->table, (char *)T, (char **)&infoT);
            (void) st_lookup(info->table, (char *)Ereg, (char **)&infoE);
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoT->mintermsP/2.0 -
                    ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
            } else {
#ifdef DD_DEBUG
                assert(infoN->parity == 2);
#endif
                impact = impactN;
                minterms = ((E == Ereg) ? infoE->mintermsN :
                            infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
            }
            numOnset = impact * minterms;
        } else {
            DdNode *Ereg = Cudd_Regular(E);
            DdNode *TT = cuddT(T);
            DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
            if (T->index == Ereg->index && TT == ET) {
                shared = TT;
                replace = REPLACE_TT;
            } else {
                DdNode *TE = cuddE(T);
                DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
                if (T->index == Ereg->index && TE == EE) {
                    shared = TE;
                    replace = REPLACE_TE;
                } else {
                    replace = REPLACE_N;
                }
            }
            numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
            savings = computeSavings(dd,node,shared,info,localQueue);
            if (shared != NULL) {
                NodeData *infoS;
                (void) st_lookup(info->table, (char *)Cudd_Regular(shared),
                                 (char **)&infoS);
                if (Cudd_IsComplement(shared)) {
                    numOnset -= (infoS->mintermsN * impactP +
                        infoS->mintermsP * impactN)/2.0;
                } else {
                    numOnset -= (infoS->mintermsP * impactP +
                        infoS->mintermsN * impactN)/2.0;
                }
                savings--;
            }
        }

        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
        if (replace == REPLACE_T || replace == REPLACE_E)
            (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
                          node, impact, numOnset, savings);
        else
            (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
                          node, impactP, impactN, numOnset, savings);
#endif
        if ((1 - numOnset / info->minterms) >
            quality * (1 - (double) savings / info->size)) {
            infoN->replace = replace;
            info->size -= savings;
            info->minterms -=numOnset;
#if 0
            (void) printf("remap(%d): new size = %d new minterms = %g\n",
                          replace, info->size, info->minterms);
#endif
            if (replace == REPLACE_N) {
                savings -= updateRefs(dd,node,NULL,info,localQueue);
            } else if (replace == REPLACE_T) {
                savings -= updateRefs(dd,node,E,info,localQueue);
            } else if (replace == REPLACE_E) {
                savings -= updateRefs(dd,node,T,info,localQueue);
            } else {
#ifdef DD_DEBUG
                assert(replace == REPLACE_TT || replace == REPLACE_TE);
#endif
                savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
            }
            assert(savings == 0);
        } else {
            replace = NOTHING;
        }
        if (replace == REPLACE_N) continue;
        if ((replace == REPLACE_E || replace == NOTHING) &&
            !cuddIsConstant(cuddT(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (replace == REPLACE_E) {
                item->impactP += impactP;
                item->impactN += impactN;
            } else {
                item->impactP += impactP/2.0;
                item->impactN += impactN/2.0;
            }
        }
        if ((replace == REPLACE_T || replace == NOTHING) &&
            !Cudd_IsConstant(cuddE(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (Cudd_IsComplement(cuddE(node))) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
        }
        if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
            !Cudd_IsConstant(shared)) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
                                         cuddI(dd,Cudd_Regular(shared)->index));
            if (Cudd_IsComplement(shared)) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
        }
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of BAmarkNodes */

static int computeSavings	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	skip,
		ApproxInfo *	info,
		DdLevelQueue *	queue
	)			[static]

Function********************************************************************

Synopsis [Counts the nodes that would be eliminated if a given node were replaced by zero.]

Description [Counts the nodes that would be eliminated if a given node were replaced by zero. This procedure uses a queue passed by the caller for efficiency: since the queue is left empty at the endof the search, it can be reused as is by the next search. Returns the count (always striclty positive) if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddUnderApprox]

Definition at line 970 of file cuddApprox.c.

{
    NodeData *infoN;
    LocalQueueItem *item;
    DdNode *node;
    int savings = 0;

    node = Cudd_Regular(f);
    skip = Cudd_Regular(skip);
    /* Insert the given node in the level queue. Its local reference
    ** count is set equal to the function reference count so that the
    ** search will continue from it when it is retrieved. */
    item = (LocalQueueItem *)
        cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL)
        return(0);
    (void) st_lookup(info->table, (char *)node, (char **)&infoN);
    item->localRef = infoN->functionRef;

    /* Process the queue. */
    while (queue->first != NULL) {
        item = (LocalQueueItem *) queue->first;
        node = item->node;
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
        if (node == skip) continue;
        (void) st_lookup(info->table, (char *)node, (char **)&infoN);
        if (item->localRef != infoN->functionRef) {
            /* This node is shared. */
            continue;
        }
        savings++;
        if (!cuddIsConstant(cuddT(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (item == NULL) return(0);
            item->localRef++;
        }
        if (!Cudd_IsConstant(cuddE(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (item == NULL) return(0);
            item->localRef++;
        }
    }

#ifdef DD_DEBUG
    /* At the end of a local search the queue should be empty. */
    assert(queue->size == 0);
#endif
    return(savings);

} /* end of computeSavings */

DdNode* Cudd_BiasedOverApprox	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		int	numVars,
		int	threshold,
		double	quality1,
		double	quality0
	)

Function********************************************************************

Synopsis [Extracts a dense superset from a BDD with the biased underapproximation method.]

Description [Extracts a dense superset from a BDD. The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. Returns a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.]

SideEffects [None]

SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]

Definition at line 432 of file cuddApprox.c.

{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    do {
        dd->reordered = 0;
        subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
                                      quality0);
    } while (dd->reordered == 1);
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_BiasedOverApprox */

DdNode* Cudd_BiasedUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		int	numVars,
		int	threshold,
		double	quality1,
		double	quality0
	)

Function********************************************************************

Synopsis [Extracts a dense subset from a BDD with the biased underapproximation method.]

Description [Extracts a dense subset from a BDD. This procedure uses a biased remapping technique and density as the cost function. The bias is a function. This procedure tries to approximate where the bias is 0 and preserve the given function where the bias is 1. Returns a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.]

SideEffects [None]

SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_RemapUnderApprox Cudd_ReadSize]

Definition at line 382 of file cuddApprox.c.

{
    DdNode *subset;

    do {
        dd->reordered = 0;
        subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
                                       quality0);
    } while (dd->reordered == 1);

    return(subset);

} /* end of Cudd_BiasedUnderApprox */

DdNode* Cudd_OverApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	safe,
		double	quality
	)

Function********************************************************************

Synopsis [Extracts a dense superset from a BDD with Shiple's underapproximation method.]

Description [Extracts a dense superset from a BDD. The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. Returns a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.]

SideEffects [None]

SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]

Definition at line 244 of file cuddApprox.c.

{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    do {
        dd->reordered = 0;
        subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
    } while (dd->reordered == 1);
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_OverApprox */

DdNode* Cudd_RemapOverApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		double	quality
	)

Function********************************************************************

Synopsis [Extracts a dense superset from a BDD with the remapping underapproximation method.]

Description [Extracts a dense superset from a BDD. The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. Returns a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.]

SideEffects [None]

SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]

Definition at line 335 of file cuddApprox.c.

{
    DdNode *subset, *g;

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

DdNode* Cudd_RemapUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		double	quality
	)

Function********************************************************************

Synopsis [Extracts a dense subset from a BDD with the remapping underapproximation method.]

Description [Extracts a dense subset from a BDD. This procedure uses a remapping technique and density as the cost function. Returns a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.]

SideEffects [None]

SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize]

Definition at line 289 of file cuddApprox.c.

{
    DdNode *subset;

    do {
        dd->reordered = 0;
        subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
    } while (dd->reordered == 1);

    return(subset);

} /* end of Cudd_RemapUnderApprox */

DdNode* Cudd_UnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	safe,
		double	quality
	)

AutomaticEnd Function********************************************************************

Synopsis [Extracts a dense subset from a BDD with Shiple's underapproximation method.]

Description [Extracts a dense subset from a BDD. This procedure uses a variant of Tom Shiple's underapproximation method. The main difference from the original method is that density is used as cost function. Returns a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.]

SideEffects [None]

SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]

Definition at line 197 of file cuddApprox.c.

{
    DdNode *subset;

    do {
        dd->reordered = 0;
        subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
    } while (dd->reordered == 1);

    return(subset);

} /* end of Cudd_UnderApprox */

DdNode* cuddBiasedUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		int	numVars,
		int	threshold,
		double	quality1,
		double	quality0
	)

Function********************************************************************

Synopsis [Applies the biased remapping underappoximation algorithm.]

Description [Applies the biased remapping underappoximation algorithm. Proceeds in three phases:

• collect information on each node in the BDD; this is done via DFS.
• traverse the BDD in top-down fashion and compute for each node whether remapping increases density.
• traverse the BDD via DFS and actually perform the elimination.

Returns the approximated BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_BiasedUnderApprox]

Definition at line 660 of file cuddApprox.c.

{
    ApproxInfo *info;
    DdNode *subset;
    int result;
    DdHashTable *cache;

    if (f == NULL) {
        fprintf(dd->err, "Cannot subset, nil object\n");
        dd->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

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

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, TRUE);
    if (info == NULL) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }

    cache = cuddHashTableInit(dd,2,2);
    result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
    if (result == CARE_ERROR) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        cuddHashTableQuit(cache);
        FREE(info->page);
        st_free_table(info->table);
        FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    cuddHashTableQuit(cache);

    /* Mark nodes that should be replaced by zero. */
    result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
    if (result == 0) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        FREE(info->page);
        st_free_table(info->table);
        FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }

    /* Build the result. */
    subset = RAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
        (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                       info->size, Cudd_DagSize(subset));
#endif
    FREE(info->page);
    st_free_table(info->table);
    FREE(info);

#ifdef DD_DEBUG
    if (subset != NULL) {
        cuddRef(subset);
#if 0
        (void) Cudd_DebugCheck(dd);
        (void) Cudd_CheckKeys(dd);
#endif
        if (!Cudd_bddLeq(dd, subset, f)) {
            (void) fprintf(dd->err, "Wrong subset\n");
        }
        cuddDeref(subset);
        dd->errorCode = CUDD_INTERNAL_ERROR;
    }
#endif
    return(subset);

} /* end of cuddBiasedUnderApprox */

DdNode* cuddRemapUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		double	quality
	)

Function********************************************************************

Synopsis [Applies the remapping underappoximation algorithm.]

Description [Applies the remapping underappoximation algorithm. Proceeds in three phases:

• collect information on each node in the BDD; this is done via DFS.
• traverse the BDD in top-down fashion and compute for each node whether remapping increases density.
• traverse the BDD via DFS and actually perform the elimination.

Returns the approximated BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_RemapUnderApprox]

Definition at line 570 of file cuddApprox.c.

{
    ApproxInfo *info;
    DdNode *subset;
    int result;

    if (f == NULL) {
        fprintf(dd->err, "Cannot subset, nil object\n");
        dd->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

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

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, TRUE);
    if (info == NULL) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }

    /* Mark nodes that should be replaced by zero. */
    result = RAmarkNodes(dd, f, info, threshold, quality);
    if (result == 0) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        FREE(info->page);
        st_free_table(info->table);
        FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }

    /* Build the result. */
    subset = RAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
        (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                       info->size, Cudd_DagSize(subset));
#endif
    FREE(info->page);
    st_free_table(info->table);
    FREE(info);

#ifdef DD_DEBUG
    if (subset != NULL) {
        cuddRef(subset);
#if 0
        (void) Cudd_DebugCheck(dd);
        (void) Cudd_CheckKeys(dd);
#endif
        if (!Cudd_bddLeq(dd, subset, f)) {
            (void) fprintf(dd->err, "Wrong subset\n");
        }
        cuddDeref(subset);
        dd->errorCode = CUDD_INTERNAL_ERROR;
    }
#endif
    return(subset);

} /* end of cuddRemapUnderApprox */

DdNode* cuddUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	safe,
		double	quality
	)

Function********************************************************************

Synopsis [Applies Tom Shiple's underappoximation algorithm.]

Description [Applies Tom Shiple's underappoximation algorithm. Proceeds in three phases:

• collect information on each node in the BDD; this is done via DFS.
• traverse the BDD in top-down fashion and compute for each node whether its elimination increases density.
• traverse the BDD via DFS and actually perform the elimination.

Returns the approximated BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_UnderApprox]

Definition at line 480 of file cuddApprox.c.

{
    ApproxInfo *info;
    DdNode *subset;
    int result;

    if (f == NULL) {
        fprintf(dd->err, "Cannot subset, nil object\n");
        return(NULL);
    }

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

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, safe);
    if (info == NULL) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }

    /* Mark nodes that should be replaced by zero. */
    result = UAmarkNodes(dd, f, info, threshold, safe, quality);
    if (result == 0) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        FREE(info->page);
        st_free_table(info->table);
        FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }

    /* Build the result. */
    subset = UAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
        (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                       info->size, Cudd_DagSize(subset));
#endif
    FREE(info->page);
    st_free_table(info->table);
    FREE(info);

#ifdef DD_DEBUG
    if (subset != NULL) {
        cuddRef(subset);
#if 0
        (void) Cudd_DebugCheck(dd);
        (void) Cudd_CheckKeys(dd);
#endif
        if (!Cudd_bddLeq(dd, subset, f)) {
            (void) fprintf(dd->err, "Wrong subset\n");
            dd->errorCode = CUDD_INTERNAL_ERROR;
        }
        cuddDeref(subset);
    }
#endif
    return(subset);

} /* end of cuddUnderApprox */

static ApproxInfo* gatherInfo	(	DdManager *	dd,
		DdNode *	node,
		int	numVars,
		int	parity
	)			[static]

Function********************************************************************

Synopsis [Gathers information about each node.]

Description [Counts minterms and computes reference counts of each node in the BDD . The minterm count is separately computed for the node and its complement. This is to avoid cancellation errors. Returns a pointer to the data structure holding the information gathered if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddUnderApprox gatherInfoAux]

Definition at line 876 of file cuddApprox.c.

{
    ApproxInfo  *info;
    NodeData *infoTop;

    /* If user did not give 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) {
        numVars = DBL_MAX_EXP - 1;
    }

    info = ALLOC(ApproxInfo,1);
    if (info == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    info->max = pow(2.0,(double) numVars);
    info->one = DD_ONE(dd);
    info->zero = Cudd_Not(info->one);
    info->size = Cudd_DagSize(node);
    /* All the information gathered will be stored in a contiguous
    ** piece of memory, which is allocated here. This can be done
    ** efficiently because we have counted the number of nodes of the
    ** BDD. info->index points to the next available entry in the array
    ** that stores the per-node information. */
    info->page = ALLOC(NodeData,info->size);
    if (info->page == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        FREE(info);
        return(NULL);
    }
    memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
    info->table = st_init_table(st_ptrcmp,st_ptrhash);
    if (info->table == NULL) {
        FREE(info->page);
        FREE(info);
        return(NULL);
    }
    /* We visit the DAG in post-order DFS. Hence, the constant node is
    ** in first position, and the root of the DAG is in last position. */

    /* Info for the constant node: Initialize only fields different from 0. */
    if (st_insert(info->table, (char *)info->one, (char *)info->page) == ST_OUT_OF_MEM) {
        FREE(info->page);
        FREE(info);
        st_free_table(info->table);
        return(NULL);
    }
    info->page[0].mintermsP = info->max;
    info->index = 1;

    infoTop = gatherInfoAux(node,info,parity);
    if (infoTop == NULL) {
        FREE(info->page);
        st_free_table(info->table);
        FREE(info);
        return(NULL);
    }
    if (Cudd_IsComplement(node)) {
        info->minterms = infoTop->mintermsN;
    } else {
        info->minterms = infoTop->mintermsP;
    }

    infoTop->functionRef = 1;
    return(info);

} /* end of gatherInfo */

static NodeData* gatherInfoAux	(	DdNode *	node,
		ApproxInfo *	info,
		int	parity
	)			[static]

Function********************************************************************

Synopsis [Recursively counts minterms and computes reference counts of each node in the BDD.]

Description [Recursively counts minterms and computes reference counts of each node in the BDD. Similar to the cuddCountMintermAux which recursively counts the number of minterms for the dag rooted at each node in terms of the total number of variables (max). It assumes that the node pointer passed to it is regular and it maintains the invariant.]

SideEffects [None]

SeeAlso [gatherInfo]

Definition at line 806 of file cuddApprox.c.

{
    DdNode      *N, *Nt, *Ne;
    NodeData    *infoN, *infoT, *infoE;

    N = Cudd_Regular(node);

    /* Check whether entry for this node exists. */
    if (st_lookup(info->table, (char *)N, (char **)&infoN)) {
        if (parity) {
            /* Update parity and propagate. */
            updateParity(N, info, 1 +  (int) Cudd_IsComplement(node));
        }
        return(infoN);
    }

    /* Compute the cofactors. */
    Nt = Cudd_NotCond(cuddT(N), N != node);
    Ne = Cudd_NotCond(cuddE(N), N != node);

    infoT = gatherInfoAux(Nt, info, parity);
    if (infoT == NULL) return(NULL);
    infoE = gatherInfoAux(Ne, info, parity);
    if (infoE == NULL) return(NULL);

    infoT->functionRef++;
    infoE->functionRef++;

    /* Point to the correct location in the page. */
    infoN = &(info->page[info->index++]);
    infoN->parity |= 1 + (short) Cudd_IsComplement(node);

    infoN->mintermsP = infoT->mintermsP/2;
    infoN->mintermsN = infoT->mintermsN/2;
    if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
        infoN->mintermsP += infoE->mintermsN/2;
        infoN->mintermsN += infoE->mintermsP/2;
    } else {
        infoN->mintermsP += infoE->mintermsP/2;
        infoN->mintermsN += infoE->mintermsN/2;
    }

    /* Insert entry for the node in the table. */
    if (st_insert(info->table,(char *)N, (char *)infoN) == ST_OUT_OF_MEM) {
        return(NULL);
    }
    return(infoN);

} /* end of gatherInfoAux */

static DdNode* RAbuildSubset	(	DdManager *	dd,
		DdNode *	node,
		ApproxInfo *	info
	)			[static]

Function********************************************************************

Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]

Description [Builds the subset BDDfor cuddRemapUnderApprox. Based on the info table, performs remapping or replacement at selected nodes. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddRemapUnderApprox]

Definition at line 1973 of file cuddApprox.c.

{
    DdNode *Nt, *Ne, *N, *t, *e, *r;
    NodeData *infoN;

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

    N = Cudd_Regular(node);

    Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
    Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));

    if (st_lookup(info->table, (char *)N, (char **)&infoN)) {
        if (N == node ) {
            if (infoN->resultP != NULL) {
                return(infoN->resultP);
            }
        } else {
            if (infoN->resultN != NULL) {
                return(infoN->resultN);
            }
        }
        if (infoN->replace == REPLACE_T) {
            r = RAbuildSubset(dd, Ne, info);
            return(r);
        } else if (infoN->replace == REPLACE_E) {
            r = RAbuildSubset(dd, Nt, info);
            return(r);
        } else if (infoN->replace == REPLACE_N) {
            return(info->zero);
        } else if (infoN->replace == REPLACE_TT) {
            DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
                                       Cudd_IsComplement(node));
            int index = cuddT(N)->index;
            DdNode *e = info->zero;
            DdNode *t = RAbuildSubset(dd, Ntt, info);
            if (t == NULL) {
                return(NULL);
            }
            cuddRef(t);
            if (Cudd_IsComplement(t)) {
                t = Cudd_Not(t);
                e = Cudd_Not(e);
                r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
                if (r == NULL) {
                    Cudd_RecursiveDeref(dd, t);
                    return(NULL);
                }
                r = Cudd_Not(r);
            } else {
                r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
                if (r == NULL) {
                    Cudd_RecursiveDeref(dd, t);
                    return(NULL);
                }
            }
            cuddDeref(t);
            return(r);
        } else if (infoN->replace == REPLACE_TE) {
            DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
                                       Cudd_IsComplement(node));
            int index = cuddT(N)->index;
            DdNode *t = info->one;
            DdNode *e = RAbuildSubset(dd, Nte, info);
            if (e == NULL) {
                return(NULL);
            }
            cuddRef(e);
            e = Cudd_Not(e);
            r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
            if (r == NULL) {
                Cudd_RecursiveDeref(dd, e);
                return(NULL);
            }
            r =Cudd_Not(r);
            cuddDeref(e);
            return(r);
        }
    } else {
        (void) fprintf(dd->err,
                       "Something is wrong, ought to be in info table\n");
        dd->errorCode = CUDD_INTERNAL_ERROR;
        return(NULL);
    }

    t = RAbuildSubset(dd, Nt, info);
    if (t == NULL) {
        return(NULL);
    }
    cuddRef(t);

    e = RAbuildSubset(dd, Ne, info);
    if (e == NULL) {
        Cudd_RecursiveDeref(dd,t);
        return(NULL);
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
        t = Cudd_Not(t);
        e = Cudd_Not(e);
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
        r = Cudd_Not(r);
    } else {
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
    }
    cuddDeref(t);
    cuddDeref(e);

    if (N == node) {
        infoN->resultP = r;
    } else {
        infoN->resultN = r;
    }

    return(r);

} /* end of RAbuildSubset */

static int RAmarkNodes	(	DdManager *	dd,
		DdNode *	f,
		ApproxInfo *	info,
		int	threshold,
		double	quality
	)			[static]

Function********************************************************************

Synopsis [Marks nodes for remapping.]

Description [Marks nodes for remapping. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddRemapUnderApprox]

Definition at line 1342 of file cuddApprox.c.

{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN, *infoT, *infoE;
    GlobalQueueItem *item;
    DdNode *node, *T, *E;
    DdNode *shared; /* grandchild shared by the two children of node */
    double numOnset;
    double impact, impactP, impactN;
    double minterms;
    int savings;
    int replace;

#if 0
    (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
                  info->size, info->minterms);
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
        return(0);
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
                                    dd->initSlots);
    if (localQueue == NULL) {
        cuddLevelQueueQuit(queue);
        return(0);
    }
    /* Enqueue regular pointer to root and initialize impact. */
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *)
        cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL) {
        cuddLevelQueueQuit(queue);
        cuddLevelQueueQuit(localQueue);
        return(0);
    }
    if (Cudd_IsComplement(f)) {
        item->impactP = 0.0;
        item->impactN = 1.0;
    } else {
        item->impactP = 1.0;
        item->impactN = 0.0;
    }
    /* The nodes retrieved here are guaranteed to be non-terminal.
    ** The initial node is not terminal because constant nodes are
    ** dealt with in the calling procedure. Subsequent nodes are inserted
    ** only if they are not terminal. */
    while (queue->first != NULL) {
        /* If the size of the subset is below the threshold, quit. */
        if (info->size <= threshold)
            break;
        item = (GlobalQueueItem *) queue->first;
        node = item->node;
#ifdef DD_DEBUG
        assert(item->impactP >= 0 && item->impactP <= 1.0);
        assert(item->impactN >= 0 && item->impactN <= 1.0);
        assert(!Cudd_IsComplement(node));
        assert(!Cudd_IsConstant(node));
#endif
        if (!st_lookup(info->table, (char *)node, (char **)&infoN)) {
            cuddLevelQueueQuit(queue);
            cuddLevelQueueQuit(localQueue);
            return(0);
        }
#ifdef DD_DEBUG
        assert(infoN->parity >= 1 && infoN->parity <= 3);
#endif
        if (infoN->parity == 3) {
            /* This node can be reached through paths of different parity.
            ** It is not safe to replace it, because remapping will give
            ** an incorrect result, while replacement by 0 may cause node
            ** splitting. */
            cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
            continue;
        }
        T = cuddT(node);
        E = cuddE(node);
        shared = NULL;
        impactP = item->impactP;
        impactN = item->impactN;
        if (Cudd_bddLeq(dd,T,E)) {
            /* Here we know that E is regular. */
#ifdef DD_DEBUG
            assert(!Cudd_IsComplement(E));
#endif
            (void) st_lookup(info->table, (char *)T, (char **)&infoT);
            (void) st_lookup(info->table, (char *)E, (char **)&infoE);
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
            } else {
#ifdef DD_DEBUG
                assert(infoN->parity == 2);
#endif
                impact = impactN;
                minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
            }
            numOnset = impact * minterms;
        } else if (Cudd_bddLeq(dd,E,T)) {
            /* Here E may be complemented. */
            DdNode *Ereg = Cudd_Regular(E);
            (void) st_lookup(info->table, (char *)T, (char **)&infoT);
            (void) st_lookup(info->table, (char *)Ereg, (char **)&infoE);
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoT->mintermsP/2.0 -
                    ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
            } else {
#ifdef DD_DEBUG
                assert(infoN->parity == 2);
#endif
                impact = impactN;
                minterms = ((E == Ereg) ? infoE->mintermsN :
                            infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
            }
            numOnset = impact * minterms;
        } else {
            DdNode *Ereg = Cudd_Regular(E);
            DdNode *TT = cuddT(T);
            DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
            if (T->index == Ereg->index && TT == ET) {
                shared = TT;
                replace = REPLACE_TT;
            } else {
                DdNode *TE = cuddE(T);
                DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
                if (T->index == Ereg->index && TE == EE) {
                    shared = TE;
                    replace = REPLACE_TE;
                } else {
                    replace = REPLACE_N;
                }
            }
            numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
            savings = computeSavings(dd,node,shared,info,localQueue);
            if (shared != NULL) {
                NodeData *infoS;
                (void) st_lookup(info->table, (char *)Cudd_Regular(shared),
                                 (char **)&infoS);
                if (Cudd_IsComplement(shared)) {
                    numOnset -= (infoS->mintermsN * impactP +
                        infoS->mintermsP * impactN)/2.0;
                } else {
                    numOnset -= (infoS->mintermsP * impactP +
                        infoS->mintermsN * impactN)/2.0;
                }
                savings--;
            }
        }

        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
        if (replace == REPLACE_T || replace == REPLACE_E)
            (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
                          node, impact, numOnset, savings);
        else
            (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
                          node, impactP, impactN, numOnset, savings);
#endif
        if ((1 - numOnset / info->minterms) >
            quality * (1 - (double) savings / info->size)) {
            infoN->replace = replace;
            info->size -= savings;
            info->minterms -=numOnset;
#if 0
            (void) printf("remap(%d): new size = %d new minterms = %g\n",
                          replace, info->size, info->minterms);
#endif
            if (replace == REPLACE_N) {
                savings -= updateRefs(dd,node,NULL,info,localQueue);
            } else if (replace == REPLACE_T) {
                savings -= updateRefs(dd,node,E,info,localQueue);
            } else if (replace == REPLACE_E) {
                savings -= updateRefs(dd,node,T,info,localQueue);
            } else {
#ifdef DD_DEBUG
                assert(replace == REPLACE_TT || replace == REPLACE_TE);
#endif
                savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
            }
            assert(savings == 0);
        } else {
            replace = NOTHING;
        }
        if (replace == REPLACE_N) continue;
        if ((replace == REPLACE_E || replace == NOTHING) &&
            !cuddIsConstant(cuddT(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (replace == REPLACE_E) {
                item->impactP += impactP;
                item->impactN += impactN;
            } else {
                item->impactP += impactP/2.0;
                item->impactN += impactN/2.0;
            }
        }
        if ((replace == REPLACE_T || replace == NOTHING) &&
            !Cudd_IsConstant(cuddE(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (Cudd_IsComplement(cuddE(node))) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
        }
        if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
            !Cudd_IsConstant(shared)) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
                                         cuddI(dd,Cudd_Regular(shared)->index));
            if (Cudd_IsComplement(shared)) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
        }
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of RAmarkNodes */

static DdNode* UAbuildSubset	(	DdManager *	dd,
		DdNode *	node,
		ApproxInfo *	info
	)			[static]

Function********************************************************************

Synopsis [Builds the subset BDD.]

Description [Builds the subset BDD. Based on the info table, replaces selected nodes by zero. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddUnderApprox]

Definition at line 1247 of file cuddApprox.c.

{

    DdNode *Nt, *Ne, *N, *t, *e, *r;
    NodeData *infoN;

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

    N = Cudd_Regular(node);

    if (st_lookup(info->table, (char *)N, (char **)&infoN)) {
        if (infoN->replace == TRUE) {
            return(info->zero);
        }
        if (N == node ) {
            if (infoN->resultP != NULL) {
                return(infoN->resultP);
            }
        } else {
            if (infoN->resultN != NULL) {
                return(infoN->resultN);
            }
        }
    } else {
        (void) fprintf(dd->err,
                       "Something is wrong, ought to be in info table\n");
        dd->errorCode = CUDD_INTERNAL_ERROR;
        return(NULL);
    }

    Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
    Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));

    t = UAbuildSubset(dd, Nt, info);
    if (t == NULL) {
        return(NULL);
    }
    cuddRef(t);

    e = UAbuildSubset(dd, Ne, info);
    if (e == NULL) {
        Cudd_RecursiveDeref(dd,t);
        return(NULL);
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
        t = Cudd_Not(t);
        e = Cudd_Not(e);
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
        r = Cudd_Not(r);
    } else {
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
    }
    cuddDeref(t);
    cuddDeref(e);

    if (N == node) {
        infoN->resultP = r;
    } else {
        infoN->resultN = r;
    }

    return(r);

} /* end of UAbuildSubset */

static int UAmarkNodes	(	DdManager *	dd,
		DdNode *	f,
		ApproxInfo *	info,
		int	threshold,
		int	safe,
		double	quality
	)			[static]

Function********************************************************************

Synopsis [Marks nodes for replacement by zero.]

Description [Marks nodes for replacement by zero. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddUnderApprox]

Definition at line 1123 of file cuddApprox.c.

{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN;
    GlobalQueueItem *item;
    DdNode *node;
    double numOnset;
    double impactP, impactN;
    int savings;

#if 0
    (void) printf("initial size = %d initial minterms = %g\n",
                  info->size, info->minterms);
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
        return(0);
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
                                    dd->initSlots);
    if (localQueue == NULL) {
        cuddLevelQueueQuit(queue);
        return(0);
    }
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL) {
        cuddLevelQueueQuit(queue);
        cuddLevelQueueQuit(localQueue);
        return(0);
    }
    if (Cudd_IsComplement(f)) {
        item->impactP = 0.0;
        item->impactN = 1.0;
    } else {
        item->impactP = 1.0;
        item->impactN = 0.0;
    }
    while (queue->first != NULL) {
        /* If the size of the subset is below the threshold, quit. */
        if (info->size <= threshold)
            break;
        item = (GlobalQueueItem *) queue->first;
        node = item->node;
        node = Cudd_Regular(node);
        (void) st_lookup(info->table, (char *)node, (char **)&infoN);
        if (safe && infoN->parity == 3) {
            cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
            continue;
        }
        impactP = item->impactP;
        impactN = item->impactN;
        numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
        savings = computeSavings(dd,node,NULL,info,localQueue);
        if (savings == 0) {
            cuddLevelQueueQuit(queue);
            cuddLevelQueueQuit(localQueue);
            return(0);
        }
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
        (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
                      node, impactP, impactN, numOnset, savings);
#endif
        if ((1 - numOnset / info->minterms) >
            quality * (1 - (double) savings / info->size)) {
            infoN->replace = TRUE;
            info->size -= savings;
            info->minterms -=numOnset;
#if 0
            (void) printf("replace: new size = %d new minterms = %g\n",
                          info->size, info->minterms);
#endif
            savings -= updateRefs(dd,node,NULL,info,localQueue);
            assert(savings == 0);
            continue;
        }
        if (!cuddIsConstant(cuddT(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            item->impactP += impactP/2.0;
            item->impactN += impactN/2.0;
        }
        if (!Cudd_IsConstant(cuddE(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (Cudd_IsComplement(cuddE(node))) {
                item->impactP += impactN/2.0;
                item->impactN += impactP/2.0;
            } else {
                item->impactP += impactP/2.0;
                item->impactN += impactN/2.0;
            }
        }
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of UAmarkNodes */

static void updateParity	(	DdNode *	node,
		ApproxInfo *	info,
		int	newparity
	)			[static]

Function********************************************************************

Synopsis [Recursively update the parity of the paths reaching a node.]

Description [Recursively update the parity of the paths reaching a node. Assumes that node is regular and propagates the invariant.]

SideEffects [None]

SeeAlso [gatherInfoAux]

Definition at line 764 of file cuddApprox.c.

{
    NodeData *infoN;
    DdNode *E;

    if (!st_lookup(info->table, (char *)node, (char **)&infoN)) return;
    if ((infoN->parity & newparity) != 0) return;
    infoN->parity |= newparity;
    if (Cudd_IsConstant(node)) return;
    updateParity(cuddT(node),info,newparity);
    E = cuddE(node);
    if (Cudd_IsComplement(E)) {
        updateParity(Cudd_Not(E),info,3-newparity);
    } else {
        updateParity(E,info,newparity);
    }
    return;

} /* end of updateParity */

static int updateRefs	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	skip,
		ApproxInfo *	info,
		DdLevelQueue *	queue
	)			[static]

Function********************************************************************

Synopsis [Update function reference counts.]

Description [Update function reference counts to account for replacement. Returns the number of nodes saved if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [UAmarkNodes RAmarkNodes]

Definition at line 1042 of file cuddApprox.c.

{
    NodeData *infoN;
    LocalQueueItem *item;
    DdNode *node;
    int savings = 0;

    node = Cudd_Regular(f);
    /* Insert the given node in the level queue. Its function reference
    ** count is set equal to 0 so that the search will continue from it
    ** when it is retrieved. */
    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL)
        return(0);
    (void) st_lookup(info->table, (char *)node, (char **)&infoN);
    infoN->functionRef = 0;

    if (skip != NULL) {
        /* Increase the function reference count of the node to be skipped
        ** by 1 to account for the node pointing to it that will be created. */
        skip = Cudd_Regular(skip);
        (void) st_lookup(info->table, (char *)skip, (char **)&infoN);
        infoN->functionRef++;
    }

    /* Process the queue. */
    while (queue->first != NULL) {
        item = (LocalQueueItem *) queue->first;
        node = item->node;
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
        (void) st_lookup(info->table, (char *)node, (char **)&infoN);
        if (infoN->functionRef != 0) {
            /* This node is shared or must be skipped. */
            continue;
        }
        savings++;
        if (!cuddIsConstant(cuddT(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (item == NULL) return(0);
            (void) st_lookup(info->table, (char *)cuddT(node),
                             (char **)&infoN);
            infoN->functionRef--;
        }
        if (!Cudd_IsConstant(cuddE(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (item == NULL) return(0);
            (void) st_lookup(info->table, (char *)Cudd_Regular(cuddE(node)),
                             (char **)&infoN);
            infoN->functionRef--;
        }
    }

#ifdef DD_DEBUG
    /* At the end of a local search the queue should be empty. */
    assert(queue->size == 0);
#endif
    return(savings);

} /* end of updateRefs */

---

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddApprox.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static]

Definition at line 140 of file cuddApprox.c.