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.c270
1 files changed, 135 insertions, 135 deletions
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 0f5714d1..1d534670 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -129,15 +129,15 @@ long lastTimeG;
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static NodeStat * CreateBotDist (DdNode * node, st_table * distanceTable);
-static double CountMinterms (DdNode * node, double max, st_table * mintermTable, FILE *fp);
+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 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***************************************************************/
@@ -771,7 +771,7 @@ Cudd_bddVarDisjDecomp(
static NodeStat *
CreateBotDist(
DdNode * node,
- st_table * distanceTable)
+ st__table * distanceTable)
{
DdNode *N, *Nv, *Nnv;
int distance, distanceNv, distanceNnv;
@@ -785,7 +785,7 @@ CreateBotDist(
/* Return the entry in the table if found. */
N = Cudd_Regular(node);
- if (st_lookup(distanceTable, (const char *)N, (char **)&nodeStat)) {
+ if ( st__lookup(distanceTable, (const char *)N, (char **)&nodeStat)) {
nodeStat->localRef++;
return(nodeStat);
}
@@ -815,8 +815,8 @@ CreateBotDist(
nodeStat->distance = distance;
nodeStat->localRef = 1;
- if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
- ST_OUT_OF_MEM) {
+ if ( st__insert(distanceTable, (char *)N, (char *)nodeStat) ==
+ st__OUT_OF_MEM) {
return(0);
}
@@ -841,7 +841,7 @@ static double
CountMinterms(
DdNode * node,
double max,
- st_table * mintermTable,
+ st__table * mintermTable,
FILE *fp)
{
DdNode *N, *Nv, *Nnv;
@@ -859,7 +859,7 @@ CountMinterms(
}
/* Return the entry in the table if found. */
- if (st_lookup(mintermTable, (const char *)node, (char **)&dummy)) {
+ if ( st__lookup(mintermTable, (const char *)node, (char **)&dummy)) {
min = *dummy;
return(min);
}
@@ -881,7 +881,7 @@ CountMinterms(
dummy = ABC_ALLOC(double, 1);
if (dummy == NULL) return(-1.0);
*dummy = min;
- if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
+ if ( st__insert(mintermTable, (char *)node, (char *)dummy) == st__OUT_OF_MEM) {
(void) fprintf(fp, "st table insert failed\n");
}
return(min);
@@ -944,14 +944,14 @@ static int
PairInTables(
DdNode * g,
DdNode * h,
- st_table * ghTable)
+ st__table * ghTable)
{
int valueG, valueH, gPresent, hPresent;
valueG = valueH = gPresent = hPresent = 0;
- gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
- hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
+ gPresent = st__lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
+ hPresent = st__lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
if (!gPresent && !hPresent) return(NONE);
@@ -995,8 +995,8 @@ CheckTablesCacheAndReturn(
DdNode * node,
DdNode * g,
DdNode * h,
- st_table * ghTable,
- st_table * cacheTable)
+ st__table * ghTable,
+ st__table * cacheTable)
{
int pairValue;
int value;
@@ -1014,13 +1014,13 @@ CheckTablesCacheAndReturn(
if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
if (g != one) {
value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
+ 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g),
+ (char *)(long)value) == st__OUT_OF_MEM) {
return(NULL);
}
}
@@ -1029,13 +1029,13 @@ CheckTablesCacheAndReturn(
} else if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
if (h != one) {
value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
+ 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h),
+ (char *)(long)value) == st__OUT_OF_MEM) {
return(NULL);
}
}
@@ -1044,8 +1044,8 @@ CheckTablesCacheAndReturn(
} 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g),
+ (char *)(long)value) == st__OUT_OF_MEM) {
return(NULL);
}
}
@@ -1054,8 +1054,8 @@ CheckTablesCacheAndReturn(
} 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h),
+ (char *)(long)value) == st__OUT_OF_MEM) {
return(NULL);
}
}
@@ -1071,7 +1071,7 @@ CheckTablesCacheAndReturn(
}
/* cache the result for this node */
- if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
+ if ( st__insert(cacheTable, (char *)node, (char *)factors) == st__OUT_OF_MEM) {
ABC_FREE(factors);
return(NULL);
}
@@ -1102,8 +1102,8 @@ PickOnePair(
DdNode * h1,
DdNode * g2,
DdNode * h2,
- st_table * ghTable,
- st_table * cacheTable)
+ st__table * ghTable,
+ st__table * cacheTable)
{
int value;
Conjuncts *factors;
@@ -1146,19 +1146,19 @@ PickOnePair(
if (factors->g != one) {
/* insert g in htable */
value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
+ 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) {
+ 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(factors->g),
+ (char *)(long)value) == st__OUT_OF_MEM) {
ABC_FREE(factors);
return(NULL);
}
@@ -1168,19 +1168,19 @@ PickOnePair(
if (factors->h != one) {
/* insert h in htable */
value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
+ 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) {
+ 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(factors->h),
+ (char *)(long)value) == st__OUT_OF_MEM) {
ABC_FREE(factors);
return(NULL);
}
@@ -1188,8 +1188,8 @@ PickOnePair(
}
/* Store factors in cache table for later use. */
- if (st_insert(cacheTable, (char *)node, (char *)factors) ==
- ST_OUT_OF_MEM) {
+ if ( st__insert(cacheTable, (char *)node, (char *)factors) ==
+ st__OUT_OF_MEM) {
ABC_FREE(factors);
return(NULL);
}
@@ -1220,8 +1220,8 @@ CheckInTables(
DdNode * h1,
DdNode * g2,
DdNode * h2,
- st_table * ghTable,
- st_table * cacheTable,
+ st__table * ghTable,
+ st__table * cacheTable,
int * outOfMem)
{
int pairValue1, pairValue2;
@@ -1264,8 +1264,8 @@ CheckInTables(
factors->h = h1;
if (h1 != one) {
value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(h1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h1),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1277,8 +1277,8 @@ CheckInTables(
factors->h = h1;
if (h1 != one) {
value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(h1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h1),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1290,8 +1290,8 @@ CheckInTables(
factors->h = h1;
if (g1 != one) {
value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(g1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g1),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1303,8 +1303,8 @@ CheckInTables(
factors->h = h1;
if (g1 != one) {
value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(g1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g1),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1316,8 +1316,8 @@ CheckInTables(
factors->h = h2;
if (h2 != one) {
value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(h2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h2),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1329,8 +1329,8 @@ CheckInTables(
factors->h = h2;
if (h2 != one) {
value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(h2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h2),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1342,8 +1342,8 @@ CheckInTables(
factors->h = h2;
if (g2 != one) {
value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(g2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g2),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1355,8 +1355,8 @@ CheckInTables(
factors->h = h2;
if (g2 != one) {
value = 3;
- if (st_insert(ghTable, (char *)Cudd_Regular(g2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g2),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1368,8 +1368,8 @@ CheckInTables(
factors->h = g1;
if (h1 != one) {
value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(h1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h1),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1381,8 +1381,8 @@ CheckInTables(
factors->h = g1;
if (g1 != one) {
value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(g1),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g1),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1394,8 +1394,8 @@ CheckInTables(
factors->h = g2;
if (h2 != one) {
value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(h2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(h2),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1407,8 +1407,8 @@ CheckInTables(
factors->h = g2;
if (g2 != one) {
value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(g2),
- (char *)(long)value) == ST_OUT_OF_MEM) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(g2),
+ (char *)(long)value) == st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1417,8 +1417,8 @@ CheckInTables(
}
/* Store factors in cache table for later use. */
- if (st_insert(cacheTable, (char *)node, (char *)factors) ==
- ST_OUT_OF_MEM) {
+ if ( st__insert(cacheTable, (char *)node, (char *)factors) ==
+ st__OUT_OF_MEM) {
*outOfMem = 1;
ABC_FREE(factors);
return(NULL);
@@ -1448,8 +1448,8 @@ ZeroCase(
DdManager * dd,
DdNode * node,
Conjuncts * factorsNv,
- st_table * ghTable,
- st_table * cacheTable,
+ st__table * ghTable,
+ st__table * cacheTable,
int switched)
{
int topid;
@@ -1479,7 +1479,7 @@ ZeroCase(
factors->g = x;
factors->h = factorsNv->h;
/* cache the result*/
- if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
+ 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);
@@ -1488,12 +1488,12 @@ ZeroCase(
}
/* store x in g table, the other node is already in the table */
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
+ 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == st__OUT_OF_MEM) {
dd->errorCode = CUDD_MEMORY_OUT;
return NULL;
}
@@ -1513,7 +1513,7 @@ ZeroCase(
factors->g = factorsNv->g;
factors->h = x;
/* cache the result. */
- if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
+ 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);
@@ -1521,12 +1521,12 @@ ZeroCase(
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)) {
+ 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) {
+ if ( st__insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == st__OUT_OF_MEM) {
dd->errorCode = CUDD_MEMORY_OUT;
return NULL;
}
@@ -1685,12 +1685,12 @@ static Conjuncts *
BuildConjuncts(
DdManager * dd,
DdNode * node,
- st_table * distanceTable,
- st_table * cacheTable,
+ st__table * distanceTable,
+ st__table * cacheTable,
int approxDistance,
int maxLocalRef,
- st_table * ghTable,
- st_table * mintermTable)
+ st__table * ghTable,
+ st__table * mintermTable)
{
int topid, distance;
Conjuncts *factorsNv = NULL, *factorsNnv = NULL, *factors;
@@ -1717,14 +1717,14 @@ BuildConjuncts(
}
/* If result (a pair of conjuncts) in cache, return the factors. */
- if (st_lookup(cacheTable, (const char *)node, (char **)&dummy)) {
+ 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, (const char *)N, (char **)&nodeStat)) {
+ 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);
@@ -1742,7 +1742,7 @@ BuildConjuncts(
}
/* alternate assigning (f,1) */
value = 0;
- if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
+ if ( st__lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
if (value == 3) {
if (!lastTimeG) {
factors->g = node;
@@ -1765,7 +1765,7 @@ BuildConjuncts(
factors->h = one;
lastTimeG = 1;
value = 1;
- if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
+ 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;
@@ -1775,7 +1775,7 @@ BuildConjuncts(
factors->h = node;
lastTimeG = 0;
value = 2;
- if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
+ 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;
@@ -1794,7 +1794,7 @@ BuildConjuncts(
* minterms. We go first where there are more minterms.
*/
if (!Cudd_IsConstant(Nv)) {
- if (!st_lookup(mintermTable, (const char *)Nv, (char **)&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);
@@ -1803,7 +1803,7 @@ BuildConjuncts(
}
if (!Cudd_IsConstant(Nnv)) {
- if (!st_lookup(mintermTable, (const char *)Nnv, (char **)&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);
@@ -2008,11 +2008,11 @@ cuddConjunctsAux(
DdNode ** c1,
DdNode ** c2)
{
- st_table *distanceTable = NULL;
- st_table *cacheTable = NULL;
- st_table *mintermTable = NULL;
- st_table *ghTable = NULL;
- st_generator *stGen;
+ st__table *distanceTable = NULL;
+ st__table *cacheTable = NULL;
+ st__table *mintermTable = NULL;
+ st__table *ghTable = NULL;
+ st__generator *stGen;
char *key, *value;
Conjuncts *factors;
int distance, approxDistance;
@@ -2026,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 */
@@ -2034,7 +2034,7 @@ cuddConjunctsAux(
if (nodeStat == NULL) goto outOfMem;
nodeStat->distance = 0;
nodeStat->localRef = 1;
- if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) {
+ if ( st__insert(distanceTable, (char *)one, (char *)nodeStat) == st__OUT_OF_MEM) {
goto outOfMem;
}
@@ -2051,39 +2051,39 @@ cuddConjunctsAux(
*c1 = f;
*c2 = DD_ONE(dd);
cuddRef(*c1); cuddRef(*c2);
- stGen = st_init_gen(distanceTable);
+ stGen = st__init_gen(distanceTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
ABC_FREE(value);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(distanceTable);
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(distanceTable);
return(1);
}
/* record the maximum local reference count */
maxLocalRef = 0;
- stGen = st_init_gen(distanceTable);
+ stGen = st__init_gen(distanceTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
nodeStat = (NodeStat *)value;
maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
nodeStat->localRef : maxLocalRef;
}
- st_free_gen(stGen); stGen = NULL;
+ 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;
lastTimeG = Cudd_Random() & 1;
- cacheTable = st_init_table(st_ptrcmp, st_ptrhash);
+ cacheTable = st__init_table( st__ptrcmp, st__ptrhash);
if (cacheTable == NULL) goto outOfMem;
- ghTable = st_init_table(st_ptrcmp, st_ptrhash);
+ ghTable = st__init_table( st__ptrcmp, st__ptrhash);
if (ghTable == NULL) goto outOfMem;
/* Build conjuncts. */
@@ -2092,22 +2092,22 @@ cuddConjunctsAux(
if (factors == NULL) goto outOfMem;
/* free up tables */
- stGen = st_init_gen(distanceTable);
+ stGen = st__init_gen(distanceTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
ABC_FREE(value);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(distanceTable); distanceTable = NULL;
- st_free_table(ghTable); ghTable = NULL;
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(distanceTable); distanceTable = NULL;
+ st__free_table(ghTable); ghTable = NULL;
- stGen = st_init_gen(mintermTable);
+ stGen = st__init_gen(mintermTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
ABC_FREE(value);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(mintermTable); mintermTable = NULL;
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(mintermTable); mintermTable = NULL;
freeFactors = FactorsNotStored(factors);
factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
@@ -2135,45 +2135,45 @@ cuddConjunctsAux(
#endif
}
- stGen = st_init_gen(cacheTable);
+ stGen = st__init_gen(cacheTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
ConjunctsFree(dd, (Conjuncts *)value);
}
- st_free_gen(stGen); stGen = NULL;
+ st__free_gen(stGen); stGen = NULL;
- st_free_table(cacheTable); cacheTable = NULL;
+ st__free_table(cacheTable); cacheTable = NULL;
return(1);
outOfMem:
if (distanceTable != NULL) {
- stGen = st_init_gen(distanceTable);
+ stGen = st__init_gen(distanceTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
ABC_FREE(value);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(distanceTable); distanceTable = NULL;
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(distanceTable); distanceTable = NULL;
}
if (mintermTable != NULL) {
- stGen = st_init_gen(mintermTable);
+ stGen = st__init_gen(mintermTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
ABC_FREE(value);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(mintermTable); mintermTable = NULL;
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(mintermTable); mintermTable = NULL;
}
- if (ghTable != NULL) st_free_table(ghTable);
+ if (ghTable != NULL) st__free_table(ghTable);
if (cacheTable != NULL) {
- stGen = st_init_gen(cacheTable);
+ stGen = st__init_gen(cacheTable);
if (stGen == NULL) goto outOfMem;
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ 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;
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(cacheTable); cacheTable = NULL;
}
dd->errorCode = CUDD_MEMORY_OUT;
return(0);
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-21 16:58:21 +0000