src/cuBdd/cuddApprox.c File Reference

#include "util.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 (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)
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)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $"

Define Documentation

#define CARE   1

Definition at line 96 of file cuddApprox.c.

#define CARE_ERROR   3

Definition at line 98 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:

Internal procedures included in this module:

Static procedures included in this module:

]

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

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 79 of file cuddApprox.c.

#define DONT_CARE   0

Definition at line 95 of file cuddApprox.c.

#define NOTHING   0

Definition at line 88 of file cuddApprox.c.

#define REPLACE_E   2

Definition at line 90 of file cuddApprox.c.

#define REPLACE_N   3

Definition at line 91 of file cuddApprox.c.

#define REPLACE_T   1

Definition at line 89 of file cuddApprox.c.

#define REPLACE_TE   5

Definition at line 93 of file cuddApprox.c.

#define REPLACE_TT   4

Definition at line 92 of file cuddApprox.c.

#define TOTAL_CARE   2

Definition at line 97 of file cuddApprox.c.

Function Documentation

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 2134 of file cuddApprox.c.

02140 {
02141     DdNode *one, *zero, *res;
02142     DdNode *Ft, *Fe, *B, *Bt, *Be;
02143     unsigned int topf, topb;
02144     NodeData *infoF;
02145     int careT, careE;
02146 
02147     one = DD_ONE(dd);
02148     zero = Cudd_Not(one);
02149 
02150     if (!st_lookup(info->table, f, &infoF))
02151         return(CARE_ERROR);
02152     if (f == one) return(TOTAL_CARE);
02153     if (b == zero) return(infoF->care);
02154     if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
02155 
02156     if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
02157         (res = cuddHashTableLookup2(cache,f,b)) != NULL) {
02158         if (res->ref == 0) {
02159             cache->manager->dead++;
02160             cache->manager->constants.dead++;
02161         }
02162         return(infoF->care);
02163     }
02164 
02165     topf = dd->perm[f->index];
02166     B = Cudd_Regular(b);
02167     topb = cuddI(dd,B->index);
02168     if (topf <= topb) {
02169         Ft = cuddT(f); Fe = cuddE(f);
02170     } else {
02171         Ft = Fe = f;
02172     }
02173     if (topb <= topf) {
02174         /* We know that b is not constant because f is not. */
02175         Bt = cuddT(B); Be = cuddE(B);
02176         if (Cudd_IsComplement(b)) {
02177             Bt = Cudd_Not(Bt);
02178             Be = Cudd_Not(Be);
02179         }
02180     } else {
02181         Bt = Be = b;
02182     }
02183 
02184     careT = BAapplyBias(dd, Ft, Bt, info, cache);
02185     if (careT == CARE_ERROR)
02186         return(CARE_ERROR);
02187     careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
02188     if (careE == CARE_ERROR)
02189         return(CARE_ERROR);
02190     if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
02191         infoF->care = TOTAL_CARE;
02192     } else {
02193         infoF->care = CARE;
02194     }
02195 
02196     if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
02197         ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
02198         cuddSatDec(fanout);
02199         if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
02200             return(CARE_ERROR);
02201         }
02202     }
02203     return(infoF->care);
02204 
02205 } /* 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 1669 of file cuddApprox.c.

01676 {
01677     DdLevelQueue *queue;
01678     DdLevelQueue *localQueue;
01679     NodeData *infoN, *infoT, *infoE;
01680     GlobalQueueItem *item;
01681     DdNode *node, *T, *E;
01682     DdNode *shared; /* grandchild shared by the two children of node */
01683     double numOnset;
01684     double impact, impactP, impactN;
01685     double minterms;
01686     double quality;
01687     int savings;
01688     int replace;
01689 
01690 #if 0
01691     (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
01692                   info->size, info->minterms);
01693 #endif
01694     queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
01695     if (queue == NULL) {
01696         return(0);
01697     }
01698     localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
01699                                     dd->initSlots);
01700     if (localQueue == NULL) {
01701         cuddLevelQueueQuit(queue);
01702         return(0);
01703     }
01704     /* Enqueue regular pointer to root and initialize impact. */
01705     node = Cudd_Regular(f);
01706     item = (GlobalQueueItem *)
01707         cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
01708     if (item == NULL) {
01709         cuddLevelQueueQuit(queue);
01710         cuddLevelQueueQuit(localQueue);
01711         return(0);
01712     }
01713     if (Cudd_IsComplement(f)) {
01714         item->impactP = 0.0;
01715         item->impactN = 1.0;
01716     } else {
01717         item->impactP = 1.0;
01718         item->impactN = 0.0;
01719     }
01720     /* The nodes retrieved here are guaranteed to be non-terminal.
01721     ** The initial node is not terminal because constant nodes are
01722     ** dealt with in the calling procedure. Subsequent nodes are inserted
01723     ** only if they are not terminal. */
01724     while (queue->first != NULL) {
01725         /* If the size of the subset is below the threshold, quit. */
01726         if (info->size <= threshold)
01727             break;
01728         item = (GlobalQueueItem *) queue->first;
01729         node = item->node;
01730 #ifdef DD_DEBUG
01731         assert(item->impactP >= 0 && item->impactP <= 1.0);
01732         assert(item->impactN >= 0 && item->impactN <= 1.0);
01733         assert(!Cudd_IsComplement(node));
01734         assert(!Cudd_IsConstant(node));
01735 #endif
01736         if (!st_lookup(info->table, node, &infoN)) {
01737             cuddLevelQueueQuit(queue);
01738             cuddLevelQueueQuit(localQueue);
01739             return(0);
01740         }
01741         quality = infoN->care ? quality1 : quality0;
01742 #ifdef DD_DEBUG
01743         assert(infoN->parity >= 1 && infoN->parity <= 3);
01744 #endif
01745         if (infoN->parity == 3) {
01746             /* This node can be reached through paths of different parity.
01747             ** It is not safe to replace it, because remapping will give
01748             ** an incorrect result, while replacement by 0 may cause node
01749             ** splitting. */
01750             cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01751             continue;
01752         }
01753         T = cuddT(node);
01754         E = cuddE(node);
01755         shared = NULL;
01756         impactP = item->impactP;
01757         impactN = item->impactN;
01758         if (Cudd_bddLeq(dd,T,E)) {
01759             /* Here we know that E is regular. */
01760 #ifdef DD_DEBUG
01761             assert(!Cudd_IsComplement(E));
01762 #endif
01763             (void) st_lookup(info->table, T, &infoT);
01764             (void) st_lookup(info->table, E, &infoE);
01765             if (infoN->parity == 1) {
01766                 impact = impactP;
01767                 minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
01768                 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
01769                     savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
01770                     if (savings == 1) {
01771                         cuddLevelQueueQuit(queue);
01772                         cuddLevelQueueQuit(localQueue);
01773                         return(0);
01774                     }
01775                 } else {
01776                     savings = 1;
01777                 }
01778                 replace = REPLACE_E;
01779             } else {
01780 #ifdef DD_DEBUG
01781                 assert(infoN->parity == 2);
01782 #endif
01783                 impact = impactN;
01784                 minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
01785                 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
01786                     savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
01787                     if (savings == 1) {
01788                         cuddLevelQueueQuit(queue);
01789                         cuddLevelQueueQuit(localQueue);
01790                         return(0);
01791                     }
01792                 } else {
01793                     savings = 1;
01794                 }
01795                 replace = REPLACE_T;
01796             }
01797             numOnset = impact * minterms;
01798         } else if (Cudd_bddLeq(dd,E,T)) {
01799             /* Here E may be complemented. */
01800             DdNode *Ereg = Cudd_Regular(E);
01801             (void) st_lookup(info->table, T, &infoT);
01802             (void) st_lookup(info->table, Ereg, &infoE);
01803             if (infoN->parity == 1) {
01804                 impact = impactP;
01805                 minterms = infoT->mintermsP/2.0 -
01806                     ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
01807                 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
01808                     savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
01809                     if (savings == 1) {
01810                         cuddLevelQueueQuit(queue);
01811                         cuddLevelQueueQuit(localQueue);
01812                         return(0);
01813                     }
01814                 } else {
01815                     savings = 1;
01816                 }
01817                 replace = REPLACE_T;
01818             } else {
01819 #ifdef DD_DEBUG
01820                 assert(infoN->parity == 2);
01821 #endif
01822                 impact = impactN;
01823                 minterms = ((E == Ereg) ? infoE->mintermsN :
01824                             infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
01825                 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
01826                     savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
01827                     if (savings == 1) {
01828                         cuddLevelQueueQuit(queue);
01829                         cuddLevelQueueQuit(localQueue);
01830                         return(0);
01831                     }
01832                 } else {
01833                     savings = 1;
01834                 }
01835                 replace = REPLACE_E;
01836             }
01837             numOnset = impact * minterms;
01838         } else {
01839             DdNode *Ereg = Cudd_Regular(E);
01840             DdNode *TT = cuddT(T);
01841             DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
01842             if (T->index == Ereg->index && TT == ET) {
01843                 shared = TT;
01844                 replace = REPLACE_TT;
01845             } else {
01846                 DdNode *TE = cuddE(T);
01847                 DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
01848                 if (T->index == Ereg->index && TE == EE) {
01849                     shared = TE;
01850                     replace = REPLACE_TE;
01851                 } else {
01852                     replace = REPLACE_N;
01853                 }
01854             }
01855             numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
01856             savings = computeSavings(dd,node,shared,info,localQueue);
01857             if (shared != NULL) {
01858                 NodeData *infoS;
01859                 (void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
01860                 if (Cudd_IsComplement(shared)) {
01861                     numOnset -= (infoS->mintermsN * impactP +
01862                         infoS->mintermsP * impactN)/2.0;
01863                 } else {
01864                     numOnset -= (infoS->mintermsP * impactP +
01865                         infoS->mintermsN * impactN)/2.0;
01866                 }
01867                 savings--;
01868             }
01869         }
01870 
01871         cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01872 #if 0
01873         if (replace == REPLACE_T || replace == REPLACE_E)
01874             (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
01875                           node, impact, numOnset, savings);
01876         else
01877             (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
01878                           node, impactP, impactN, numOnset, savings);
01879 #endif
01880         if ((1 - numOnset / info->minterms) >
01881             quality * (1 - (double) savings / info->size)) {
01882             infoN->replace = (char) replace;
01883             info->size -= savings;
01884             info->minterms -=numOnset;
01885 #if 0
01886             (void) printf("remap(%d): new size = %d new minterms = %g\n",
01887                           replace, info->size, info->minterms);
01888 #endif
01889             if (replace == REPLACE_N) {
01890                 savings -= updateRefs(dd,node,NULL,info,localQueue);
01891             } else if (replace == REPLACE_T) {
01892                 savings -= updateRefs(dd,node,E,info,localQueue);
01893             } else if (replace == REPLACE_E) {
01894                 savings -= updateRefs(dd,node,T,info,localQueue);
01895             } else {
01896 #ifdef DD_DEBUG
01897                 assert(replace == REPLACE_TT || replace == REPLACE_TE);
01898 #endif
01899                 savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
01900             }
01901             assert(savings == 0);
01902         } else {
01903             replace = NOTHING;
01904         }
01905         if (replace == REPLACE_N) continue;
01906         if ((replace == REPLACE_E || replace == NOTHING) &&
01907             !cuddIsConstant(cuddT(node))) {
01908             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
01909                                          cuddI(dd,cuddT(node)->index));
01910             if (replace == REPLACE_E) {
01911                 item->impactP += impactP;
01912                 item->impactN += impactN;
01913             } else {
01914                 item->impactP += impactP/2.0;
01915                 item->impactN += impactN/2.0;
01916             }
01917         }
01918         if ((replace == REPLACE_T || replace == NOTHING) &&
01919             !Cudd_IsConstant(cuddE(node))) {
01920             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
01921                                          cuddI(dd,Cudd_Regular(cuddE(node))->index));
01922             if (Cudd_IsComplement(cuddE(node))) {
01923                 if (replace == REPLACE_T) {
01924                     item->impactP += impactN;
01925                     item->impactN += impactP;
01926                 } else {
01927                     item->impactP += impactN/2.0;
01928                     item->impactN += impactP/2.0;
01929                 }
01930             } else {
01931                 if (replace == REPLACE_T) {
01932                     item->impactP += impactP;
01933                     item->impactN += impactN;
01934                 } else {
01935                     item->impactP += impactP/2.0;
01936                     item->impactN += impactN/2.0;
01937                 }
01938             }
01939         }
01940         if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
01941             !Cudd_IsConstant(shared)) {
01942             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
01943                                          cuddI(dd,Cudd_Regular(shared)->index));
01944             if (Cudd_IsComplement(shared)) {
01945                 if (replace == REPLACE_T) {
01946                     item->impactP += impactN;
01947                     item->impactN += impactP;
01948                 } else {
01949                     item->impactP += impactN/2.0;
01950                     item->impactN += impactP/2.0;
01951                 }
01952             } else {
01953                 if (replace == REPLACE_T) {
01954                     item->impactP += impactP;
01955                     item->impactN += impactN;
01956                 } else {
01957                     item->impactP += impactP/2.0;
01958                     item->impactN += impactN/2.0;
01959                 }
01960             }
01961         }
01962     }
01963 
01964     cuddLevelQueueQuit(queue);
01965     cuddLevelQueueQuit(localQueue);
01966     return(1);
01967 
01968 } /* 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 997 of file cuddApprox.c.

01003 {
01004     NodeData *infoN;
01005     LocalQueueItem *item;
01006     DdNode *node;
01007     int savings = 0;
01008 
01009     node = Cudd_Regular(f);
01010     skip = Cudd_Regular(skip);
01011     /* Insert the given node in the level queue. Its local reference
01012     ** count is set equal to the function reference count so that the
01013     ** search will continue from it when it is retrieved. */
01014     item = (LocalQueueItem *)
01015         cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
01016     if (item == NULL)
01017         return(0);
01018     (void) st_lookup(info->table, node, &infoN);
01019     item->localRef = infoN->functionRef;
01020 
01021     /* Process the queue. */
01022     while (queue->first != NULL) {
01023         item = (LocalQueueItem *) queue->first;
01024         node = item->node;
01025         cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01026         if (node == skip) continue;
01027         (void) st_lookup(info->table, node, &infoN);
01028         if (item->localRef != infoN->functionRef) {
01029             /* This node is shared. */
01030             continue;
01031         }
01032         savings++;
01033         if (!cuddIsConstant(cuddT(node))) {
01034             item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
01035                                          cuddI(dd,cuddT(node)->index));
01036             if (item == NULL) return(0);
01037             item->localRef++;
01038         }
01039         if (!Cudd_IsConstant(cuddE(node))) {
01040             item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
01041                                          cuddI(dd,Cudd_Regular(cuddE(node))->index));
01042             if (item == NULL) return(0);
01043             item->localRef++;
01044         }
01045     }
01046 
01047 #ifdef DD_DEBUG
01048     /* At the end of a local search the queue should be empty. */
01049     assert(queue->size == 0);
01050 #endif
01051     return(savings);
01052 
01053 } /* 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 459 of file cuddApprox.c.

00467 {
00468     DdNode *subset, *g;
00469 
00470     g = Cudd_Not(f);    
00471     do {
00472         dd->reordered = 0;
00473         subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
00474                                       quality0);
00475     } while (dd->reordered == 1);
00476     
00477     return(Cudd_NotCond(subset, (subset != NULL)));
00478     
00479 } /* 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 409 of file cuddApprox.c.

00417 {
00418     DdNode *subset;
00419 
00420     do {
00421         dd->reordered = 0;
00422         subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
00423                                        quality0);
00424     } while (dd->reordered == 1);
00425 
00426     return(subset);
00427 
00428 } /* 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 271 of file cuddApprox.c.

00278 {
00279     DdNode *subset, *g;
00280 
00281     g = Cudd_Not(f);    
00282     do {
00283         dd->reordered = 0;
00284         subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
00285     } while (dd->reordered == 1);
00286     
00287     return(Cudd_NotCond(subset, (subset != NULL)));
00288     
00289 } /* 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 362 of file cuddApprox.c.

00368 {
00369     DdNode *subset, *g;
00370 
00371     g = Cudd_Not(f);    
00372     do {
00373         dd->reordered = 0;
00374         subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
00375     } while (dd->reordered == 1);
00376     
00377     return(Cudd_NotCond(subset, (subset != NULL)));
00378     
00379 } /* 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 316 of file cuddApprox.c.

00322 {
00323     DdNode *subset;
00324 
00325     do {
00326         dd->reordered = 0;
00327         subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
00328     } while (dd->reordered == 1);
00329 
00330     return(subset);
00331 
00332 } /* 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 224 of file cuddApprox.c.

00231 {
00232     DdNode *subset;
00233 
00234     do {
00235         dd->reordered = 0;
00236         subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
00237     } while (dd->reordered == 1);
00238 
00239     return(subset);
00240 
00241 } /* 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 687 of file cuddApprox.c.

00695 {
00696     ApproxInfo *info;
00697     DdNode *subset;
00698     int result;
00699     DdHashTable *cache;
00700 
00701     if (f == NULL) {
00702         fprintf(dd->err, "Cannot subset, nil object\n");
00703         dd->errorCode = CUDD_INVALID_ARG;
00704         return(NULL);
00705     }
00706 
00707     if (Cudd_IsConstant(f)) {
00708         return(f);
00709     }
00710 
00711     /* Create table where node data are accessible via a hash table. */
00712     info = gatherInfo(dd, f, numVars, TRUE);
00713     if (info == NULL) {
00714         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00715         dd->errorCode = CUDD_MEMORY_OUT;
00716         return(NULL);
00717     }
00718 
00719     cache = cuddHashTableInit(dd,2,2);
00720     result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
00721     if (result == CARE_ERROR) {
00722         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00723         cuddHashTableQuit(cache);
00724         FREE(info->page);
00725         st_free_table(info->table);
00726         FREE(info);
00727         dd->errorCode = CUDD_MEMORY_OUT;
00728         return(NULL);
00729     }
00730     cuddHashTableQuit(cache);
00731 
00732     /* Mark nodes that should be replaced by zero. */
00733     result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
00734     if (result == 0) {
00735         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00736         FREE(info->page);
00737         st_free_table(info->table);
00738         FREE(info);
00739         dd->errorCode = CUDD_MEMORY_OUT;
00740         return(NULL);
00741     }
00742 
00743     /* Build the result. */
00744     subset = RAbuildSubset(dd, f, info);
00745 #if 1
00746     if (subset && info->size < Cudd_DagSize(subset))
00747         (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
00748                        info->size, Cudd_DagSize(subset));
00749 #endif
00750     FREE(info->page);
00751     st_free_table(info->table);
00752     FREE(info);
00753 
00754 #ifdef DD_DEBUG
00755     if (subset != NULL) {
00756         cuddRef(subset);
00757 #if 0
00758         (void) Cudd_DebugCheck(dd);
00759         (void) Cudd_CheckKeys(dd);
00760 #endif
00761         if (!Cudd_bddLeq(dd, subset, f)) {
00762             (void) fprintf(dd->err, "Wrong subset\n");
00763         }
00764         cuddDeref(subset);
00765         dd->errorCode = CUDD_INTERNAL_ERROR;
00766     }
00767 #endif
00768     return(subset);
00769 
00770 } /* 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 597 of file cuddApprox.c.

00603 {
00604     ApproxInfo *info;
00605     DdNode *subset;
00606     int result;
00607 
00608     if (f == NULL) {
00609         fprintf(dd->err, "Cannot subset, nil object\n");
00610         dd->errorCode = CUDD_INVALID_ARG;
00611         return(NULL);
00612     }
00613 
00614     if (Cudd_IsConstant(f)) {
00615         return(f);
00616     }
00617 
00618     /* Create table where node data are accessible via a hash table. */
00619     info = gatherInfo(dd, f, numVars, TRUE);
00620     if (info == NULL) {
00621         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00622         dd->errorCode = CUDD_MEMORY_OUT;
00623         return(NULL);
00624     }
00625 
00626     /* Mark nodes that should be replaced by zero. */
00627     result = RAmarkNodes(dd, f, info, threshold, quality);
00628     if (result == 0) {
00629         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00630         FREE(info->page);
00631         st_free_table(info->table);
00632         FREE(info);
00633         dd->errorCode = CUDD_MEMORY_OUT;
00634         return(NULL);
00635     }
00636 
00637     /* Build the result. */
00638     subset = RAbuildSubset(dd, f, info);
00639 #if 1
00640     if (subset && info->size < Cudd_DagSize(subset))
00641         (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
00642                        info->size, Cudd_DagSize(subset));
00643 #endif
00644     FREE(info->page);
00645     st_free_table(info->table);
00646     FREE(info);
00647 
00648 #ifdef DD_DEBUG
00649     if (subset != NULL) {
00650         cuddRef(subset);
00651 #if 0
00652         (void) Cudd_DebugCheck(dd);
00653         (void) Cudd_CheckKeys(dd);
00654 #endif
00655         if (!Cudd_bddLeq(dd, subset, f)) {
00656             (void) fprintf(dd->err, "Wrong subset\n");
00657         }
00658         cuddDeref(subset);
00659         dd->errorCode = CUDD_INTERNAL_ERROR;
00660     }
00661 #endif
00662     return(subset);
00663 
00664 } /* 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 507 of file cuddApprox.c.

00514 {
00515     ApproxInfo *info;
00516     DdNode *subset;
00517     int result;
00518 
00519     if (f == NULL) {
00520         fprintf(dd->err, "Cannot subset, nil object\n");
00521         return(NULL);
00522     }
00523 
00524     if (Cudd_IsConstant(f)) {
00525         return(f);
00526     }
00527 
00528     /* Create table where node data are accessible via a hash table. */
00529     info = gatherInfo(dd, f, numVars, safe);
00530     if (info == NULL) {
00531         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00532         dd->errorCode = CUDD_MEMORY_OUT;
00533         return(NULL);
00534     }
00535 
00536     /* Mark nodes that should be replaced by zero. */
00537     result = UAmarkNodes(dd, f, info, threshold, safe, quality);
00538     if (result == 0) {
00539         (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
00540         FREE(info->page);
00541         st_free_table(info->table);
00542         FREE(info);
00543         dd->errorCode = CUDD_MEMORY_OUT;
00544         return(NULL);
00545     }
00546 
00547     /* Build the result. */
00548     subset = UAbuildSubset(dd, f, info);
00549 #if 1
00550     if (subset && info->size < Cudd_DagSize(subset))
00551         (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
00552                        info->size, Cudd_DagSize(subset));
00553 #endif
00554     FREE(info->page);
00555     st_free_table(info->table);
00556     FREE(info);
00557 
00558 #ifdef DD_DEBUG
00559     if (subset != NULL) {
00560         cuddRef(subset);
00561 #if 0
00562         (void) Cudd_DebugCheck(dd);
00563         (void) Cudd_CheckKeys(dd);
00564 #endif
00565         if (!Cudd_bddLeq(dd, subset, f)) {
00566             (void) fprintf(dd->err, "Wrong subset\n");
00567             dd->errorCode = CUDD_INTERNAL_ERROR;
00568         }
00569         cuddDeref(subset);
00570     }
00571 #endif
00572     return(subset);
00573 
00574 } /* 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 903 of file cuddApprox.c.

00908 {
00909     ApproxInfo  *info;
00910     NodeData *infoTop;
00911 
00912     /* If user did not give numVars value, set it to the maximum
00913     ** exponent that the pow function can take. The -1 is due to the
00914     ** discrepancy in the value that pow takes and the value that
00915     ** log gives.
00916     */
00917     if (numVars == 0) {
00918         numVars = DBL_MAX_EXP - 1;
00919     }
00920 
00921     info = ALLOC(ApproxInfo,1);
00922     if (info == NULL) {
00923         dd->errorCode = CUDD_MEMORY_OUT;
00924         return(NULL);
00925     }
00926     info->max = pow(2.0,(double) numVars);
00927     info->one = DD_ONE(dd);
00928     info->zero = Cudd_Not(info->one);
00929     info->size = Cudd_DagSize(node);
00930     /* All the information gathered will be stored in a contiguous
00931     ** piece of memory, which is allocated here. This can be done
00932     ** efficiently because we have counted the number of nodes of the
00933     ** BDD. info->index points to the next available entry in the array
00934     ** that stores the per-node information. */
00935     info->page = ALLOC(NodeData,info->size);
00936     if (info->page == NULL) {
00937         dd->errorCode = CUDD_MEMORY_OUT;
00938         FREE(info);
00939         return(NULL);
00940     }
00941     memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
00942     info->table = st_init_table(st_ptrcmp,st_ptrhash);
00943     if (info->table == NULL) {
00944         FREE(info->page);
00945         FREE(info);
00946         return(NULL);
00947     }
00948     /* We visit the DAG in post-order DFS. Hence, the constant node is
00949     ** in first position, and the root of the DAG is in last position. */
00950 
00951     /* Info for the constant node: Initialize only fields different from 0. */
00952     if (st_insert(info->table, (char *)info->one, (char *)info->page) == ST_OUT_OF_MEM) {
00953         FREE(info->page);
00954         FREE(info);
00955         st_free_table(info->table);
00956         return(NULL);
00957     }
00958     info->page[0].mintermsP = info->max;
00959     info->index = 1;
00960 
00961     infoTop = gatherInfoAux(node,info,parity);
00962     if (infoTop == NULL) {
00963         FREE(info->page);
00964         st_free_table(info->table);
00965         FREE(info);
00966         return(NULL);
00967     }
00968     if (Cudd_IsComplement(node)) {
00969         info->minterms = infoTop->mintermsN;
00970     } else {
00971         info->minterms = infoTop->mintermsP;
00972     }
00973 
00974     infoTop->functionRef = 1;
00975     return(info);
00976 
00977 } /* 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 833 of file cuddApprox.c.

00837 {
00838     DdNode      *N, *Nt, *Ne;
00839     NodeData    *infoN, *infoT, *infoE;
00840 
00841     N = Cudd_Regular(node);
00842 
00843     /* Check whether entry for this node exists. */
00844     if (st_lookup(info->table, N, &infoN)) {
00845         if (parity) {
00846             /* Update parity and propagate. */
00847             updateParity(N, info, 1 +  (int) Cudd_IsComplement(node));
00848         }
00849         return(infoN);
00850     }
00851 
00852     /* Compute the cofactors. */
00853     Nt = Cudd_NotCond(cuddT(N), N != node);
00854     Ne = Cudd_NotCond(cuddE(N), N != node);
00855 
00856     infoT = gatherInfoAux(Nt, info, parity);
00857     if (infoT == NULL) return(NULL);
00858     infoE = gatherInfoAux(Ne, info, parity);
00859     if (infoE == NULL) return(NULL);
00860 
00861     infoT->functionRef++;
00862     infoE->functionRef++;
00863 
00864     /* Point to the correct location in the page. */
00865     infoN = &(info->page[info->index++]);
00866     infoN->parity |= (short) (1 + Cudd_IsComplement(node));
00867 
00868     infoN->mintermsP = infoT->mintermsP/2;
00869     infoN->mintermsN = infoT->mintermsN/2;
00870     if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
00871         infoN->mintermsP += infoE->mintermsN/2;
00872         infoN->mintermsN += infoE->mintermsP/2;
00873     } else {
00874         infoN->mintermsP += infoE->mintermsP/2;
00875         infoN->mintermsN += infoE->mintermsN/2;
00876     }
00877 
00878     /* Insert entry for the node in the table. */
00879     if (st_insert(info->table,(char *)N, (char *)infoN) == ST_OUT_OF_MEM) {
00880         return(NULL);
00881     }
00882     return(infoN);
00883 
00884 } /* 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 1986 of file cuddApprox.c.

01990 {
01991     DdNode *Nt, *Ne, *N, *t, *e, *r;
01992     NodeData *infoN;
01993 
01994     if (Cudd_IsConstant(node))
01995         return(node);
01996 
01997     N = Cudd_Regular(node);
01998 
01999     Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
02000     Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
02001 
02002     if (st_lookup(info->table, N, &infoN)) {
02003         if (N == node ) {
02004             if (infoN->resultP != NULL) {
02005                 return(infoN->resultP);
02006             }
02007         } else {
02008             if (infoN->resultN != NULL) {
02009                 return(infoN->resultN);
02010             }
02011         }
02012         if (infoN->replace == REPLACE_T) {
02013             r = RAbuildSubset(dd, Ne, info);
02014             return(r);
02015         } else if (infoN->replace == REPLACE_E) {
02016             r = RAbuildSubset(dd, Nt, info);
02017             return(r);
02018         } else if (infoN->replace == REPLACE_N) {
02019             return(info->zero);
02020         } else if (infoN->replace == REPLACE_TT) {
02021             DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
02022                                        Cudd_IsComplement(node));
02023             int index = cuddT(N)->index;
02024             e = info->zero;
02025             t = RAbuildSubset(dd, Ntt, info);
02026             if (t == NULL) {
02027                 return(NULL);
02028             }
02029             cuddRef(t);
02030             if (Cudd_IsComplement(t)) {
02031                 t = Cudd_Not(t);
02032                 e = Cudd_Not(e);
02033                 r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
02034                 if (r == NULL) {
02035                     Cudd_RecursiveDeref(dd, t);
02036                     return(NULL);
02037                 }
02038                 r = Cudd_Not(r);
02039             } else {
02040                 r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
02041                 if (r == NULL) {
02042                     Cudd_RecursiveDeref(dd, t);
02043                     return(NULL);
02044                 }
02045             }
02046             cuddDeref(t);
02047             return(r);
02048         } else if (infoN->replace == REPLACE_TE) {
02049             DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
02050                                        Cudd_IsComplement(node));
02051             int index = cuddT(N)->index;
02052             t = info->one;
02053             e = RAbuildSubset(dd, Nte, info);
02054             if (e == NULL) {
02055                 return(NULL);
02056             }
02057             cuddRef(e);
02058             e = Cudd_Not(e);
02059             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
02060             if (r == NULL) {
02061                 Cudd_RecursiveDeref(dd, e);
02062                 return(NULL);
02063             }
02064             r =Cudd_Not(r);
02065             cuddDeref(e);
02066             return(r);
02067         }
02068     } else {
02069         (void) fprintf(dd->err,
02070                        "Something is wrong, ought to be in info table\n");
02071         dd->errorCode = CUDD_INTERNAL_ERROR;
02072         return(NULL);
02073     }
02074 
02075     t = RAbuildSubset(dd, Nt, info);
02076     if (t == NULL) {
02077         return(NULL);
02078     }
02079     cuddRef(t);
02080 
02081     e = RAbuildSubset(dd, Ne, info);
02082     if (e == NULL) {
02083         Cudd_RecursiveDeref(dd,t);
02084         return(NULL);
02085     }
02086     cuddRef(e);
02087 
02088     if (Cudd_IsComplement(t)) {
02089         t = Cudd_Not(t);
02090         e = Cudd_Not(e);
02091         r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
02092         if (r == NULL) {
02093             Cudd_RecursiveDeref(dd, e);
02094             Cudd_RecursiveDeref(dd, t);
02095             return(NULL);
02096         }
02097         r = Cudd_Not(r);
02098     } else {
02099         r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
02100         if (r == NULL) {
02101             Cudd_RecursiveDeref(dd, e);
02102             Cudd_RecursiveDeref(dd, t);
02103             return(NULL);
02104         }
02105     }
02106     cuddDeref(t);
02107     cuddDeref(e);
02108 
02109     if (N == node) {
02110         infoN->resultP = r;
02111     } else {
02112         infoN->resultN = r;
02113     }
02114 
02115     return(r);
02116 
02117 } /* 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 1367 of file cuddApprox.c.

01373 {
01374     DdLevelQueue *queue;
01375     DdLevelQueue *localQueue;
01376     NodeData *infoN, *infoT, *infoE;
01377     GlobalQueueItem *item;
01378     DdNode *node, *T, *E;
01379     DdNode *shared; /* grandchild shared by the two children of node */
01380     double numOnset;
01381     double impact, impactP, impactN;
01382     double minterms;
01383     int savings;
01384     int replace;
01385 
01386 #if 0
01387     (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
01388                   info->size, info->minterms);
01389 #endif
01390     queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
01391     if (queue == NULL) {
01392         return(0);
01393     }
01394     localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
01395                                     dd->initSlots);
01396     if (localQueue == NULL) {
01397         cuddLevelQueueQuit(queue);
01398         return(0);
01399     }
01400     /* Enqueue regular pointer to root and initialize impact. */
01401     node = Cudd_Regular(f);
01402     item = (GlobalQueueItem *)
01403         cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
01404     if (item == NULL) {
01405         cuddLevelQueueQuit(queue);
01406         cuddLevelQueueQuit(localQueue);
01407         return(0);
01408     }
01409     if (Cudd_IsComplement(f)) {
01410         item->impactP = 0.0;
01411         item->impactN = 1.0;
01412     } else {
01413         item->impactP = 1.0;
01414         item->impactN = 0.0;
01415     }
01416     /* The nodes retrieved here are guaranteed to be non-terminal.
01417     ** The initial node is not terminal because constant nodes are
01418     ** dealt with in the calling procedure. Subsequent nodes are inserted
01419     ** only if they are not terminal. */
01420     while (queue->first != NULL) {
01421         /* If the size of the subset is below the threshold, quit. */
01422         if (info->size <= threshold)
01423             break;
01424         item = (GlobalQueueItem *) queue->first;
01425         node = item->node;
01426 #ifdef DD_DEBUG
01427         assert(item->impactP >= 0 && item->impactP <= 1.0);
01428         assert(item->impactN >= 0 && item->impactN <= 1.0);
01429         assert(!Cudd_IsComplement(node));
01430         assert(!Cudd_IsConstant(node));
01431 #endif
01432         if (!st_lookup(info->table, node, &infoN)) {
01433             cuddLevelQueueQuit(queue);
01434             cuddLevelQueueQuit(localQueue);
01435             return(0);
01436         }
01437 #ifdef DD_DEBUG
01438         assert(infoN->parity >= 1 && infoN->parity <= 3);
01439 #endif
01440         if (infoN->parity == 3) {
01441             /* This node can be reached through paths of different parity.
01442             ** It is not safe to replace it, because remapping will give
01443             ** an incorrect result, while replacement by 0 may cause node
01444             ** splitting. */
01445             cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01446             continue;
01447         }
01448         T = cuddT(node);
01449         E = cuddE(node);
01450         shared = NULL;
01451         impactP = item->impactP;
01452         impactN = item->impactN;
01453         if (Cudd_bddLeq(dd,T,E)) {
01454             /* Here we know that E is regular. */
01455 #ifdef DD_DEBUG
01456             assert(!Cudd_IsComplement(E));
01457 #endif
01458             (void) st_lookup(info->table, T, &infoT);
01459             (void) st_lookup(info->table, E, &infoE);
01460             if (infoN->parity == 1) {
01461                 impact = impactP;
01462                 minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
01463                 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
01464                     savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
01465                     if (savings == 1) {
01466                         cuddLevelQueueQuit(queue);
01467                         cuddLevelQueueQuit(localQueue);
01468                         return(0);
01469                     }
01470                 } else {
01471                     savings = 1;
01472                 }
01473                 replace = REPLACE_E;
01474             } else {
01475 #ifdef DD_DEBUG
01476                 assert(infoN->parity == 2);
01477 #endif
01478                 impact = impactN;
01479                 minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
01480                 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
01481                     savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
01482                     if (savings == 1) {
01483                         cuddLevelQueueQuit(queue);
01484                         cuddLevelQueueQuit(localQueue);
01485                         return(0);
01486                     }
01487                 } else {
01488                     savings = 1;
01489                 }
01490                 replace = REPLACE_T;
01491             }
01492             numOnset = impact * minterms;
01493         } else if (Cudd_bddLeq(dd,E,T)) {
01494             /* Here E may be complemented. */
01495             DdNode *Ereg = Cudd_Regular(E);
01496             (void) st_lookup(info->table, T, &infoT);
01497             (void) st_lookup(info->table, Ereg, &infoE);
01498             if (infoN->parity == 1) {
01499                 impact = impactP;
01500                 minterms = infoT->mintermsP/2.0 -
01501                     ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
01502                 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
01503                     savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
01504                     if (savings == 1) {
01505                         cuddLevelQueueQuit(queue);
01506                         cuddLevelQueueQuit(localQueue);
01507                         return(0);
01508                     }
01509                 } else {
01510                     savings = 1;
01511                 }
01512                 replace = REPLACE_T;
01513             } else {
01514 #ifdef DD_DEBUG
01515                 assert(infoN->parity == 2);
01516 #endif
01517                 impact = impactN;
01518                 minterms = ((E == Ereg) ? infoE->mintermsN :
01519                             infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
01520                 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
01521                     savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
01522                     if (savings == 1) {
01523                         cuddLevelQueueQuit(queue);
01524                         cuddLevelQueueQuit(localQueue);
01525                         return(0);
01526                     }
01527                 } else {
01528                     savings = 1;
01529                 }
01530                 replace = REPLACE_E;
01531             }
01532             numOnset = impact * minterms;
01533         } else {
01534             DdNode *Ereg = Cudd_Regular(E);
01535             DdNode *TT = cuddT(T);
01536             DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
01537             if (T->index == Ereg->index && TT == ET) {
01538                 shared = TT;
01539                 replace = REPLACE_TT;
01540             } else {
01541                 DdNode *TE = cuddE(T);
01542                 DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
01543                 if (T->index == Ereg->index && TE == EE) {
01544                     shared = TE;
01545                     replace = REPLACE_TE;
01546                 } else {
01547                     replace = REPLACE_N;
01548                 }
01549             }
01550             numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
01551             savings = computeSavings(dd,node,shared,info,localQueue);
01552             if (shared != NULL) {
01553                 NodeData *infoS;
01554                 (void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
01555                 if (Cudd_IsComplement(shared)) {
01556                     numOnset -= (infoS->mintermsN * impactP +
01557                         infoS->mintermsP * impactN)/2.0;
01558                 } else {
01559                     numOnset -= (infoS->mintermsP * impactP +
01560                         infoS->mintermsN * impactN)/2.0;
01561                 }
01562                 savings--;
01563             }
01564         }
01565 
01566         cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01567 #if 0
01568         if (replace == REPLACE_T || replace == REPLACE_E)
01569             (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
01570                           node, impact, numOnset, savings);
01571         else
01572             (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
01573                           node, impactP, impactN, numOnset, savings);
01574 #endif
01575         if ((1 - numOnset / info->minterms) >
01576             quality * (1 - (double) savings / info->size)) {
01577             infoN->replace = (char) replace;
01578             info->size -= savings;
01579             info->minterms -=numOnset;
01580 #if 0
01581             (void) printf("remap(%d): new size = %d new minterms = %g\n",
01582                           replace, info->size, info->minterms);
01583 #endif
01584             if (replace == REPLACE_N) {
01585                 savings -= updateRefs(dd,node,NULL,info,localQueue);
01586             } else if (replace == REPLACE_T) {
01587                 savings -= updateRefs(dd,node,E,info,localQueue);
01588             } else if (replace == REPLACE_E) {
01589                 savings -= updateRefs(dd,node,T,info,localQueue);
01590             } else {
01591 #ifdef DD_DEBUG
01592                 assert(replace == REPLACE_TT || replace == REPLACE_TE);
01593 #endif
01594                 savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
01595             }
01596             assert(savings == 0);
01597         } else {
01598             replace = NOTHING;
01599         }
01600         if (replace == REPLACE_N) continue;
01601         if ((replace == REPLACE_E || replace == NOTHING) &&
01602             !cuddIsConstant(cuddT(node))) {
01603             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
01604                                          cuddI(dd,cuddT(node)->index));
01605             if (replace == REPLACE_E) {
01606                 item->impactP += impactP;
01607                 item->impactN += impactN;
01608             } else {
01609                 item->impactP += impactP/2.0;
01610                 item->impactN += impactN/2.0;
01611             }
01612         }
01613         if ((replace == REPLACE_T || replace == NOTHING) &&
01614             !Cudd_IsConstant(cuddE(node))) {
01615             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
01616                                          cuddI(dd,Cudd_Regular(cuddE(node))->index));
01617             if (Cudd_IsComplement(cuddE(node))) {
01618                 if (replace == REPLACE_T) {
01619                     item->impactP += impactN;
01620                     item->impactN += impactP;
01621                 } else {
01622                     item->impactP += impactN/2.0;
01623                     item->impactN += impactP/2.0;
01624                 }
01625             } else {
01626                 if (replace == REPLACE_T) {
01627                     item->impactP += impactP;
01628                     item->impactN += impactN;
01629                 } else {
01630                     item->impactP += impactP/2.0;
01631                     item->impactN += impactN/2.0;
01632                 }
01633             }
01634         }
01635         if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
01636             !Cudd_IsConstant(shared)) {
01637             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
01638                                          cuddI(dd,Cudd_Regular(shared)->index));
01639             if (Cudd_IsComplement(shared)) {
01640                 item->impactP += impactN;
01641                 item->impactN += impactP;
01642             } else {
01643                 item->impactP += impactP;
01644                 item->impactN += impactN;
01645             }
01646         }
01647     }
01648 
01649     cuddLevelQueueQuit(queue);
01650     cuddLevelQueueQuit(localQueue);
01651     return(1);
01652 
01653 } /* 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 1272 of file cuddApprox.c.

01276 {
01277 
01278     DdNode *Nt, *Ne, *N, *t, *e, *r;
01279     NodeData *infoN;
01280 
01281     if (Cudd_IsConstant(node))
01282         return(node);
01283 
01284     N = Cudd_Regular(node);
01285 
01286     if (st_lookup(info->table, N, &infoN)) {
01287         if (infoN->replace == TRUE) {
01288             return(info->zero);
01289         }
01290         if (N == node ) {
01291             if (infoN->resultP != NULL) {
01292                 return(infoN->resultP);
01293             }
01294         } else {
01295             if (infoN->resultN != NULL) {
01296                 return(infoN->resultN);
01297             }
01298         }
01299     } else {
01300         (void) fprintf(dd->err,
01301                        "Something is wrong, ought to be in info table\n");
01302         dd->errorCode = CUDD_INTERNAL_ERROR;
01303         return(NULL);
01304     }
01305 
01306     Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
01307     Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
01308 
01309     t = UAbuildSubset(dd, Nt, info);
01310     if (t == NULL) {
01311         return(NULL);
01312     }
01313     cuddRef(t);
01314 
01315     e = UAbuildSubset(dd, Ne, info);
01316     if (e == NULL) {
01317         Cudd_RecursiveDeref(dd,t);
01318         return(NULL);
01319     }
01320     cuddRef(e);
01321 
01322     if (Cudd_IsComplement(t)) {
01323         t = Cudd_Not(t);
01324         e = Cudd_Not(e);
01325         r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
01326         if (r == NULL) {
01327             Cudd_RecursiveDeref(dd, e);
01328             Cudd_RecursiveDeref(dd, t);
01329             return(NULL);
01330         }
01331         r = Cudd_Not(r);
01332     } else {
01333         r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
01334         if (r == NULL) {
01335             Cudd_RecursiveDeref(dd, e);
01336             Cudd_RecursiveDeref(dd, t);
01337             return(NULL);
01338         }
01339     }
01340     cuddDeref(t);
01341     cuddDeref(e);
01342 
01343     if (N == node) {
01344         infoN->resultP = r;
01345     } else {
01346         infoN->resultN = r;
01347     }
01348 
01349     return(r);
01350 
01351 } /* 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 1148 of file cuddApprox.c.

01155 {
01156     DdLevelQueue *queue;
01157     DdLevelQueue *localQueue;
01158     NodeData *infoN;
01159     GlobalQueueItem *item;
01160     DdNode *node;
01161     double numOnset;
01162     double impactP, impactN;
01163     int savings;
01164 
01165 #if 0
01166     (void) printf("initial size = %d initial minterms = %g\n",
01167                   info->size, info->minterms);
01168 #endif
01169     queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
01170     if (queue == NULL) {
01171         return(0);
01172     }
01173     localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
01174                                     dd->initSlots);
01175     if (localQueue == NULL) {
01176         cuddLevelQueueQuit(queue);
01177         return(0);
01178     }
01179     node = Cudd_Regular(f);
01180     item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
01181     if (item == NULL) {
01182         cuddLevelQueueQuit(queue);
01183         cuddLevelQueueQuit(localQueue);
01184         return(0);
01185     }
01186     if (Cudd_IsComplement(f)) {
01187         item->impactP = 0.0;
01188         item->impactN = 1.0;
01189     } else {
01190         item->impactP = 1.0;
01191         item->impactN = 0.0;
01192     }
01193     while (queue->first != NULL) {
01194         /* If the size of the subset is below the threshold, quit. */
01195         if (info->size <= threshold)
01196             break;
01197         item = (GlobalQueueItem *) queue->first;
01198         node = item->node;
01199         node = Cudd_Regular(node);
01200         (void) st_lookup(info->table, node, &infoN);
01201         if (safe && infoN->parity == 3) {
01202             cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01203             continue;
01204         }
01205         impactP = item->impactP;
01206         impactN = item->impactN;
01207         numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
01208         savings = computeSavings(dd,node,NULL,info,localQueue);
01209         if (savings == 0) {
01210             cuddLevelQueueQuit(queue);
01211             cuddLevelQueueQuit(localQueue);
01212             return(0);
01213         }
01214         cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01215 #if 0
01216         (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
01217                       node, impactP, impactN, numOnset, savings);
01218 #endif
01219         if ((1 - numOnset / info->minterms) >
01220             quality * (1 - (double) savings / info->size)) {
01221             infoN->replace = TRUE;
01222             info->size -= savings;
01223             info->minterms -=numOnset;
01224 #if 0
01225             (void) printf("replace: new size = %d new minterms = %g\n",
01226                           info->size, info->minterms);
01227 #endif
01228             savings -= updateRefs(dd,node,NULL,info,localQueue);
01229             assert(savings == 0);
01230             continue;
01231         }
01232         if (!cuddIsConstant(cuddT(node))) {
01233             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
01234                                          cuddI(dd,cuddT(node)->index));
01235             item->impactP += impactP/2.0;
01236             item->impactN += impactN/2.0;
01237         }
01238         if (!Cudd_IsConstant(cuddE(node))) {
01239             item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
01240                                          cuddI(dd,Cudd_Regular(cuddE(node))->index));
01241             if (Cudd_IsComplement(cuddE(node))) {
01242                 item->impactP += impactN/2.0;
01243                 item->impactN += impactP/2.0;
01244             } else {
01245                 item->impactP += impactP/2.0;
01246                 item->impactN += impactN/2.0;
01247             }
01248         }
01249     }
01250 
01251     cuddLevelQueueQuit(queue);
01252     cuddLevelQueueQuit(localQueue);
01253     return(1);
01254 
01255 } /* end of UAmarkNodes */

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

