diff options
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddApprox.c')
| -rw-r--r-- | abc70930/src/bdd/cudd/cuddApprox.c | 2192 |
1 files changed, 0 insertions, 2192 deletions
diff --git a/abc70930/src/bdd/cudd/cuddApprox.c b/abc70930/src/bdd/cudd/cuddApprox.c deleted file mode 100644 index debcf48b..00000000 --- a/abc70930/src/bdd/cudd/cuddApprox.c +++ /dev/null @@ -1,2192 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddApprox.c] - - PackageName [cudd] - - Synopsis [Procedures to approximate a given BDD.] - - Description [External procedures provided by this module: - <ul> - <li> Cudd_UnderApprox() - <li> Cudd_OverApprox() - <li> Cudd_RemapUnderApprox() - <li> Cudd_RemapOverApprox() - <li> Cudd_BiasedUnderApprox() - <li> Cudd_BiasedOverApprox() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddUnderApprox() - <li> cuddRemapUnderApprox() - <li> cuddBiasedUnderApprox() - </ul> - Static procedures included in this module: - <ul> - <li> gatherInfoAux() - <li> gatherInfo() - <li> computeSavings() - <li> UAmarkNodes() - <li> UAbuildSubset() - <li> updateRefs() - <li> RAmarkNodes() - <li> BAmarkNodes() - <li> RAbuildSubset() - </ul> - ] - - 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.] - -******************************************************************************/ - -#ifdef __STDC__ -#include <float.h> -#else -#define DBL_MAX_EXP 1024 -#endif -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -#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 - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/* Data structure to store the information on each node. It keeps the -** number of minterms of the function rooted at this node in terms of -** the number of variables specified by the user; the number of -** minterms of the complement; the impact of the number of minterms of -** this function on the number of minterms of the root function; the -** reference count of the node from within the root function; the -** reference count of the node from an internal node; and the flag -** that says whether the node should be replaced and how. */ -typedef struct NodeData { - double mintermsP; /* minterms for the regular node */ - double mintermsN; /* minterms for the complemented node */ - int functionRef; /* references from within this function */ - char care; /* node intersects care set */ - char replace; /* replacement decision */ - short int parity; /* 1: even; 2: odd; 3: both */ - DdNode *resultP; /* result for even parity */ - DdNode *resultN; /* result for odd parity */ -} NodeData; - -typedef struct ApproxInfo { - DdNode *one; /* one constant */ - DdNode *zero; /* BDD zero constant */ - NodeData *page; /* per-node information */ - st_table *table; /* hash table to access the per-node info */ - int index; /* index of the current node */ - double max; /* max number of minterms */ - int size; /* how many nodes are left */ - double minterms; /* how many minterms are left */ -} ApproxInfo; - -/* Item of the queue used in the levelized traversal of the BDD. */ -#ifdef __osf__ -#pragma pointer_size save -#pragma pointer_size short -#endif -typedef struct GlobalQueueItem { - struct GlobalQueueItem *next; - struct GlobalQueueItem *cnext; - DdNode *node; - double impactP; - double impactN; -} GlobalQueueItem; - -typedef struct LocalQueueItem { - struct LocalQueueItem *next; - struct LocalQueueItem *cnext; - DdNode *node; - int localRef; -} LocalQueueItem; -#ifdef __osf__ -#pragma pointer_size restore -#endif - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -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 updateRefs 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 DdNode * RAbuildSubset ARGS((DdManager *dd, DdNode *node, ApproxInfo *info)); -static int BAapplyBias ARGS((DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**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] - -******************************************************************************/ -DdNode * -Cudd_UnderApprox( - DdManager * dd /* manager */, - DdNode * f /* function to be subset */, - int numVars /* number of variables in the support of f */, - int threshold /* when to stop approximation */, - int safe /* enforce safe approximation */, - double quality /* minimum improvement for accepted changes */) -{ - DdNode *subset; - - do { - dd->reordered = 0; - subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality); - } while (dd->reordered == 1); - - return(subset); - -} /* end of Cudd_UnderApprox */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_OverApprox( - DdManager * dd /* manager */, - DdNode * f /* function to be superset */, - int numVars /* number of variables in the support of f */, - int threshold /* when to stop approximation */, - int safe /* enforce safe approximation */, - double quality /* minimum improvement for accepted changes */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_RemapUnderApprox( - DdManager * dd /* manager */, - DdNode * f /* function to be subset */, - int numVars /* number of variables in the support of f */, - int threshold /* when to stop approximation */, - double quality /* minimum improvement for accepted changes */) -{ - DdNode *subset; - - do { - dd->reordered = 0; - subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality); - } while (dd->reordered == 1); - - return(subset); - -} /* end of Cudd_RemapUnderApprox */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_RemapOverApprox( - DdManager * dd /* manager */, - DdNode * f /* function to be superset */, - int numVars /* number of variables in the support of f */, - int threshold /* when to stop approximation */, - double quality /* minimum improvement for accepted changes */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_BiasedUnderApprox( - DdManager *dd /* manager */, - DdNode *f /* function to be subset */, - DdNode *b /* bias function */, - int numVars /* number of variables in the support of f */, - int threshold /* when to stop approximation */, - double quality1 /* minimum improvement for accepted changes when b=1 */, - double quality0 /* minimum improvement for accepted changes when b=0 */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_BiasedOverApprox( - DdManager *dd /* manager */, - DdNode *f /* function to be superset */, - DdNode *b /* bias function */, - int numVars /* number of variables in the support of f */, - int threshold /* when to stop approximation */, - double quality1 /* minimum improvement for accepted changes when b=1*/, - double quality0 /* minimum improvement for accepted changes when b=0 */) -{ - 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 */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Applies Tom Shiple's underappoximation algorithm.] - - Description [Applies Tom Shiple's underappoximation algorithm. Proceeds - in three phases: - <ul> - <li> collect information on each node in the BDD; this is done via DFS. - <li> traverse the BDD in top-down fashion and compute for each node - whether its elimination increases density. - <li> traverse the BDD via DFS and actually perform the elimination. - </ul> - Returns the approximated BDD if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_UnderApprox] - -******************************************************************************/ -DdNode * -cuddUnderApprox( - DdManager * dd /* DD manager */, - DdNode * f /* current DD */, - int numVars /* maximum number of variables */, - int threshold /* threshold under which approximation stops */, - int safe /* enforce safe approximation */, - double quality /* minimum improvement for accepted changes */) -{ - 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 */ - - -/**Function******************************************************************** - - Synopsis [Applies the remapping underappoximation algorithm.] - - Description [Applies the remapping underappoximation algorithm. - Proceeds in three phases: - <ul> - <li> collect information on each node in the BDD; this is done via DFS. - <li> traverse the BDD in top-down fashion and compute for each node - whether remapping increases density. - <li> traverse the BDD via DFS and actually perform the elimination. - </ul> - Returns the approximated BDD if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_RemapUnderApprox] - -******************************************************************************/ -DdNode * -cuddRemapUnderApprox( - DdManager * dd /* DD manager */, - DdNode * f /* current DD */, - int numVars /* maximum number of variables */, - int threshold /* threshold under which approximation stops */, - double quality /* minimum improvement for accepted changes */) -{ - 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 */ - - -/**Function******************************************************************** - - Synopsis [Applies the biased remapping underappoximation algorithm.] - - Description [Applies the biased remapping underappoximation algorithm. - Proceeds in three phases: - <ul> - <li> collect information on each node in the BDD; this is done via DFS. - <li> traverse the BDD in top-down fashion and compute for each node - whether remapping increases density. - <li> traverse the BDD via DFS and actually perform the elimination. - </ul> - Returns the approximated BDD if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_BiasedUnderApprox] - -******************************************************************************/ -DdNode * -cuddBiasedUnderApprox( - DdManager *dd /* DD manager */, - DdNode *f /* current DD */, - DdNode *b /* bias function */, - int numVars /* maximum number of variables */, - int threshold /* threshold under which approximation stops */, - double quality1 /* minimum improvement for accepted changes when b=1 */, - double quality0 /* minimum improvement for accepted changes when b=1 */) -{ - 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 */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**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] - -******************************************************************************/ -static void -updateParity( - DdNode * node /* function to analyze */, - ApproxInfo * info /* info on BDD */, - int newparity /* new parity for node */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static NodeData * -gatherInfoAux( - DdNode * node /* function to analyze */, - ApproxInfo * info /* info on BDD */, - int parity /* gather parity information */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static ApproxInfo * -gatherInfo( - DdManager * dd /* manager */, - DdNode * node /* function to be analyzed */, - int numVars /* number of variables node depends on */, - int parity /* gather parity information */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static int -computeSavings( - DdManager * dd, - DdNode * f, - DdNode * skip, - ApproxInfo * info, - DdLevelQueue * queue) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static int -updateRefs( - DdManager * dd, - DdNode * f, - DdNode * skip, - ApproxInfo * info, - DdLevelQueue * queue) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static int -UAmarkNodes( - DdManager * dd /* manager */, - DdNode * f /* function to be analyzed */, - ApproxInfo * info /* info on BDD */, - int threshold /* when to stop approximating */, - int safe /* enforce safe approximation */, - double quality /* minimum improvement for accepted changes */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static DdNode * -UAbuildSubset( - DdManager * dd /* DD manager */, - DdNode * node /* current node */, - ApproxInfo * info /* node info */) -{ - - 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 */ - - -/**Function******************************************************************** - - Synopsis [Marks nodes for remapping.] - - Description [Marks nodes for remapping. Returns 1 if successful; 0 - otherwise.] - - SideEffects [None] - - SeeAlso [cuddRemapUnderApprox] - -******************************************************************************/ -static int -RAmarkNodes( - DdManager * dd /* manager */, - DdNode * f /* function to be analyzed */, - ApproxInfo * info /* info on BDD */, - int threshold /* when to stop approximating */, - double quality /* minimum improvement for accepted changes */) -{ - 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 */ - - -/**Function******************************************************************** - - Synopsis [Marks nodes for remapping.] - - Description [Marks nodes for remapping. Returns 1 if successful; 0 - otherwise.] - - SideEffects [None] - - SeeAlso [cuddRemapUnderApprox] - -******************************************************************************/ -static int -BAmarkNodes( - DdManager *dd /* manager */, - DdNode *f /* function to be analyzed */, - ApproxInfo *info /* info on BDD */, - int threshold /* when to stop approximating */, - double quality1 /* minimum improvement for accepted changes when b=1 */, - double quality0 /* minimum improvement for accepted changes when b=0 */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static DdNode * -RAbuildSubset( - DdManager * dd /* DD manager */, - DdNode * node /* current node */, - ApproxInfo * info /* node info */) -{ - 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 */ - - -/**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] - -******************************************************************************/ -static int -BAapplyBias( - DdManager *dd, - DdNode *f, - DdNode *b, - ApproxInfo *info, - DdHashTable *cache) -{ - 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 */ |