summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddDecomp.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddDecomp.c')
-rw-r--r--src/bdd/cudd/cuddDecomp.c1773
1 files changed, 901 insertions, 872 deletions
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 95a00536..34eaef0c 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -7,30 +7,57 @@
Synopsis [Functions for BDD decomposition.]
Description [External procedures included in this file:
- <ul>
- <li> Cudd_bddApproxConjDecomp()
- <li> Cudd_bddApproxDisjDecomp()
- <li> Cudd_bddIterConjDecomp()
- <li> Cudd_bddIterDisjDecomp()
- <li> Cudd_bddGenConjDecomp()
- <li> Cudd_bddGenDisjDecomp()
- <li> Cudd_bddVarConjDecomp()
- <li> Cudd_bddVarDisjDecomp()
- </ul>
- Static procedures included in this module:
- <ul>
- <li> cuddConjunctsAux()
- <li> CreateBotDist()
- <li> BuildConjuncts()
- <li> ConjunctsFree()
- </ul>]
+ <ul>
+ <li> Cudd_bddApproxConjDecomp()
+ <li> Cudd_bddApproxDisjDecomp()
+ <li> Cudd_bddIterConjDecomp()
+ <li> Cudd_bddIterDisjDecomp()
+ <li> Cudd_bddGenConjDecomp()
+ <li> Cudd_bddGenDisjDecomp()
+ <li> Cudd_bddVarConjDecomp()
+ <li> Cudd_bddVarDisjDecomp()
+ </ul>
+ Static procedures included in this module:
+ <ul>
+ <li> cuddConjunctsAux()
+ <li> CreateBotDist()
+ <li> BuildConjuncts()
+ <li> ConjunctsFree()
+ </ul>]
Author [Kavita Ravi, 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.]
******************************************************************************/
@@ -40,6 +67,7 @@
ABC_NAMESPACE_IMPL_START
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -78,10 +106,10 @@ typedef struct NodeStat {
/*---------------------------------------------------------------------------*/
#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $";
#endif
-static DdNode *one, *zero;
+static DdNode *one, *zero;
long lastTimeG;
/*---------------------------------------------------------------------------*/
@@ -101,16 +129,16 @@ long lastTimeG;
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static NodeStat * CreateBotDist ARGS((DdNode * node, st_table * distanceTable));
-static double CountMinterms ARGS((DdNode * node, double max, st_table * mintermTable, FILE *fp));
-static void ConjunctsFree ARGS((DdManager * dd, Conjuncts * factors));
-static int PairInTables ARGS((DdNode * g, DdNode * h, st_table * ghTable));
-static Conjuncts * CheckTablesCacheAndReturn ARGS((DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable));
-static Conjuncts * PickOnePair ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable));
-static Conjuncts * CheckInTables ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem));
-static Conjuncts * ZeroCase ARGS((DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched));
-static Conjuncts * BuildConjuncts ARGS((DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable));
-static int cuddConjunctsAux ARGS((DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2));
+static NodeStat * CreateBotDist (DdNode * node, st_table * distanceTable);
+static double CountMinterms (DdNode * node, double max, st_table * mintermTable, FILE *fp);
+static void ConjunctsFree (DdManager * dd, Conjuncts * factors);
+static int PairInTables (DdNode * g, DdNode * h, st_table * ghTable);
+static Conjuncts * CheckTablesCacheAndReturn (DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable);
+static Conjuncts * PickOnePair (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable);
+static Conjuncts * CheckInTables (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem);
+static Conjuncts * ZeroCase (DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched);
+static Conjuncts * BuildConjuncts (DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable);
+static int cuddConjunctsAux (DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2);
/**AutomaticEnd***************************************************************/
@@ -158,8 +186,8 @@ Cudd_bddApproxConjDecomp(
cuddRef(superset1);
superset2 = Cudd_bddSqueeze(dd,f,superset1);
if (superset2 == NULL) {
- Cudd_RecursiveDeref(dd,superset1);
- return(0);
+ Cudd_RecursiveDeref(dd,superset1);
+ return(0);
}
cuddRef(superset2);
Cudd_RecursiveDeref(dd,superset1);
@@ -167,8 +195,8 @@ Cudd_bddApproxConjDecomp(
/* Compute the second factor by minimization. */
hlocal = Cudd_bddLICompaction(dd,f,superset2);
if (hlocal == NULL) {
- Cudd_RecursiveDeref(dd,superset2);
- return(0);
+ Cudd_RecursiveDeref(dd,superset2);
+ return(0);
}
cuddRef(hlocal);
@@ -176,47 +204,47 @@ Cudd_bddApproxConjDecomp(
** step guarantees that g will be 1. */
glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
if (glocal == NULL) {
- Cudd_RecursiveDeref(dd,superset2);
- Cudd_RecursiveDeref(dd,hlocal);
- return(0);
+ Cudd_RecursiveDeref(dd,superset2);
+ Cudd_RecursiveDeref(dd,hlocal);
+ return(0);
}
cuddRef(glocal);
Cudd_RecursiveDeref(dd,superset2);
if (glocal != DD_ONE(dd)) {
- if (hlocal != DD_ONE(dd)) {
- *conjuncts = ABC_ALLOC(DdNode *,2);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- Cudd_RecursiveDeref(dd,hlocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ if (hlocal != DD_ONE(dd)) {
+ *conjuncts = ABC_ALLOC(DdNode *,2);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,glocal);
+ Cudd_RecursiveDeref(dd,hlocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = glocal;
+ (*conjuncts)[1] = hlocal;
+ return(2);
+ } else {
+ Cudd_RecursiveDeref(dd,hlocal);
+ *conjuncts = ABC_ALLOC(DdNode *,1);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,glocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = glocal;
+ return(1);
}
- (*conjuncts)[0] = glocal;
- (*conjuncts)[1] = hlocal;
- return(2);
} else {
- Cudd_RecursiveDeref(dd,hlocal);
+ Cudd_RecursiveDeref(dd,glocal);
*conjuncts = ABC_ALLOC(DdNode *,1);
if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ Cudd_RecursiveDeref(dd,hlocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
}
- (*conjuncts)[0] = glocal;
+ (*conjuncts)[0] = hlocal;
return(1);
}
- } else {
- Cudd_RecursiveDeref(dd,glocal);
- *conjuncts = ABC_ALLOC(DdNode *,1);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,hlocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- (*conjuncts)[0] = hlocal;
- return(1);
- }
} /* end of Cudd_bddApproxConjDecomp */
@@ -251,7 +279,7 @@ Cudd_bddApproxDisjDecomp(
result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
for (i = 0; i < result; i++) {
- (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
+ (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
}
return(result);
@@ -298,59 +326,59 @@ Cudd_bddIterConjDecomp(
sizeOld = Cudd_SharingSize(old,2);
do {
- /* Find a tentative first factor by overapproximation and
- ** minimization. */
- superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
- if (superset1 == NULL) {
- Cudd_RecursiveDeref(dd,old[0]);
- Cudd_RecursiveDeref(dd,old[1]);
- return(0);
- }
- cuddRef(superset1);
- superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
- if (superset2 == NULL) {
- Cudd_RecursiveDeref(dd,old[0]);
- Cudd_RecursiveDeref(dd,old[1]);
+ /* Find a tentative first factor by overapproximation and
+ ** minimization. */
+ superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
+ if (superset1 == NULL) {
+ Cudd_RecursiveDeref(dd,old[0]);
+ Cudd_RecursiveDeref(dd,old[1]);
+ return(0);
+ }
+ cuddRef(superset1);
+ superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
+ if (superset2 == NULL) {
+ Cudd_RecursiveDeref(dd,old[0]);
+ Cudd_RecursiveDeref(dd,old[1]);
+ Cudd_RecursiveDeref(dd,superset1);
+ return(0);
+ }
+ cuddRef(superset2);
Cudd_RecursiveDeref(dd,superset1);
- return(0);
- }
- cuddRef(superset2);
- Cudd_RecursiveDeref(dd,superset1);
- res[0] = Cudd_bddAnd(dd,old[0],superset2);
- if (res[0] == NULL) {
+ res[0] = Cudd_bddAnd(dd,old[0],superset2);
+ if (res[0] == NULL) {
+ Cudd_RecursiveDeref(dd,superset2);
+ Cudd_RecursiveDeref(dd,old[0]);
+ Cudd_RecursiveDeref(dd,old[1]);
+ return(0);
+ }
+ cuddRef(res[0]);
Cudd_RecursiveDeref(dd,superset2);
- Cudd_RecursiveDeref(dd,old[0]);
- Cudd_RecursiveDeref(dd,old[1]);
- return(0);
- }
- cuddRef(res[0]);
- Cudd_RecursiveDeref(dd,superset2);
- if (res[0] == old[0]) {
- Cudd_RecursiveDeref(dd,res[0]);
- break; /* avoid infinite loop */
- }
-
- /* Compute the second factor by minimization. */
- res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
- if (res[1] == NULL) {
- Cudd_RecursiveDeref(dd,old[0]);
- Cudd_RecursiveDeref(dd,old[1]);
- return(0);
- }
- cuddRef(res[1]);
+ if (res[0] == old[0]) {
+ Cudd_RecursiveDeref(dd,res[0]);
+ break; /* avoid infinite loop */
+ }
- sizeNew = Cudd_SharingSize(res,2);
- if (sizeNew <= sizeOld) {
- Cudd_RecursiveDeref(dd,old[0]);
- old[0] = res[0];
- Cudd_RecursiveDeref(dd,old[1]);
- old[1] = res[1];
- sizeOld = sizeNew;
- } else {
- Cudd_RecursiveDeref(dd,res[0]);
- Cudd_RecursiveDeref(dd,res[1]);
- break;
- }
+ /* Compute the second factor by minimization. */
+ res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
+ if (res[1] == NULL) {
+ Cudd_RecursiveDeref(dd,old[0]);
+ Cudd_RecursiveDeref(dd,old[1]);
+ return(0);
+ }
+ cuddRef(res[1]);
+
+ sizeNew = Cudd_SharingSize(res,2);
+ if (sizeNew <= sizeOld) {
+ Cudd_RecursiveDeref(dd,old[0]);
+ old[0] = res[0];
+ Cudd_RecursiveDeref(dd,old[1]);
+ old[1] = res[1];
+ sizeOld = sizeNew;
+ } else {
+ Cudd_RecursiveDeref(dd,res[0]);
+ Cudd_RecursiveDeref(dd,res[1]);
+ break;
+ }
} while (1);
@@ -358,48 +386,48 @@ Cudd_bddIterConjDecomp(
** be f, this step guarantees that g will be 1. */
superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
if (superset1 == NULL) {
- Cudd_RecursiveDeref(dd,old[0]);
- Cudd_RecursiveDeref(dd,old[1]);
- return(0);
+ Cudd_RecursiveDeref(dd,old[0]);
+ Cudd_RecursiveDeref(dd,old[1]);
+ return(0);
}
cuddRef(superset1);
Cudd_RecursiveDeref(dd,old[0]);
old[0] = superset1;
if (old[0] != DD_ONE(dd)) {
- if (old[1] != DD_ONE(dd)) {
- *conjuncts = ABC_ALLOC(DdNode *,2);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,old[0]);
- Cudd_RecursiveDeref(dd,old[1]);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ if (old[1] != DD_ONE(dd)) {
+ *conjuncts = ABC_ALLOC(DdNode *,2);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,old[0]);
+ Cudd_RecursiveDeref(dd,old[1]);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = old[0];
+ (*conjuncts)[1] = old[1];
+ return(2);
+ } else {
+ Cudd_RecursiveDeref(dd,old[1]);
+ *conjuncts = ABC_ALLOC(DdNode *,1);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,old[0]);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = old[0];
+ return(1);
}
- (*conjuncts)[0] = old[0];
- (*conjuncts)[1] = old[1];
- return(2);
} else {
- Cudd_RecursiveDeref(dd,old[1]);
+ Cudd_RecursiveDeref(dd,old[0]);
*conjuncts = ABC_ALLOC(DdNode *,1);
if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,old[0]);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ Cudd_RecursiveDeref(dd,old[1]);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
}
- (*conjuncts)[0] = old[0];
+ (*conjuncts)[0] = old[1];
return(1);
}
- } else {
- Cudd_RecursiveDeref(dd,old[0]);
- *conjuncts = ABC_ALLOC(DdNode *,1);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,old[1]);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- (*conjuncts)[0] = old[1];
- return(1);
- }
} /* end of Cudd_bddIterConjDecomp */
@@ -434,7 +462,7 @@ Cudd_bddIterDisjDecomp(
result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
for (i = 0; i < result; i++) {
- (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
+ (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
}
return(result);
@@ -477,48 +505,48 @@ Cudd_bddGenConjDecomp(
zero = Cudd_Not(one);
do {
- dd->reordered = 0;
- result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
+ dd->reordered = 0;
+ result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
} while (dd->reordered == 1);
if (result == 0) {
- return(0);
+ return(0);
}
if (glocal != one) {
- if (hlocal != one) {
- *conjuncts = ABC_ALLOC(DdNode *,2);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- Cudd_RecursiveDeref(dd,hlocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ if (hlocal != one) {
+ *conjuncts = ABC_ALLOC(DdNode *,2);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,glocal);
+ Cudd_RecursiveDeref(dd,hlocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = glocal;
+ (*conjuncts)[1] = hlocal;
+ return(2);
+ } else {
+ Cudd_RecursiveDeref(dd,hlocal);
+ *conjuncts = ABC_ALLOC(DdNode *,1);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,glocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = glocal;
+ return(1);
}
- (*conjuncts)[0] = glocal;
- (*conjuncts)[1] = hlocal;
- return(2);
} else {
- Cudd_RecursiveDeref(dd,hlocal);
+ Cudd_RecursiveDeref(dd,glocal);
*conjuncts = ABC_ALLOC(DdNode *,1);
if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ Cudd_RecursiveDeref(dd,hlocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
}
- (*conjuncts)[0] = glocal;
+ (*conjuncts)[0] = hlocal;
return(1);
}
- } else {
- Cudd_RecursiveDeref(dd,glocal);
- *conjuncts = ABC_ALLOC(DdNode *,1);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,hlocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- (*conjuncts)[0] = hlocal;
- return(1);
- }
} /* end of Cudd_bddGenConjDecomp */
@@ -553,7 +581,7 @@ Cudd_bddGenDisjDecomp(
result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
for (i = 0; i < result; i++) {
- (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
+ (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
}
return(result);
@@ -597,30 +625,30 @@ Cudd_bddVarConjDecomp(
support = Cudd_Support(dd,f);
if (support == NULL) return(0);
if (Cudd_IsConstant(support)) {
- *conjuncts = ABC_ALLOC(DdNode *,1);
- if (*conjuncts == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- (*conjuncts)[0] = f;
- cuddRef((*conjuncts)[0]);
- return(1);
+ *conjuncts = ABC_ALLOC(DdNode *,1);
+ if (*conjuncts == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = f;
+ cuddRef((*conjuncts)[0]);
+ return(1);
}
cuddRef(support);
min = 1000000000;
best = -1;
scan = support;
while (!Cudd_IsConstant(scan)) {
- int i = scan->index;
- int est1 = Cudd_EstimateCofactor(dd,f,i,1);
- int est0 = Cudd_EstimateCofactor(dd,f,i,0);
- /* Minimize the size of the larger of the two cofactors. */
- int est = (est1 > est0) ? est1 : est0;
- if (est < min) {
- min = est;
- best = i;
- }
- scan = cuddT(scan);
+ int i = scan->index;
+ int est1 = Cudd_EstimateCofactor(dd,f,i,1);
+ int est0 = Cudd_EstimateCofactor(dd,f,i,0);
+ /* Minimize the size of the larger of the two cofactors. */
+ int est = (est1 > est0) ? est1 : est0;
+ if (est < min) {
+ min = est;
+ best = i;
+ }
+ scan = cuddT(scan);
}
#ifdef DD_DEBUG
assert(best >= 0 && best < dd->size);
@@ -630,50 +658,50 @@ Cudd_bddVarConjDecomp(
var = Cudd_bddIthVar(dd,best);
glocal = Cudd_bddOr(dd,f,var);
if (glocal == NULL) {
- return(0);
+ return(0);
}
cuddRef(glocal);
hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
if (hlocal == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- return(0);
+ Cudd_RecursiveDeref(dd,glocal);
+ return(0);
}
cuddRef(hlocal);
if (glocal != DD_ONE(dd)) {
- if (hlocal != DD_ONE(dd)) {
- *conjuncts = ABC_ALLOC(DdNode *,2);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- Cudd_RecursiveDeref(dd,hlocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ if (hlocal != DD_ONE(dd)) {
+ *conjuncts = ABC_ALLOC(DdNode *,2);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,glocal);
+ Cudd_RecursiveDeref(dd,hlocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = glocal;
+ (*conjuncts)[1] = hlocal;
+ return(2);
+ } else {
+ Cudd_RecursiveDeref(dd,hlocal);
+ *conjuncts = ABC_ALLOC(DdNode *,1);
+ if (*conjuncts == NULL) {
+ Cudd_RecursiveDeref(dd,glocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ (*conjuncts)[0] = glocal;
+ return(1);
}
- (*conjuncts)[0] = glocal;
- (*conjuncts)[1] = hlocal;
- return(2);
} else {
- Cudd_RecursiveDeref(dd,hlocal);
+ Cudd_RecursiveDeref(dd,glocal);
*conjuncts = ABC_ALLOC(DdNode *,1);
if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,glocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
+ Cudd_RecursiveDeref(dd,hlocal);
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
}
- (*conjuncts)[0] = glocal;
+ (*conjuncts)[0] = hlocal;
return(1);
}
- } else {
- Cudd_RecursiveDeref(dd,glocal);
- *conjuncts = ABC_ALLOC(DdNode *,1);
- if (*conjuncts == NULL) {
- Cudd_RecursiveDeref(dd,hlocal);
- dd->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- (*conjuncts)[0] = hlocal;
- return(1);
- }
} /* end of Cudd_bddVarConjDecomp */
@@ -711,7 +739,7 @@ Cudd_bddVarDisjDecomp(
result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
for (i = 0; i < result; i++) {
- (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
+ (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
}
return(result);
@@ -751,15 +779,15 @@ CreateBotDist(
#if 0
if (Cudd_IsConstant(node)) {
- return(0);
+ return(0);
}
#endif
/* Return the entry in the table if found. */
N = Cudd_Regular(node);
- if (st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) {
- nodeStat->localRef++;
- return(nodeStat);
+ if (st_lookup(distanceTable, (const char *)N, (char **)&nodeStat)) {
+ nodeStat->localRef++;
+ return(nodeStat);
}
Nv = cuddT(N);
@@ -782,14 +810,14 @@ CreateBotDist(
nodeStat = ABC_ALLOC(NodeStat, 1);
if (nodeStat == NULL) {
- return(0);
+ return(0);
}
nodeStat->distance = distance;
nodeStat->localRef = 1;
if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
- ST_OUT_OF_MEM) {
- return(0);
+ ST_OUT_OF_MEM) {
+ return(0);
}
return(nodeStat);
@@ -823,17 +851,17 @@ CountMinterms(
N = Cudd_Regular(node);
if (cuddIsConstant(N)) {
- if (node == zero) {
- return(0);
- } else {
- return(max);
- }
+ if (node == zero) {
+ return(0);
+ } else {
+ return(max);
+ }
}
/* Return the entry in the table if found. */
- if (st_lookup(mintermTable, (char *)node, (char **)&dummy)) {
- min = *dummy;
- return(min);
+ if (st_lookup(mintermTable, (const char *)node, (char **)&dummy)) {
+ min = *dummy;
+ return(min);
}
Nv = cuddT(N);
@@ -854,7 +882,7 @@ CountMinterms(
if (dummy == NULL) return(-1.0);
*dummy = min;
if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
- (void) fprintf(fp, "st table insert failed\n");
+ (void) fprintf(fp, "st table insert failed\n");
}
return(min);
@@ -928,21 +956,21 @@ PairInTables(
if (!gPresent && !hPresent) return(NONE);
if (!hPresent) {
- if (valueG & 1) return(G_ST);
- if (valueG & 2) return(G_CR);
+ if (valueG & 1) return(G_ST);
+ if (valueG & 2) return(G_CR);
}
if (!gPresent) {
- if (valueH & 1) return(H_CR);
- if (valueH & 2) return(H_ST);
+ if (valueH & 1) return(H_CR);
+ if (valueH & 2) return(H_ST);
}
/* both in tables */
if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
if (valueG & 1) {
- return(BOTH_G);
+ return(BOTH_G);
} else {
- return(BOTH_H);
+ return(BOTH_H);
}
} /* end of PairInTables */
@@ -984,74 +1012,74 @@ CheckTablesCacheAndReturn(
factors = ABC_ALLOC(Conjuncts, 1);
if (factors == NULL) return(NULL);
if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
- if (g != one) {
- value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
- value |= 1;
- } else {
- value = 1;
- }
- if (st_insert(ghTable, (char *)Cudd_Regular(g),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- return(NULL);
+ if (g != one) {
+ value = 0;
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
+ value |= 1;
+ } else {
+ value = 1;
+ }
+ if (st_insert(ghTable, (char *)Cudd_Regular(g),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ return(NULL);
+ }
}
- }
- factors->g = g;
- factors->h = h;
+ factors->g = g;
+ factors->h = h;
} else if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
- if (h != one) {
- value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
- value |= 2;
- } else {
- value = 2;
- }
- if (st_insert(ghTable, (char *)Cudd_Regular(h),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- return(NULL);
+ if (h != one) {
+ value = 0;
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
+ value |= 2;
+ } else {
+ value = 2;
+ }
+ if (st_insert(ghTable, (char *)Cudd_Regular(h),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ return(NULL);
+ }
}
- }
- factors->g = g;
- factors->h = h;
+ factors->g = g;
+ factors->h = h;
} else if (pairValue == H_CR) {
- if (g != one) {
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(g),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- return(NULL);
+ if (g != one) {
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ return(NULL);
+ }
}
- }
- factors->g = h;
- factors->h = g;
+ factors->g = h;
+ factors->h = g;
} else if (pairValue == G_CR) {
- if (h != one) {
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(h),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- return(NULL);
+ if (h != one) {
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ return(NULL);
+ }
}
- }
- factors->g = h;
- factors->h = g;
+ factors->g = h;
+ factors->h = g;
} else if (pairValue == PAIR_CR) {
/* pair exists in table */
- factors->g = h;
- factors->h = g;
+ factors->g = h;
+ factors->h = g;
} else if (pairValue == PAIR_ST) {
- factors->g = g;
- factors->h = h;
+ factors->g = g;
+ factors->h = h;
}
-
+
/* cache the result for this node */
if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
- ABC_FREE(factors);
- return(NULL);
+ ABC_FREE(factors);
+ return(NULL);
}
return(factors);
} /* end of CheckTablesCacheAndReturn */
-
+
/**Function********************************************************************
Synopsis [Check the tables for the existence of pair and return one
@@ -1086,29 +1114,29 @@ PickOnePair(
/* count the number of pointers to pair 2 */
if (h2 == one) {
- twoRef = (Cudd_Regular(g2))->ref;
+ twoRef = (Cudd_Regular(g2))->ref;
} else if (g2 == one) {
- twoRef = (Cudd_Regular(h2))->ref;
+ twoRef = (Cudd_Regular(h2))->ref;
} else {
- twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
+ twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
}
/* count the number of pointers to pair 1 */
if (h1 == one) {
- oneRef = (Cudd_Regular(g1))->ref;
+ oneRef = (Cudd_Regular(g1))->ref;
} else if (g1 == one) {
- oneRef = (Cudd_Regular(h1))->ref;
+ oneRef = (Cudd_Regular(h1))->ref;
} else {
- oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
+ oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
}
/* pick the pair with higher reference count */
if (oneRef >= twoRef) {
- factors->g = g1;
- factors->h = h1;
+ factors->g = g1;
+ factors->h = h1;
} else {
- factors->g = g2;
- factors->h = h2;
+ factors->g = g2;
+ factors->h = h2;
}
/*
@@ -1116,54 +1144,54 @@ PickOnePair(
* recombination.
*/
if (factors->g != one) {
- /* insert g in htable */
- value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
- if (value == 2) {
- value |= 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- ABC_FREE(factors);
- return(NULL);
- }
- }
- } else {
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- ABC_FREE(factors);
- return(NULL);
+ /* insert g in htable */
+ value = 0;
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
+ if (value == 2) {
+ value |= 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ ABC_FREE(factors);
+ return(NULL);
+ }
+ }
+ } else {
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
}
- }
if (factors->h != one) {
- /* insert h in htable */
- value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
- if (value == 1) {
- value |= 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- ABC_FREE(factors);
- return(NULL);
- }
- }
- } else {
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- ABC_FREE(factors);
- return(NULL);
+ /* insert h in htable */
+ value = 0;
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
+ if (value == 1) {
+ value |= 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ ABC_FREE(factors);
+ return(NULL);
+ }
+ }
+ } else {
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
}
- }
/* Store factors in cache table for later use. */
if (st_insert(cacheTable, (char *)node, (char *)factors) ==
- ST_OUT_OF_MEM) {
- ABC_FREE(factors);
- return(NULL);
+ ST_OUT_OF_MEM) {
+ ABC_FREE(factors);
+ return(NULL);
}
return(factors);
@@ -1208,192 +1236,192 @@ CheckInTables(
/* if none of the 4 exist in the gh tables, return NULL */
if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
- return NULL;
+ return NULL;
}
factors = ABC_ALLOC(Conjuncts, 1);
if (factors == NULL) {
- *outOfMem = 1;
- return NULL;
+ *outOfMem = 1;
+ return NULL;
}
/* pairs that already exist in the table get preference. */
if (pairValue1 == PAIR_ST) {
- factors->g = g1;
- factors->h = h1;
+ factors->g = g1;
+ factors->h = h1;
} else if (pairValue2 == PAIR_ST) {
- factors->g = g2;
- factors->h = h2;
+ factors->g = g2;
+ factors->h = h2;
} else if (pairValue1 == PAIR_CR) {
- factors->g = h1;
- factors->h = g1;
+ factors->g = h1;
+ factors->h = g1;
} else if (pairValue2 == PAIR_CR) {
- factors->g = h2;
- factors->h = g2;
+ factors->g = h2;
+ factors->h = g2;
} else if (pairValue1 == G_ST) {
- /* g exists in the table, h is not found in either table */
- factors->g = g1;
- factors->h = h1;
- if (h1 != one) {
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(h1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g exists in the table, h is not found in either table */
+ factors->g = g1;
+ factors->h = h1;
+ if (h1 != one) {
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h1),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue1 == BOTH_G) {
- /* g and h are found in the g table */
- factors->g = g1;
- factors->h = h1;
- if (h1 != one) {
- value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(h1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g and h are found in the g table */
+ factors->g = g1;
+ factors->h = h1;
+ if (h1 != one) {
+ value = 3;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h1),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue1 == H_ST) {
- /* h exists in the table, g is not found in either table */
- factors->g = g1;
- factors->h = h1;
- if (g1 != one) {
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(g1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* h exists in the table, g is not found in either table */
+ factors->g = g1;
+ factors->h = h1;
+ if (g1 != one) {
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g1),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue1 == BOTH_H) {
- /* g and h are found in the h table */
- factors->g = g1;
- factors->h = h1;
- if (g1 != one) {
- value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(g1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g and h are found in the h table */
+ factors->g = g1;
+ factors->h = h1;
+ if (g1 != one) {
+ value = 3;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g1),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue2 == G_ST) {
- /* g exists in the table, h is not found in either table */
- factors->g = g2;
- factors->h = h2;
- if (h2 != one) {
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(h2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g exists in the table, h is not found in either table */
+ factors->g = g2;
+ factors->h = h2;
+ if (h2 != one) {
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h2),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue2 == BOTH_G) {
- /* g and h are found in the g table */
- factors->g = g2;
- factors->h = h2;
- if (h2 != one) {
- value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(h2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g and h are found in the g table */
+ factors->g = g2;
+ factors->h = h2;
+ if (h2 != one) {
+ value = 3;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h2),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue2 == H_ST) {
- /* h exists in the table, g is not found in either table */
- factors->g = g2;
- factors->h = h2;
- if (g2 != one) {
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(g2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* h exists in the table, g is not found in either table */
+ factors->g = g2;
+ factors->h = h2;
+ if (g2 != one) {
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g2),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue2 == BOTH_H) {
- /* g and h are found in the h table */
- factors->g = g2;
- factors->h = h2;
- if (g2 != one) {
- value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(g2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g and h are found in the h table */
+ factors->g = g2;
+ factors->h = h2;
+ if (g2 != one) {
+ value = 3;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g2),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue1 == G_CR) {
- /* g found in h table and h in none */
- factors->g = h1;
- factors->h = g1;
- if (h1 != one) {
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(h1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g found in h table and h in none */
+ factors->g = h1;
+ factors->h = g1;
+ if (h1 != one) {
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h1),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue1 == H_CR) {
- /* h found in g table and g in none */
- factors->g = h1;
- factors->h = g1;
- if (g1 != one) {
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(g1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* h found in g table and g in none */
+ factors->g = h1;
+ factors->h = g1;
+ if (g1 != one) {
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g1),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue2 == G_CR) {
- /* g found in h table and h in none */
- factors->g = h2;
- factors->h = g2;
- if (h2 != one) {
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(h2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* g found in h table and h in none */
+ factors->g = h2;
+ factors->h = g2;
+ if (h2 != one) {
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(h2),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
- }
} else if (pairValue2 == H_CR) {
- /* h found in g table and g in none */
- factors->g = h2;
- factors->h = g2;
- if (g2 != one) {
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(g2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ /* h found in g table and g in none */
+ factors->g = h2;
+ factors->h = g2;
+ if (g2 != one) {
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(g2),
+ (char *)(long)value) == ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
+ }
}
}
- }
/* Store factors in cache table for later use. */
if (st_insert(cacheTable, (char *)node, (char *)factors) ==
- ST_OUT_OF_MEM) {
- *outOfMem = 1;
- ABC_FREE(factors);
- return(NULL);
+ ST_OUT_OF_MEM) {
+ *outOfMem = 1;
+ ABC_FREE(factors);
+ return(NULL);
}
return factors;
} /* end of CheckInTables */
@@ -1440,69 +1468,69 @@ ZeroCase(
/* Seprate variable and child */
if (factorsNv->g == one) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- factors = ABC_ALLOC(Conjuncts, 1);
- if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, x);
- return(NULL);
- }
- factors->g = x;
- factors->h = factorsNv->h;
- /* cache the result*/
- if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, x);
- ABC_FREE(factors);
- return NULL;
- }
-
- /* store x in g table, the other node is already in the table */
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
- value |= 1;
- } else {
- value = 1;
- }
- if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
- dd->errorCode = CUDD_MEMORY_OUT;
- return NULL;
- }
- return(factors);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ factors = ABC_ALLOC(Conjuncts, 1);
+ if (factors == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, x);
+ return(NULL);
+ }
+ factors->g = x;
+ factors->h = factorsNv->h;
+ /* cache the result*/
+ if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, x);
+ ABC_FREE(factors);
+ return NULL;
+ }
+
+ /* store x in g table, the other node is already in the table */
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
+ value |= 1;
+ } else {
+ value = 1;
+ }
+ if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return NULL;
+ }
+ return(factors);
}
/* Seprate variable and child */
if (factorsNv->h == one) {
- Cudd_RecursiveDeref(dd, factorsNv->h);
- factors = ABC_ALLOC(Conjuncts, 1);
- if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, x);
- return(NULL);
- }
- factors->g = factorsNv->g;
- factors->h = x;
- /* cache the result. */
- if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, x);
- ABC_FREE(factors);
- return(NULL);
- }
- /* store x in h table, the other node is already in the table */
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
- value |= 2;
- } else {
- value = 2;
- }
- if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
- dd->errorCode = CUDD_MEMORY_OUT;
- return NULL;
- }
- return(factors);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ factors = ABC_ALLOC(Conjuncts, 1);
+ if (factors == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, x);
+ return(NULL);
+ }
+ factors->g = factorsNv->g;
+ factors->h = x;
+ /* cache the result. */
+ if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, x);
+ ABC_FREE(factors);
+ return(NULL);
+ }
+ /* store x in h table, the other node is already in the table */
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
+ value |= 2;
+ } else {
+ value = 2;
+ }
+ if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return NULL;
+ }
+ return(factors);
}
G = Cudd_Regular(factorsNv->g);
@@ -1512,29 +1540,29 @@ ZeroCase(
Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node));
/* if the child below is a variable */
if ((Gv == zero) || (Gnv == zero)) {
- h = factorsNv->h;
- g = cuddBddAndRecur(dd, x, factorsNv->g);
- if (g != NULL) cuddRef(g);
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, x);
- if (g == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->h);
- return NULL;
- }
- /* CheckTablesCacheAndReturn responsible for allocating
- * factors structure., g,h referenced for cache store the
- */
- factors = CheckTablesCacheAndReturn(node,
- g,
- h,
- ghTable,
- cacheTable);
- if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, g);
- Cudd_RecursiveDeref(dd, h);
- }
- return(factors);
+ h = factorsNv->h;
+ g = cuddBddAndRecur(dd, x, factorsNv->g);
+ if (g != NULL) cuddRef(g);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, x);
+ if (g == NULL) {
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ return NULL;
+ }
+ /* CheckTablesCacheAndReturn responsible for allocating
+ * factors structure., g,h referenced for cache store the
+ */
+ factors = CheckTablesCacheAndReturn(node,
+ g,
+ h,
+ ghTable,
+ cacheTable);
+ if (factors == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, g);
+ Cudd_RecursiveDeref(dd, h);
+ }
+ return(factors);
}
H = Cudd_Regular(factorsNv->h);
@@ -1544,29 +1572,29 @@ ZeroCase(
Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node));
/* if the child below is a variable */
if ((Hv == zero) || (Hnv == zero)) {
- g = factorsNv->g;
- h = cuddBddAndRecur(dd, x, factorsNv->h);
- if (h!= NULL) cuddRef(h);
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, x);
- if (h == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- return NULL;
- }
- /* CheckTablesCacheAndReturn responsible for allocating
- * factors structure.g,h referenced for table store
- */
- factors = CheckTablesCacheAndReturn(node,
- g,
- h,
- ghTable,
- cacheTable);
- if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, g);
- Cudd_RecursiveDeref(dd, h);
- }
- return(factors);
+ g = factorsNv->g;
+ h = cuddBddAndRecur(dd, x, factorsNv->h);
+ if (h!= NULL) cuddRef(h);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, x);
+ if (h == NULL) {
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ return NULL;
+ }
+ /* CheckTablesCacheAndReturn responsible for allocating
+ * factors structure.g,h referenced for table store
+ */
+ factors = CheckTablesCacheAndReturn(node,
+ g,
+ h,
+ ghTable,
+ cacheTable);
+ if (factors == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, g);
+ Cudd_RecursiveDeref(dd, h);
+ }
+ return(factors);
}
/* build g1 = x*g; h1 = h */
@@ -1576,60 +1604,60 @@ ZeroCase(
g1 = cuddBddAndRecur(dd, x, factorsNv->g);
if (g1 != NULL) cuddRef(g1);
if (g1 == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, factorsNv->h);
- return NULL;
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ return NULL;
}
g2 = factorsNv->g;
h2 = cuddBddAndRecur(dd, x, factorsNv->h);
if (h2 != NULL) cuddRef(h2);
if (h2 == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, factorsNv->g);
- return NULL;
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ return NULL;
}
/* check whether any pair is in tables */
factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
if (outOfMem) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- Cudd_RecursiveDeref(dd, g2);
- Cudd_RecursiveDeref(dd, h2);
- return NULL;
- }
- if (factors != NULL) {
- if ((factors->g == g1) || (factors->g == h1)) {
- Cudd_RecursiveDeref(dd, g2);
- Cudd_RecursiveDeref(dd, h2);
- } else {
+ dd->errorCode = CUDD_MEMORY_OUT;
Cudd_RecursiveDeref(dd, g1);
Cudd_RecursiveDeref(dd, h1);
+ Cudd_RecursiveDeref(dd, g2);
+ Cudd_RecursiveDeref(dd, h2);
+ return NULL;
}
- return factors;
+ if (factors != NULL) {
+ if ((factors->g == g1) || (factors->g == h1)) {
+ Cudd_RecursiveDeref(dd, g2);
+ Cudd_RecursiveDeref(dd, h2);
+ } else {
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
+ }
+ return factors;
}
/* check for each pair in tables and choose one */
factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- Cudd_RecursiveDeref(dd, g2);
- Cudd_RecursiveDeref(dd, h2);
- } else {
- /* now free what was created and not used */
- if ((factors->g == g1) || (factors->g == h1)) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
Cudd_RecursiveDeref(dd, g2);
Cudd_RecursiveDeref(dd, h2);
} else {
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- }
+ /* now free what was created and not used */
+ if ((factors->g == g1) || (factors->g == h1)) {
+ Cudd_RecursiveDeref(dd, g2);
+ Cudd_RecursiveDeref(dd, h2);
+ } else {
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
+ }
}
-
+
return(factors);
} /* end of ZeroCase */
@@ -1665,8 +1693,7 @@ BuildConjuncts(
st_table * mintermTable)
{
int topid, distance;
- Conjuncts *factorsNv = NULL, *factorsNnv = NULL; // Suppress "might be used uninitialized"
- Conjuncts *factors;
+ Conjuncts *factorsNv, *factorsNnv, *factors;
Conjuncts *dummy;
DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
double minNv = 0.0, minNnv = 0.0;
@@ -1679,82 +1706,82 @@ BuildConjuncts(
/* if f is constant, return (f,f) */
if (Cudd_IsConstant(node)) {
- factors = ABC_ALLOC(Conjuncts, 1);
- if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- return(NULL);
- }
- factors->g = node;
- factors->h = node;
- return(FactorsComplement(factors));
+ factors = ABC_ALLOC(Conjuncts, 1);
+ if (factors == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(NULL);
+ }
+ factors->g = node;
+ factors->h = node;
+ return(FactorsComplement(factors));
}
/* If result (a pair of conjuncts) in cache, return the factors. */
- if (st_lookup(cacheTable, (char *)node, (char **)&dummy)) {
- factors = dummy;
- return(factors);
+ if (st_lookup(cacheTable, (const char *)node, (char **)&dummy)) {
+ factors = dummy;
+ return(factors);
}
/* check distance and local reference count of this node */
N = Cudd_Regular(node);
- if (!st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) {
- (void) fprintf(dd->err, "Not in table, Something wrong\n");
- dd->errorCode = CUDD_INTERNAL_ERROR;
- return(NULL);
+ if (!st_lookup(distanceTable, (const char *)N, (char **)&nodeStat)) {
+ (void) fprintf(dd->err, "Not in table, Something wrong\n");
+ dd->errorCode = CUDD_INTERNAL_ERROR;
+ return(NULL);
}
distance = nodeStat->distance;
/* at or below decomposition point, return (f, 1) */
if (((nodeStat->localRef > maxLocalRef*2/3) &&
- (distance < approxDistance*2/3)) ||
- (distance <= approxDistance/4)) {
- factors = ABC_ALLOC(Conjuncts, 1);
- if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- return(NULL);
- }
- /* alternate assigning (f,1) */
- value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
- if (value == 3) {
- if (!lastTimeG) {
+ (distance < approxDistance*2/3)) ||
+ (distance <= approxDistance/4)) {
+ factors = ABC_ALLOC(Conjuncts, 1);
+ if (factors == NULL) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return(NULL);
+ }
+ /* alternate assigning (f,1) */
+ value = 0;
+ if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
+ if (value == 3) {
+ if (!lastTimeG) {
+ factors->g = node;
+ factors->h = one;
+ lastTimeG = 1;
+ } else {
+ factors->g = one;
+ factors->h = node;
+ lastTimeG = 0;
+ }
+ } else if (value == 1) {
+ factors->g = node;
+ factors->h = one;
+ } else {
+ factors->g = one;
+ factors->h = node;
+ }
+ } else if (!lastTimeG) {
factors->g = node;
factors->h = one;
lastTimeG = 1;
+ value = 1;
+ if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ ABC_FREE(factors);
+ return NULL;
+ }
} else {
factors->g = one;
factors->h = node;
- lastTimeG = 0;
- }
- } else if (value == 1) {
- factors->g = node;
- factors->h = one;
- } else {
- factors->g = one;
- factors->h = node;
- }
- } else if (!lastTimeG) {
- factors->g = node;
- factors->h = one;
- lastTimeG = 1;
- value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
- dd->errorCode = CUDD_MEMORY_OUT;
- ABC_FREE(factors);
- return NULL;
- }
- } else {
- factors->g = one;
- factors->h = node;
- lastTimeG = 0;
- value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
- dd->errorCode = CUDD_MEMORY_OUT;
- ABC_FREE(factors);
- return NULL;
+ lastTimeG = 0;
+ value = 2;
+ if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ ABC_FREE(factors);
+ return NULL;
+ }
}
- }
- return(FactorsComplement(factors));
+ return(FactorsComplement(factors));
}
/* get the children and recur */
@@ -1767,87 +1794,87 @@ BuildConjuncts(
* minterms. We go first where there are more minterms.
*/
if (!Cudd_IsConstant(Nv)) {
- if (!st_lookup(mintermTable, (char *)Nv, (char **)&doubleDummy)) {
- (void) fprintf(dd->err, "Not in table: Something wrong\n");
- dd->errorCode = CUDD_INTERNAL_ERROR;
- return(NULL);
- }
- minNv = *doubleDummy;
+ if (!st_lookup(mintermTable, (const char *)Nv, (char **)&doubleDummy)) {
+ (void) fprintf(dd->err, "Not in table: Something wrong\n");
+ dd->errorCode = CUDD_INTERNAL_ERROR;
+ return(NULL);
+ }
+ minNv = *doubleDummy;
}
if (!Cudd_IsConstant(Nnv)) {
- if (!st_lookup(mintermTable, (char *)Nnv, (char **)&doubleDummy)) {
- (void) fprintf(dd->err, "Not in table: Something wrong\n");
- dd->errorCode = CUDD_INTERNAL_ERROR;
- return(NULL);
- }
- minNnv = *doubleDummy;
+ if (!st_lookup(mintermTable, (const char *)Nnv, (char **)&doubleDummy)) {
+ (void) fprintf(dd->err, "Not in table: Something wrong\n");
+ dd->errorCode = CUDD_INTERNAL_ERROR;
+ return(NULL);
+ }
+ minNnv = *doubleDummy;
}
if (minNv < minNnv) {
- temp = Nv;
- Nv = Nnv;
- Nnv = temp;
- switched = 1;
+ temp = Nv;
+ Nv = Nnv;
+ Nnv = temp;
+ switched = 1;
}
/* build gt, ht recursively */
if (Nv != zero) {
- factorsNv = BuildConjuncts(dd, Nv, distanceTable,
- cacheTable, approxDistance, maxLocalRef,
- ghTable, mintermTable);
- if (factorsNv == NULL) return(NULL);
- freeNv = FactorsNotStored(factorsNv);
- factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
- cuddRef(factorsNv->g);
- cuddRef(factorsNv->h);
-
- /* Deal with the zero case */
- if (Nnv == zero) {
- /* is responsible for freeing factorsNv */
- factors = ZeroCase(dd, node, factorsNv, ghTable,
- cacheTable, switched);
- if (freeNv) ABC_FREE(factorsNv);
- return(factors);
- }
+ factorsNv = BuildConjuncts(dd, Nv, distanceTable,
+ cacheTable, approxDistance, maxLocalRef,
+ ghTable, mintermTable);
+ if (factorsNv == NULL) return(NULL);
+ freeNv = FactorsNotStored(factorsNv);
+ factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
+ cuddRef(factorsNv->g);
+ cuddRef(factorsNv->h);
+
+ /* Deal with the zero case */
+ if (Nnv == zero) {
+ /* is responsible for freeing factorsNv */
+ factors = ZeroCase(dd, node, factorsNv, ghTable,
+ cacheTable, switched);
+ if (freeNv) ABC_FREE(factorsNv);
+ return(factors);
+ }
}
/* build ge, he recursively */
if (Nnv != zero) {
- factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
- cacheTable, approxDistance, maxLocalRef,
- ghTable, mintermTable);
- if (factorsNnv == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, factorsNv->h);
- if (freeNv) ABC_FREE(factorsNv);
- return(NULL);
- }
- freeNnv = FactorsNotStored(factorsNnv);
- factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
- cuddRef(factorsNnv->g);
- cuddRef(factorsNnv->h);
-
- /* Deal with the zero case */
- if (Nv == zero) {
- /* is responsible for freeing factorsNv */
- factors = ZeroCase(dd, node, factorsNnv, ghTable,
- cacheTable, switched);
- if (freeNnv) ABC_FREE(factorsNnv);
- return(factors);
- }
+ factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
+ cacheTable, approxDistance, maxLocalRef,
+ ghTable, mintermTable);
+ if (factorsNnv == NULL) {
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ if (freeNv) ABC_FREE(factorsNv);
+ return(NULL);
+ }
+ freeNnv = FactorsNotStored(factorsNnv);
+ factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
+ cuddRef(factorsNnv->g);
+ cuddRef(factorsNnv->h);
+
+ /* Deal with the zero case */
+ if (Nv == zero) {
+ /* is responsible for freeing factorsNv */
+ factors = ZeroCase(dd, node, factorsNnv, ghTable,
+ cacheTable, switched);
+ if (freeNnv) ABC_FREE(factorsNnv);
+ return(factors);
+ }
}
/* construct the 2 pairs */
/* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
/* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
if (switched) {
- factors = factorsNnv;
- factorsNnv = factorsNv;
- factorsNv = factors;
- freeTemp = freeNv;
- freeNv = freeNnv;
- freeNnv = freeTemp;
+ factors = factorsNnv;
+ factorsNnv = factorsNv;
+ factorsNv = factors;
+ freeTemp = freeNv;
+ freeNv = freeNnv;
+ freeNnv = freeTemp;
}
/* Build the factors for this node. */
@@ -1856,42 +1883,42 @@ BuildConjuncts(
g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g);
if (g1 == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, factorsNnv->g);
- Cudd_RecursiveDeref(dd, factorsNnv->h);
- if (freeNv) ABC_FREE(factorsNv);
- if (freeNnv) ABC_FREE(factorsNnv);
- return(NULL);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, factorsNnv->g);
+ Cudd_RecursiveDeref(dd, factorsNnv->h);
+ if (freeNv) ABC_FREE(factorsNv);
+ if (freeNnv) ABC_FREE(factorsNnv);
+ return(NULL);
}
cuddRef(g1);
h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h);
if (h1 == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, factorsNnv->g);
- Cudd_RecursiveDeref(dd, factorsNnv->h);
- Cudd_RecursiveDeref(dd, g1);
- if (freeNv) ABC_FREE(factorsNv);
- if (freeNnv) ABC_FREE(factorsNnv);
- return(NULL);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, factorsNnv->g);
+ Cudd_RecursiveDeref(dd, factorsNnv->h);
+ Cudd_RecursiveDeref(dd, g1);
+ if (freeNv) ABC_FREE(factorsNv);
+ if (freeNnv) ABC_FREE(factorsNnv);
+ return(NULL);
}
cuddRef(h1);
g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h);
if (g2 == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, factorsNnv->g);
- Cudd_RecursiveDeref(dd, factorsNnv->h);
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- if (freeNv) ABC_FREE(factorsNv);
- if (freeNnv) ABC_FREE(factorsNnv);
- return(NULL);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, factorsNnv->g);
+ Cudd_RecursiveDeref(dd, factorsNnv->h);
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
+ if (freeNv) ABC_FREE(factorsNv);
+ if (freeNnv) ABC_FREE(factorsNnv);
+ return(NULL);
}
cuddRef(g2);
Cudd_RecursiveDeref(dd, factorsNv->g);
@@ -1899,16 +1926,16 @@ BuildConjuncts(
h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g);
if (h2 == NULL) {
- Cudd_RecursiveDeref(dd, factorsNv->g);
- Cudd_RecursiveDeref(dd, factorsNv->h);
- Cudd_RecursiveDeref(dd, factorsNnv->g);
- Cudd_RecursiveDeref(dd, factorsNnv->h);
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- Cudd_RecursiveDeref(dd, g2);
- if (freeNv) ABC_FREE(factorsNv);
- if (freeNnv) ABC_FREE(factorsNnv);
- return(NULL);
+ Cudd_RecursiveDeref(dd, factorsNv->g);
+ Cudd_RecursiveDeref(dd, factorsNv->h);
+ Cudd_RecursiveDeref(dd, factorsNnv->g);
+ Cudd_RecursiveDeref(dd, factorsNnv->h);
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
+ Cudd_RecursiveDeref(dd, g2);
+ if (freeNv) ABC_FREE(factorsNv);
+ if (freeNnv) ABC_FREE(factorsNnv);
+ return(NULL);
}
cuddRef(h2);
Cudd_RecursiveDeref(dd, factorsNv->h);
@@ -1919,43 +1946,43 @@ BuildConjuncts(
/* check for each pair in tables and choose one */
factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
if (outOfMem) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- Cudd_RecursiveDeref(dd, g2);
- Cudd_RecursiveDeref(dd, h2);
- return(NULL);
- }
- if (factors != NULL) {
- if ((factors->g == g1) || (factors->g == h1)) {
- Cudd_RecursiveDeref(dd, g2);
- Cudd_RecursiveDeref(dd, h2);
- } else {
+ dd->errorCode = CUDD_MEMORY_OUT;
Cudd_RecursiveDeref(dd, g1);
Cudd_RecursiveDeref(dd, h1);
+ Cudd_RecursiveDeref(dd, g2);
+ Cudd_RecursiveDeref(dd, h2);
+ return(NULL);
}
- return(factors);
+ if (factors != NULL) {
+ if ((factors->g == g1) || (factors->g == h1)) {
+ Cudd_RecursiveDeref(dd, g2);
+ Cudd_RecursiveDeref(dd, h2);
+ } else {
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
+ }
+ return(factors);
}
/* if not in tables, pick one pair */
factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
if (factors == NULL) {
- dd->errorCode = CUDD_MEMORY_OUT;
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- Cudd_RecursiveDeref(dd, g2);
- Cudd_RecursiveDeref(dd, h2);
- } else {
- /* now free what was created and not used */
- if ((factors->g == g1) || (factors->g == h1)) {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
Cudd_RecursiveDeref(dd, g2);
Cudd_RecursiveDeref(dd, h2);
} else {
- Cudd_RecursiveDeref(dd, g1);
- Cudd_RecursiveDeref(dd, h1);
- }
+ /* now free what was created and not used */
+ if ((factors->g == g1) || (factors->g == h1)) {
+ Cudd_RecursiveDeref(dd, g2);
+ Cudd_RecursiveDeref(dd, h2);
+ } else {
+ Cudd_RecursiveDeref(dd, g1);
+ Cudd_RecursiveDeref(dd, h1);
+ }
}
-
+
return(factors);
} /* end of BuildConjuncts */
@@ -1999,7 +2026,7 @@ cuddConjunctsAux(
*c2 = NULL;
/* initialize distances table */
- distanceTable = st_init_table(st_ptrcmp, st_ptrhash);;
+ distanceTable = st_init_table(st_ptrcmp,st_ptrhash);
if (distanceTable == NULL) goto outOfMem;
/* make the entry for the constant */
@@ -2008,7 +2035,7 @@ cuddConjunctsAux(
nodeStat->distance = 0;
nodeStat->localRef = 1;
if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) {
- goto outOfMem;
+ goto outOfMem;
}
/* Count node distances from constant. */
@@ -2020,18 +2047,18 @@ cuddConjunctsAux(
distance = nodeStat->distance;
if (distance < approxDistance) {
- /* Too small to bother. */
- *c1 = f;
- *c2 = DD_ONE(dd);
- cuddRef(*c1); cuddRef(*c2);
- stGen = st_init_gen(distanceTable);
- if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ABC_FREE(value);
- }
- st_free_gen(stGen); stGen = NULL;
- st_free_table(distanceTable);
- return(1);
+ /* Too small to bother. */
+ *c1 = f;
+ *c2 = DD_ONE(dd);
+ cuddRef(*c1); cuddRef(*c2);
+ stGen = st_init_gen(distanceTable);
+ if (stGen == NULL) goto outOfMem;
+ while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ ABC_FREE(value);
+ }
+ st_free_gen(stGen); stGen = NULL;
+ st_free_table(distanceTable);
+ return(1);
}
/* record the maximum local reference count */
@@ -2039,16 +2066,16 @@ cuddConjunctsAux(
stGen = st_init_gen(distanceTable);
if (stGen == NULL) goto outOfMem;
while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- nodeStat = (NodeStat *)value;
- maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
- nodeStat->localRef : maxLocalRef;
+ nodeStat = (NodeStat *)value;
+ maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
+ nodeStat->localRef : maxLocalRef;
}
st_free_gen(stGen); stGen = NULL;
-
+
/* Count minterms for each node. */
max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
- mintermTable = st_init_table(st_ptrcmp, st_ptrhash);;
+ mintermTable = st_init_table(st_ptrcmp,st_ptrhash);
if (mintermTable == NULL) goto outOfMem;
minterms = CountMinterms(f, max, mintermTable, dd->err);
if (minterms == -1.0) goto outOfMem;
@@ -2061,14 +2088,14 @@ cuddConjunctsAux(
/* Build conjuncts. */
factors = BuildConjuncts(dd, f, distanceTable, cacheTable,
- approxDistance, maxLocalRef, ghTable, mintermTable);
+ approxDistance, maxLocalRef, ghTable, mintermTable);
if (factors == NULL) goto outOfMem;
- /* Free up tables */
+ /* free up tables */
stGen = st_init_gen(distanceTable);
if (stGen == NULL) goto outOfMem;
while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ABC_FREE(value);
+ ABC_FREE(value);
}
st_free_gen(stGen); stGen = NULL;
st_free_table(distanceTable); distanceTable = NULL;
@@ -2077,7 +2104,7 @@ cuddConjunctsAux(
stGen = st_init_gen(mintermTable);
if (stGen == NULL) goto outOfMem;
while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ABC_FREE(value);
+ ABC_FREE(value);
}
st_free_gen(stGen); stGen = NULL;
st_free_table(mintermTable); mintermTable = NULL;
@@ -2085,33 +2112,33 @@ cuddConjunctsAux(
freeFactors = FactorsNotStored(factors);
factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
if (factors != NULL) {
- *c1 = factors->g;
- *c2 = factors->h;
- cuddRef(*c1);
- cuddRef(*c2);
- if (freeFactors) ABC_FREE(factors);
-
+ *c1 = factors->g;
+ *c2 = factors->h;
+ cuddRef(*c1);
+ cuddRef(*c2);
+ if (freeFactors) ABC_FREE(factors);
+
#if 0
- if ((*c1 == f) && (!Cudd_IsConstant(f))) {
- assert(*c2 == one);
- }
- if ((*c2 == f) && (!Cudd_IsConstant(f))) {
- assert(*c1 == one);
- }
-
- if ((*c1 != one) && (!Cudd_IsConstant(f))) {
- assert(!Cudd_bddLeq(dd, *c2, *c1));
- }
- if ((*c2 != one) && (!Cudd_IsConstant(f))) {
- assert(!Cudd_bddLeq(dd, *c1, *c2));
- }
+ if ((*c1 == f) && (!Cudd_IsConstant(f))) {
+ assert(*c2 == one);
+ }
+ if ((*c2 == f) && (!Cudd_IsConstant(f))) {
+ assert(*c1 == one);
+ }
+
+ if ((*c1 != one) && (!Cudd_IsConstant(f))) {
+ assert(!Cudd_bddLeq(dd, *c2, *c1));
+ }
+ if ((*c2 != one) && (!Cudd_IsConstant(f))) {
+ assert(!Cudd_bddLeq(dd, *c1, *c2));
+ }
#endif
}
stGen = st_init_gen(cacheTable);
if (stGen == NULL) goto outOfMem;
while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ConjunctsFree(dd, (Conjuncts *)value);
+ ConjunctsFree(dd, (Conjuncts *)value);
}
st_free_gen(stGen); stGen = NULL;
@@ -2121,36 +2148,38 @@ cuddConjunctsAux(
outOfMem:
if (distanceTable != NULL) {
- stGen = st_init_gen(distanceTable);
- if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ABC_FREE(value);
- }
- st_free_gen(stGen); stGen = NULL;
- st_free_table(distanceTable); distanceTable = NULL;
+ stGen = st_init_gen(distanceTable);
+ if (stGen == NULL) goto outOfMem;
+ while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ ABC_FREE(value);
+ }
+ st_free_gen(stGen); stGen = NULL;
+ st_free_table(distanceTable); distanceTable = NULL;
}
if (mintermTable != NULL) {
- stGen = st_init_gen(mintermTable);
- if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ABC_FREE(value);
- }
- st_free_gen(stGen); stGen = NULL;
- st_free_table(mintermTable); mintermTable = NULL;
+ stGen = st_init_gen(mintermTable);
+ if (stGen == NULL) goto outOfMem;
+ while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ ABC_FREE(value);
+ }
+ st_free_gen(stGen); stGen = NULL;
+ st_free_table(mintermTable); mintermTable = NULL;
}
if (ghTable != NULL) st_free_table(ghTable);
if (cacheTable != NULL) {
- stGen = st_init_gen(cacheTable);
- if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
- ConjunctsFree(dd, (Conjuncts *)value);
- }
- st_free_gen(stGen); stGen = NULL;
- st_free_table(cacheTable); cacheTable = NULL;
+ stGen = st_init_gen(cacheTable);
+ if (stGen == NULL) goto outOfMem;
+ while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ ConjunctsFree(dd, (Conjuncts *)value);
+ }
+ st_free_gen(stGen); stGen = NULL;
+ st_free_table(cacheTable); cacheTable = NULL;
}
dd->errorCode = CUDD_MEMORY_OUT;
return(0);
} /* end of cuddConjunctsAux */
+
+
ABC_NAMESPACE_IMPL_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 22:57:57 +0000