From e7b544f11151f09a4a3fbe39b4a176795a82f677 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 13:42:25 -0800 Subject: Upgrade to the latest CUDD 2.4.2. --- src/bdd/cudd/cuddApprox.c | 1840 +++++++++++++++++++++++---------------------- 1 file changed, 928 insertions(+), 912 deletions(-) (limited to 'src/bdd/cudd/cuddApprox.c') diff --git a/src/bdd/cudd/cuddApprox.c b/src/bdd/cudd/cuddApprox.c index 9641aac0..1fdb595f 100644 --- a/src/bdd/cudd/cuddApprox.c +++ b/src/bdd/cudd/cuddApprox.c @@ -8,41 +8,68 @@ Description [External procedures provided by this module: - Internal procedures included in this module: - - Static procedures included in this module: - - ] +
  • Cudd_UnderApprox() +
  • Cudd_OverApprox() +
  • Cudd_RemapUnderApprox() +
  • Cudd_RemapOverApprox() +
  • Cudd_BiasedUnderApprox() +
  • Cudd_BiasedOverApprox() + + Internal procedures included in this module: + + Static procedures included in this module: + + ] 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.] + 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.] ******************************************************************************/ @@ -57,21 +84,22 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* 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 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 +#define DONT_CARE 0 +#define CARE 1 +#define TOTAL_CARE 2 +#define CARE_ERROR 3 /*---------------------------------------------------------------------------*/ /* Stucture declarations */ @@ -90,25 +118,25 @@ ABC_NAMESPACE_IMPL_START ** 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 */ + 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 */ + 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. */ @@ -140,7 +168,7 @@ typedef struct LocalQueueItem { /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -153,17 +181,17 @@ static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.1.1.1 2003/02/24 22:23:51 /* 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)); +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); /**AutomaticEnd***************************************************************/ @@ -208,8 +236,8 @@ Cudd_UnderApprox( DdNode *subset; do { - dd->reordered = 0; - subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality); + dd->reordered = 0; + subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality); } while (dd->reordered == 1); return(subset); @@ -256,8 +284,8 @@ Cudd_OverApprox( g = Cudd_Not(f); do { - dd->reordered = 0; - subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality); + dd->reordered = 0; + subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality); } while (dd->reordered == 1); return(Cudd_NotCond(subset, (subset != NULL))); @@ -299,8 +327,8 @@ Cudd_RemapUnderApprox( DdNode *subset; do { - dd->reordered = 0; - subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality); + dd->reordered = 0; + subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality); } while (dd->reordered == 1); return(subset); @@ -346,8 +374,8 @@ Cudd_RemapOverApprox( g = Cudd_Not(f); do { - dd->reordered = 0; - subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality); + dd->reordered = 0; + subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality); } while (dd->reordered == 1); return(Cudd_NotCond(subset, (subset != NULL))); @@ -394,9 +422,9 @@ Cudd_BiasedUnderApprox( DdNode *subset; do { - dd->reordered = 0; - subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1, - quality0); + dd->reordered = 0; + subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1, + quality0); } while (dd->reordered == 1); return(subset); @@ -445,9 +473,9 @@ Cudd_BiasedOverApprox( g = Cudd_Not(f); do { - dd->reordered = 0; - subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1, - quality0); + dd->reordered = 0; + subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1, + quality0); } while (dd->reordered == 1); return(Cudd_NotCond(subset, (subset != NULL))); @@ -493,39 +521,39 @@ cuddUnderApprox( int result; if (f == NULL) { - fprintf(dd->err, "Cannot subset, nil object\n"); - return(NULL); + fprintf(dd->err, "Cannot subset, nil object\n"); + return(NULL); } if (Cudd_IsConstant(f)) { - return(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); + (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"); - ABC_FREE(info->page); - st_free_table(info->table); - ABC_FREE(info); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n"); + ABC_FREE(info->page); + st_free_table(info->table); + ABC_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)); + (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n", + info->size, Cudd_DagSize(subset)); #endif ABC_FREE(info->page); st_free_table(info->table); @@ -533,16 +561,16 @@ cuddUnderApprox( #ifdef DD_DEBUG if (subset != NULL) { - cuddRef(subset); + cuddRef(subset); #if 0 - (void) Cudd_DebugCheck(dd); - (void) Cudd_CheckKeys(dd); + (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); + if (!Cudd_bddLeq(dd, subset, f)) { + (void) fprintf(dd->err, "Wrong subset\n"); + dd->errorCode = CUDD_INTERNAL_ERROR; + } + cuddDeref(subset); } #endif return(subset); @@ -582,40 +610,40 @@ cuddRemapUnderApprox( int result; if (f == NULL) { - fprintf(dd->err, "Cannot subset, nil object\n"); - dd->errorCode = CUDD_INVALID_ARG; - return(NULL); + fprintf(dd->err, "Cannot subset, nil object\n"); + dd->errorCode = CUDD_INVALID_ARG; + return(NULL); } if (Cudd_IsConstant(f)) { - return(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); + (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"); - ABC_FREE(info->page); - st_free_table(info->table); - ABC_FREE(info); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n"); + ABC_FREE(info->page); + st_free_table(info->table); + ABC_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)); + (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n", + info->size, Cudd_DagSize(subset)); #endif ABC_FREE(info->page); st_free_table(info->table); @@ -623,16 +651,16 @@ cuddRemapUnderApprox( #ifdef DD_DEBUG if (subset != NULL) { - cuddRef(subset); + cuddRef(subset); #if 0 - (void) Cudd_DebugCheck(dd); - (void) Cudd_CheckKeys(dd); + (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; + if (!Cudd_bddLeq(dd, subset, f)) { + (void) fprintf(dd->err, "Wrong subset\n"); + } + cuddDeref(subset); + dd->errorCode = CUDD_INTERNAL_ERROR; } #endif return(subset); @@ -667,61 +695,61 @@ cuddBiasedUnderApprox( 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 */) + double quality0 /* minimum improvement for accepted changes when b=0 */) { ApproxInfo *info; DdNode *subset; int result; - DdHashTable *cache; + DdHashTable *cache; if (f == NULL) { - fprintf(dd->err, "Cannot subset, nil object\n"); - dd->errorCode = CUDD_INVALID_ARG; - return(NULL); + fprintf(dd->err, "Cannot subset, nil object\n"); + dd->errorCode = CUDD_INVALID_ARG; + return(NULL); } if (Cudd_IsConstant(f)) { - return(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); + (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); - ABC_FREE(info->page); - st_free_table(info->table); - ABC_FREE(info); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n"); + cuddHashTableQuit(cache); + ABC_FREE(info->page); + st_free_table(info->table); + ABC_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"); - ABC_FREE(info->page); - st_free_table(info->table); - ABC_FREE(info); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n"); + ABC_FREE(info->page); + st_free_table(info->table); + ABC_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)); + (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n", + info->size, Cudd_DagSize(subset)); #endif ABC_FREE(info->page); st_free_table(info->table); @@ -729,16 +757,16 @@ cuddBiasedUnderApprox( #ifdef DD_DEBUG if (subset != NULL) { - cuddRef(subset); + cuddRef(subset); #if 0 - (void) Cudd_DebugCheck(dd); - (void) Cudd_CheckKeys(dd); + (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; + if (!Cudd_bddLeq(dd, subset, f)) { + (void) fprintf(dd->err, "Wrong subset\n"); + } + cuddDeref(subset); + dd->errorCode = CUDD_INTERNAL_ERROR; } #endif return(subset); @@ -772,16 +800,16 @@ updateParity( NodeData *infoN; DdNode *E; - if (!st_lookup(info->table, (char *)node, (char **)&infoN)) return; + if (!st_lookup(info->table, (const char *)node, (char **)&infoN)) return; if ((infoN->parity & newparity) != 0) return; - infoN->parity |= newparity; + infoN->parity |= (short) 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); + updateParity(Cudd_Not(E),info,3-newparity); } else { - updateParity(E,info,newparity); + updateParity(E,info,newparity); } return; @@ -811,18 +839,18 @@ gatherInfoAux( ApproxInfo * info /* info on BDD */, int parity /* gather parity information */) { - DdNode *N, *Nt, *Ne; + 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); + if (st_lookup(info->table, (const char *)N, (char **)&infoN)) { + if (parity) { + /* Update parity and propagate. */ + updateParity(N, info, 1 + (int) Cudd_IsComplement(node)); + } + return(infoN); } /* Compute the cofactors. */ @@ -839,21 +867,21 @@ gatherInfoAux( /* Point to the correct location in the page. */ infoN = &(info->page[info->index++]); - infoN->parity |= 1 + (short) Cudd_IsComplement(node); + infoN->parity |= (short) (1 + 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; + infoN->mintermsP += infoE->mintermsN/2; + infoN->mintermsN += infoE->mintermsP/2; } else { - infoN->mintermsP += infoE->mintermsP/2; - infoN->mintermsN += infoE->mintermsN/2; + 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(NULL); } return(infoN); @@ -882,7 +910,7 @@ gatherInfo( int numVars /* number of variables node depends on */, int parity /* gather parity information */) { - ApproxInfo *info; + ApproxInfo *info; NodeData *infoTop; /* If user did not give numVars value, set it to the maximum @@ -891,13 +919,13 @@ gatherInfo( ** log gives. */ if (numVars == 0) { - numVars = DBL_MAX_EXP - 1; + numVars = DBL_MAX_EXP - 1; } info = ABC_ALLOC(ApproxInfo,1); if (info == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); } info->max = pow(2.0,(double) numVars); info->one = DD_ONE(dd); @@ -910,41 +938,41 @@ gatherInfo( ** that stores the per-node information. */ info->page = ABC_ALLOC(NodeData,info->size); if (info->page == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - ABC_FREE(info); - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + ABC_FREE(info); + return(NULL); } memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */ - info->table = st_init_table(st_ptrcmp, st_ptrhash);; + info->table = st_init_table(st_ptrcmp,st_ptrhash); if (info->table == NULL) { - ABC_FREE(info->page); - ABC_FREE(info); - return(NULL); + ABC_FREE(info->page); + ABC_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) { - ABC_FREE(info->page); - ABC_FREE(info); - st_free_table(info->table); - return(NULL); + ABC_FREE(info->page); + ABC_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) { - ABC_FREE(info->page); - st_free_table(info->table); - ABC_FREE(info); - return(NULL); + ABC_FREE(info->page); + st_free_table(info->table); + ABC_FREE(info); + return(NULL); } if (Cudd_IsComplement(node)) { - info->minterms = infoTop->mintermsN; + info->minterms = infoTop->mintermsN; } else { - info->minterms = infoTop->mintermsP; + info->minterms = infoTop->mintermsP; } infoTop->functionRef = 1; @@ -988,36 +1016,36 @@ computeSavings( ** 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)); + cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index)); if (item == NULL) - return(0); - (void) st_lookup(info->table, (char *)node, (char **)&infoN); + return(0); + (void) st_lookup(info->table, (const 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++; - } + item = (LocalQueueItem *) queue->first; + node = item->node; + cuddLevelQueueDequeue(queue,cuddI(dd,node->index)); + if (node == skip) continue; + (void) st_lookup(info->table, (const 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 @@ -1060,45 +1088,43 @@ updateRefs( ** 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); + return(0); + (void) st_lookup(info->table, (const 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++; + /* 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, (const 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--; - } + item = (LocalQueueItem *) queue->first; + node = item->node; + cuddLevelQueueDequeue(queue,cuddI(dd,node->index)); + (void) st_lookup(info->table, (const 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, (const 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, (const char *)Cudd_Regular(cuddE(node)), (char **)&infoN); + infoN->functionRef--; + } } #ifdef DD_DEBUG @@ -1142,88 +1168,88 @@ UAmarkNodes( #if 0 (void) printf("initial size = %d initial minterms = %g\n", - info->size, info->minterms); + info->size, info->minterms); #endif queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size); if (queue == NULL) { - return(0); + return(0); } localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem), - dd->initSlots); + dd->initSlots); if (localQueue == NULL) { - cuddLevelQueueQuit(queue); - return(0); + 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); + cuddLevelQueueQuit(queue); + cuddLevelQueueQuit(localQueue); + return(0); } if (Cudd_IsComplement(f)) { - item->impactP = 0.0; - item->impactN = 1.0; + item->impactP = 0.0; + item->impactN = 1.0; } else { - item->impactP = 1.0; - item->impactN = 0.0; + 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) { + /* 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, (const 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)); - 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); + (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 ((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); + (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; + 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); @@ -1257,28 +1283,28 @@ UAbuildSubset( NodeData *infoN; if (Cudd_IsConstant(node)) - return(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); + if (st_lookup(info->table, (const char *)N, (char **)&infoN)) { + if (infoN->replace == TRUE) { + return(info->zero); } - } else { - if (infoN->resultN != NULL) { - return(infoN->resultN); + 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); + (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)); @@ -1286,42 +1312,42 @@ UAbuildSubset( t = UAbuildSubset(dd, Nt, info); if (t == NULL) { - return(NULL); + return(NULL); } cuddRef(t); e = UAbuildSubset(dd, Ne, info); if (e == NULL) { - Cudd_RecursiveDeref(dd,t); - return(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); + 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); - } + 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; + infoN->resultP = r; } else { - infoN->resultN = r; + infoN->resultN = r; } return(r); @@ -1363,277 +1389,266 @@ RAmarkNodes( #if 0 (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n", - info->size, info->minterms); + info->size, info->minterms); #endif queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size); if (queue == NULL) { - return(0); + return(0); } localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem), - dd->initSlots); + dd->initSlots); if (localQueue == NULL) { - cuddLevelQueueQuit(queue); - return(0); + 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)); + cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index)); if (item == NULL) { - cuddLevelQueueQuit(queue); - cuddLevelQueueQuit(localQueue); - return(0); + cuddLevelQueueQuit(queue); + cuddLevelQueueQuit(localQueue); + return(0); } if (Cudd_IsComplement(f)) { - item->impactP = 0.0; - item->impactN = 1.0; + item->impactP = 0.0; + item->impactN = 1.0; } else { - item->impactP = 1.0; - item->impactN = 0.0; + 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); - } + /* 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(infoN->parity >= 1 && infoN->parity <= 3); + 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 (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) { + if (!st_lookup(info->table, (const char *)node, (char **)&infoN)) { cuddLevelQueueQuit(queue); cuddLevelQueueQuit(localQueue); return(0); - } - } else { - savings = 1; } - replace = REPLACE_E; - } else { #ifdef DD_DEBUG - assert(infoN->parity == 2); + assert(infoN->parity >= 1 && infoN->parity <= 3); #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; + 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; } - 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); + 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, (const char *)T, (char **)&infoT); + (void) st_lookup(info->table, (const 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; } - } else { - savings = 1; - } - replace = REPLACE_T; - } else { + 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, (const char *)T, (char **)&infoT); + (void) st_lookup(info->table, (const 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); + 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); + 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 { - 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--; + 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, (const 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)); + 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); + 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 ((1 - numOnset / info->minterms) > + quality * (1 - (double) savings / info->size)) { + infoN->replace = (char) 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); + (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 { + 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); + 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; + savings -= updateRefs(dd,node,shared,info,localQueue) - 1; + } + assert(savings == 0); } else { - item->impactP += impactN/2.0; - item->impactN += impactP/2.0; + replace = NOTHING; } - } 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; + 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; + } } - } 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_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)) { + item->impactP += impactN; + item->impactN += impactP; + } else { + item->impactP += impactP; + item->impactN += impactN; + } } } - } cuddLevelQueueQuit(queue); cuddLevelQueueQuit(localQueue); @@ -1678,278 +1693,277 @@ BAmarkNodes( #if 0 (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n", - info->size, info->minterms); + info->size, info->minterms); #endif queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size); if (queue == NULL) { - return(0); + return(0); } localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem), - dd->initSlots); + dd->initSlots); if (localQueue == NULL) { - cuddLevelQueueQuit(queue); - return(0); + 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)); + cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index)); if (item == NULL) { - cuddLevelQueueQuit(queue); - cuddLevelQueueQuit(localQueue); - return(0); + cuddLevelQueueQuit(queue); + cuddLevelQueueQuit(localQueue); + return(0); } if (Cudd_IsComplement(f)) { - item->impactP = 0.0; - item->impactN = 1.0; + item->impactP = 0.0; + item->impactN = 1.0; } else { - item->impactP = 1.0; - item->impactN = 0.0; + 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; + /* 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)); + 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) { + if (!st_lookup(info->table, (const char *)node, (char **)&infoN)) { cuddLevelQueueQuit(queue); cuddLevelQueueQuit(localQueue); return(0); - } - } else { - savings = 1; } - replace = REPLACE_E; - } else { + quality = infoN->care ? quality1 : quality0; #ifdef DD_DEBUG - assert(infoN->parity == 2); + assert(infoN->parity >= 1 && infoN->parity <= 3); #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; + 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; } - 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); + 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, (const char *)T, (char **)&infoT); + (void) st_lookup(info->table, (const 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; } - } else { - savings = 1; - } - replace = REPLACE_T; - } else { + 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, (const char *)T, (char **)&infoT); + (void) st_lookup(info->table, (const 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); + 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); + 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 { - 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--; + 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, (const 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)); + 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); + 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 ((1 - numOnset / info->minterms) > + quality * (1 - (double) savings / info->size)) { + infoN->replace = (char) 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); + (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 { + 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); + 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; + savings -= updateRefs(dd,node,shared,info,localQueue) - 1; + } + assert(savings == 0); } else { - item->impactP += impactP/2.0; - item->impactN += impactN/2.0; - } + replace = NOTHING; } - } - 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; + 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; + } } - } 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_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); @@ -1982,124 +1996,124 @@ RAbuildSubset( NodeData *infoN; if (Cudd_IsConstant(node)) - return(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); + if (st_lookup(info->table, (const char *)N, (char **)&infoN)) { + if (N == node ) { + if (infoN->resultP != NULL) { + return(infoN->resultP); + } } 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); + if (infoN->resultN != NULL) { + return(infoN->resultN); + } } - cuddRef(e); - e = Cudd_Not(e); - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_RecursiveDeref(dd, e); - return(NULL); + 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; + e = info->zero; + 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; + t = info->one; + 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); } - 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); + (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); + return(NULL); } cuddRef(t); e = RAbuildSubset(dd, Ne, info); if (e == NULL) { - Cudd_RecursiveDeref(dd,t); - return(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); + 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); - } + 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; + infoN->resultP = r; } else { - infoN->resultN = r; + infoN->resultN = r; } return(r); @@ -2137,61 +2151,63 @@ BAapplyBias( one = DD_ONE(dd); zero = Cudd_Not(one); - if (!st_lookup(info->table, (char *) f, (char **)&infoF)) - return(CARE_ERROR); + if (!st_lookup(info->table, (const 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); + (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); + Ft = cuddT(f); Fe = cuddE(f); } else { - Ft = Fe = f; + 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); - } + /* 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; + Bt = Be = b; } careT = BAapplyBias(dd, Ft, Bt, info, cache); if (careT == CARE_ERROR) - return(CARE_ERROR); + return(CARE_ERROR); careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache); if (careE == CARE_ERROR) - return(CARE_ERROR); + return(CARE_ERROR); if (careT == TOTAL_CARE && careE == TOTAL_CARE) { - infoF->care = TOTAL_CARE; + infoF->care = TOTAL_CARE; } else { - infoF->care = CARE; + 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); - } + 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 */ + + ABC_NAMESPACE_IMPL_END -- cgit v1.2.3