AutomaticStart

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 791 of file cuddApprox.c.

00795 {
00796     NodeData *infoN;
00797     DdNode *E;
00798 
00799     if (!st_lookup(info->table, node, &infoN)) return;
00800     if ((infoN->parity & newparity) != 0) return;
00801     infoN->parity |= (short) newparity;
00802     if (Cudd_IsConstant(node)) return;
00803     updateParity(cuddT(node),info,newparity);
00804     E = cuddE(node);
00805     if (Cudd_IsComplement(E)) {
00806         updateParity(Cudd_Not(E),info,3-newparity);
00807     } else {
00808         updateParity(E,info,newparity);
00809     }
00810     return;
00811 
00812 } /* 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 1069 of file cuddApprox.c.

01075 {
01076     NodeData *infoN;
01077     LocalQueueItem *item;
01078     DdNode *node;
01079     int savings = 0;
01080 
01081     node = Cudd_Regular(f);
01082     /* Insert the given node in the level queue. Its function reference
01083     ** count is set equal to 0 so that the search will continue from it
01084     ** when it is retrieved. */
01085     item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
01086     if (item == NULL)
01087         return(0);
01088     (void) st_lookup(info->table, node, &infoN);
01089     infoN->functionRef = 0;
01090 
01091     if (skip != NULL) {
01092         /* Increase the function reference count of the node to be skipped
01093         ** by 1 to account for the node pointing to it that will be created. */
01094         skip = Cudd_Regular(skip);
01095         (void) st_lookup(info->table, skip, &infoN);
01096         infoN->functionRef++;
01097     }
01098 
01099     /* Process the queue. */
01100     while (queue->first != NULL) {
01101         item = (LocalQueueItem *) queue->first;
01102         node = item->node;
01103         cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
01104         (void) st_lookup(info->table, node, &infoN);
01105         if (infoN->functionRef != 0) {
01106             /* This node is shared or must be skipped. */
01107             continue;
01108         }
01109         savings++;
01110         if (!cuddIsConstant(cuddT(node))) {
01111             item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
01112                                          cuddI(dd,cuddT(node)->index));
01113             if (item == NULL) return(0);
01114             (void) st_lookup(info->table, cuddT(node), &infoN);
01115             infoN->functionRef--;
01116         }
01117         if (!Cudd_IsConstant(cuddE(node))) {
01118             item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
01119                                          cuddI(dd,Cudd_Regular(cuddE(node))->index));
01120             if (item == NULL) return(0);
01121             (void) st_lookup(info->table, Cudd_Regular(cuddE(node)), &infoN);
01122             infoN->functionRef--;
01123         }
01124     }
01125 
01126 #ifdef DD_DEBUG
01127     /* At the end of a local search the queue should be empty. */
01128     assert(queue->size == 0);
01129 #endif
01130     return(savings);
01131 
01132 } /* end of updateRefs */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $" [static]

Definition at line 167 of file cuddApprox.c.

Generated on Tue Jan 12 13:57:18 2010 for glu-2.2 by  doxygen 1.6.1