summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddApprox.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-02-13 13:42:25 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-02-13 13:42:25 -0800
commite7b544f11151f09a4a3fbe39b4a176795a82f677 (patch)
treea6cbbeb138c9bfe5b2554a5838124ffc3a6c0a5b /src/bdd/cudd/cuddApprox.c
parentd99de60e6c88e5f6157b1d5c9b25cfd5d08a1c9a (diff)
downloadabc-e7b544f11151f09a4a3fbe39b4a176795a82f677.tar.gz
abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.tar.bz2
abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.zip
Upgrade to the latest CUDD 2.4.2.
Diffstat (limited to 'src/bdd/cudd/cuddApprox.c')
-rw-r--r--src/bdd/cudd/cuddApprox.c1840
1 files changed, 928 insertions, 912 deletions
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:
<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>
- ]
+ <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.]
+ 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 19:17:05 +0000