summaryrefslogtreecommitdiffstats
path: root/src/bdd
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-09-29 17:11:03 -0400
committerAlan Mishchenko <alanmi@berkeley.edu>2012-09-29 17:11:03 -0400
commit71bdfae94122fff6f245c47721d284f78c286164 (patch)
treec63b5c3eb3fc06d565f32a31d2f82ba273bdafaf /src/bdd
parent5cf9d6ddd7fb5a22731f4d61cc984abc48e3f930 (diff)
downloadabc-71bdfae94122fff6f245c47721d284f78c286164.tar.gz
abc-71bdfae94122fff6f245c47721d284f78c286164.tar.bz2
abc-71bdfae94122fff6f245c47721d284f78c286164.zip
Replacing 'st_table' by 'st__table' to resolve linker problems.
Diffstat (limited to 'src/bdd')
-rw-r--r--src/bdd/cas/casCore.c70
-rw-r--r--src/bdd/cudd/cuddApa.c32
-rw-r--r--src/bdd/cudd/cuddApprox.c76
-rw-r--r--src/bdd/cudd/cuddBddCorr.c42
-rw-r--r--src/bdd/cudd/cuddBridge.c24
-rw-r--r--src/bdd/cudd/cuddCheck.c46
-rw-r--r--src/bdd/cudd/cuddDecomp.c270
-rw-r--r--src/bdd/cudd/cuddEssent.c26
-rw-r--r--src/bdd/cudd/cuddExport.c96
-rw-r--r--src/bdd/cudd/cuddGenCof.c58
-rw-r--r--src/bdd/cudd/cuddGenetic.c44
-rw-r--r--src/bdd/cudd/cuddInt.h12
-rw-r--r--src/bdd/cudd/cuddSat.c70
-rw-r--r--src/bdd/cudd/cuddSign.c22
-rw-r--r--src/bdd/cudd/cuddSplit.c26
-rw-r--r--src/bdd/cudd/cuddSubsetHB.c142
-rw-r--r--src/bdd/cudd/cuddSubsetSP.c112
-rw-r--r--src/bdd/cudd/cuddUtil.c114
-rw-r--r--src/bdd/cudd/cuddZddCount.c56
-rw-r--r--src/bdd/cudd/cuddZddMisc.c14
-rw-r--r--src/bdd/cudd/cuddZddUtil.c36
-rw-r--r--src/bdd/dsd/dsdCheck.c12
-rw-r--r--src/bdd/dsd/dsdInt.h4
-rw-r--r--src/bdd/dsd/dsdLocal.c20
-rw-r--r--src/bdd/dsd/dsdMan.c12
-rw-r--r--src/bdd/dsd/dsdProc.c42
-rw-r--r--src/bdd/dsd/dsdTree.c6
27 files changed, 742 insertions, 742 deletions
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index 941784fd..35b1145c 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -821,13 +821,13 @@ void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char *
// (some part of the code is borrowed from Cudd_DumpDot())
{
int i;
- st_table * visited;
- st_generator * gen = NULL;
+ st__table * visited;
+ st__generator * gen = NULL;
long refAddr, diff, mask;
DdNode * Node, * Else, * ElseR, * Then;
/* Initialize symbol table for visited nodes. */
- visited = st_init_table( st_ptrcmp, st_ptrhash );
+ visited = st__init_table( st__ptrcmp, st__ptrhash );
/* Collect all the nodes of this DD in the symbol table. */
cuddCollectNodes( Cudd_Regular(Func), visited );
@@ -846,12 +846,12 @@ void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char *
/* Find the bits that are different. */
refAddr = ( long )Cudd_Regular(Func);
diff = 0;
- gen = st_init_gen( visited );
- while ( st_gen( gen, ( const char ** ) &Node, NULL ) )
+ gen = st__init_gen( visited );
+ while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
{
diff |= refAddr ^ ( long ) Node;
}
- st_free_gen( gen );
+ st__free_gen( gen );
gen = NULL;
/* Choose the mask. */
@@ -868,8 +868,8 @@ void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char *
fprintf( pFile, "%s 1\n", (Cudd_IsComplement(Func))? "0": "1" );
- gen = st_init_gen( visited );
- while ( st_gen( gen, ( const char ** ) &Node, NULL ) )
+ gen = st__init_gen( visited );
+ while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
{
if ( Node->index == CUDD_MAXINDEX )
{
@@ -904,7 +904,7 @@ void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char *
fprintf( pFile, "1-1 1\n" );
// if the inverter is written, skip
- if ( !st_find( visited, (char *)ElseR, (char ***)&pSlot ) )
+ if ( ! st__find( visited, (char *)ElseR, (char ***)&pSlot ) )
assert( 0 );
if ( *pSlot )
continue;
@@ -916,9 +916,9 @@ void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char *
fprintf( pFile, "0 1\n" );
}
}
- st_free_gen( gen );
+ st__free_gen( gen );
gen = NULL;
- st_free_table( visited );
+ st__free_table( visited );
}
@@ -946,8 +946,8 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
// (some part of the code is borrowed from Cudd_DumpDot())
{
int i;
- st_table * visited;
- st_generator * gen = NULL;
+ st__table * visited;
+ st__generator * gen = NULL;
long refAddr, diff, mask;
DdNode * Node, * Else, * ElseR, * Then;
@@ -972,7 +972,7 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
/* Initialize symbol table for visited nodes. */
- visited = st_init_table( st_ptrcmp, st_ptrhash );
+ visited = st__init_table( st__ptrcmp, st__ptrhash );
/* Collect all the nodes of this DD in the symbol table. */
cuddCollectNodes( Cudd_Regular(bFmin), visited );
@@ -991,12 +991,12 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
/* Find the bits that are different. */
refAddr = ( long )Cudd_Regular(bFmin);
diff = 0;
- gen = st_init_gen( visited );
- while ( st_gen( gen, ( const char ** ) &Node, NULL ) )
+ gen = st__init_gen( visited );
+ while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
{
diff |= refAddr ^ ( long ) Node;
}
- st_free_gen( gen );
+ st__free_gen( gen );
gen = NULL;
/* Choose the mask. */
@@ -1013,8 +1013,8 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
fprintf( pFile, "%s 1\n", (Cudd_IsComplement(bFmin))? "0": "1" );
- gen = st_init_gen( visited );
- while ( st_gen( gen, ( const char ** ) &Node, NULL ) )
+ gen = st__init_gen( visited );
+ while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
{
if ( Node->index == CUDD_MAXINDEX )
{
@@ -1053,9 +1053,9 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
fprintf( pFile, "0 1\n" );
}
}
- st_free_gen( gen );
+ st__free_gen( gen );
gen = NULL;
- st_free_table( visited );
+ st__free_table( visited );
//////////////////////////////////////////////////
@@ -1070,7 +1070,7 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
/// TRANSFER WITH MAPPING ///
////////////////////////////////////////////////////////////////////////
static DdNode * cuddBddTransferPermuteRecur
-ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute ));
+ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute ));
static DdNode * cuddBddTransferPermute
ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute));
@@ -1128,11 +1128,11 @@ DdNode *
cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute )
{
DdNode *res;
- st_table *table = NULL;
- st_generator *gen = NULL;
+ st__table *table = NULL;
+ st__generator *gen = NULL;
DdNode *key, *value;
- table = st_init_table( st_ptrcmp, st_ptrhash );
+ table = st__init_table( st__ptrcmp, st__ptrhash );
if ( table == NULL )
goto failure;
res = cuddBddTransferPermuteRecur( ddS, ddD, f, table, Permute );
@@ -1142,16 +1142,16 @@ cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Perm
/* Dereference all elements in the table and dispose of the table.
** This must be done also if res is NULL to avoid leaks in case of
** reordering. */
- gen = st_init_gen( table );
+ gen = st__init_gen( table );
if ( gen == NULL )
goto failure;
- while ( st_gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
+ while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
{
Cudd_RecursiveDeref( ddD, value );
}
- st_free_gen( gen );
+ st__free_gen( gen );
gen = NULL;
- st_free_table( table );
+ st__free_table( table );
table = NULL;
if ( res != NULL )
@@ -1160,9 +1160,9 @@ cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Perm
failure:
if ( table != NULL )
- st_free_table( table );
+ st__free_table( table );
if ( gen != NULL )
- st_free_gen( gen );
+ st__free_gen( gen );
return ( NULL );
} /* end of cuddBddTransferPermute */
@@ -1182,7 +1182,7 @@ cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Perm
******************************************************************************/
static DdNode *
cuddBddTransferPermuteRecur( DdManager * ddS,
- DdManager * ddD, DdNode * f, st_table * table, int * Permute )
+ DdManager * ddD, DdNode * f, st__table * table, int * Permute )
{
DdNode *ft, *fe, *t, *e, *var, *res;
DdNode *one, *zero;
@@ -1202,7 +1202,7 @@ cuddBddTransferPermuteRecur( DdManager * ddS,
/* Now f is a regular pointer to a non-constant node. */
/* Check the cache. */
- if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
+ if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) )
return ( Cudd_NotCond( res, comple ) );
/* Recursive step. */
@@ -1244,8 +1244,8 @@ cuddBddTransferPermuteRecur( DdManager * ddS,
Cudd_RecursiveDeref( ddD, t );
Cudd_RecursiveDeref( ddD, e );
- if ( st_add_direct( table, ( char * ) f, ( char * ) res ) ==
- ST_OUT_OF_MEM )
+ if ( st__add_direct( table, ( char * ) f, ( char * ) res ) ==
+ st__OUT_OF_MEM )
{
Cudd_RecursiveDeref( ddD, res );
return ( NULL );
diff --git a/src/bdd/cudd/cuddApa.c b/src/bdd/cudd/cuddApa.c
index 91dd1a2f..548461da 100644
--- a/src/bdd/cudd/cuddApa.c
+++ b/src/bdd/cudd/cuddApa.c
@@ -113,8 +113,8 @@ extern "C" {
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static DdApaNumber cuddApaCountMintermAux (DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st_table * table);
-static enum st_retval cuddApaStCountfree (char * key, char * value, char * arg);
+static DdApaNumber cuddApaCountMintermAux (DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st__table * table);
+static enum st__retval cuddApaStCountfree (char * key, char * value, char * arg);
/**AutomaticEnd***************************************************************/
@@ -688,7 +688,7 @@ Cudd_ApaCountMinterm(
int * digits)
{
DdApaNumber max, min;
- st_table *table;
+ st__table *table;
DdApaNumber i,count;
background = manager->background;
@@ -706,7 +706,7 @@ Cudd_ApaCountMinterm(
return(NULL);
}
Cudd_ApaSetToLiteral(*digits,min,0);
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) {
ABC_FREE(max);
ABC_FREE(min);
@@ -716,16 +716,16 @@ Cudd_ApaCountMinterm(
if (i == NULL) {
ABC_FREE(max);
ABC_FREE(min);
- st_foreach(table, cuddApaStCountfree, NULL);
- st_free_table(table);
+ st__foreach(table, cuddApaStCountfree, NULL);
+ st__free_table(table);
return(NULL);
}
count = Cudd_NewApaNumber(*digits);
if (count == NULL) {
ABC_FREE(max);
ABC_FREE(min);
- st_foreach(table, cuddApaStCountfree, NULL);
- st_free_table(table);
+ st__foreach(table, cuddApaStCountfree, NULL);
+ st__free_table(table);
if (Cudd_Regular(node)->ref == 1) ABC_FREE(i);
return(NULL);
}
@@ -736,8 +736,8 @@ Cudd_ApaCountMinterm(
}
ABC_FREE(max);
ABC_FREE(min);
- st_foreach(table, cuddApaStCountfree, NULL);
- st_free_table(table);
+ st__foreach(table, cuddApaStCountfree, NULL);
+ st__free_table(table);
if (Cudd_Regular(node)->ref == 1) ABC_FREE(i);
return(count);
@@ -901,7 +901,7 @@ cuddApaCountMintermAux(
int digits,
DdApaNumber max,
DdApaNumber min,
- st_table * table)
+ st__table * table)
{
DdNode *Nt, *Ne;
DdApaNumber mint, mint1, mint2;
@@ -914,7 +914,7 @@ cuddApaCountMintermAux(
return(max);
}
}
- if (node->ref > 1 && st_lookup(table, (const char *)node, (char **)&mint)) {
+ if (node->ref > 1 && st__lookup(table, (const char *)node, (char **)&mint)) {
return(mint);
}
@@ -947,7 +947,7 @@ cuddApaCountMintermAux(
if (Cudd_Regular(Ne)->ref == 1) ABC_FREE(mint2);
if (node->ref > 1) {
- if (st_insert(table, (char *)node, (char *)mint) == ST_OUT_OF_MEM) {
+ if ( st__insert(table, (char *)node, (char *)mint) == st__OUT_OF_MEM) {
ABC_FREE(mint);
return(NULL);
}
@@ -963,12 +963,12 @@ cuddApaCountMintermAux(
in the visited table.]
Description [Frees the memory used to store the minterm counts
- recorded in the visited table. Returns ST_CONTINUE.]
+ recorded in the visited table. Returns st__CONTINUE.]
SideEffects [None]
******************************************************************************/
-static enum st_retval
+static enum st__retval
cuddApaStCountfree(
char * key,
char * value,
@@ -978,7 +978,7 @@ cuddApaStCountfree(
d = (DdApaNumber) value;
ABC_FREE(d);
- return(ST_CONTINUE);
+ return( st__CONTINUE);
} /* end of cuddApaStCountfree */
diff --git a/src/bdd/cudd/cuddApprox.c b/src/bdd/cudd/cuddApprox.c
index 5df43364..cf0c0d41 100644
--- a/src/bdd/cudd/cuddApprox.c
+++ b/src/bdd/cudd/cuddApprox.c
@@ -132,7 +132,7 @@ 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 */
+ 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 */
@@ -542,7 +542,7 @@ cuddUnderApprox(
if (result == 0) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
@@ -556,7 +556,7 @@ cuddUnderApprox(
info->size, Cudd_DagSize(subset));
#endif
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
#ifdef DD_DEBUG
@@ -632,7 +632,7 @@ cuddRemapUnderApprox(
if (result == 0) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
@@ -646,7 +646,7 @@ cuddRemapUnderApprox(
info->size, Cudd_DagSize(subset));
#endif
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
#ifdef DD_DEBUG
@@ -726,7 +726,7 @@ cuddBiasedUnderApprox(
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
cuddHashTableQuit(cache);
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
@@ -738,7 +738,7 @@ cuddBiasedUnderApprox(
if (result == 0) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
@@ -752,7 +752,7 @@ cuddBiasedUnderApprox(
info->size, Cudd_DagSize(subset));
#endif
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
#ifdef DD_DEBUG
@@ -800,7 +800,7 @@ updateParity(
NodeData *infoN;
DdNode *E;
- if (!st_lookup(info->table, (const char *)node, (char **)&infoN)) return;
+ if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) return;
if ((infoN->parity & newparity) != 0) return;
infoN->parity |= (short) newparity;
if (Cudd_IsConstant(node)) return;
@@ -845,7 +845,7 @@ gatherInfoAux(
N = Cudd_Regular(node);
/* Check whether entry for this node exists. */
- if (st_lookup(info->table, (const char *)N, (char **)&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));
@@ -880,7 +880,7 @@ gatherInfoAux(
}
/* Insert entry for the node in the table. */
- if (st_insert(info->table,(char *)N, (char *)infoN) == ST_OUT_OF_MEM) {
+ if ( st__insert(info->table,(char *)N, (char *)infoN) == st__OUT_OF_MEM) {
return(NULL);
}
return(infoN);
@@ -943,7 +943,7 @@ gatherInfo(
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);
@@ -953,10 +953,10 @@ gatherInfo(
** 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) {
+ 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);
+ st__free_table(info->table);
return(NULL);
}
info->page[0].mintermsP = info->max;
@@ -965,7 +965,7 @@ gatherInfo(
infoTop = gatherInfoAux(node,info,parity);
if (infoTop == NULL) {
ABC_FREE(info->page);
- st_free_table(info->table);
+ st__free_table(info->table);
ABC_FREE(info);
return(NULL);
}
@@ -1019,7 +1019,7 @@ computeSavings(
cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL)
return(0);
- (void) st_lookup(info->table, (const char *)node, (char **)&infoN);
+ (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
item->localRef = infoN->functionRef;
/* Process the queue. */
@@ -1028,7 +1028,7 @@ computeSavings(
node = item->node;
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
if (node == skip) continue;
- (void) st_lookup(info->table, (const char *)node, (char **)&infoN);
+ (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
if (item->localRef != infoN->functionRef) {
/* This node is shared. */
continue;
@@ -1089,14 +1089,14 @@ updateRefs(
item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL)
return(0);
- (void) st_lookup(info->table, (const char *)node, (char **)&infoN);
+ (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, (const char *)skip, (char **)&infoN);
+ (void) st__lookup(info->table, (const char *)skip, (char **)&infoN);
infoN->functionRef++;
}
@@ -1105,7 +1105,7 @@ updateRefs(
item = (LocalQueueItem *) queue->first;
node = item->node;
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
- (void) st_lookup(info->table, (const char *)node, (char **)&infoN);
+ (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
if (infoN->functionRef != 0) {
/* This node is shared or must be skipped. */
continue;
@@ -1115,14 +1115,14 @@ updateRefs(
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);
+ (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);
+ (void) st__lookup(info->table, (const char *)Cudd_Regular(cuddE(node)), (char **)&infoN);
infoN->functionRef--;
}
}
@@ -1201,7 +1201,7 @@ UAmarkNodes(
item = (GlobalQueueItem *) queue->first;
node = item->node;
node = Cudd_Regular(node);
- (void) st_lookup(info->table, (const char *)node, (char **)&infoN);
+ (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
if (safe && infoN->parity == 3) {
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
continue;
@@ -1287,7 +1287,7 @@ UAbuildSubset(
N = Cudd_Regular(node);
- if (st_lookup(info->table, (const char *)N, (char **)&infoN)) {
+ if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
if (infoN->replace == TRUE) {
return(info->zero);
}
@@ -1433,7 +1433,7 @@ RAmarkNodes(
assert(!Cudd_IsComplement(node));
assert(!Cudd_IsConstant(node));
#endif
- if (!st_lookup(info->table, (const char *)node, (char **)&infoN)) {
+ if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
@@ -1459,8 +1459,8 @@ RAmarkNodes(
#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);
+ (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;
@@ -1497,8 +1497,8 @@ RAmarkNodes(
} 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);
+ (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 -
@@ -1555,7 +1555,7 @@ RAmarkNodes(
savings = computeSavings(dd,node,shared,info,localQueue);
if (shared != NULL) {
NodeData *infoS;
- (void) st_lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&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;
@@ -1737,7 +1737,7 @@ BAmarkNodes(
assert(!Cudd_IsComplement(node));
assert(!Cudd_IsConstant(node));
#endif
- if (!st_lookup(info->table, (const char *)node, (char **)&infoN)) {
+ if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
@@ -1764,8 +1764,8 @@ BAmarkNodes(
#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);
+ (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;
@@ -1802,8 +1802,8 @@ BAmarkNodes(
} 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);
+ (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 -
@@ -1860,7 +1860,7 @@ BAmarkNodes(
savings = computeSavings(dd,node,shared,info,localQueue);
if (shared != NULL) {
NodeData *infoS;
- (void) st_lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&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;
@@ -2003,7 +2003,7 @@ RAbuildSubset(
Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
- if (st_lookup(info->table, (const char *)N, (char **)&infoN)) {
+ if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
if (N == node ) {
if (infoN->resultP != NULL) {
return(infoN->resultP);
@@ -2151,7 +2151,7 @@ BAapplyBias(
one = DD_ONE(dd);
zero = Cudd_Not(one);
- if (!st_lookup(info->table, (const char *)f, (char **)&infoF))
+ 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);
diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c
index 4d2c22d6..9cf3c64c 100644
--- a/src/bdd/cudd/cuddBddCorr.c
+++ b/src/bdd/cudd/cuddBddCorr.c
@@ -111,11 +111,11 @@ extern "C" {
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static double bddCorrelationAux (DdManager *dd, DdNode *f, DdNode *g, st_table *table);
-static double bddCorrelationWeightsAux (DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table);
+static double bddCorrelationAux (DdManager *dd, DdNode *f, DdNode *g, st__table *table);
+static double bddCorrelationWeightsAux (DdManager *dd, DdNode *f, DdNode *g, double *prob, st__table *table);
static int CorrelCompare (const char *key1, const char *key2);
static int CorrelHash (const char *key, int modulus);
-static enum st_retval CorrelCleanUp (char *key, char *value, char *arg);
+static enum st__retval CorrelCleanUp (char *key, char *value, char *arg);
/**AutomaticEnd***************************************************************/
@@ -150,18 +150,18 @@ Cudd_bddCorrelation(
DdNode * g)
{
- st_table *table;
+ st__table *table;
double correlation;
#ifdef CORREL_STATS
num_calls = 0;
#endif
- table = st_init_table(CorrelCompare,CorrelHash);
+ table = st__init_table(CorrelCompare,CorrelHash);
if (table == NULL) return((double)CUDD_OUT_OF_MEM);
correlation = bddCorrelationAux(manager,f,g,table);
- st_foreach(table, CorrelCleanUp, NIL(char));
- st_free_table(table);
+ st__foreach(table, CorrelCleanUp, NIL(char));
+ st__free_table(table);
return(correlation);
} /* end of Cudd_bddCorrelation */
@@ -193,18 +193,18 @@ Cudd_bddCorrelationWeights(
double * prob)
{
- st_table *table;
+ st__table *table;
double correlation;
#ifdef CORREL_STATS
num_calls = 0;
#endif
- table = st_init_table(CorrelCompare,CorrelHash);
+ table = st__init_table(CorrelCompare,CorrelHash);
if (table == NULL) return((double)CUDD_OUT_OF_MEM);
correlation = bddCorrelationWeightsAux(manager,f,g,prob,table);
- st_foreach(table, CorrelCleanUp, NIL(char));
- st_free_table(table);
+ st__foreach(table, CorrelCleanUp, NIL(char));
+ st__free_table(table);
return(correlation);
} /* end of Cudd_bddCorrelationWeights */
@@ -238,7 +238,7 @@ bddCorrelationAux(
DdManager * dd,
DdNode * f,
DdNode * g,
- st_table * table)
+ st__table * table)
{
DdNode *Fv, *Fnv, *G, *Gv, *Gnv;
double min, *pmin, min1, min2, *dummy;
@@ -279,7 +279,7 @@ bddCorrelationAux(
** correlation(f,g') = 1 - correlation(f,g)
** to minimize the risk of cancellation.
*/
- if (st_lookup(table, (const char *)entry, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)entry, (char **)&dummy)) {
min = *dummy;
ABC_FREE(entry);
return(min);
@@ -314,7 +314,7 @@ bddCorrelationAux(
}
*pmin = min;
- if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
+ if ( st__insert(table,(char *)entry, (char *)pmin) == st__OUT_OF_MEM) {
ABC_FREE(entry);
ABC_FREE(pmin);
return((double)CUDD_OUT_OF_MEM);
@@ -341,7 +341,7 @@ bddCorrelationWeightsAux(
DdNode * f,
DdNode * g,
double * prob,
- st_table * table)
+ st__table * table)
{
DdNode *Fv, *Fnv, *G, *Gv, *Gnv;
double min, *pmin, min1, min2, *dummy;
@@ -382,7 +382,7 @@ bddCorrelationWeightsAux(
** correlation(f,g') = 1 - correlation(f,g)
** to minimize the risk of cancellation.
*/
- if (st_lookup(table, (const char *)entry, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)entry, (char **)&dummy)) {
min = *dummy;
ABC_FREE(entry);
return(min);
@@ -423,7 +423,7 @@ bddCorrelationWeightsAux(
}
*pmin = min;
- if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
+ if ( st__insert(table,(char *)entry, (char *)pmin) == st__OUT_OF_MEM) {
ABC_FREE(entry);
ABC_FREE(pmin);
return((double)CUDD_OUT_OF_MEM);
@@ -465,7 +465,7 @@ CorrelCompare(
Synopsis [Hashes a hash table entry.]
Description [Hashes a hash table entry. It is patterned after
- st_strhash. Returns a value between 0 and modulus.]
+ st__strhash. Returns a value between 0 and modulus.]
SideEffects [None]
@@ -495,12 +495,12 @@ CorrelHash(
Synopsis [Frees memory associated with hash table.]
Description [Frees memory associated with hash table. Returns
- ST_CONTINUE.]
+ st__CONTINUE.]
SideEffects [None]
******************************************************************************/
-static enum st_retval
+static enum st__retval
CorrelCleanUp(
char * key,
char * value,
@@ -513,7 +513,7 @@ CorrelCleanUp(
ABC_FREE(entry);
d = (double *)value;
ABC_FREE(d);
- return ST_CONTINUE;
+ return st__CONTINUE;
} /* end of CorrelCleanUp */
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index 07db26d0..8cbb22d5 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -121,7 +121,7 @@ static DdNode * addBddDoStrictThreshold (DdManager *dd, DdNode *f, DdNode *val);
static DdNode * addBddDoInterval (DdManager *dd, DdNode *f, DdNode *l, DdNode *u);
static DdNode * addBddDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
static DdNode * ddBddToAddRecur (DdManager *dd, DdNode *B);
-static DdNode * cuddBddTransferRecur (DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table);
+static DdNode * cuddBddTransferRecur (DdManager *ddS, DdManager *ddD, DdNode *f, st__table *table);
/**AutomaticEnd***************************************************************/
@@ -446,11 +446,11 @@ cuddBddTransfer(
DdNode * f)
{
DdNode *res;
- st_table *table = NULL;
- st_generator *gen = NULL;
+ st__table *table = NULL;
+ st__generator *gen = NULL;
DdNode *key, *value;
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) goto failure;
res = cuddBddTransferRecur(ddS, ddD, f, table);
if (res != NULL) cuddRef(res);
@@ -458,20 +458,20 @@ cuddBddTransfer(
/* Dereference all elements in the table and dispose of the table.
** This must be done also if res is NULL to avoid leaks in case of
** reordering. */
- gen = st_init_gen(table);
+ gen = st__init_gen(table);
if (gen == NULL) goto failure;
- while (st_gen(gen, (const char **)&key, (char **)&value)) {
+ while ( st__gen(gen, (const char **)&key, (char **)&value)) {
Cudd_RecursiveDeref(ddD, value);
}
- st_free_gen(gen); gen = NULL;
- st_free_table(table); table = NULL;
+ st__free_gen(gen); gen = NULL;
+ st__free_table(table); table = NULL;
if (res != NULL) cuddDeref(res);
return(res);
failure:
/* No need to free gen because it is always NULL here. */
- if (table != NULL) st_free_table(table);
+ if (table != NULL) st__free_table(table);
return(NULL);
} /* end of cuddBddTransfer */
@@ -954,7 +954,7 @@ cuddBddTransferRecur(
DdManager * ddS,
DdManager * ddD,
DdNode * f,
- st_table * table)
+ st__table * table)
{
DdNode *ft, *fe, *t, *e, *var, *res;
DdNode *one, *zero;
@@ -973,7 +973,7 @@ cuddBddTransferRecur(
/* Now f is a regular pointer to a non-constant node. */
/* Check the cache. */
- if (st_lookup(table, (const char *)f, (char **)&res))
+ if ( st__lookup(table, (const char *)f, (char **)&res))
return(Cudd_NotCond(res,comple));
if ( ddS->TimeStop && clock() > ddS->TimeStop )
@@ -1015,7 +1015,7 @@ cuddBddTransferRecur(
Cudd_RecursiveDeref(ddD, t);
Cudd_RecursiveDeref(ddD, e);
- if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
+ if ( st__add_direct(table, (char *) f, (char *) res) == st__OUT_OF_MEM) {
Cudd_RecursiveDeref(ddD, res);
return(NULL);
}
diff --git a/src/bdd/cudd/cuddCheck.c b/src/bdd/cudd/cuddCheck.c
index fef85a67..32893a4a 100644
--- a/src/bdd/cudd/cuddCheck.c
+++ b/src/bdd/cudd/cuddCheck.c
@@ -148,15 +148,15 @@ Cudd_DebugCheck(
DdNodePtr *nodelist;
DdNode *f;
DdNode *sentinel = &(table->sentinel);
- st_table *edgeTable; /* stores internal ref count for each node */
- st_generator *gen;
+ st__table *edgeTable; /* stores internal ref count for each node */
+ st__generator *gen;
int flag = 0;
int totalNode;
int deadNode;
int index;
- edgeTable = st_init_table(st_ptrcmp,st_ptrhash);
+ edgeTable = st__init_table( st__ptrcmp, st__ptrhash);
if (edgeTable == NULL) return(CUDD_OUT_OF_MEM);
/* Check the BDD/ADD subtables. */
@@ -212,29 +212,29 @@ Cudd_DebugCheck(
/* Increment the internal reference count for the
** then child of the current node.
*/
- if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
+ if ( st__lookup_int(edgeTable,(char *)cuddT(f),&count)) {
count++;
} else {
count = 1;
}
- if (st_insert(edgeTable,(char *)cuddT(f),
- (char *)(long)count) == ST_OUT_OF_MEM) {
- st_free_table(edgeTable);
+ if ( st__insert(edgeTable,(char *)cuddT(f),
+ (char *)(long)count) == st__OUT_OF_MEM) {
+ st__free_table(edgeTable);
return(CUDD_OUT_OF_MEM);
}
/* Increment the internal reference count for the
** else child of the current node.
*/
- if (st_lookup_int(edgeTable,(char *)Cudd_Regular(cuddE(f)),
+ if ( st__lookup_int(edgeTable,(char *)Cudd_Regular(cuddE(f)),
&count)) {
count++;
} else {
count = 1;
}
- if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
- (char *)(long)count) == ST_OUT_OF_MEM) {
- st_free_table(edgeTable);
+ if ( st__insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
+ (char *)(long)count) == st__OUT_OF_MEM) {
+ st__free_table(edgeTable);
return(CUDD_OUT_OF_MEM);
}
} else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
@@ -318,28 +318,28 @@ Cudd_DebugCheck(
/* Increment the internal reference count for the
** then child of the current node.
*/
- if (st_lookup_int(edgeTable,(char *)cuddT(f),&count)) {
+ if ( st__lookup_int(edgeTable,(char *)cuddT(f),&count)) {
count++;
} else {
count = 1;
}
- if (st_insert(edgeTable,(char *)cuddT(f),
- (char *)(long)count) == ST_OUT_OF_MEM) {
- st_free_table(edgeTable);
+ if ( st__insert(edgeTable,(char *)cuddT(f),
+ (char *)(long)count) == st__OUT_OF_MEM) {
+ st__free_table(edgeTable);
return(CUDD_OUT_OF_MEM);
}
/* Increment the internal reference count for the
** else child of the current node.
*/
- if (st_lookup_int(edgeTable,(char *)cuddE(f),&count)) {
+ if ( st__lookup_int(edgeTable,(char *)cuddE(f),&count)) {
count++;
} else {
count = 1;
}
- if (st_insert(edgeTable,(char *)cuddE(f),
- (char *)(long)count) == ST_OUT_OF_MEM) {
- st_free_table(edgeTable);
+ if ( st__insert(edgeTable,(char *)cuddE(f),
+ (char *)(long)count) == st__OUT_OF_MEM) {
+ st__free_table(edgeTable);
table->errorCode = CUDD_MEMORY_OUT;
return(CUDD_OUT_OF_MEM);
}
@@ -411,8 +411,8 @@ Cudd_DebugCheck(
"Error: wrong number of dead nodes in constants\n");
flag = 1;
}
- gen = st_init_gen(edgeTable);
- while (st_gen(gen, (const char **)&f, (char **)&count)) {
+ gen = st__init_gen(edgeTable);
+ while ( st__gen(gen, (const char **)&f, (char **)&count)) {
if (count > (int)(f->ref) && f->ref != DD_MAXREF) {
#if SIZEOF_VOID_P == 8
fprintf(table->err,"ref count error at node 0x%lx, count = %d, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",(ptruint)f,count,f->index,f->ref,(ptruint)cuddT(f),(ptruint)cuddE(f));
@@ -423,8 +423,8 @@ Cudd_DebugCheck(
flag = 1;
}
}
- st_free_gen(gen);
- st_free_table(edgeTable);
+ st__free_gen(gen);
+ st__free_table(edgeTable);
return (flag);
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);
diff --git a/src/bdd/cudd/cuddEssent.c b/src/bdd/cudd/cuddEssent.c
index f2baf37f..fb6f3275 100644
--- a/src/bdd/cudd/cuddEssent.c
+++ b/src/bdd/cudd/cuddEssent.c
@@ -166,7 +166,7 @@ static BitVector *Eolp;
/*---------------------------------------------------------------------------*/
static DdNode * ddFindEssentialRecur (DdManager *dd, DdNode *f);
-static DdTlcInfo * ddFindTwoLiteralClausesRecur (DdManager * dd, DdNode * f, st_table *table);
+static DdTlcInfo * ddFindTwoLiteralClausesRecur (DdManager * dd, DdNode * f, st__table *table);
static DdTlcInfo * computeClauses (DdTlcInfo *Tres, DdTlcInfo *Eres, DdHalfWord label, int size);
static DdTlcInfo * computeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase);
static DdTlcInfo * emptyClauseSet (void);
@@ -279,8 +279,8 @@ Cudd_FindTwoLiteralClauses(
DdNode * f)
{
DdTlcInfo *res;
- st_table *table;
- st_generator *gen;
+ st__table *table;
+ st__generator *gen;
DdTlcInfo *tlc;
DdNode *node;
int size = dd->size;
@@ -289,29 +289,29 @@ Cudd_FindTwoLiteralClauses(
res = emptyClauseSet();
return(res);
}
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) return(NULL);
Tolv = bitVectorAlloc(size);
if (Tolv == NULL) {
- st_free_table(table);
+ st__free_table(table);
return(NULL);
}
Tolp = bitVectorAlloc(size);
if (Tolp == NULL) {
- st_free_table(table);
+ st__free_table(table);
bitVectorFree(Tolv);
return(NULL);
}
Eolv = bitVectorAlloc(size);
if (Eolv == NULL) {
- st_free_table(table);
+ st__free_table(table);
bitVectorFree(Tolv);
bitVectorFree(Tolp);
return(NULL);
}
Eolp = bitVectorAlloc(size);
if (Eolp == NULL) {
- st_free_table(table);
+ st__free_table(table);
bitVectorFree(Tolv);
bitVectorFree(Tolp);
bitVectorFree(Eolv);
@@ -320,12 +320,12 @@ Cudd_FindTwoLiteralClauses(
res = ddFindTwoLiteralClausesRecur(dd,f,table);
/* Dispose of table contents and free table. */
- st_foreach_item(table, gen, (const char **)&node, (char **)&tlc) {
+ st__foreach_item(table, gen, (const char **)&node, (char **)&tlc) {
if (node != f) {
Cudd_tlcInfoFree(tlc);
}
}
- st_free_table(table);
+ st__free_table(table);
bitVectorFree(Tolv);
bitVectorFree(Tolp);
bitVectorFree(Eolv);
@@ -620,7 +620,7 @@ static DdTlcInfo *
ddFindTwoLiteralClausesRecur(
DdManager * dd,
DdNode * f,
- st_table *table)
+ st__table *table)
{
DdNode *T, *E, *F;
DdNode *one, *lzero, *azero;
@@ -633,7 +633,7 @@ ddFindTwoLiteralClausesRecur(
/* Check computed table. Separate entries are necessary for
** a node and its complement. We should update the counter here. */
- if (st_lookup(table, (const char *)f, (char **)&res)) {
+ if ( st__lookup(table, (const char *)f, (char **)&res)) {
return(res);
}
@@ -742,7 +742,7 @@ ddFindTwoLiteralClausesRecur(
}
/* Cache results. */
- if (st_add_direct(table, (char *)f, (char *)res) == ST_OUT_OF_MEM) {
+ if ( st__add_direct(table, (char *)f, (char *)res) == st__OUT_OF_MEM) {
ABC_FREE(res);
return(NULL);
}
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c
index 241c63ec..41735a8c 100644
--- a/src/bdd/cudd/cuddExport.c
+++ b/src/bdd/cudd/cuddExport.c
@@ -99,9 +99,9 @@ static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.22 2009/03/08 02:49:02 fa
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int ddDoDumpBlif (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, int mv);
-static int ddDoDumpDaVinci (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, ptruint mask);
-static int ddDoDumpDDcal (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, ptruint mask);
+static int ddDoDumpBlif (DdManager *dd, DdNode *f, FILE *fp, st__table *visited, char **names, int mv);
+static int ddDoDumpDaVinci (DdManager *dd, DdNode *f, FILE *fp, st__table *visited, char **names, ptruint mask);
+static int ddDoDumpDDcal (DdManager *dd, DdNode *f, FILE *fp, st__table *visited, char **names, ptruint mask);
static int ddDoDumpFactoredForm (DdManager *dd, DdNode *f, FILE *fp, char **names);
/**AutomaticEnd***************************************************************/
@@ -258,12 +258,12 @@ Cudd_DumpBlifBody(
FILE * fp /* pointer to the dump file */,
int mv /* 0: blif, 1: blif-MV */)
{
- st_table *visited = NULL;
+ st__table *visited = NULL;
int retval;
int i;
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
/* Call the function that really gets the job done. */
@@ -301,11 +301,11 @@ Cudd_DumpBlifBody(
if (retval == EOF) goto failure;
}
- st_free_table(visited);
+ st__free_table(visited);
return(1);
failure:
- if (visited != NULL) st_free_table(visited);
+ if (visited != NULL) st__free_table(visited);
return(0);
} /* end of Cudd_DumpBlifBody */
@@ -353,8 +353,8 @@ Cudd_DumpDot(
DdNode *scan;
int *sorted = NULL;
int nvars = dd->size;
- st_table *visited = NULL;
- st_generator *gen = NULL;
+ st__table *visited = NULL;
+ st__generator *gen = NULL;
int retval;
int i, j;
int slots;
@@ -382,7 +382,7 @@ Cudd_DumpDot(
support = NULL; /* so that we do not try to free it in case of failure */
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
/* Collect all the nodes of this DD in the symbol table. */
@@ -405,12 +405,12 @@ Cudd_DumpDot(
/* Find the bits that are different. */
refAddr = (long) Cudd_Regular(f[0]);
diff = 0;
- gen = st_init_gen(visited);
+ gen = st__init_gen(visited);
if (gen == NULL) goto failure;
- while (st_gen(gen, (const char **)&scan, NULL)) {
+ while ( st__gen(gen, (const char **)&scan, NULL)) {
diff |= refAddr ^ (long) scan;
}
- st_free_gen(gen); gen = NULL;
+ st__free_gen(gen); gen = NULL;
/* Choose the mask. */
for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
@@ -482,7 +482,7 @@ Cudd_DumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%lx\";\n", ((mask & (ptrint) scan) / sizeof(DdNode)));
if (retval == EOF) goto failure;
}
@@ -503,7 +503,7 @@ Cudd_DumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%lx\";\n", ((mask & (ptrint) scan) / sizeof(DdNode)));
if (retval == EOF) goto failure;
}
@@ -539,7 +539,7 @@ Cudd_DumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp, "\"%lx\" -> \"%lx\";\n",
((mask & (ptrint) scan) / sizeof(DdNode)),
((mask & (ptrint) cuddT(scan)) / sizeof(DdNode)));
@@ -567,7 +567,7 @@ Cudd_DumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%lx\" [label = \"%g\"];\n",
((mask & (ptrint) scan) / sizeof(DdNode)), cuddV(scan));
if (retval == EOF) goto failure;
@@ -580,14 +580,14 @@ Cudd_DumpDot(
retval = fprintf(fp,"}\n");
if (retval == EOF) goto failure;
- st_free_table(visited);
+ st__free_table(visited);
ABC_FREE(sorted);
return(1);
failure:
if (sorted != NULL) ABC_FREE(sorted);
if (support != NULL) Cudd_RecursiveDeref(dd,support);
- if (visited != NULL) st_free_table(visited);
+ if (visited != NULL) st__free_table(visited);
return(0);
} /* end of Cudd_DumpDot */
@@ -622,14 +622,14 @@ Cudd_DumpDaVinci(
{
DdNode *support = NULL;
DdNode *scan;
- st_table *visited = NULL;
+ st__table *visited = NULL;
int retval;
int i;
- st_generator *gen;
+ st__generator *gen;
ptruint refAddr, diff, mask;
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
/* Collect all the nodes of this DD in the symbol table. */
@@ -652,21 +652,21 @@ Cudd_DumpDaVinci(
/* Find the bits that are different. */
refAddr = (ptruint) Cudd_Regular(f[0]);
diff = 0;
- gen = st_init_gen(visited);
- while (st_gen(gen, (const char **)&scan, NULL)) {
+ gen = st__init_gen(visited);
+ while ( st__gen(gen, (const char **)&scan, NULL)) {
diff |= refAddr ^ (ptruint) scan;
}
- st_free_gen(gen);
+ st__free_gen(gen);
/* Choose the mask. */
for (i = 0; (unsigned) i < 8 * sizeof(ptruint); i += 4) {
mask = (1 << i) - 1;
if (diff <= mask) break;
}
- st_free_table(visited);
+ st__free_table(visited);
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
retval = fprintf(fp, "[");
@@ -696,12 +696,12 @@ Cudd_DumpDaVinci(
retval = fprintf(fp, "]\n");
if (retval == EOF) goto failure;
- st_free_table(visited);
+ st__free_table(visited);
return(1);
failure:
if (support != NULL) Cudd_RecursiveDeref(dd,support);
- if (visited != NULL) st_free_table(visited);
+ if (visited != NULL) st__free_table(visited);
return(0);
} /* end of Cudd_DumpDaVinci */
@@ -738,14 +738,14 @@ Cudd_DumpDDcal(
DdNode *scan;
int *sorted = NULL;
int nvars = dd->size;
- st_table *visited = NULL;
+ st__table *visited = NULL;
int retval;
int i;
- st_generator *gen;
+ st__generator *gen;
ptruint refAddr, diff, mask;
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
/* Collect all the nodes of this DD in the symbol table. */
@@ -768,18 +768,18 @@ Cudd_DumpDDcal(
/* Find the bits that are different. */
refAddr = (ptruint) Cudd_Regular(f[0]);
diff = 0;
- gen = st_init_gen(visited);
- while (st_gen(gen, (const char **)&scan, NULL)) {
+ gen = st__init_gen(visited);
+ while ( st__gen(gen, (const char **)&scan, NULL)) {
diff |= refAddr ^ (ptruint) scan;
}
- st_free_gen(gen);
+ st__free_gen(gen);
/* Choose the mask. */
for (i = 0; (unsigned) i < 8 * sizeof(ptruint); i += 4) {
mask = (1 << i) - 1;
if (diff <= mask) break;
}
- st_free_table(visited);
+ st__free_table(visited);
visited = NULL;
/* Build a bit array with the support of f. */
@@ -817,7 +817,7 @@ Cudd_DumpDDcal(
sorted = NULL;
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
/* Call the function that really gets the job done. */
@@ -853,13 +853,13 @@ Cudd_DumpDDcal(
if (retval == EOF) goto failure;
if ( visited )
- st_free_table(visited);
+ st__free_table(visited);
return(1);
failure:
if (sorted != NULL) ABC_FREE(sorted);
if (support != NULL) Cudd_RecursiveDeref(dd,support);
- if (visited != NULL) st_free_table(visited);
+ if (visited != NULL) st__free_table(visited);
return(0);
} /* end of Cudd_DumpDDcal */
@@ -957,7 +957,7 @@ ddDoDumpBlif(
DdManager * dd,
DdNode * f,
FILE * fp,
- st_table * visited,
+ st__table * visited,
char ** names,
int mv)
{
@@ -969,7 +969,7 @@ ddDoDumpBlif(
#endif
/* If already visited, nothing to do. */
- if (st_is_member(visited, (char *) f) == 1)
+ if ( st__is_member(visited, (char *) f) == 1)
return(1);
/* Check for abnormal condition that should never happen. */
@@ -977,7 +977,7 @@ ddDoDumpBlif(
return(0);
/* Mark node as visited. */
- if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
+ if ( st__insert(visited, (char *) f, NULL) == st__OUT_OF_MEM)
return(0);
/* Check for special case: If constant node, generate constant 1. */
@@ -1118,7 +1118,7 @@ ddDoDumpDaVinci(
DdManager * dd,
DdNode * f,
FILE * fp,
- st_table * visited,
+ st__table * visited,
char ** names,
ptruint mask)
{
@@ -1133,7 +1133,7 @@ ddDoDumpDaVinci(
id = ((ptruint) f & mask) / sizeof(DdNode);
/* If already visited, insert a reference. */
- if (st_is_member(visited, (char *) f) == 1) {
+ if ( st__is_member(visited, (char *) f) == 1) {
retval = fprintf(fp,"r(\"%p\")", (void *) id);
if (retval == EOF) {
return(0);
@@ -1147,7 +1147,7 @@ ddDoDumpDaVinci(
return(0);
/* Mark node as visited. */
- if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
+ if ( st__insert(visited, (char *) f, NULL) == st__OUT_OF_MEM)
return(0);
/* Check for special case: If constant node, generate constant 1. */
@@ -1217,7 +1217,7 @@ ddDoDumpDDcal(
DdManager * dd,
DdNode * f,
FILE * fp,
- st_table * visited,
+ st__table * visited,
char ** names,
ptruint mask)
{
@@ -1232,7 +1232,7 @@ ddDoDumpDDcal(
id = ((ptruint) f & mask) / sizeof(DdNode);
/* If already visited, do nothing. */
- if (st_is_member(visited, (char *) f) == 1) {
+ if ( st__is_member(visited, (char *) f) == 1) {
return(1);
}
@@ -1241,7 +1241,7 @@ ddDoDumpDDcal(
return(0);
/* Mark node as visited. */
- if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
+ if ( st__insert(visited, (char *) f, NULL) == st__OUT_OF_MEM)
return(0);
/* Check for special case: If constant node, assign constant. */
diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c
index 119b07df..8b881344 100644
--- a/src/bdd/cudd/cuddGenCof.c
+++ b/src/bdd/cudd/cuddGenCof.c
@@ -134,11 +134,11 @@ extern "C" {
static int cuddBddConstrainDecomp (DdManager *dd, DdNode *f, DdNode **decomp);
static DdNode * cuddBddCharToVect (DdManager *dd, DdNode *f, DdNode *x);
-static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache);
-static DdNode * cuddBddLICBuildResult (DdManager *dd, DdNode *f, st_table *cache, st_table *table);
+static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st__table *table, st__table *cache);
+static DdNode * cuddBddLICBuildResult (DdManager *dd, DdNode *f, st__table *cache, st__table *table);
static int MarkCacheHash (const char *ptr, int modulus);
static int MarkCacheCompare (const char *ptr1, const char *ptr2);
-static enum st_retval MarkCacheCleanUp (char *key, char *value, char *arg);
+static enum st__retval MarkCacheCleanUp (char *key, char *value, char *arg);
static DdNode * cuddBddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
/**AutomaticEnd***************************************************************/
@@ -1436,7 +1436,7 @@ cuddBddLICompaction(
DdNode * f /* function to be minimized */,
DdNode * c /* constraint (care set) */)
{
- st_table *marktable, *markcache, *buildcache;
+ st__table *marktable, *markcache, *buildcache;
DdNode *res, *zero;
zero = Cudd_Not(DD_ONE(dd));
@@ -1453,31 +1453,31 @@ cuddBddLICompaction(
** appears. Hence, the same node and constrain may give different results
** in successive invocations.
*/
- marktable = st_init_table(st_ptrcmp,st_ptrhash);
+ marktable = st__init_table( st__ptrcmp, st__ptrhash);
if (marktable == NULL) {
return(NULL);
}
- markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
+ markcache = st__init_table(MarkCacheCompare,MarkCacheHash);
if (markcache == NULL) {
- st_free_table(marktable);
+ st__free_table(marktable);
return(NULL);
}
if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
- st_foreach(markcache, MarkCacheCleanUp, NULL);
- st_free_table(marktable);
- st_free_table(markcache);
+ st__foreach(markcache, MarkCacheCleanUp, NULL);
+ st__free_table(marktable);
+ st__free_table(markcache);
return(NULL);
}
- st_foreach(markcache, MarkCacheCleanUp, NULL);
- st_free_table(markcache);
- buildcache = st_init_table(st_ptrcmp,st_ptrhash);
+ st__foreach(markcache, MarkCacheCleanUp, NULL);
+ st__free_table(markcache);
+ buildcache = st__init_table( st__ptrcmp, st__ptrhash);
if (buildcache == NULL) {
- st_free_table(marktable);
+ st__free_table(marktable);
return(NULL);
}
res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
- st_free_table(buildcache);
- st_free_table(marktable);
+ st__free_table(buildcache);
+ st__free_table(marktable);
return(res);
} /* end of cuddBddLICompaction */
@@ -1648,8 +1648,8 @@ cuddBddLICMarkEdges(
DdManager * dd,
DdNode * f,
DdNode * c,
- st_table * table,
- st_table * cache)
+ st__table * table,
+ st__table * cache)
{
DdNode *Fv, *Fnv, *Cv, *Cnv;
DdNode *one, *zero;
@@ -1681,7 +1681,7 @@ cuddBddLICMarkEdges(
return(CUDD_OUT_OF_MEM);
}
key->f = f; key->c = c;
- if (st_lookup_int(cache, (char *)key, &res)) {
+ if ( st__lookup_int(cache, (char *)key, &res)) {
ABC_FREE(key);
if (comple) {
if (res == DD_LIC_0) res = DD_LIC_1;
@@ -1722,7 +1722,7 @@ cuddBddLICMarkEdges(
/* Update edge markings. */
if (topf <= topc) {
- retval = st_find_or_add(table, (char *)f, (char ***)&slot);
+ retval = st__find_or_add(table, (char *)f, (char ***)&slot);
if (retval == 0) {
*slot = (char *) (ptrint)((resT << 2) | resE);
} else if (retval == 1) {
@@ -1735,7 +1735,7 @@ cuddBddLICMarkEdges(
/* Cache result. */
res = resT | resE;
- if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
+ if ( st__insert(cache, (char *)key, (char *)(ptrint)res) == st__OUT_OF_MEM) {
ABC_FREE(key);
return(CUDD_OUT_OF_MEM);
}
@@ -1766,8 +1766,8 @@ static DdNode *
cuddBddLICBuildResult(
DdManager * dd,
DdNode * f,
- st_table * cache,
- st_table * table)
+ st__table * cache,
+ st__table * table)
{
DdNode *Fv, *Fnv, *r, *t, *e;
DdNode *one, *zero;
@@ -1784,12 +1784,12 @@ cuddBddLICBuildResult(
f = Cudd_Regular(f);
/* Check the cache. */
- if (st_lookup(cache, (const char *)f, (char **)&r)) {
+ if ( st__lookup(cache, (const char *)f, (char **)&r)) {
return(Cudd_NotCond(r,comple));
}
/* Retrieve the edge markings. */
- if (st_lookup_int(table, (char *)f, &markings) == 0)
+ if ( st__lookup_int(table, (char *)f, &markings) == 0)
return(NULL);
markT = markings >> 2;
markE = markings & 3;
@@ -1848,7 +1848,7 @@ cuddBddLICBuildResult(
cuddDeref(t);
cuddDeref(e);
- if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
+ if ( st__insert(cache, (char *)f, (char *)r) == st__OUT_OF_MEM) {
cuddRef(r);
Cudd_IterDerefBdd(dd,r);
return(NULL);
@@ -1925,14 +1925,14 @@ MarkCacheCompare(
cuddBddLICMarkEdges.]
Description [Frees memory associated with computed table of
- cuddBddLICMarkEdges. Returns ST_CONTINUE.]
+ cuddBddLICMarkEdges. Returns st__CONTINUE.]
SideEffects [None]
SeeAlso [Cudd_bddLICompaction]
******************************************************************************/
-static enum st_retval
+static enum st__retval
MarkCacheCleanUp(
char * key,
char * value,
@@ -1942,7 +1942,7 @@ MarkCacheCleanUp(
entry = (MarkCacheKey *) key;
ABC_FREE(entry);
- return ST_CONTINUE;
+ return st__CONTINUE;
} /* end of MarkCacheCleanUp */
diff --git a/src/bdd/cudd/cuddGenetic.c b/src/bdd/cudd/cuddGenetic.c
index 3cdbfe7c..a333f3a9 100644
--- a/src/bdd/cudd/cuddGenetic.c
+++ b/src/bdd/cudd/cuddGenetic.c
@@ -118,7 +118,7 @@ static int numvars; /* the number of input variables in the ckt. */
** it is a two-dimensional structure.
*/
static int *storedd;
-static st_table *computed; /* hash table to identify existing orders */
+static st__table *computed; /* hash table to identify existing orders */
static int *repeat; /* how many times an order is present */
static int large; /* stores the index of the population with
** the largest number of nodes in the DD */
@@ -240,7 +240,7 @@ cuddGa(
for (i = 0; i < popsize; i++) {
repeat[i] = 0;
}
- computed = st_init_table(array_compare,array_hash);
+ computed = st__init_table(array_compare,array_hash);
if (computed == NULL) {
table->errorCode = CUDD_MEMORY_OUT;
ABC_FREE(storedd);
@@ -255,10 +255,10 @@ cuddGa(
STOREDD(0,numvars) = table->keys - table->isolated; /* size of initial DD */
/* Store the initial order in the computed table. */
- if (st_insert(computed,(char *)storedd,(char *) 0) == ST_OUT_OF_MEM) {
+ if ( st__insert(computed,(char *)storedd,(char *) 0) == st__OUT_OF_MEM) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
repeat[0]++;
@@ -277,7 +277,7 @@ cuddGa(
table->errorCode = CUDD_MEMORY_OUT;
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
for (i = 1; i < popsize; i++) {
@@ -285,17 +285,17 @@ cuddGa(
if (!result) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
- if (st_lookup_int(computed,(char *)&STOREDD(i,0),&index)) {
+ if ( st__lookup_int(computed,(char *)&STOREDD(i,0),&index)) {
repeat[index]++;
} else {
- if (st_insert(computed,(char *)&STOREDD(i,0),(char *)(long)i) ==
- ST_OUT_OF_MEM) {
+ if ( st__insert(computed,(char *)&STOREDD(i,0),(char *)(long)i) ==
+ st__OUT_OF_MEM) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
repeat[i]++;
@@ -338,7 +338,7 @@ cuddGa(
table->errorCode = CUDD_MEMORY_OUT;
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
/* The offsprings are left in the last two entries of the
@@ -349,7 +349,7 @@ cuddGa(
if (!result) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
large = largest(); /* find the largest DD in population */
@@ -363,22 +363,22 @@ cuddGa(
** Decrease its repetition count. If the repetition count
** goes to 0, remove the largest DD from the computed table.
*/
- result = st_lookup_int(computed,(char *)&STOREDD(large,0),
+ result = st__lookup_int(computed,(char *)&STOREDD(large,0),
&index);
if (!result) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
repeat[index]--;
if (repeat[index] == 0) {
int *pointer = &STOREDD(index,0);
- result = st_delete(computed, (const char **)&pointer, NULL);
+ result = st__delete(computed, (const char **)&pointer, NULL);
if (!result) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
}
@@ -389,15 +389,15 @@ cuddGa(
for (n = 0; n <= numvars; n++) {
STOREDD(large,n) = STOREDD(i,n);
}
- if (st_lookup_int(computed,(char *)&STOREDD(large,0),
+ if ( st__lookup_int(computed,(char *)&STOREDD(large,0),
&index)) {
repeat[index]++;
} else {
- if (st_insert(computed,(char *)&STOREDD(large,0),
- (char *)(long)large) == ST_OUT_OF_MEM) {
+ if ( st__insert(computed,(char *)&STOREDD(large,0),
+ (char *)(long)large) == st__OUT_OF_MEM) {
ABC_FREE(storedd);
ABC_FREE(repeat);
- st_free_table(computed);
+ st__free_table(computed);
return(0);
}
repeat[large]++;
@@ -418,7 +418,7 @@ cuddGa(
#endif
/* Clean up, build the result DD, and return. */
- st_free_table(computed);
+ st__free_table(computed);
computed = NULL;
result = build_dd(table,small,lower,upper);
ABC_FREE(storedd);
@@ -565,7 +565,7 @@ build_dd(
/* Check the computed table. If the order already exists, it
** suffices to copy the size from the existing entry.
*/
- if (computed && st_lookup_int(computed,(char *)&STOREDD(num,0),&index)) {
+ if (computed && st__lookup_int(computed,(char *)&STOREDD(num,0),&index)) {
STOREDD(num,numvars) = STOREDD(index,numvars);
#ifdef DD_STATS
(void) fprintf(table->out,"\nCache hit for index %d", index);
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index 737d211c..07ae3e6c 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -475,7 +475,7 @@ struct DdManager { /* specialized DD symbol table */
array_t *order; /* copy of order_list */
lsHandle handle; /* where it is in network BDD list */
network_t *network;
- st_table *local_order; /* for local BDDs */
+ st__table *local_order; /* for local BDDs */
int nvars; /* variables used so far */
int threshold; /* for pseudo var threshold value*/
#endif
@@ -1149,8 +1149,8 @@ extern int cuddBddAlignToZdd( DdManager * table );
extern DdNode * cuddBddMakePrime( DdManager * dd, DdNode * cube, DdNode * f );
extern DdNode * cuddSolveEqnRecur( DdManager * bdd, DdNode * F, DdNode * Y, DdNode ** G, int n, int * yIndex, int i );
extern DdNode * cuddVerifySol( DdManager * bdd, DdNode * F, DdNode ** G, int * yIndex, int n );
-#ifdef ST_INCLUDED
-extern DdNode * cuddSplitSetRecur( DdManager * manager, st_table * mtable, int * varSeen, DdNode * p, double n, double max, int index );
+#ifdef st__INCLUDED
+extern DdNode * cuddSplitSetRecur( DdManager * manager, st__table * mtable, int * varSeen, DdNode * p, double n, double max, int index );
#endif
extern DdNode * cuddSubsetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold );
extern DdNode * cuddSubsetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit );
@@ -1174,9 +1174,9 @@ extern int cuddDestroySubtables( DdManager * unique, int n );
extern int cuddResizeTableZdd( DdManager * unique, int index );
extern void cuddSlowTableGrowth( DdManager * unique );
extern int cuddP( DdManager * dd, DdNode * f );
-#ifdef ST_INCLUDED
-extern enum st_retval cuddStCountfree( char * key, char * value, char * arg );
-extern int cuddCollectNodes( DdNode * f, st_table * visited );
+#ifdef st__INCLUDED
+extern enum st__retval cuddStCountfree( char * key, char * value, char * arg );
+extern int cuddCollectNodes( DdNode * f, st__table * visited );
#endif
extern DdNodePtr * cuddNodeArray( DdNode * f, int * n );
extern int cuddWindowReorder( DdManager * table, int low, int high, Cudd_ReorderingType submethod );
diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c
index 1e0126e9..c92981d1 100644
--- a/src/bdd/cudd/cuddSat.c
+++ b/src/bdd/cudd/cuddSat.c
@@ -121,11 +121,11 @@ extern "C" {
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static enum st_retval freePathPair (char *key, char *value, char *arg);
-static cuddPathPair getShortest (DdNode *root, int *cost, int *support, st_table *visited);
-static DdNode * getPath (DdManager *manager, st_table *visited, DdNode *f, int *weight, int cost);
-static cuddPathPair getLargest (DdNode *root, st_table *visited);
-static DdNode * getCube (DdManager *manager, st_table *visited, DdNode *f, int cost);
+static enum st__retval freePathPair (char *key, char *value, char *arg);
+static cuddPathPair getShortest (DdNode *root, int *cost, int *support, st__table *visited);
+static DdNode * getPath (DdManager *manager, st__table *visited, DdNode *f, int *weight, int cost);
+static cuddPathPair getLargest (DdNode *root, st__table *visited);
+static DdNode * getCube (DdManager *manager, st__table *visited, DdNode *f, int cost);
/**AutomaticEnd***************************************************************/
@@ -206,7 +206,7 @@ Cudd_ShortestPath(
int * length)
{
DdNode *F;
- st_table *visited;
+ st__table *visited;
DdNode *sol;
cuddPathPair *rootPair;
int complement, cost;
@@ -234,7 +234,7 @@ Cudd_ShortestPath(
manager->reordered = 0;
/* Initialize visited table. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
/* Now get the length of the shortest path(s) from f to 1. */
(void) getShortest(f, weight, support, visited);
@@ -243,7 +243,7 @@ Cudd_ShortestPath(
F = Cudd_Regular(f);
- if (!st_lookup(visited, (const char *)F, (char **)&rootPair)) return(NULL);
+ if (! st__lookup(visited, (const char *)F, (char **)&rootPair)) return(NULL);
if (complement) {
cost = rootPair->neg;
@@ -254,8 +254,8 @@ Cudd_ShortestPath(
/* Recover an actual shortest path. */
sol = getPath(manager,visited,f,weight,cost);
- st_foreach(visited, freePathPair, NULL);
- st_free_table(visited);
+ st__foreach(visited, freePathPair, NULL);
+ st__free_table(visited);
} while (manager->reordered == 1);
@@ -288,7 +288,7 @@ Cudd_LargestCube(
int * length)
{
register DdNode *F;
- st_table *visited;
+ st__table *visited;
DdNode *sol;
cuddPathPair *rootPair;
int complement, cost;
@@ -306,7 +306,7 @@ Cudd_LargestCube(
manager->reordered = 0;
/* Initialize visited table. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
/* Now get the length of the shortest path(s) from f to 1. */
(void) getLargest(f, visited);
@@ -315,7 +315,7 @@ Cudd_LargestCube(
F = Cudd_Regular(f);
- if (!st_lookup(visited, (const char *)F, (char **)&rootPair)) return(NULL);
+ if (! st__lookup(visited, (const char *)F, (char **)&rootPair)) return(NULL);
if (complement) {
cost = rootPair->neg;
@@ -326,8 +326,8 @@ Cudd_LargestCube(
/* Recover an actual shortest path. */
sol = getCube(manager,visited,f,cost);
- st_foreach(visited, freePathPair, NULL);
- st_free_table(visited);
+ st__foreach(visited, freePathPair, NULL);
+ st__free_table(visited);
} while (manager->reordered == 1);
@@ -360,7 +360,7 @@ Cudd_ShortestLength(
int * weight)
{
register DdNode *F;
- st_table *visited;
+ st__table *visited;
cuddPathPair *my_pair;
int complement, cost;
@@ -373,7 +373,7 @@ Cudd_ShortestLength(
/* From this point on, a path exists. */
/* Initialize visited table and support. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
/* Now get the length of the shortest path(s) from f to 1. */
(void) getShortest(f, weight, NULL, visited);
@@ -382,7 +382,7 @@ Cudd_ShortestLength(
F = Cudd_Regular(f);
- if (!st_lookup(visited, (const char *)F, (char **)&my_pair)) return(CUDD_OUT_OF_MEM);
+ if (! st__lookup(visited, (const char *)F, (char **)&my_pair)) return(CUDD_OUT_OF_MEM);
if (complement) {
cost = my_pair->neg;
@@ -390,8 +390,8 @@ Cudd_ShortestLength(
cost = my_pair->pos;
}
- st_foreach(visited, freePathPair, NULL);
- st_free_table(visited);
+ st__foreach(visited, freePathPair, NULL);
+ st__free_table(visited);
return(cost);
@@ -955,12 +955,12 @@ cuddBddMakePrime(
Synopsis [Frees the entries of the visited symbol table.]
Description [Frees the entries of the visited symbol table. Returns
- ST_CONTINUE.]
+ st__CONTINUE.]
SideEffects [None]
******************************************************************************/
-static enum st_retval
+static enum st__retval
freePathPair(
char * key,
char * value,
@@ -970,7 +970,7 @@ freePathPair(
pair = (cuddPathPair *) value;
ABC_FREE(pair);
- return(ST_CONTINUE);
+ return( st__CONTINUE);
} /* end of freePathPair */
@@ -998,7 +998,7 @@ getShortest(
DdNode * root,
int * cost,
int * support,
- st_table * visited)
+ st__table * visited)
{
cuddPathPair *my_pair, res_pair, pair_T, pair_E;
DdNode *my_root, *T, *E;
@@ -1006,7 +1006,7 @@ getShortest(
my_root = Cudd_Regular(root);
- if (st_lookup(visited, (const char *)my_root, (char **)&my_pair)) {
+ if ( st__lookup(visited, (const char *)my_root, (char **)&my_pair)) {
if (Cudd_IsComplement(root)) {
res_pair.pos = my_pair->neg;
res_pair.neg = my_pair->pos;
@@ -1058,7 +1058,7 @@ getShortest(
my_pair->pos = res_pair.pos;
my_pair->neg = res_pair.neg;
- st_insert(visited, (char *)my_root, (char *)my_pair);
+ st__insert(visited, (char *)my_root, (char *)my_pair);
if (Cudd_IsComplement(root)) {
res_pair.pos = my_pair->neg;
res_pair.neg = my_pair->pos;
@@ -1092,7 +1092,7 @@ getShortest(
static DdNode *
getPath(
DdManager * manager,
- st_table * visited,
+ st__table * visited,
DdNode * f,
int * weight,
int cost)
@@ -1118,7 +1118,7 @@ getPath(
if (complement) {T = Cudd_Not(T); E = Cudd_Not(E);}
- st_lookup(visited, (const char *)Cudd_Regular(T), (char **)&T_pair);
+ st__lookup(visited, (const char *)Cudd_Regular(T), (char **)&T_pair);
if ((Cudd_IsComplement(T) && T_pair->neg == Tcost) ||
(!Cudd_IsComplement(T) && T_pair->pos == Tcost)) {
tmp = cuddBddAndRecur(manager,manager->vars[my_dd->index],sol);
@@ -1135,7 +1135,7 @@ getPath(
cost = Tcost;
continue;
}
- st_lookup(visited, (const char *)Cudd_Regular(E), (char **)&E_pair);
+ st__lookup(visited, (const char *)Cudd_Regular(E), (char **)&E_pair);
if ((Cudd_IsComplement(E) && E_pair->neg == Ecost) ||
(!Cudd_IsComplement(E) && E_pair->pos == Ecost)) {
tmp = cuddBddAndRecur(manager,Cudd_Not(manager->vars[my_dd->index]),sol);
@@ -1185,14 +1185,14 @@ getPath(
static cuddPathPair
getLargest(
DdNode * root,
- st_table * visited)
+ st__table * visited)
{
cuddPathPair *my_pair, res_pair, pair_T, pair_E;
DdNode *my_root, *T, *E;
my_root = Cudd_Regular(root);
- if (st_lookup(visited, (const char *)my_root, (char **)&my_pair)) {
+ if ( st__lookup(visited, (const char *)my_root, (char **)&my_pair)) {
if (Cudd_IsComplement(root)) {
res_pair.pos = my_pair->neg;
res_pair.neg = my_pair->pos;
@@ -1239,7 +1239,7 @@ getLargest(
my_pair->neg = res_pair.neg;
/* Caching may fail without affecting correctness. */
- st_insert(visited, (char *)my_root, (char *)my_pair);
+ st__insert(visited, (char *)my_root, (char *)my_pair);
if (Cudd_IsComplement(root)) {
res_pair.pos = my_pair->neg;
res_pair.neg = my_pair->pos;
@@ -1273,7 +1273,7 @@ getLargest(
static DdNode *
getCube(
DdManager * manager,
- st_table * visited,
+ st__table * visited,
DdNode * f,
int cost)
{
@@ -1298,7 +1298,7 @@ getCube(
if (complement) {T = Cudd_Not(T); E = Cudd_Not(E);}
- if (!st_lookup(visited, (const char *)Cudd_Regular(T), (char **)&T_pair)) return(NULL);
+ if (! st__lookup(visited, (const char *)Cudd_Regular(T), (char **)&T_pair)) return(NULL);
if ((Cudd_IsComplement(T) && T_pair->neg == Tcost) ||
(!Cudd_IsComplement(T) && T_pair->pos == Tcost)) {
tmp = cuddBddAndRecur(manager,manager->vars[my_dd->index],sol);
@@ -1315,7 +1315,7 @@ getCube(
cost = Tcost;
continue;
}
- if (!st_lookup(visited, (const char *)Cudd_Regular(E), (char **)&E_pair)) return(NULL);
+ if (! st__lookup(visited, (const char *)Cudd_Regular(E), (char **)&E_pair)) return(NULL);
if ((Cudd_IsComplement(E) && E_pair->neg == Ecost) ||
(!Cudd_IsComplement(E) && E_pair->pos == Ecost)) {
tmp = cuddBddAndRecur(manager,Cudd_Not(manager->vars[my_dd->index]),sol);
diff --git a/src/bdd/cudd/cuddSign.c b/src/bdd/cudd/cuddSign.c
index c3fcfa9d..4b54d639 100644
--- a/src/bdd/cudd/cuddSign.c
+++ b/src/bdd/cudd/cuddSign.c
@@ -102,7 +102,7 @@ static int table_mem;
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static double * ddCofMintermAux (DdManager *dd, DdNode *node, st_table *table);
+static double * ddCofMintermAux (DdManager *dd, DdNode *node, st__table *table);
/**AutomaticEnd***************************************************************/
@@ -132,7 +132,7 @@ Cudd_CofMinterm(
DdManager * dd,
DdNode * node)
{
- st_table *table;
+ st__table *table;
double *values;
double *result = NULL;
int i, firstLevel;
@@ -141,10 +141,10 @@ Cudd_CofMinterm(
long startTime;
startTime = util_cpu_time();
num_calls = 0;
- table_mem = sizeof(st_table);
+ table_mem = sizeof( st__table);
#endif
- table = st_init_table(st_ptrcmp, st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) {
(void) fprintf(dd->err,
"out-of-memory, couldn't measure DD cofactors.\n");
@@ -177,11 +177,11 @@ Cudd_CofMinterm(
}
#ifdef DD_STATS
- table_mem += table->num_bins * sizeof(st_table_entry *);
+ table_mem += table->num_bins * sizeof( st__table_entry *);
#endif
if (Cudd_Regular(node)->ref == 1) ABC_FREE(values);
- st_foreach(table, cuddStCountfree, NULL);
- st_free_table(table);
+ st__foreach(table, cuddStCountfree, NULL);
+ st__free_table(table);
#ifdef DD_STATS
(void) fprintf(dd->out,"Number of calls: %d\tTable memory: %d bytes\n",
num_calls, table_mem);
@@ -232,7 +232,7 @@ static double *
ddCofMintermAux(
DdManager * dd,
DdNode * node,
- st_table * table)
+ st__table * table)
{
DdNode *N; /* regular version of node */
DdNode *Nv, *Nnv;
@@ -247,7 +247,7 @@ ddCofMintermAux(
num_calls++;
#endif
- if (st_lookup(table, (const char *)node, (char **)&values)) {
+ if ( st__lookup(table, (const char *)node, (char **)&values)) {
return(values);
}
@@ -309,12 +309,12 @@ ddCofMintermAux(
}
if (N->ref > 1) {
- if (st_add_direct(table, (char *) node, (char *) values) == ST_OUT_OF_MEM) {
+ if ( st__add_direct(table, (char *) node, (char *) values) == st__OUT_OF_MEM) {
ABC_FREE(values);
return(NULL);
}
#ifdef DD_STATS
- table_mem += localSize * sizeof(double) + sizeof(st_table_entry);
+ table_mem += localSize * sizeof(double) + sizeof( st__table_entry);
#endif
}
return(values);
diff --git a/src/bdd/cudd/cuddSplit.c b/src/bdd/cudd/cuddSplit.c
index b2f6d793..70f0f0d9 100644
--- a/src/bdd/cudd/cuddSplit.c
+++ b/src/bdd/cudd/cuddSplit.c
@@ -98,7 +98,7 @@ ABC_NAMESPACE_IMPL_START
static DdNode * selectMintermsFromUniverse (DdManager *manager, int *varSeen, double n);
static DdNode * mintermsFromUniverse (DdManager *manager, DdNode **vars, int numVars, double n, int index);
-static double bddAnnotateMintermCount (DdManager *manager, DdNode *node, double max, st_table *table);
+static double bddAnnotateMintermCount (DdManager *manager, DdNode *node, double max, st__table *table);
/**AutomaticEnd***************************************************************/
@@ -135,7 +135,7 @@ Cudd_SplitSet(
DdNode *result;
DdNode *zero, *one;
double max, num;
- st_table *mtable;
+ st__table *mtable;
int *varSeen;
int i,index, size;
@@ -183,7 +183,7 @@ Cudd_SplitSet(
cuddRef(result);
ABC_FREE(varSeen);
} else {
- mtable = st_init_table(st_ptrcmp,st_ptrhash);
+ mtable = st__init_table( st__ptrcmp, st__ptrhash);
if (mtable == NULL) {
(void) fprintf(manager->out,
"Cudd_SplitSet: out-of-memory.\n");
@@ -197,8 +197,8 @@ Cudd_SplitSet(
*/
num = bddAnnotateMintermCount(manager,S,max,mtable);
if (m == num) {
- st_foreach(mtable,cuddStCountfree,NIL(char));
- st_free_table(mtable);
+ st__foreach(mtable,cuddStCountfree,NIL(char));
+ st__free_table(mtable);
ABC_FREE(varSeen);
return(S);
}
@@ -206,8 +206,8 @@ Cudd_SplitSet(
result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0);
if (result)
cuddRef(result);
- st_foreach(mtable,cuddStCountfree,NULL);
- st_free_table(mtable);
+ st__foreach(mtable,cuddStCountfree,NULL);
+ st__free_table(mtable);
ABC_FREE(varSeen);
}
} while (manager->reordered == 1);
@@ -246,7 +246,7 @@ Cudd_SplitSet(
DdNode*
cuddSplitSetRecur(
DdManager * manager,
- st_table * mtable,
+ st__table * mtable,
int * varSeen,
DdNode * p,
double n,
@@ -307,7 +307,7 @@ cuddSplitSetRecur(
/* Lookup the # of minterms in the onset of the node from the table. */
if (!Cudd_IsConstant(Nv)) {
- if (!st_lookup(mtable, (const char *)Nv, (char **)&dummy)) return(NULL);
+ if (! st__lookup(mtable, (const char *)Nv, (char **)&dummy)) return(NULL);
numT = *dummy/(2*(1<<index));
} else if (Nv == one) {
numT = max/(2*(1<<index));
@@ -316,7 +316,7 @@ cuddSplitSetRecur(
}
if (!Cudd_IsConstant(Nnv)) {
- if (!st_lookup(mtable, (const char *)Nnv, (char **)&dummy)) return(NULL);
+ if (! st__lookup(mtable, (const char *)Nnv, (char **)&dummy)) return(NULL);
numE = *dummy/(2*(1<<index));
} else if (Nnv == one) {
numE = max/(2*(1<<index));
@@ -634,7 +634,7 @@ bddAnnotateMintermCount(
DdManager * manager,
DdNode * node,
double max,
- st_table * table)
+ st__table * table)
{
DdNode *N,*Nv,*Nnv;
@@ -653,7 +653,7 @@ bddAnnotateMintermCount(
}
}
- if (st_lookup(table, (const char *)node, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)node, (char **)&dummy)) {
return(*dummy);
}
@@ -680,7 +680,7 @@ bddAnnotateMintermCount(
}
*pmin = min_N;
- if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
+ if ( st__insert(table,(char *)node, (char *)pmin) == st__OUT_OF_MEM) {
ABC_FREE(pmin);
return((double)CUDD_OUT_OF_MEM);
}
diff --git a/src/bdd/cudd/cuddSubsetHB.c b/src/bdd/cudd/cuddSubsetHB.c
index a9d677f4..fb8eba61 100644
--- a/src/bdd/cudd/cuddSubsetHB.c
+++ b/src/bdd/cudd/cuddSubsetHB.c
@@ -166,12 +166,12 @@ static int maxNodeDataPages; /* number of page pointers */
static void ResizeNodeDataPages (void);
static void ResizeCountMintermPages (void);
static void ResizeCountNodePages (void);
-static double SubsetCountMintermAux (DdNode *node, double max, st_table *table);
-static st_table * SubsetCountMinterm (DdNode *node, int nvars);
-static int SubsetCountNodesAux (DdNode *node, st_table *table, double max);
-static int SubsetCountNodes (DdNode *node, st_table *table, int nvars);
-static void StoreNodes (st_table *storeTable, DdManager *dd, DdNode *node);
-static DdNode * BuildSubsetBdd (DdManager *dd, DdNode *node, int *size, st_table *visitedTable, int threshold, st_table *storeTable, st_table *approxTable);
+static double SubsetCountMintermAux (DdNode *node, double max, st__table *table);
+static st__table * SubsetCountMinterm (DdNode *node, int nvars);
+static int SubsetCountNodesAux (DdNode *node, st__table *table, double max);
+static int SubsetCountNodes (DdNode *node, st__table *table, int nvars);
+static void StoreNodes ( st__table *storeTable, DdManager *dd, DdNode *node);
+static DdNode * BuildSubsetBdd (DdManager *dd, DdNode *node, int *size, st__table *visitedTable, int threshold, st__table *storeTable, st__table *approxTable);
/**AutomaticEnd***************************************************************/
@@ -310,13 +310,13 @@ cuddSubsetHeavyBranch(
{
int i, *size;
- st_table *visitedTable;
+ st__table *visitedTable;
int numNodes;
NodeData_t *currNodeQual;
DdNode *subset;
- st_table *storeTable, *approxTable;
+ st__table *storeTable, *approxTable;
char *key, *value;
- st_generator *stGen;
+ st__generator *stGen;
if (f == NULL) {
fprintf(dd->err, "Cannot subset, nil object\n");
@@ -344,7 +344,7 @@ cuddSubsetHeavyBranch(
max = pow(2.0, (double)numVars);
/* Create visited table where structures for node data are allocated and
- stored in a st_table */
+ stored in a st__table */
visitedTable = SubsetCountMinterm(f, numVars);
if ((visitedTable == NULL) || memOut) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
@@ -358,7 +358,7 @@ cuddSubsetHeavyBranch(
return(0);
}
- if (st_lookup(visitedTable, (const char *)f, (char **)&currNodeQual) == 0) {
+ if ( st__lookup(visitedTable, (const char *)f, (char **)&currNodeQual) == 0) {
fprintf(dd->err,
"Something is wrong, ought to be node quality table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
@@ -375,42 +375,42 @@ cuddSubsetHeavyBranch(
num_calls = 0;
#endif
/* table to store nodes being created. */
- storeTable = st_init_table(st_ptrcmp, st_ptrhash);
+ storeTable = st__init_table( st__ptrcmp, st__ptrhash);
/* insert the constant */
cuddRef(one);
- if (st_insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
- ST_OUT_OF_MEM) {
- fprintf(dd->out, "Something wrong, st_table insert failed\n");
+ if ( st__insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
+ st__OUT_OF_MEM) {
+ fprintf(dd->out, "Something wrong, st__table insert failed\n");
}
/* table to store approximations of nodes */
- approxTable = st_init_table(st_ptrcmp, st_ptrhash);
+ approxTable = st__init_table( st__ptrcmp, st__ptrhash);
subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
storeTable, approxTable);
if (subset != NULL) {
cuddRef(subset);
}
- stGen = st_init_gen(approxTable);
+ stGen = st__init_gen(approxTable);
if (stGen == NULL) {
- st_free_table(approxTable);
+ st__free_table(approxTable);
return(NULL);
}
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
Cudd_RecursiveDeref(dd, (DdNode *)value);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(approxTable);
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(approxTable);
- stGen = st_init_gen(storeTable);
+ stGen = st__init_gen(storeTable);
if (stGen == NULL) {
- st_free_table(storeTable);
+ st__free_table(storeTable);
return(NULL);
}
- while(st_gen(stGen, (const char **)&key, (char **)&value)) {
+ while( st__gen(stGen, (const char **)&key, (char **)&value)) {
Cudd_RecursiveDeref(dd, (DdNode *)key);
}
- st_free_gen(stGen); stGen = NULL;
- st_free_table(storeTable);
+ st__free_gen(stGen); stGen = NULL;
+ st__free_table(storeTable);
for (i = 0; i <= page; i++) {
ABC_FREE(mintermPages[i]);
@@ -428,7 +428,7 @@ cuddSubsetHeavyBranch(
ABC_FREE(nodeDataPages[i]);
}
ABC_FREE(nodeDataPages);
- st_free_table(visitedTable);
+ st__free_table(visitedTable);
ABC_FREE(size);
#if 0
(void) Cudd_DebugCheck(dd);
@@ -671,7 +671,7 @@ ResizeCountNodePages(void)
data structure and stores the minterm count as part of the node
data structure. ]
- SideEffects [Creates structures of type node quality and fills the st_table]
+ SideEffects [Creates structures of type node quality and fills the st__table]
SeeAlso [SubsetCountMinterm]
@@ -680,7 +680,7 @@ static double
SubsetCountMintermAux(
DdNode * node /* function to analyze */,
double max /* number of minterms of constant 1 */,
- st_table * table /* visitedTable table */)
+ st__table * table /* visitedTable table */)
{
DdNode *N,*Nv,*Nnv; /* nodes to store cofactors */
@@ -704,7 +704,7 @@ SubsetCountMintermAux(
} else {
/* check if entry for this node exists */
- if (st_lookup(table, (const char *)node, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)node, (char **)&dummy)) {
min = *(dummy->mintermPointer);
return(min);
}
@@ -730,7 +730,7 @@ SubsetCountMintermAux(
if (memOut) {
for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
return(0.0);
}
@@ -746,7 +746,7 @@ SubsetCountMintermAux(
if (memOut) {
for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
ABC_FREE(mintermPages);
- st_free_table(table);
+ st__free_table(table);
return(0.0);
}
@@ -759,13 +759,13 @@ SubsetCountMintermAux(
newEntry->nodesPointer = NULL;
/* insert entry for the node in the table */
- if (st_insert(table,(char *)node, (char *)newEntry) == ST_OUT_OF_MEM) {
+ if ( st__insert(table,(char *)node, (char *)newEntry) == st__OUT_OF_MEM) {
memOut = 1;
for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
ABC_FREE(mintermPages);
for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
return(0.0);
}
return(min);
@@ -780,19 +780,19 @@ SubsetCountMintermAux(
Description [Counts minterms of each node in the DAG. Similar to the
Cudd_CountMinterm procedure except this returns the minterm count for
- all the nodes in the bdd in an st_table.]
+ all the nodes in the bdd in an st__table.]
SideEffects [none]
SeeAlso [SubsetCountMintermAux]
******************************************************************************/
-static st_table *
+static st__table *
SubsetCountMinterm(
DdNode * node /* function to be analyzed */,
int nvars /* number of variables node depends on */)
{
- st_table *table;
+ st__table *table;
int i;
@@ -801,12 +801,12 @@ SubsetCountMinterm(
#endif
max = pow(2.0,(double) nvars);
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) goto OUT_OF_MEM;
maxPages = INITIAL_PAGES;
mintermPages = ABC_ALLOC(double *,maxPages);
if (mintermPages == NULL) {
- st_free_table(table);
+ st__free_table(table);
goto OUT_OF_MEM;
}
page = 0;
@@ -814,7 +814,7 @@ SubsetCountMinterm(
mintermPages[page] = currentMintermPage;
if (currentMintermPage == NULL) {
ABC_FREE(mintermPages);
- st_free_table(table);
+ st__free_table(table);
goto OUT_OF_MEM;
}
pageIndex = 0;
@@ -823,7 +823,7 @@ SubsetCountMinterm(
if (nodeDataPages == NULL) {
for (i = 0; i <= page ; i++) ABC_FREE(mintermPages[i]);
ABC_FREE(mintermPages);
- st_free_table(table);
+ st__free_table(table);
goto OUT_OF_MEM;
}
nodeDataPage = 0;
@@ -833,7 +833,7 @@ SubsetCountMinterm(
for (i = 0; i <= page ; i++) ABC_FREE(mintermPages[i]);
ABC_FREE(mintermPages);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
goto OUT_OF_MEM;
}
nodeDataPageIndex = 0;
@@ -860,7 +860,7 @@ OUT_OF_MEM:
this node. . Note that the same dag may be the lighter child of two
different nodes and have different counts. As with the minterm counts,
the node counts are stored in pages to be space efficient and the
- address for these node counts are stored in an st_table associated
+ address for these node counts are stored in an st__table associated
to each node. ]
SideEffects [Updates the node data table with node counts]
@@ -871,7 +871,7 @@ OUT_OF_MEM:
static int
SubsetCountNodesAux(
DdNode * node /* current node */,
- st_table * table /* table to update node count, also serves as visited table. */,
+ st__table * table /* table to update node count, also serves as visited table. */,
double max /* maximum number of variables */)
{
int tval, eval, i;
@@ -884,7 +884,7 @@ SubsetCountNodesAux(
return(0);
/* if this node has been processed do nothing */
- if (st_lookup(table, (const char *)node, (char **)&dummyN) == 1) {
+ if ( st__lookup(table, (const char *)node, (char **)&dummyN) == 1) {
val = dummyN->nodesPointer;
if (val != NULL)
return(0);
@@ -907,7 +907,7 @@ SubsetCountNodesAux(
minNv = max;
}
} else {
- if (st_lookup(table, (const char *)Nv, (char **)&dummyNv) == 1)
+ if ( st__lookup(table, (const char *)Nv, (char **)&dummyNv) == 1)
minNv = *(dummyNv->mintermPointer);
else {
return(0);
@@ -920,7 +920,7 @@ SubsetCountNodesAux(
minNnv = max;
}
} else {
- if (st_lookup(table, (const char *)Nnv, (char **)&dummyNnv) == 1) {
+ if ( st__lookup(table, (const char *)Nnv, (char **)&dummyNnv) == 1) {
minNnv = *(dummyNnv->mintermPointer);
}
else {
@@ -943,7 +943,7 @@ SubsetCountNodesAux(
ABC_FREE(mintermPages);
for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
return(0);
}
pmin = currentLightNodePage + pageIndex;
@@ -963,7 +963,7 @@ SubsetCountNodesAux(
ABC_FREE(mintermPages);
for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
return(0);
}
pmin = currentLightNodePage + pageIndex;
@@ -983,14 +983,14 @@ SubsetCountNodesAux(
branch. Its complement will be reached later on a lighter branch.
Hence the complement has zero node count. */
- if (st_lookup(table, (const char *)Cudd_Not(node), (char **)&dummyNBar) == 1) {
+ if ( st__lookup(table, (const char *)Cudd_Not(node), (char **)&dummyNBar) == 1) {
if (pageIndex == pageSize) ResizeCountNodePages();
if (memOut) {
for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
ABC_FREE(mintermPages);
for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
return(0);
}
pminBar = currentLightNodePage + pageIndex;
@@ -1005,7 +1005,7 @@ SubsetCountNodesAux(
ABC_FREE(mintermPages);
for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
ABC_FREE(nodeDataPages);
- st_free_table(table);
+ st__free_table(table);
return(0);
}
pminBar = currentNodePage + pageIndex;
@@ -1035,7 +1035,7 @@ SubsetCountNodesAux(
static int
SubsetCountNodes(
DdNode * node /* function to be analyzed */,
- st_table * table /* node quality table */,
+ st__table * table /* node quality table */,
int nvars /* number of variables node depends on */)
{
int num;
@@ -1111,7 +1111,7 @@ OUT_OF_MEM:
******************************************************************************/
static void
StoreNodes(
- st_table * storeTable,
+ st__table * storeTable,
DdManager * dd,
DdNode * node)
{
@@ -1120,12 +1120,12 @@ StoreNodes(
return;
}
N = Cudd_Regular(node);
- if (st_lookup(storeTable, (char *)N, NIL(char *))) {
+ if ( st__lookup(storeTable, (char *)N, NIL(char *))) {
return;
}
cuddRef(N);
- if (st_insert(storeTable, (char *)N, NIL(char)) == ST_OUT_OF_MEM) {
- fprintf(dd->err,"Something wrong, st_table insert failed\n");
+ if ( st__insert(storeTable, (char *)N, NIL(char)) == st__OUT_OF_MEM) {
+ fprintf(dd->err,"Something wrong, st__table insert failed\n");
}
Nt = Cudd_T(N);
@@ -1159,10 +1159,10 @@ BuildSubsetBdd(
DdManager * dd /* DD manager */,
DdNode * node /* current node */,
int * size /* current size of the subset */,
- st_table * visitedTable /* visited table storing all node data */,
+ st__table * visitedTable /* visited table storing all node data */,
int threshold,
- st_table * storeTable,
- st_table * approxTable)
+ st__table * storeTable,
+ st__table * approxTable)
{
DdNode *Nv, *Nnv, *N, *topv, *neW;
@@ -1189,7 +1189,7 @@ BuildSubsetBdd(
return(node);
/* Look up minterm count for this node. */
- if (!st_lookup(visitedTable, (const char *)node, (char **)&currNodeQual)) {
+ if (! st__lookup(visitedTable, (const char *)node, (char **)&currNodeQual)) {
fprintf(dd->err,
"Something is wrong, ought to be in node quality table\n");
}
@@ -1205,7 +1205,7 @@ BuildSubsetBdd(
if (!Cudd_IsConstant(Nv)) {
/* find out minterms and nodes contributed by then child */
- if (!st_lookup(visitedTable, (const char *)Nv, (char **)&currNodeQualT)) {
+ if (! st__lookup(visitedTable, (const char *)Nv, (char **)&currNodeQualT)) {
fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
@@ -1222,7 +1222,7 @@ BuildSubsetBdd(
}
if (!Cudd_IsConstant(Nnv)) {
/* find out minterms and nodes contributed by else child */
- if (!st_lookup(visitedTable, (const char *)Nnv, (char **)&currNodeQualE)) {
+ if (! st__lookup(visitedTable, (const char *)Nnv, (char **)&currNodeQualE)) {
fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
@@ -1255,11 +1255,11 @@ BuildSubsetBdd(
* subset, or one whose approximation has been computed, or
* Zero.
*/
- if (st_lookup(storeTable, (char *)Cudd_Regular(Nnv), &dummy)) {
+ if ( st__lookup(storeTable, (char *)Cudd_Regular(Nnv), &dummy)) {
ElseBranch = Nnv;
cuddRef(ElseBranch);
} else {
- if (st_lookup(approxTable, (char *)Nnv, &dummy)) {
+ if ( st__lookup(approxTable, (char *)Nnv, &dummy)) {
ElseBranch = (DdNode *)dummy;
cuddRef(ElseBranch);
} else {
@@ -1281,11 +1281,11 @@ BuildSubsetBdd(
* subset, or one whose approximation has been computed, or
* Zero.
*/
- if (st_lookup(storeTable, (char *)Cudd_Regular(Nv), &dummy)) {
+ if ( st__lookup(storeTable, (char *)Cudd_Regular(Nv), &dummy)) {
ThenBranch = Nv;
cuddRef(ThenBranch);
} else {
- if (st_lookup(approxTable, (char *)Nv, &dummy)) {
+ if ( st__lookup(approxTable, (char *)Nv, &dummy)) {
ThenBranch = (DdNode *)dummy;
cuddRef(ThenBranch);
} else {
@@ -1312,18 +1312,18 @@ BuildSubsetBdd(
return(NULL);
else {
/* store this node in the store table */
- if (!st_lookup(storeTable, (char *)Cudd_Regular(neW), &dummy)) {
+ if (! st__lookup(storeTable, (char *)Cudd_Regular(neW), &dummy)) {
cuddRef(neW);
- if (!st_insert(storeTable, (char *)Cudd_Regular(neW), NIL(char)))
+ if (! st__insert(storeTable, (char *)Cudd_Regular(neW), NIL(char)))
return (NULL);
}
/* store the approximation for this node */
if (N != Cudd_Regular(neW)) {
- if (st_lookup(approxTable, (char *)node, &dummy)) {
+ if ( st__lookup(approxTable, (char *)node, &dummy)) {
fprintf(dd->err, "This node should not be in the approximated table\n");
} else {
cuddRef(neW);
- if (!st_insert(approxTable, (char *)node, (char *)neW))
+ if (! st__insert(approxTable, (char *)node, (char *)neW))
return(NULL);
}
}
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index 36848eec..84cae32c 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -111,7 +111,7 @@ struct AssortedInfo {
unsigned int maxpath;
int findShortestPath;
int thresholdReached;
- st_table *maxpathTable;
+ st__table *maxpathTable;
int threshold;
};
@@ -170,12 +170,12 @@ extern "C" {
static void ResizeNodeDistPages (void);
static void ResizeQueuePages (void);
-static void CreateTopDist (st_table *pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode **childPage, int childQueueIndex, int numParents, FILE *fp);
-static int CreateBotDist (DdNode *node, st_table *pathTable, unsigned int *pathLengthArray, FILE *fp);
-static st_table * CreatePathTable (DdNode *node, unsigned int *pathLengthArray, FILE *fp);
+static void CreateTopDist ( st__table *pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode **childPage, int childQueueIndex, int numParents, FILE *fp);
+static int CreateBotDist (DdNode *node, st__table *pathTable, unsigned int *pathLengthArray, FILE *fp);
+static st__table * CreatePathTable (DdNode *node, unsigned int *pathLengthArray, FILE *fp);
static unsigned int AssessPathLength (unsigned int *pathLengthArray, int threshold, int numVars, unsigned int *excess, FILE *fp);
-static DdNode * BuildSubsetBdd (DdManager *dd, st_table *pathTable, DdNode *node, struct AssortedInfo *info, st_table *subsetNodeTable);
-static enum st_retval stPathTableDdFree (char *key, char *value, char *arg);
+static DdNode * BuildSubsetBdd (DdManager *dd, st__table *pathTable, DdNode *node, struct AssortedInfo *info, st__table *subsetNodeTable);
+static enum st__retval stPathTableDdFree (char *key, char *value, char *arg);
/**AutomaticEnd***************************************************************/
@@ -320,7 +320,7 @@ cuddSubsetShortPaths(
int threshold /* maximum number of nodes allowed in the subset */,
int hardlimit /* flag determining whether thershold should be respected strictly */)
{
- st_table *pathTable;
+ st__table *pathTable;
DdNode *N, *subset;
unsigned int *pathLengthArray;
@@ -328,7 +328,7 @@ cuddSubsetShortPaths(
int i;
NodeDist_t *nodeStat;
struct AssortedInfo *info;
- st_table *subsetNodeTable;
+ st__table *subsetNodeTable;
one = DD_ONE(dd);
zero = Cudd_Not(one);
@@ -361,7 +361,7 @@ cuddSubsetShortPaths(
if ((pathTable == NULL) || (memOut)) {
if (pathTable != NULL)
- st_free_table(pathTable);
+ st__free_table(pathTable);
ABC_FREE(pathLengthArray);
return (NIL(DdNode));
}
@@ -377,7 +377,7 @@ cuddSubsetShortPaths(
info->maxpath = maxpath;
info->findShortestPath = 0;
info->thresholdReached = *excess;
- info->maxpathTable = st_init_table(st_ptrcmp, st_ptrhash);
+ info->maxpathTable = st__init_table( st__ptrcmp, st__ptrhash);
info->threshold = threshold;
#ifdef DD_DEBUG
@@ -397,7 +397,7 @@ cuddSubsetShortPaths(
#endif
N = Cudd_Regular(f);
- if (!st_lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
+ if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
fprintf(dd->err, "Something wrong, root node must be in table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
ABC_FREE(excess);
@@ -431,9 +431,9 @@ cuddSubsetShortPaths(
#endif
/* initialize a table to store computed nodes */
if (hardlimit) {
- subsetNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
+ subsetNodeTable = st__init_table( st__ptrcmp, st__ptrhash);
} else {
- subsetNodeTable = NIL(st_table);
+ subsetNodeTable = NIL( st__table);
}
subset = BuildSubsetBdd(dd, pathTable, f, info, subsetNodeTable);
if (subset != NULL) {
@@ -446,11 +446,11 @@ cuddSubsetShortPaths(
hits, thishit, numCalls);
#endif
- if (subsetNodeTable != NIL(st_table)) {
- st_free_table(subsetNodeTable);
+ if (subsetNodeTable != NIL( st__table)) {
+ st__free_table(subsetNodeTable);
}
- st_free_table(info->maxpathTable);
- st_foreach(pathTable, stPathTableDdFree, (char *)dd);
+ st__free_table(info->maxpathTable);
+ st__foreach(pathTable, stPathTableDdFree, (char *)dd);
ABC_FREE(info);
@@ -459,7 +459,7 @@ cuddSubsetShortPaths(
cuddRef(subset);
}
ABC_FREE(excess);
- st_free_table(pathTable);
+ st__free_table(pathTable);
ABC_FREE(pathLengthArray);
for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
ABC_FREE(nodeDistPages);
@@ -633,7 +633,7 @@ ResizeQueuePages(void)
******************************************************************************/
static void
CreateTopDist(
- st_table * pathTable /* hast table to store path lengths */,
+ st__table * pathTable /* hast table to store path lengths */,
int parentPage /* the pointer to the page on which the first parent in the queue is to be found. */,
int parentQueueIndex /* pointer to the first parent on the page */,
int topLen /* current distance from the root */,
@@ -699,7 +699,7 @@ CreateTopDist(
/* check is already visited, if not add a new entry in
* the path Table
*/
- if (!st_lookup(pathTable, (const char *)regChild, (char **)&nodeStat)) {
+ if (! st__lookup(pathTable, (const char *)regChild, (char **)&nodeStat)) {
/* if not in table, has never been visited */
/* create entry for table */
if (nodeDistPageIndex == nodeDistPageSize)
@@ -707,7 +707,7 @@ CreateTopDist(
if (memOut) {
for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
ABC_FREE(queuePages);
- st_free_table(pathTable);
+ st__free_table(pathTable);
return;
}
/* New entry for child in path Table is created here */
@@ -731,15 +731,15 @@ CreateTopDist(
}
/* insert entry element for child in the table */
- if (st_insert(pathTable, (char *)regChild,
- (char *)nodeStat) == ST_OUT_OF_MEM) {
+ if ( st__insert(pathTable, (char *)regChild,
+ (char *)nodeStat) == st__OUT_OF_MEM) {
memOut = 1;
for (i = 0; i <= nodeDistPage; i++)
ABC_FREE(nodeDistPages[i]);
ABC_FREE(nodeDistPages);
for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
ABC_FREE(queuePages);
- st_free_table(pathTable);
+ st__free_table(pathTable);
return;
}
@@ -754,7 +754,7 @@ CreateTopDist(
for (i = 0; i <= nodeDistPage; i++)
ABC_FREE(nodeDistPages[i]);
ABC_FREE(nodeDistPages);
- st_free_table(pathTable);
+ st__free_table(pathTable);
return;
}
*(currentQueuePage + queuePageIndex) = child;
@@ -773,7 +773,7 @@ CreateTopDist(
for (i = 0; i <= nodeDistPage; i++)
ABC_FREE(nodeDistPages[i]);
ABC_FREE(nodeDistPages);
- st_free_table(pathTable);
+ st__free_table(pathTable);
return;
}
@@ -789,7 +789,7 @@ CreateTopDist(
childrenCount++;
}
- } /* end of else (not found in st_table) */
+ } /* end of else (not found in st__table) */
} /*end of if Not constant child */
processingDone--;
} /*end of while processing Nv, Nnv */
@@ -835,7 +835,7 @@ CreateTopDist(
static int
CreateBotDist(
DdNode * node /* current node */,
- st_table * pathTable /* path table with path lengths */,
+ st__table * pathTable /* path table with path lengths */,
unsigned int * pathLengthArray /* array that stores number of nodes belonging to a particular path length. */,
FILE *fp /* where to write messages */)
{
@@ -853,7 +853,7 @@ CreateBotDist(
/* each node has one table entry */
/* update as you go down the min dist of each node from
the root in each (odd and even) parity */
- if (!st_lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
+ if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
fprintf(fp, "Something wrong, the entry doesn't exist\n");
return(0);
}
@@ -899,7 +899,7 @@ CreateBotDist(
nodeStat->evenBotDist = 1;
} else {
/* If node not in table, recur. */
- if (!st_lookup(pathTable, (const char *)regChild, (char **)&nodeStatChild)) {
+ if (! st__lookup(pathTable, (const char *)regChild, (char **)&nodeStatChild)) {
fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
return(0);
}
@@ -1015,14 +1015,14 @@ CreateBotDist(
SeeAlso [CreateTopDist CreateBotDist]
******************************************************************************/
-static st_table *
+static st__table *
CreatePathTable(
DdNode * node /* root of function */,
unsigned int * pathLengthArray /* array of path lengths to store nodes labeled with the various path lengths */,
FILE *fp /* where to write messages */)
{
- st_table *pathTable;
+ st__table *pathTable;
NodeDist_t *nodeStat;
DdHalfWord topLen;
DdNode *N;
@@ -1033,7 +1033,7 @@ CreatePathTable(
int childQueueIndex, parentQueueIndex;
/* Creating path Table for storing data about nodes */
- pathTable = st_init_table(st_ptrcmp,st_ptrhash);
+ pathTable = st__init_table( st__ptrcmp, st__ptrhash);
/* initializing pages for info about each node */
maxNodeDistPages = INITIAL_PAGES;
@@ -1083,7 +1083,7 @@ CreatePathTable(
ABC_FREE(nodeDistPages);
for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
ABC_FREE(queuePages);
- st_free_table(pathTable);
+ st__free_table(pathTable);
goto OUT_OF_MEM;
}
@@ -1097,17 +1097,17 @@ CreatePathTable(
nodeStat->regResult = NULL;
nodeStat->compResult = NULL;
- insertValue = st_insert(pathTable, (char *)N, (char *)nodeStat);
- if (insertValue == ST_OUT_OF_MEM) {
+ insertValue = st__insert(pathTable, (char *)N, (char *)nodeStat);
+ if (insertValue == st__OUT_OF_MEM) {
memOut = 1;
for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
ABC_FREE(nodeDistPages);
for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
ABC_FREE(queuePages);
- st_free_table(pathTable);
+ st__free_table(pathTable);
goto OUT_OF_MEM;
} else if (insertValue == 1) {
- fprintf(fp, "Something wrong, the entry exists but didnt show up in st_lookup\n");
+ fprintf(fp, "Something wrong, the entry exists but didnt show up in st__lookup\n");
return(NULL);
}
@@ -1254,10 +1254,10 @@ AssessPathLength(
static DdNode *
BuildSubsetBdd(
DdManager * dd /* DD manager */,
- st_table * pathTable /* path table with path lengths and computed results */,
+ st__table * pathTable /* path table with path lengths and computed results */,
DdNode * node /* current node */,
struct AssortedInfo * info /* assorted information structure */,
- st_table * subsetNodeTable /* table storing computed results */)
+ st__table * subsetNodeTable /* table storing computed results */)
{
DdNode *N, *Nv, *Nnv;
DdNode *ThenBranch, *ElseBranch, *childBranch;
@@ -1280,7 +1280,7 @@ BuildSubsetBdd(
N = Cudd_Regular(node);
/* Find node in table. */
- if (!st_lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
+ if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
(void) fprintf(dd->err, "Something wrong, node must be in table \n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
@@ -1349,7 +1349,7 @@ BuildSubsetBdd(
/* Derive regular child for table lookup. */
regNv = Cudd_Regular(Nv);
/* Get node data for shortest path length. */
- if (!st_lookup(pathTable, (const char *)regNv, (char **)&nodeStatNv) ) {
+ if (! st__lookup(pathTable, (const char *)regNv, (char **)&nodeStatNv) ) {
(void) fprintf(dd->err, "Something wrong, node must be in table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
@@ -1393,7 +1393,7 @@ BuildSubsetBdd(
/* Derive regular child for table lookup. */
regNnv = Cudd_Regular(Nnv);
/* Get node data for shortest path length. */
- if (!st_lookup(pathTable, (const char *)regNnv, (char **)&nodeStatNnv) ) {
+ if (! st__lookup(pathTable, (const char *)regNnv, (char **)&nodeStatNnv) ) {
(void) fprintf(dd->err, "Something wrong, node must be in table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
@@ -1470,7 +1470,7 @@ BuildSubsetBdd(
} else { /* Case: path length of node = maxpath */
/* If the node labeled with maxpath is found in the
** maxpathTable, use it to build the subset BDD. */
- if (st_lookup(info->maxpathTable, (char *)regChild,
+ if ( st__lookup(info->maxpathTable, (char *)regChild,
(char **)&entry)) {
/* When a node that is already been chosen is hit,
** the quest for a complete path is over. */
@@ -1486,8 +1486,8 @@ BuildSubsetBdd(
** replace the node with a zero. */
if (info->thresholdReached <= 0) {
if (info->findShortestPath) {
- if (st_insert(info->maxpathTable, (char *)regChild,
- (char *)NIL(char)) == ST_OUT_OF_MEM) {
+ if ( st__insert(info->maxpathTable, (char *)regChild,
+ (char *)NIL(char)) == st__OUT_OF_MEM) {
memOut = 1;
(void) fprintf(dd->err, "OUT of memory\n");
info->thresholdReached = 0;
@@ -1503,8 +1503,8 @@ BuildSubsetBdd(
}
} else { /* Threshold hasn't been reached,
** need the node. */
- if (st_insert(info->maxpathTable, (char *)regChild,
- (char *)NIL(char)) == ST_OUT_OF_MEM) {
+ if ( st__insert(info->maxpathTable, (char *)regChild,
+ (char *)NIL(char)) == st__OUT_OF_MEM) {
memOut = 1;
(void) fprintf(dd->err, "OUT of memory\n");
info->thresholdReached = 0;
@@ -1517,7 +1517,7 @@ BuildSubsetBdd(
childBranch = BuildSubsetBdd(dd, pathTable,
child, info, subsetNodeTable);
- } /* end of st_insert successful */
+ } /* end of st__insert successful */
} /* end of threshold hasnt been reached yet */
} /* end of else node not found in maxpath table */
} /* end of if (path length of node = maxpath) */
@@ -1560,20 +1560,20 @@ BuildSubsetBdd(
/* Hard Limit of threshold has been imposed */
- if (subsetNodeTable != NIL(st_table)) {
+ if (subsetNodeTable != NIL( st__table)) {
/* check if a new node is created */
regNew = Cudd_Regular(neW);
/* subset node table keeps all new nodes that have been created to keep
* a running count of how many nodes have been built in the subset.
*/
- if (!st_lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) {
+ if (! st__lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) {
if (!Cudd_IsConstant(regNew)) {
- if (st_insert(subsetNodeTable, (char *)regNew,
- (char *)NULL) == ST_OUT_OF_MEM) {
+ if ( st__insert(subsetNodeTable, (char *)regNew,
+ (char *)NULL) == st__OUT_OF_MEM) {
(void) fprintf(dd->err, "Out of memory\n");
return (NULL);
}
- if (st_count(subsetNodeTable) > info->threshold) {
+ if ( st__count(subsetNodeTable) > info->threshold) {
info->thresholdReached = 0;
}
}
@@ -1639,7 +1639,7 @@ BuildSubsetBdd(
SeeAlso []
******************************************************************************/
-static enum st_retval
+static enum st__retval
stPathTableDdFree(
char * key,
char * value,
@@ -1656,7 +1656,7 @@ stPathTableDdFree(
if (nodeStat->compResult != NULL) {
Cudd_RecursiveDeref(dd, nodeStat->compResult);
}
- return(ST_CONTINUE);
+ return( st__CONTINUE);
} /* end of stPathTableFree */
diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c
index f4848c4d..da591692 100644
--- a/src/bdd/cudd/cuddUtil.c
+++ b/src/bdd/cudd/cuddUtil.c
@@ -168,23 +168,23 @@ extern "C" {
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int dp2 (DdManager *dd, DdNode *f, st_table *t);
+static int dp2 (DdManager *dd, DdNode *f, st__table *t);
static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list);
static int ddDagInt (DdNode *n);
static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index);
-static int cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr);
+static int cuddEstimateCofactor (DdManager *dd, st__table *table, DdNode * node, int i, int phase, DdNode ** ptr);
static DdNode * cuddUniqueLookup (DdManager * unique, int index, DdNode * T, DdNode * E);
static int cuddEstimateCofactorSimple (DdNode * node, int i);
static double ddCountMintermAux (DdNode *node, double max, DdHashTable *table);
-static int ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st_table *table);
-static double ddCountPathAux (DdNode *node, st_table *table);
-static double ddCountPathsToNonZero (DdNode * N, st_table * table);
+static int ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st__table *table);
+static double ddCountPathAux (DdNode *node, st__table *table);
+static double ddCountPathsToNonZero (DdNode * N, st__table * table);
static void ddSupportStep (DdNode *f, int *support);
static void ddClearFlag (DdNode *f);
static int ddLeavesInt (DdNode *n);
static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string);
static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string);
-static enum st_retval ddEpdFree (char * key, char * value, char * arg);
+static enum st__retval ddEpdFree (char * key, char * value, char * arg);
/**AutomaticEnd***************************************************************/
@@ -483,13 +483,13 @@ Cudd_EstimateCofactor(
{
int val;
DdNode *ptr;
- st_table *table;
+ st__table *table;
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) return(CUDD_OUT_OF_MEM);
val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
ddClearFlag(Cudd_Regular(f));
- st_free_table(table);
+ st__free_table(table);
return(val);
@@ -624,16 +624,16 @@ Cudd_CountPath(
DdNode * node)
{
- st_table *table;
+ st__table *table;
double i;
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) {
return((double)CUDD_OUT_OF_MEM);
}
i = ddCountPathAux(Cudd_Regular(node),table);
- st_foreach(table, cuddStCountfree, NULL);
- st_free_table(table);
+ st__foreach(table, cuddStCountfree, NULL);
+ st__free_table(table);
return(i);
} /* end of Cudd_CountPath */
@@ -661,21 +661,21 @@ Cudd_EpdCountMinterm(
EpDouble * epd)
{
EpDouble max, tmp;
- st_table *table;
+ st__table *table;
int status;
background = manager->background;
zero = Cudd_Not(manager->one);
EpdPow2(nvars, &max);
- table = st_init_table(EpdCmp, st_ptrhash);
+ table = st__init_table(EpdCmp, st__ptrhash);
if (table == NULL) {
EpdMakeZero(epd, 0);
return(CUDD_OUT_OF_MEM);
}
status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
- st_foreach(table, ddEpdFree, NULL);
- st_free_table(table);
+ st__foreach(table, ddEpdFree, NULL);
+ st__free_table(table);
if (status == CUDD_OUT_OF_MEM) {
EpdMakeZero(epd, 0);
return(CUDD_OUT_OF_MEM);
@@ -708,16 +708,16 @@ Cudd_CountPathsToNonZero(
DdNode * node)
{
- st_table *table;
+ st__table *table;
double i;
- table = st_init_table(st_ptrcmp,st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) {
return((double)CUDD_OUT_OF_MEM);
}
i = ddCountPathsToNonZero(node,table);
- st_foreach(table, cuddStCountfree, NULL);
- st_free_table(table);
+ st__foreach(table, cuddStCountfree, NULL);
+ st__free_table(table);
return(i);
} /* end of Cudd_CountPathsToNonZero */
@@ -2868,12 +2868,12 @@ cuddP(
DdNode * f)
{
int retval;
- st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
+ st__table *table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) return(0);
retval = dp2(dd,f,table);
- st_free_table(table);
+ st__free_table(table);
(void) fputc('\n',dd->out);
return(retval);
@@ -2886,12 +2886,12 @@ cuddP(
in the visited table.]
Description [Frees the memory used to store the minterm counts
- recorded in the visited table. Returns ST_CONTINUE.]
+ recorded in the visited table. Returns st__CONTINUE.]
SideEffects [None]
******************************************************************************/
-enum st_retval
+enum st__retval
cuddStCountfree(
char * key,
char * value,
@@ -2901,7 +2901,7 @@ cuddStCountfree(
d = (double *)value;
ABC_FREE(d);
- return(ST_CONTINUE);
+ return( st__CONTINUE);
} /* end of cuddStCountfree */
@@ -2924,7 +2924,7 @@ cuddStCountfree(
int
cuddCollectNodes(
DdNode * f,
- st_table * visited)
+ st__table * visited)
{
DdNode *T, *E;
int retval;
@@ -2934,7 +2934,7 @@ cuddCollectNodes(
#endif
/* If already visited, nothing to do. */
- if (st_is_member(visited, (char *) f) == 1)
+ if ( st__is_member(visited, (char *) f) == 1)
return(1);
/* Check for abnormal condition that should never happen. */
@@ -2942,7 +2942,7 @@ cuddCollectNodes(
return(0);
/* Mark node as visited. */
- if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
+ if ( st__add_direct(visited, (char *) f, NULL) == st__OUT_OF_MEM)
return(0);
/* Check terminal case. */
@@ -3018,7 +3018,7 @@ static int
dp2(
DdManager *dd,
DdNode * f,
- st_table * t)
+ st__table * t)
{
DdNode *g, *n, *N;
int T,E;
@@ -3037,10 +3037,10 @@ dp2(
#endif
return(1);
}
- if (st_is_member(t,(char *) g) == 1) {
+ if ( st__is_member(t,(char *) g) == 1) {
return(1);
}
- if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
+ if ( st__add_direct(t,(char *) g,NULL) == st__OUT_OF_MEM)
return(0);
#ifdef DD_STATS
#if SIZEOF_VOID_P == 8
@@ -3239,7 +3239,7 @@ cuddNodeArrayRecur(
static int
cuddEstimateCofactor(
DdManager *dd,
- st_table *table,
+ st__table *table,
DdNode * node,
int i,
int phase,
@@ -3249,9 +3249,9 @@ cuddEstimateCofactor(
DdNode *ptrT, *ptrE;
if (Cudd_IsComplement(node->next)) {
- if (!st_lookup(table,(char *)node,(char **)ptr)) {
- if (st_add_direct(table,(char *)node,(char *)node) ==
- ST_OUT_OF_MEM)
+ if (! st__lookup(table,(char *)node,(char **)ptr)) {
+ if ( st__add_direct(table,(char *)node,(char *)node) ==
+ st__OUT_OF_MEM)
return(CUDD_OUT_OF_MEM);
*ptr = node;
}
@@ -3260,7 +3260,7 @@ cuddEstimateCofactor(
node->next = Cudd_Not(node->next);
if (cuddIsConstant(node)) {
*ptr = node;
- if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM)
+ if ( st__add_direct(table,(char *)node,(char *)node) == st__OUT_OF_MEM)
return(CUDD_OUT_OF_MEM);
return(1);
}
@@ -3273,8 +3273,8 @@ cuddEstimateCofactor(
val = ddDagInt(Cudd_Regular(cuddE(node)));
}
if (node->ref > 1) {
- if (st_add_direct(table,(char *)node,(char *)*ptr) ==
- ST_OUT_OF_MEM)
+ if ( st__add_direct(table,(char *)node,(char *)*ptr) ==
+ st__OUT_OF_MEM)
return(CUDD_OUT_OF_MEM);
}
return(val);
@@ -3284,8 +3284,8 @@ cuddEstimateCofactor(
tval = ddDagInt(cuddT(node));
eval = ddDagInt(Cudd_Regular(cuddE(node)));
if (node->ref > 1) {
- if (st_add_direct(table,(char *)node,(char *)node) ==
- ST_OUT_OF_MEM)
+ if ( st__add_direct(table,(char *)node,(char *)node) ==
+ st__OUT_OF_MEM)
return(CUDD_OUT_OF_MEM);
}
val = 1 + tval + eval;
@@ -3299,8 +3299,8 @@ cuddEstimateCofactor(
*ptr = ptrT;
val = tval;
if (node->ref > 1) {
- if (st_add_direct(table,(char *)node,(char *)*ptr) ==
- ST_OUT_OF_MEM)
+ if ( st__add_direct(table,(char *)node,(char *)*ptr) ==
+ st__OUT_OF_MEM)
return(CUDD_OUT_OF_MEM);
}
} else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
@@ -3311,8 +3311,8 @@ cuddEstimateCofactor(
val = 1 + tval + eval;
}
if (node->ref > 1) {
- if (st_add_direct(table,(char *)node,(char *)*ptr) ==
- ST_OUT_OF_MEM)
+ if ( st__add_direct(table,(char *)node,(char *)*ptr) ==
+ st__OUT_OF_MEM)
return(CUDD_OUT_OF_MEM);
}
} else {
@@ -3511,7 +3511,7 @@ ddCountMintermAux(
static double
ddCountPathAux(
DdNode * node,
- st_table * table)
+ st__table * table)
{
DdNode *Nv, *Nnv;
@@ -3522,7 +3522,7 @@ ddCountPathAux(
if (cuddIsConstant(node)) {
return(1.0);
}
- if (st_lookup(table, (const char *)node, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)node, (char **)&dummy)) {
paths = *dummy;
return(paths);
}
@@ -3542,7 +3542,7 @@ ddCountPathAux(
*ppaths = paths;
- if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
+ if ( st__add_direct(table,(char *)node, (char *)ppaths) == st__OUT_OF_MEM) {
ABC_FREE(ppaths);
return((double)CUDD_OUT_OF_MEM);
}
@@ -3574,7 +3574,7 @@ ddEpdCountMintermAux(
DdNode * node,
EpDouble * max,
EpDouble * epd,
- st_table * table)
+ st__table * table)
{
DdNode *Nt, *Ne;
EpDouble *min, minT, minE;
@@ -3590,7 +3590,7 @@ ddEpdCountMintermAux(
}
return(0);
}
- if (node->ref != 1 && st_lookup(table, (const char *)node, (char **)&res)) {
+ if (node->ref != 1 && st__lookup(table, (const char *)node, (char **)&res)) {
EpdCopy(res, epd);
return(0);
}
@@ -3614,7 +3614,7 @@ ddEpdCountMintermAux(
if (!min)
return(CUDD_OUT_OF_MEM);
EpdCopy(epd, min);
- if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) {
+ if ( st__insert(table, (char *)node, (char *)min) == st__OUT_OF_MEM) {
EpdFree(min);
return(CUDD_OUT_OF_MEM);
}
@@ -3644,7 +3644,7 @@ ddEpdCountMintermAux(
static double
ddCountPathsToNonZero(
DdNode * N,
- st_table * table)
+ st__table * table)
{
DdNode *node, *Nt, *Ne;
@@ -3655,7 +3655,7 @@ ddCountPathsToNonZero(
if (cuddIsConstant(node)) {
return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
}
- if (st_lookup(table, (const char *)N, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)N, (char **)&dummy)) {
paths = *dummy;
return(paths);
}
@@ -3678,7 +3678,7 @@ ddCountPathsToNonZero(
*ppaths = paths;
- if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
+ if ( st__add_direct(table,(char *)N, (char *)ppaths) == st__OUT_OF_MEM) {
ABC_FREE(ppaths);
return((double)CUDD_OUT_OF_MEM);
}
@@ -3913,12 +3913,12 @@ ddPickRepresentativeCube(
in the visited table.]
Description [Frees the memory used to store the minterm counts
- recorded in the visited table. Returns ST_CONTINUE.]
+ recorded in the visited table. Returns st__CONTINUE.]
SideEffects [None]
******************************************************************************/
-static enum st_retval
+static enum st__retval
ddEpdFree(
char * key,
char * value,
@@ -3928,7 +3928,7 @@ ddEpdFree(
epd = (EpDouble *) value;
EpdFree(epd);
- return(ST_CONTINUE);
+ return( st__CONTINUE);
} /* end of ddEpdFree */
diff --git a/src/bdd/cudd/cuddZddCount.c b/src/bdd/cudd/cuddZddCount.c
index 0667a08b..aefdc124 100644
--- a/src/bdd/cudd/cuddZddCount.c
+++ b/src/bdd/cudd/cuddZddCount.c
@@ -18,8 +18,8 @@
<ul>
<li> cuddZddCountStep();
<li> cuddZddCountDoubleStep();
- <li> st_zdd_count_dbl_free()
- <li> st_zdd_countfree()
+ <li> st__zdd_count_dbl_free()
+ <li> st__zdd_countfree()
</ul>
]
@@ -105,10 +105,10 @@ extern "C" {
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int cuddZddCountStep (DdNode *P, st_table *table, DdNode *base, DdNode *empty);
-static double cuddZddCountDoubleStep (DdNode *P, st_table *table, DdNode *base, DdNode *empty);
-static enum st_retval st_zdd_countfree (char *key, char *value, char *arg);
-static enum st_retval st_zdd_count_dbl_free (char *key, char *value, char *arg);
+static int cuddZddCountStep (DdNode *P, st__table *table, DdNode *base, DdNode *empty);
+static double cuddZddCountDoubleStep (DdNode *P, st__table *table, DdNode *base, DdNode *empty);
+static enum st__retval st__zdd_countfree (char *key, char *value, char *arg);
+static enum st__retval st__zdd_count_dbl_free (char *key, char *value, char *arg);
/**AutomaticEnd***************************************************************/
@@ -138,20 +138,20 @@ Cudd_zddCount(
DdManager * zdd,
DdNode * P)
{
- st_table *table;
+ st__table *table;
int res;
DdNode *base, *empty;
base = DD_ONE(zdd);
empty = DD_ZERO(zdd);
- table = st_init_table(st_ptrcmp, st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) return(CUDD_OUT_OF_MEM);
res = cuddZddCountStep(P, table, base, empty);
if (res == CUDD_OUT_OF_MEM) {
zdd->errorCode = CUDD_MEMORY_OUT;
}
- st_foreach(table, st_zdd_countfree, NIL(char));
- st_free_table(table);
+ st__foreach(table, st__zdd_countfree, NIL(char));
+ st__free_table(table);
return(res);
@@ -177,20 +177,20 @@ Cudd_zddCountDouble(
DdManager * zdd,
DdNode * P)
{
- st_table *table;
+ st__table *table;
double res;
DdNode *base, *empty;
base = DD_ONE(zdd);
empty = DD_ZERO(zdd);
- table = st_init_table(st_ptrcmp, st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) return((double)CUDD_OUT_OF_MEM);
res = cuddZddCountDoubleStep(P, table, base, empty);
if (res == (double)CUDD_OUT_OF_MEM) {
zdd->errorCode = CUDD_MEMORY_OUT;
}
- st_foreach(table, st_zdd_count_dbl_free, NIL(char));
- st_free_table(table);
+ st__foreach(table, st__zdd_count_dbl_free, NIL(char));
+ st__free_table(table);
return(res);
@@ -221,7 +221,7 @@ Cudd_zddCountDouble(
static int
cuddZddCountStep(
DdNode * P,
- st_table * table,
+ st__table * table,
DdNode * base,
DdNode * empty)
{
@@ -234,7 +234,7 @@ cuddZddCountStep(
return(1);
/* Check cache. */
- if (st_lookup(table, (const char *)P, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)P, (char **)&dummy)) {
res = *dummy;
return(res);
}
@@ -247,7 +247,7 @@ cuddZddCountStep(
return(CUDD_OUT_OF_MEM);
}
*dummy = res;
- if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
+ if ( st__insert(table, (char *)P, (char *)dummy) == st__OUT_OF_MEM) {
ABC_FREE(dummy);
return(CUDD_OUT_OF_MEM);
}
@@ -271,7 +271,7 @@ cuddZddCountStep(
static double
cuddZddCountDoubleStep(
DdNode * P,
- st_table * table,
+ st__table * table,
DdNode * base,
DdNode * empty)
{
@@ -284,7 +284,7 @@ cuddZddCountDoubleStep(
return((double)1.0);
/* Check cache */
- if (st_lookup(table, (const char *)P, (char **)&dummy)) {
+ if ( st__lookup(table, (const char *)P, (char **)&dummy)) {
res = *dummy;
return(res);
}
@@ -297,7 +297,7 @@ cuddZddCountDoubleStep(
return((double)CUDD_OUT_OF_MEM);
}
*dummy = res;
- if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
+ if ( st__insert(table, (char *)P, (char *)dummy) == st__OUT_OF_MEM) {
ABC_FREE(dummy);
return((double)CUDD_OUT_OF_MEM);
}
@@ -319,8 +319,8 @@ cuddZddCountDoubleStep(
SeeAlso []
******************************************************************************/
-static enum st_retval
-st_zdd_countfree(
+static enum st__retval
+ st__zdd_countfree(
char * key,
char * value,
char * arg)
@@ -329,9 +329,9 @@ st_zdd_countfree(
d = (int *)value;
ABC_FREE(d);
- return(ST_CONTINUE);
+ return( st__CONTINUE);
-} /* end of st_zdd_countfree */
+} /* end of st__zdd_countfree */
/**Function********************************************************************
@@ -346,8 +346,8 @@ st_zdd_countfree(
SeeAlso []
******************************************************************************/
-static enum st_retval
-st_zdd_count_dbl_free(
+static enum st__retval
+ st__zdd_count_dbl_free(
char * key,
char * value,
char * arg)
@@ -356,9 +356,9 @@ st_zdd_count_dbl_free(
d = (double *)value;
ABC_FREE(d);
- return(ST_CONTINUE);
+ return( st__CONTINUE);
-} /* end of st_zdd_count_dbl_free */
+} /* end of st__zdd_count_dbl_free */
ABC_NAMESPACE_IMPL_END
diff --git a/src/bdd/cudd/cuddZddMisc.c b/src/bdd/cudd/cuddZddMisc.c
index 05b3e92f..e5d5f5e8 100644
--- a/src/bdd/cudd/cuddZddMisc.c
+++ b/src/bdd/cudd/cuddZddMisc.c
@@ -101,7 +101,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.16 2009/02/20 02:14:58 f
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int cuddZddDagInt (DdNode *n, st_table *tab);
+static int cuddZddDagInt (DdNode *n, st__table *tab);
/**AutomaticEnd***************************************************************/
@@ -129,11 +129,11 @@ Cudd_zddDagSize(
{
int i;
- st_table *table;
+ st__table *table;
- table = st_init_table(st_ptrcmp, st_ptrhash);
+ table = st__init_table( st__ptrcmp, st__ptrhash);
i = cuddZddDagInt(p_node, table);
- st_free_table(table);
+ st__free_table(table);
return(i);
} /* end of Cudd_zddDagSize */
@@ -264,18 +264,18 @@ Cudd_zddPrintSubtable(
static int
cuddZddDagInt(
DdNode * n,
- st_table * tab)
+ st__table * tab)
{
if (n == NIL(DdNode))
return(0);
- if (st_is_member(tab, (char *)n) == 1)
+ if ( st__is_member(tab, (char *)n) == 1)
return(0);
if (Cudd_IsConstant(n))
return(0);
- (void)st_insert(tab, (char *)n, NIL(char));
+ (void) st__insert(tab, (char *)n, NIL(char));
return(1 + cuddZddDagInt(cuddT(n), tab) +
cuddZddDagInt(cuddE(n), tab));
diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c
index a596c8ab..6a63227f 100644
--- a/src/bdd/cudd/cuddZddUtil.c
+++ b/src/bdd/cudd/cuddZddUtil.c
@@ -107,7 +107,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddUtil.c,v 1.27 2009/03/08 02:49:02 f
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int zp2 (DdManager *zdd, DdNode *f, st_table *t);
+static int zp2 (DdManager *zdd, DdNode *f, st__table *t);
static void zdd_print_minterm_aux (DdManager *zdd, DdNode *node, int level, int *list);
static void zddPrintCoverAux (DdManager *zdd, DdNode *node, int level, int *list);
@@ -558,8 +558,8 @@ Cudd_zddDumpDot(
DdNode *scan;
int *sorted = NULL;
int nvars = dd->sizeZ;
- st_table *visited = NULL;
- st_generator *gen;
+ st__table *visited = NULL;
+ st__generator *gen;
int retval;
int i, j;
int slots;
@@ -589,7 +589,7 @@ Cudd_zddDumpDot(
support = NULL; /* so that we do not try to free it in case of failure */
/* Initialize symbol table for visited nodes. */
- visited = st_init_table(st_ptrcmp, st_ptrhash);
+ visited = st__init_table( st__ptrcmp, st__ptrhash);
if (visited == NULL) goto failure;
/* Collect all the nodes of this DD in the symbol table. */
@@ -612,11 +612,11 @@ Cudd_zddDumpDot(
/* Find the bits that are different. */
refAddr = (long) f[0];
diff = 0;
- gen = st_init_gen(visited);
- while (st_gen(gen, (const char **)&scan, NULL)) {
+ gen = st__init_gen(visited);
+ while ( st__gen(gen, (const char **)&scan, NULL)) {
diff |= refAddr ^ (long) scan;
}
- st_free_gen(gen);
+ st__free_gen(gen);
/* Choose the mask. */
for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
@@ -688,7 +688,7 @@ Cudd_zddDumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%p\";\n", (void *)
((mask & (ptrint) scan) /
sizeof(DdNode)));
@@ -711,7 +711,7 @@ Cudd_zddDumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%p\";\n", (void *)
((mask & (ptrint) scan) / sizeof(DdNode)));
if (retval == EOF) goto failure;
@@ -745,7 +745,7 @@ Cudd_zddDumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,
"\"%p\" -> \"%p\";\n",
(void *) ((mask & (ptrint) scan) / sizeof(DdNode)),
@@ -773,7 +773,7 @@ Cudd_zddDumpDot(
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
- if (st_is_member(visited,(char *) scan)) {
+ if ( st__is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n",
(void *) ((mask & (ptrint) scan) /
sizeof(DdNode)),
@@ -788,13 +788,13 @@ Cudd_zddDumpDot(
retval = fprintf(fp,"}\n");
if (retval == EOF) goto failure;
- st_free_table(visited);
+ st__free_table(visited);
ABC_FREE(sorted);
return(1);
failure:
if (sorted != NULL) ABC_FREE(sorted);
- if (visited != NULL) st_free_table(visited);
+ if (visited != NULL) st__free_table(visited);
return(0);
} /* end of Cudd_zddDumpBlif */
@@ -824,12 +824,12 @@ cuddZddP(
DdNode * f)
{
int retval;
- st_table *table = st_init_table(st_ptrcmp, st_ptrhash);
+ st__table *table = st__init_table( st__ptrcmp, st__ptrhash);
if (table == NULL) return(0);
retval = zp2(zdd, f, table);
- st_free_table(table);
+ st__free_table(table);
(void) fputc('\n', zdd->out);
return(retval);
@@ -857,7 +857,7 @@ static int
zp2(
DdManager * zdd,
DdNode * f,
- st_table * t)
+ st__table * t)
{
DdNode *n;
int T, E;
@@ -870,10 +870,10 @@ zp2(
(void)fprintf(zdd->out, "ID = %d\n", (f == base));
return(1);
}
- if (st_is_member(t, (char *)f) == 1)
+ if ( st__is_member(t, (char *)f) == 1)
return(1);
- if (st_insert(t, (char *) f, NULL) == ST_OUT_OF_MEM)
+ if ( st__insert(t, (char *) f, NULL) == st__OUT_OF_MEM)
return(0);
#if SIZEOF_VOID_P == 8
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index 4de75a92..c36fbef4 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -80,7 +80,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
}
// otherwise, there is no need to allocate, just clean
Dsd_CheckCacheClear();
-// printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize );
+// printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize );
}
/**Function********************************************************************
@@ -133,10 +133,10 @@ void Dsd_CheckCacheClear()
int Dsd_CheckRootFunctionIdentity( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 )
{
int RetValue;
-// pCache->nSuccess = 0;
-// pCache->nFailure = 0;
+// pCache->nSuccess = 0;
+// pCache->nFailure = 0;
RetValue = Dsd_CheckRootFunctionIdentity_rec(dd, bF1, bF2, bC1, bC2);
-// printf( "Cache success = %d. Cache failure = %d.\n", pCache->nSuccess, pCache->nFailure );
+// printf( "Cache success = %d. Cache failure = %d.\n", pCache->nSuccess, pCache->nFailure );
return RetValue;
}
@@ -156,7 +156,7 @@ int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF
unsigned HKey;
// if either bC1 or bC2 is zero, the test is true
-// if ( bC1 == b0 || bC2 == b0 ) return 1;
+// if ( bC1 == b0 || bC2 == b0 ) return 1;
assert( bC1 != b0 );
assert( bC2 != b0 );
@@ -178,7 +178,7 @@ int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF
// otherwise, keep expanding
// check cache
-// HKey = _Hash( ((unsigned)bF1), ((unsigned)bF2), ((unsigned)bC1), ((unsigned)bC2) );
+// HKey = _Hash( ((unsigned)bF1), ((unsigned)bF2), ((unsigned)bC1), ((unsigned)bC2) );
HKey = hashKey4( bF1, bF2, bC1, bC2, pCache->nTableSize );
if ( pCache->pTable[HKey].bX[0] == bF1 &&
pCache->pTable[HKey].bX[1] == bF2 &&
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 787f1747..16a0594a 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -40,7 +40,7 @@ typedef unsigned char byte;
struct Dsd_Manager_t_
{
DdManager * dd; // the BDD manager
- st_table * Table; // the mapping of BDDs into their DEs
+ st__table * Table; // the mapping of BDDs into their DEs
int nInputs; // the number of primary inputs
int nRoots; // the number of primary outputs
int nRootsAlloc;// the number of primary outputs
@@ -54,7 +54,7 @@ struct Dsd_Manager_t_
struct Dsd_Node_t_
{
Dsd_Type_t Type; // decomposition type
- DdNode * G; // function of the node
+ DdNode * G; // function of the node
DdNode * S; // support of this function
Dsd_Node_t ** pDecs; // pointer to structures for formal inputs
int Mark; // the mark used by CASE 4 of disjoint decomposition
diff --git a/src/bdd/dsd/dsdLocal.c b/src/bdd/dsd/dsdLocal.c
index a61b656c..552b53e9 100644
--- a/src/bdd/dsd/dsdLocal.c
+++ b/src/bdd/dsd/dsdLocal.c
@@ -29,7 +29,7 @@ ABC_NAMESPACE_IMPL_START
/// STATIC VARIABLES ///
////////////////////////////////////////////////////////////////////////
-static DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bFunc, st_table * pCache,
+static DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bFunc, st__table * pCache,
int * pVar2Form, int * pForm2Var, DdNode * pbCube0[], DdNode * pbCube1[] );
static DdNode * Extra_bddNodePointedByCube( DdManager * dd, DdNode * bF, DdNode * bC );
@@ -58,7 +58,7 @@ DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode )
int i, iVar, iLev, * pPermute;
DdNode ** pbCube0, ** pbCube1;
DdNode * bFunc, * bRes, * bTemp;
- st_table * pCache;
+ st__table * pCache;
pPermute = ABC_ALLOC( int, dd->size );
pVar2Form = ABC_ALLOC( int, dd->size );
@@ -100,9 +100,9 @@ DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode )
}
// remap the function
- pCache = st_init_table(st_ptrcmp, st_ptrhash);;
+ pCache = st__init_table( st__ptrcmp, st__ptrhash);;
bRes = Extra_dsdRemap( dd, bFunc, pCache, pVar2Form, pForm2Var, pbCube0, pbCube1 ); Cudd_Ref( bRes );
- st_free_table( pCache );
+ st__free_table( pCache );
Cudd_RecursiveDeref( dd, bFunc );
for ( i = 0; i < pNode->nDecs; i++ )
@@ -143,7 +143,7 @@ DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode )
SeeAlso []
***********************************************************************/
-DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bF, st_table * pCache,
+DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bF, st__table * pCache,
int * pVar2Form, int * pForm2Var, DdNode * pbCube0[], DdNode * pbCube1[] )
{
DdNode * bFR, * bF0, * bF1;
@@ -157,7 +157,7 @@ DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bF, st_table * pCache,
// check the hash-table
if ( bFR->ref != 1 )
{
- if ( st_lookup( pCache, (char *)bF, (char **)&bRes ) )
+ if ( st__lookup( pCache, (char *)bF, (char **)&bRes ) )
return bRes;
}
@@ -179,7 +179,7 @@ DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bF, st_table * pCache,
// add to the hash table
if ( bFR->ref != 1 )
- st_insert( pCache, (char *)bF, (char *)bRes );
+ st__insert( pCache, (char *)bF, (char *)bRes );
Cudd_Deref( bRes );
return bRes;
}
@@ -208,7 +208,7 @@ DdNode * Extra_bddNodePointedByCube( DdManager * dd, DdNode * bF, DdNode * bC )
// bRes = cuddCacheLookup2( dd, Extra_bddNodePointedByCube, bF, bC );
// if ( bRes )
-// return bRes;
+// return bRes;
// there is no need for caching because this operation is very fast
// there will no gain reusing the results of this operations
// instead, it will flush CUDD cache of other useful entries
@@ -310,7 +310,7 @@ DdNode * dsdTreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode, int fRemap
Cudd_RecursiveDeref( dd, bNewFunc );
// use the variable in the i-th level of the manager
-// bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
+// bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
// use the first variale in the support of the component
bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
Cudd_RecursiveDeref( dd, bCof0 );
@@ -322,7 +322,7 @@ DdNode * dsdTreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode, int fRemap
// remap the function to the top of the manager
// remap the function to the first variables of the manager
for ( i = 0; i < pNode->nDecs; i++ )
- // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
+ // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
Permute[ pNode->pDecs[i]->S->index ] = i;
bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc );
diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c
index 8d108317..1490fcf3 100644
--- a/src/bdd/dsd/dsdMan.c
+++ b/src/bdd/dsd/dsdMan.c
@@ -63,19 +63,19 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
dMan->pInputs = (Dsd_Node_t **) ABC_ALLOC( char, dMan->nInputs * sizeof(Dsd_Node_t *) );
// create the primary inputs and insert them into the table
- dMan->Table = st_init_table(st_ptrcmp, st_ptrhash);
+ dMan->Table = st__init_table( st__ptrcmp, st__ptrhash);
for ( i = 0; i < dMan->nInputs; i++ )
{
pNode = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, 0 );
pNode->G = dd->vars[i]; Cudd_Ref( pNode->G );
pNode->S = dd->vars[i]; Cudd_Ref( pNode->S );
- st_insert( dMan->Table, (char*)dd->vars[i], (char*)pNode );
+ st__insert( dMan->Table, (char*)dd->vars[i], (char*)pNode );
dMan->pInputs[i] = pNode;
}
pNode = Dsd_TreeNodeCreate( DSD_NODE_CONST1, 0, 0 );
pNode->G = b1; Cudd_Ref( pNode->G );
pNode->S = b1; Cudd_Ref( pNode->S );
- st_insert( dMan->Table, (char*)b1, (char*)pNode );
+ st__insert( dMan->Table, (char*)b1, (char*)pNode );
dMan->pConst1 = pNode;
Dsd_CheckCacheAllocate( 5000 );
@@ -99,13 +99,13 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
***********************************************************************/
void Dsd_ManagerStop( Dsd_Manager_t * dMan )
{
- st_generator * gen;
+ st__generator * gen;
Dsd_Node_t * pNode;
DdNode * bFunc;
// delete the nodes
- st_foreach_item( dMan->Table, gen, (const char**)&bFunc, (char**)&pNode )
+ st__foreach_item( dMan->Table, gen, (const char**)&bFunc, (char**)&pNode )
Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) );
- st_free_table(dMan->Table);
+ st__free_table(dMan->Table);
ABC_FREE( dMan->pInputs );
ABC_FREE( dMan->pRoots );
ABC_FREE( dMan );
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 291648b3..996fd3dc 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -202,7 +202,7 @@ s_Loops2Useless = 0;
printf( " Completely decomposable outputs = %5d\n", nCBFOutputs );
printf( " The sum of max gate sizes = %5d\n", SumMaxGateSize );
printf( " Shared BDD size = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
- printf( " Decomposition entries = %5d\n", st_count( pDsdMan->Table ) );
+ printf( " Decomposition entries = %5d\n", st__count( pDsdMan->Table ) );
printf( " Pure decomposition time = %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
}
/*
@@ -275,7 +275,7 @@ Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 )
int fCompF = (int)(bF != bFunc0);
// check cache
- if ( st_lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) )
+ if ( st__lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) )
{ // the entry is present
HashSuccess++;
return Dsd_NotCond( pTableEntry, fCompF );
@@ -338,19 +338,19 @@ Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 )
/////////////////////////////////////////////////////////////////
if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement
{ // add to the components
- pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ );
+ pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ );
dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs );
pThis = Dsd_Not(pThis);
}
else // all other cases
{ // create a new 2-input NOR gate
- pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
+ pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
pH = Dsd_Not(pH);
dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
pThis = Dsd_Not(pThis);
}
else // if ( bLow == b1 )
- /////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////
// Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High)
/////////////////////////////////////////////////////////////////
if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement
@@ -412,8 +412,8 @@ Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 )
/*
if ( Depth == 1 )
{
-// PRK(bLow,pDecTreeTotal->nInputs);
-// PRK(bHigh,pDecTreeTotal->nInputs);
+// PRK(bLow,pDecTreeTotal->nInputs);
+// PRK(bHigh,pDecTreeTotal->nInputs);
if ( s_Show )
{
PRD( pL );
@@ -503,7 +503,7 @@ if ( s_Show )
}
for ( g = 0; g < pLargeR->nDecs; g++ )
-// if ( g != c )
+// if ( g != c )
{
pDETemp = pLargeR->pDecs[g]; // cannot be complemented
if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) )
@@ -584,7 +584,7 @@ if ( s_Show )
if ( pComp ) // the decomposition is possible!
{
-// Dsd_Node_t * pComp = pLargeR->pDecs[iCompLarge];
+// Dsd_Node_t * pComp = pLargeR->pDecs[iCompLarge];
Dsd_Node_t * pCompR = Dsd_Regular( pComp );
int fComp1 = (int)( pLarge != pLargeR );
int fComp2 = (int)( pComp != pCompR );
@@ -753,7 +753,7 @@ if ( s_Show )
dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 );
Cudd_Ref( bCommF );
Cudd_Ref( bCommS );
- bFTemp = ( pL != pLR )? Cudd_Not(bF): bF;
+ bFTemp = ( pL != pLR )? Cudd_Not(bF): bF;
bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew );
Cudd_RecursiveDeref( dd, bCommF );
@@ -768,7 +768,7 @@ if ( s_Show )
// call the decomposition recursively
pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
-// assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
+// assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
Cudd_RecursiveDeref( dd, bFuncNew );
// add the first component
@@ -824,12 +824,12 @@ if ( s_Show )
Dsd_Node_t * pDENew;
DdNode * bFuncNew;
- int fCompComp = 0; // this flag can be {0,1,2}
+ int fCompComp = 0; // this flag can be {0,1,2}
// if it is 0 there is no identity
// if it is 1/2, the cofactored functions are equal in the direct/complemented polarity
if ( nCommon == pLR->nDecs )
- { // all the components are the same
+ { // all the components are the same
// find the formal input, in which pLow and pHigh differ (if such input exists)
int m;
Dsd_Node_t * pTempL, * pTempH;
@@ -1039,11 +1039,11 @@ if ( s_Show )
// find the first component in pHigher
// whose support does not overlap with supp(Lower)
// and remember the previous component
- int fPolarity;
+ int fPolarity;
Dsd_Node_t * pPrev = NULL; // the pointer to the component proceeding pCur
Dsd_Node_t * pCur = pHigher; // the first component not contained in supp(Lower)
while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) )
- { // get the next component
+ { // get the next component
pPrev = pCur;
pCur = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity );
};
@@ -1176,7 +1176,7 @@ if ( s_Show )
if ( nCommon == 0 || nCommon == 1 )
{ // one one component was found, which is the original one
- // assert( Dsd_Regular(pCommon[0]) == pCurL);
+ // assert( Dsd_Regular(pCommon[0]) == pCurL);
// add the new decomposition entry
pThis->pDecs[ nEntries++ ] = pCurL;
// assign the support to be subtracted from both components
@@ -1242,7 +1242,7 @@ EXIT:
assert( bSuppNew );
pThisR->S = bSuppNew; // takes the reference from the new support
- if ( st_insert( pDsdMan->Table, (char*)bF, (char*)pThis ) )
+ if ( st__insert( pDsdMan->Table, (char*)bF, (char*)pThis ) )
{
assert( 0 );
}
@@ -1303,8 +1303,8 @@ Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node
Dsd_Node_t * pTemp;
int i;
-// assert( !Dsd_IsComplement( pWhere ) );
-// assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) );
+// assert( !Dsd_IsComplement( pWhere ) );
+// assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) );
if ( pWhere->nDecs == 1 )
return NULL;
@@ -1408,7 +1408,7 @@ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd
// return the pointer to the array
*pCommon = Common;
// return the number of common components
- return nCommon;
+ return nCommon;
}
/**Function*************************************************************
@@ -1587,7 +1587,7 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
bGVars[dd->invperm[i]] = pR->pDecs[i]->G;
// perform the composition
- bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars ); Cudd_Ref( bRes );
+ bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bNewFunc );
/////////////////////////////////////////////////////////
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 9d1269a1..e534e00a 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -688,7 +688,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
pInputNums = ABC_ALLOC( int, pNode->nDecs );
if ( pNode->Type == DSD_NODE_CONST1 )
{
- fprintf( pFile, " Constant 1.\n" );
+ fprintf( pFile, " Constant 1.\n" );
}
else if ( pNode->Type == DSD_NODE_BUF )
{
@@ -1036,7 +1036,7 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
Cudd_RecursiveDeref( dd, bNewFunc );
// use the variable in the i-th level of the manager
-// bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
+// bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
// use the first variale in the support of the component
bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
Cudd_RecursiveDeref( dd, bCof0 );
@@ -1048,7 +1048,7 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
// remap the function to the top of the manager
// remap the function to the first variables of the manager
for ( i = 0; i < pNode->nDecs; i++ )
- // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
+ // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
Permute[ pNode->pDecs[i]->S->index ] = i;
bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc );
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-28 20:56:27 +0000