initial commit of public abc

author: Alan Mishchenko <alanmi@berkeley.edu> 2010-11-01 01:35:04 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2010-11-01 01:35:04 -0700
commit: 6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch)
tree: 0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/bdd/cudd
parent: f0e77f6797c0504b0da25a56152b707d3357f386 (diff)
download: abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz
abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2
abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip
64 files changed, 461 insertions, 131 deletions
diff --git a/src/bdd/cudd/cudd.h b/src/bdd/cudd/cudd.h
index a31fcdae..14f67abf 100644
--- a/src/bdd/cudd/cudd.h
+++ b/src/bdd/cudd/cudd.h
@@ -30,6 +30,7 @@
 #ifndef _CUDD
 #define _CUDD
 
+
 /*---------------------------------------------------------------------------*/
 /* Nested includes                                                           */
 /*---------------------------------------------------------------------------*/
@@ -37,6 +38,9 @@
 #include "mtr.h"
 #include "epd.h"
 
+ABC_NAMESPACE_HEADER_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -530,20 +534,20 @@ typedef DdApaDigit * DdApaNumber;
 /* These are potential duplicates. */
 #ifndef EXTERN
 #   ifdef __cplusplus
-#    define EXTERN extern "C"
+#       ifdef ABC_NAMESPACE
+#           define EXTERN extern
+#       else
+#           define EXTERN extern "C"
+#       endif
 #   else
 #    define EXTERN extern
 #   endif
 #endif
+
 #ifndef ARGS
-#   if defined(__STDC__) || defined(__cplusplus)
-#    define ARGS(protos)    protos        /* ANSI C */
-#   else /* !(__STDC__ || __cplusplus) */
-#    define ARGS(protos)    ()        /* K&R C */
-#   endif /* !(__STDC__ || __cplusplus) */
+#define ARGS(protos) protos
 #endif
 
-
 /**AutomaticStart*************************************************************/
 
 /*---------------------------------------------------------------------------*/
@@ -956,4 +960,8 @@ EXTERN int Cudd_bddIsVarHardGroup ARGS((DdManager *dd, int index));
 
 /**AutomaticEnd***************************************************************/
 
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif /* _CUDD */
diff --git a/src/bdd/cudd/cuddAPI.c b/src/bdd/cudd/cuddAPI.c
index cbba4d95..729dd329 100644
--- a/src/bdd/cudd/cuddAPI.c
+++ b/src/bdd/cudd/cuddAPI.c
@@ -167,6 +167,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1740,7 +1743,7 @@ Cudd_ReadGarbageCollectionTime(
 
   Synopsis    [Returns the number of nodes freed.]
 
-  Description [Returns the number of nodes returned to the ABC_FREE list if the
+  Description [Returns the number of nodes returned to the free list if the
   keeping of this statistic is enabled; -1 otherwise. This statistic is
   enabled only if the package is compiled with DD_STATS defined.]
 
@@ -3078,7 +3081,7 @@ Cudd_PrintInfo(
   Synopsis    [Reports the peak number of nodes.]
 
   Description [Reports the peak number of nodes. This number includes
-  node on the ABC_FREE list. At the peak, the number of nodes on the ABC_FREE
+  node on the free list. At the peak, the number of nodes on the free
   list is guaranteed to be less than DD_MEM_CHUNK.]
 
   SideEffects [None]
@@ -4407,3 +4410,5 @@ addMultiplicityGroups(
 
 } /* end of addMultiplicityGroups */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddAbs.c b/src/bdd/cudd/cuddAddAbs.c
index b256ad0f..40d3222b 100644
--- a/src/bdd/cudd/cuddAddAbs.c
+++ b/src/bdd/cudd/cuddAddAbs.c
@@ -35,6 +35,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -564,3 +567,5 @@ addCheckPositiveCube(
 
 } /* end of addCheckPositiveCube */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddApply.c b/src/bdd/cudd/cuddAddApply.c
index 60c06de6..5bdc5773 100644
--- a/src/bdd/cudd/cuddAddApply.c
+++ b/src/bdd/cudd/cuddAddApply.c
@@ -45,6 +45,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -915,3 +918,5 @@ cuddAddMonadicApplyRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddFind.c b/src/bdd/cudd/cuddAddFind.c
index 0469b014..6cc58f2d 100644
--- a/src/bdd/cudd/cuddAddFind.c
+++ b/src/bdd/cudd/cuddAddFind.c
@@ -30,6 +30,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -281,3 +284,5 @@ addDoIthBit(
 
 } /* end of addDoIthBit */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddInv.c b/src/bdd/cudd/cuddAddInv.c
index fc4a340b..05650c0e 100644
--- a/src/bdd/cudd/cuddAddInv.c
+++ b/src/bdd/cudd/cuddAddInv.c
@@ -27,6 +27,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -170,3 +173,5 @@ cuddAddScalarInverseRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c
index bcfae83a..def55537 100644
--- a/src/bdd/cudd/cuddAddIte.c
+++ b/src/bdd/cudd/cuddAddIte.c
@@ -36,6 +36,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -611,3 +614,5 @@ addVarToConst(
     }
 
 } /* end of addVarToConst */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddNeg.c b/src/bdd/cudd/cuddAddNeg.c
index bdb08ddc..d99d0357 100644
--- a/src/bdd/cudd/cuddAddNeg.c
+++ b/src/bdd/cudd/cuddAddNeg.c
@@ -29,6 +29,9 @@
 #include    "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -260,3 +263,5 @@ cuddAddRoundOffRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c
index 3022b73d..44b4415d 100644
--- a/src/bdd/cudd/cuddAddWalsh.c
+++ b/src/bdd/cudd/cuddAddWalsh.c
@@ -29,6 +29,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -363,3 +366,5 @@ addWalshInt(
     return(u);
 
 } /* end of addWalshInt */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 5ec47beb..9ee70498 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -27,6 +27,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -304,3 +307,5 @@ cuddBddAndAbstractRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddAnneal.c b/src/bdd/cudd/cuddAnneal.c
index 32155603..c133cdc8 100644
--- a/src/bdd/cudd/cuddAnneal.c
+++ b/src/bdd/cudd/cuddAnneal.c
@@ -38,6 +38,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -786,3 +789,5 @@ restoreOrder(
 
 } /* end of restoreOrder */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddApa.c b/src/bdd/cudd/cuddApa.c
index 13e80ce2..04dac030 100644
--- a/src/bdd/cudd/cuddApa.c
+++ b/src/bdd/cudd/cuddApa.c
@@ -31,6 +31,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -651,7 +654,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);
@@ -661,7 +664,7 @@ Cudd_ApaCountMinterm(
     if (i == NULL) {
     ABC_FREE(max);
     ABC_FREE(min);
-    st_foreach(table, cuddApaStCountfree, NULL);
+    st_foreach(table, (ST_PFSR)cuddApaStCountfree, NULL);
     st_free_table(table);
     return(NULL);
     }
@@ -669,7 +672,7 @@ Cudd_ApaCountMinterm(
     if (count == NULL) {
     ABC_FREE(max);
     ABC_FREE(min);
-    st_foreach(table, cuddApaStCountfree, NULL);
+    st_foreach(table, (ST_PFSR)cuddApaStCountfree, NULL);
     st_free_table(table);
     if (Cudd_Regular(node)->ref == 1) ABC_FREE(i);
     return(NULL);
@@ -681,7 +684,7 @@ Cudd_ApaCountMinterm(
     }
     ABC_FREE(max);
     ABC_FREE(min);
-    st_foreach(table, cuddApaStCountfree, NULL);
+    st_foreach(table, (ST_PFSR)cuddApaStCountfree, NULL);
     st_free_table(table);
     if (Cudd_Regular(node)->ref == 1) ABC_FREE(i);
     return(count);
@@ -928,3 +931,5 @@ cuddApaStCountfree(
 } /* end of cuddApaStCountfree */
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddApprox.c b/src/bdd/cudd/cuddApprox.c
index c575b54b..9641aac0 100644
--- a/src/bdd/cudd/cuddApprox.c
+++ b/src/bdd/cudd/cuddApprox.c
@@ -54,6 +54,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -912,7 +915,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);
@@ -2190,3 +2193,5 @@ BAapplyBias(
     return(infoF->care);
 
 } /* end of BAapplyBias */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c
index 9552464e..80d24ca4 100644
--- a/src/bdd/cudd/cuddBddAbs.c
+++ b/src/bdd/cudd/cuddBddAbs.c
@@ -38,6 +38,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -687,3 +690,5 @@ bddCheckPositiveCube(
 
 } /* end of bddCheckPositiveCube */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c
index a532f31d..f3f017b0 100644
--- a/src/bdd/cudd/cuddBddCorr.c
+++ b/src/bdd/cudd/cuddBddCorr.c
@@ -33,6 +33,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -80,7 +83,7 @@ static    int    num_calls;
 static double bddCorrelationAux ARGS((DdManager *dd, DdNode *f, DdNode *g, st_table *table));
 static double bddCorrelationWeightsAux ARGS((DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table));
 static int CorrelCompare ARGS((const char *key1, const char *key2));
-static int CorrelHash ARGS((char *key, int modulus));
+static int CorrelHash ARGS((const char *key, int modulus));
 static enum st_retval CorrelCleanUp ARGS((char *key, char *value, char *arg));
 
 /**AutomaticEnd***************************************************************/
@@ -122,7 +125,7 @@ Cudd_bddCorrelation(
     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_foreach(table, (ST_PFSR)CorrelCleanUp, NIL(char));
     st_free_table(table);
     return(correlation);
 
@@ -165,7 +168,7 @@ Cudd_bddCorrelationWeights(
     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_foreach(table, (ST_PFSR)CorrelCleanUp, NIL(char));
     st_free_table(table);
     return(correlation);
 
@@ -434,13 +437,13 @@ CorrelCompare(
 ******************************************************************************/
 static int
 CorrelHash(
-  char * key,
+  const char * key,
   int  modulus)
 {
-    HashEntry *entry;
+    const HashEntry *entry;
     int val = 0;
 
-    entry = (HashEntry *) key;
+    entry = (const HashEntry *) key;
 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
     val = ((int) ((long)entry->f))*997 + ((int) ((long)entry->g));
 #else
@@ -479,3 +482,5 @@ CorrelCleanUp(
 
 } /* end of CorrelCleanUp */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 672d6344..92d1171b 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -47,6 +47,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -1252,3 +1255,5 @@ bddVarToCanonicalSimple(
 
 } /* end of bddVarToCanonicalSimple */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index ccc0893f..da0b4379 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -47,6 +47,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -411,7 +414,7 @@ cuddBddTransfer(
     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);
@@ -421,7 +424,7 @@ cuddBddTransfer(
     ** reordering. */
     gen = st_init_gen(table);
     if (gen == NULL) goto failure;
-    while (st_gen(gen, (char **) &key, (char **) &value)) {
+    while (st_gen(gen, (const char **) &key, (char **) &value)) {
     Cudd_RecursiveDeref(ddD, value);
     }
     st_free_gen(gen); gen = NULL;
@@ -979,3 +982,5 @@ cuddBddTransferRecur(
 
 } /* end of cuddBddTransferRecur */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddCache.c b/src/bdd/cudd/cuddCache.c
index e4aa0299..d66a8606 100644
--- a/src/bdd/cudd/cuddCache.c
+++ b/src/bdd/cudd/cuddCache.c
@@ -39,6 +39,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -865,7 +868,7 @@ cuddCacheResize(
     unsigned int slots, oldslots;
     double offset;
     int moved = 0;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 #ifndef DD_CACHE_PROFILE
     ptruint misalignment;
@@ -899,7 +902,7 @@ cuddCacheResize(
     table->acache = oldacache;
     /* Do not try to resize again. */
     table->maxCacheHard = oldslots - 1;
-    table->cacheSlack = - (oldslots + 1);
+    table->cacheSlack = - (int)(oldslots + 1);
     return;
     }
     /* If the size of the cache entry is a power of 2, we want to
@@ -1021,3 +1024,5 @@ cuddComputeFloorLog2(
 /*---------------------------------------------------------------------------*/
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddCheck.c b/src/bdd/cudd/cuddCheck.c
index aec8246d..92c0f5e1 100644
--- a/src/bdd/cudd/cuddCheck.c
+++ b/src/bdd/cudd/cuddCheck.c
@@ -37,6 +37,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -125,7 +128,7 @@ Cudd_DebugCheck(
     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. */
@@ -380,7 +383,7 @@ Cudd_DebugCheck(
     flag = 1;
     }
     gen = st_init_gen(edgeTable);
-    while (st_gen(gen,(char **)&f,(char **)&count)) {
+    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 = %d, ref = %d, then = 0x%lx, else = 0x%lx\n",(unsigned long)f,count,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f));
@@ -849,3 +852,5 @@ debugCheckParent(
     }
 }
 #endif
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c
index 4da296ef..23331339 100644
--- a/src/bdd/cudd/cuddClip.c
+++ b/src/bdd/cudd/cuddClip.c
@@ -36,6 +36,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -529,3 +532,5 @@ cuddBddClipAndAbsRecur(
 
 } /* end of cuddBddClipAndAbsRecur */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddCof.c b/src/bdd/cudd/cuddCof.c
index f79e3f91..26ff330d 100644
--- a/src/bdd/cudd/cuddCof.c
+++ b/src/bdd/cudd/cuddCof.c
@@ -32,6 +32,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -298,3 +301,5 @@ cuddCofactorRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index 43d65a5d..6fc4fa48 100644
--- a/src/bdd/cudd/cuddCompose.c
+++ b/src/bdd/cudd/cuddCompose.c
@@ -58,6 +58,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -1720,3 +1723,5 @@ ddIsIthAddVarPair(
        cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));
 
 } /* end of ddIsIthAddVarPair */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 871a99bb..95a00536 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -37,6 +37,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -130,7 +133,7 @@ static int cuddConjunctsAux ARGS((DdManager * dd, DdNode * f, DdNode ** c1, DdNo
 
   SideEffects [The factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the conjuncts are already
+  to free it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -229,7 +232,7 @@ Cudd_bddApproxConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the disjuncts are already
+  to free it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -268,7 +271,7 @@ Cudd_bddApproxDisjDecomp(
 
   SideEffects [The factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the conjuncts are already
+  to free it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -412,7 +415,7 @@ Cudd_bddIterConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the disjuncts are already
+  to free it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -452,7 +455,7 @@ Cudd_bddIterDisjDecomp(
 
   SideEffects [The two factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the conjuncts are already
+  to free it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -531,7 +534,7 @@ Cudd_bddGenConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the disjuncts are already
+  to free it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -571,7 +574,7 @@ Cudd_bddGenDisjDecomp(
 
   SideEffects [The two factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the conjuncts are already
+  to free it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -689,7 +692,7 @@ Cudd_bddVarConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to ABC_FREE it. On successful completion, the disjuncts are already
+  to free it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -1617,7 +1620,7 @@ ZeroCase(
     Cudd_RecursiveDeref(dd, g2);
     Cudd_RecursiveDeref(dd, h2);
     } else {
-    /* now ABC_FREE what was created and not used */
+    /* now free what was created and not used */
     if ((factors->g == g1) || (factors->g == h1)) {
         Cudd_RecursiveDeref(dd, g2);
         Cudd_RecursiveDeref(dd, h2);
@@ -1943,7 +1946,7 @@ BuildConjuncts(
     Cudd_RecursiveDeref(dd, g2);
     Cudd_RecursiveDeref(dd, h2);
     } else {
-    /* now ABC_FREE what was created and not used */
+    /* now free what was created and not used */
     if ((factors->g == g1) || (factors->g == h1)) {
         Cudd_RecursiveDeref(dd, g2);
         Cudd_RecursiveDeref(dd, h2);
@@ -1996,7 +1999,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 */
@@ -2023,7 +2026,7 @@ cuddConjunctsAux(
     cuddRef(*c1); cuddRef(*c2);
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
         ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2035,7 +2038,7 @@ cuddConjunctsAux(
     maxLocalRef = 0;
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
     nodeStat = (NodeStat *)value;
     maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
         nodeStat->localRef : maxLocalRef;
@@ -2045,7 +2048,7 @@ cuddConjunctsAux(
         
     /* Count minterms for each node. */
     max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
-    mintermTable = st_init_table(st_ptrcmp,st_ptrhash);
+    mintermTable = st_init_table(st_ptrcmp, st_ptrhash);;
     if (mintermTable == NULL) goto outOfMem;
     minterms = CountMinterms(f, max, mintermTable, dd->err);
     if (minterms == -1.0) goto outOfMem;
@@ -2061,10 +2064,10 @@ cuddConjunctsAux(
                  approxDistance, maxLocalRef, ghTable, mintermTable);
     if (factors == NULL) goto outOfMem;
 
-    /* ABC_FREE up tables */
+    /* Free up tables */
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
     ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2073,7 +2076,7 @@ cuddConjunctsAux(
     
     stGen = st_init_gen(mintermTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
     ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2107,7 +2110,7 @@ cuddConjunctsAux(
 
     stGen = st_init_gen(cacheTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
     ConjunctsFree(dd, (Conjuncts *)value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2120,7 +2123,7 @@ outOfMem:
     if (distanceTable != NULL) {
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
         ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2129,7 +2132,7 @@ outOfMem:
     if (mintermTable != NULL) {
     stGen = st_init_gen(mintermTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
         ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2139,7 +2142,7 @@ outOfMem:
     if (cacheTable != NULL) {
     stGen = st_init_gen(cacheTable);
     if (stGen == NULL) goto outOfMem;
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
         ConjunctsFree(dd, (Conjuncts *)value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -2149,3 +2152,5 @@ outOfMem:
     return(0);
 
 } /* end of cuddConjunctsAux */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddEssent.c b/src/bdd/cudd/cuddEssent.c
index db4b8b49..2d82019c 100644
--- a/src/bdd/cudd/cuddEssent.c
+++ b/src/bdd/cudd/cuddEssent.c
@@ -28,6 +28,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -277,3 +280,5 @@ ddFindEssentialRecur(
 
 } /* end of ddFindEssentialRecur */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c
index 9472dd8b..b9ed4676 100644
--- a/src/bdd/cudd/cuddExact.c
+++ b/src/bdd/cudd/cuddExact.c
@@ -43,6 +43,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1002,3 +1005,5 @@ checkSymmInfo(
 
 } /* end of checkSymmInfo */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c
index 18caeaa0..cccf2465 100644
--- a/src/bdd/cudd/cuddExport.c
+++ b/src/bdd/cudd/cuddExport.c
@@ -38,6 +38,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -136,7 +139,7 @@ Cudd_DumpBlif(
     scan = cuddT(scan);
     }
     Cudd_RecursiveDeref(dd,support);
-    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
+    support = NULL; /* so that we do not try to free it in case of failure */
 
     /* Write the header (.model .inputs .outputs). */
     if (mname == NULL) {
@@ -342,7 +345,7 @@ Cudd_DumpDot(
     scan = cuddT(scan);
     }
     Cudd_RecursiveDeref(dd,support);
-    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
+    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);
@@ -370,7 +373,7 @@ Cudd_DumpDot(
     diff = 0;
     gen = st_init_gen(visited);
     if (gen == NULL) goto failure;
-    while (st_gen(gen, (char **) &scan, NULL)) {
+    while (st_gen(gen, (const char **) &scan, NULL)) {
     diff |= refAddr ^ (long) scan;
     }
     st_free_gen(gen); gen = NULL;
@@ -621,7 +624,7 @@ Cudd_DumpDaVinci(
     refAddr = (long) Cudd_Regular(f[0]);
     diff = 0;
     gen = st_init_gen(visited);
-    while (st_gen(gen, (char **) &scan, NULL)) {
+    while (st_gen(gen, (const char **) &scan, NULL)) {
     diff |= refAddr ^ (long) scan;
     }
     st_free_gen(gen);
@@ -737,7 +740,7 @@ Cudd_DumpDDcal(
     refAddr = (long) Cudd_Regular(f[0]);
     diff = 0;
     gen = st_init_gen(visited);
-    while (st_gen(gen, (char **) &scan, NULL)) {
+    while (st_gen(gen, (const char **) &scan, NULL)) {
     diff |= refAddr ^ (long) scan;
     }
     st_free_gen(gen);
@@ -767,7 +770,7 @@ Cudd_DumpDDcal(
     scan = cuddT(scan);
     }
     Cudd_RecursiveDeref(dd,support);
-    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
+    support = NULL; /* so that we do not try to free it in case of failure */
     for (i = 0; i < nvars; i++) {
         if (sorted[dd->invperm[i]]) {
         if (inames == NULL || inames[dd->invperm[i]] == NULL) {
@@ -1287,3 +1290,5 @@ ddDoDumpFactoredForm(
 
 } /* end of ddDoDumpFactoredForm */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c
index 660526ee..93e15da0 100644
--- a/src/bdd/cudd/cuddGenCof.c
+++ b/src/bdd/cudd/cuddGenCof.c
@@ -49,6 +49,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -100,7 +103,7 @@ static int cuddBddConstrainDecomp ARGS((DdManager *dd, DdNode *f, DdNode **decom
 static DdNode * cuddBddCharToVect ARGS((DdManager *dd, DdNode *f, DdNode *x));
 static int cuddBddLICMarkEdges ARGS((DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache));
 static DdNode * cuddBddLICBuildResult ARGS((DdManager *dd, DdNode *f, st_table *cache, st_table *table));
-static int MarkCacheHash ARGS((char *ptr, int modulus));
+static int MarkCacheHash ARGS((const char *ptr, int modulus));
 static int MarkCacheCompare ARGS((const char *ptr1, const char *ptr2));
 static enum st_retval MarkCacheCleanUp ARGS((char *key, char *value, char *arg));
 static DdNode * cuddBddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u));
@@ -1237,7 +1240,7 @@ 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);
     }
@@ -1247,14 +1250,14 @@ cuddBddLICompaction(
     return(NULL);
     }
     if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
-    st_foreach(markcache, MarkCacheCleanUp, NULL);
+    st_foreach(markcache, (ST_PFSR)MarkCacheCleanUp, NULL);
     st_free_table(marktable);
     st_free_table(markcache);
     return(NULL);
     }
-    st_foreach(markcache, MarkCacheCleanUp, NULL);
+    st_foreach(markcache, (ST_PFSR)MarkCacheCleanUp, NULL);
     st_free_table(markcache);
-    buildcache = st_init_table(st_ptrcmp,st_ptrhash);
+    buildcache = st_init_table(st_ptrcmp, st_ptrhash);;
     if (buildcache == NULL) {
     st_free_table(marktable);
     return(NULL);
@@ -1662,13 +1665,13 @@ cuddBddLICBuildResult(
 ******************************************************************************/
 static int
 MarkCacheHash(
-  char * ptr,
+  const char * ptr,
   int  modulus)
 {
     int val = 0;
-    MarkCacheKey *entry;
+    const MarkCacheKey *entry;
 
-    entry = (MarkCacheKey *) ptr;
+    entry = (const MarkCacheKey *) ptr;
 
     val = (int) (ptrint) entry->f;
     val = val * 997 + (int) (ptrint) entry->c;
@@ -1966,3 +1969,5 @@ cuddBddSqueeze(
     return(Cudd_NotCond(r,comple));
 
 } /* end of cuddBddSqueeze */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddGenetic.c b/src/bdd/cudd/cuddGenetic.c
index 3b10aecb..d2739c85 100644
--- a/src/bdd/cudd/cuddGenetic.c
+++ b/src/bdd/cudd/cuddGenetic.c
@@ -56,6 +56,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -115,7 +118,7 @@ static int sift_up ARGS((DdManager *table, int x, int x_low));
 static int build_dd ARGS((DdManager *table, int num, int lower, int upper));
 static int largest ARGS(());
 static int rand_int ARGS((int a));
-static int array_hash ARGS((char *array, int modulus));
+static int array_hash ARGS((const char *array, int modulus));
 static int array_compare ARGS((const char *array1, const char *array2));
 static int find_best ARGS(());
 static double find_average_fitness ARGS(());
@@ -333,7 +336,7 @@ cuddGa(
         repeat[index]--;
         if (repeat[index] == 0) {
             int *pointer = &STOREDD(index,0);
-            result = st_delete(computed, (char **)&pointer,NULL);
+            result = st_delete(computed, (const char **)&pointer,NULL);
             if (!result) {
             ABC_FREE(storedd);
             ABC_FREE(repeat);
@@ -632,14 +635,14 @@ rand_int(
 ******************************************************************************/
 static int
 array_hash(
-  char * array,
+  const char * array,
   int  modulus)
 {
     int val = 0;
     int i;
-    int *intarray;
+    const int *intarray;
 
-    intarray = (int *) array;
+    intarray = (const int *) array;
 
     for (i = 0; i < numvars; i++) {
     val = val * 997 + intarray[i];
@@ -919,3 +922,5 @@ roulette(
 
 } /* end of roulette */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c
index 3d987400..e38eee72 100644
--- a/src/bdd/cudd/cuddGroup.c
+++ b/src/bdd/cudd/cuddGroup.c
@@ -52,6 +52,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -2059,7 +2062,7 @@ ddVarGroupCheck(
         ddIsVarHandled(table, yindex)) {
         if (Cudd_bddIsVarToBeGrouped(table, xindex) ||
         Cudd_bddIsVarToBeGrouped(table, yindex) ) {
-        if (table->keys - table->isolated <= originalSize) {
+        if (table->keys - table->isolated <= (unsigned)originalSize) {
             return(1);
         }
         }
@@ -2140,3 +2143,5 @@ ddIsVarHandled(
     return dd->subtables[dd->perm[index]].varHandled;
 
 } /* end of ddIsVarHandled */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddHarwell.c b/src/bdd/cudd/cuddHarwell.c
index 45ff736c..af552148 100644
--- a/src/bdd/cudd/cuddHarwell.c
+++ b/src/bdd/cudd/cuddHarwell.c
@@ -24,6 +24,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -539,3 +542,5 @@ Cudd_addHarwell(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddInit.c b/src/bdd/cudd/cuddInit.c
index 20a88b11..43b2ac29 100644
--- a/src/bdd/cudd/cuddInit.c
+++ b/src/bdd/cudd/cuddInit.c
@@ -32,6 +32,9 @@
 #include    "util_hack.h"
 #define CUDD_MAIN
 #include    "cuddInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
 #undef CUDD_MAIN
 
 /*---------------------------------------------------------------------------*/
@@ -105,7 +108,7 @@ Cudd_Init(
     DdNode *one, *zero;
     unsigned int maxCacheSize;
     unsigned int looseUpTo;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     if (maxMemory == 0) {
@@ -171,6 +174,7 @@ Cudd_Init(
 
     unique->memused += sizeof(DdNode *) * unique->maxSize;
 
+    unique->bReached = NULL;
     return(unique);
 
 } /* end of Cudd_Init */
@@ -281,3 +285,5 @@ cuddZddFreeUniv(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index df843e33..84146132 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -25,6 +25,7 @@
 #define _CUDDINT
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Nested includes                                                           */
 /*---------------------------------------------------------------------------*/
@@ -46,6 +47,9 @@
 #include "cudd.h"
 #include "st.h"
 
+ABC_NAMESPACE_HEADER_START
+
+
 #if defined(__GNUC__)
 # define DD_INLINE __inline__
 # if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
@@ -346,7 +350,7 @@ struct DdManager {    /* specialized DD symbol table */
     long *linear;        /* linear transform matrix */
     /* Memory Management */
     DdNode **memoryList;    /* memory manager for symbol table */
-    DdNode *nextFree;        /* list of ABC_FREE nodes */
+    DdNode *nextFree;        /* list of free nodes */
     char *stash;        /* memory reserve */
 #ifndef DD_NO_DEATH_ROW
     DdNode **deathRow;        /* queue for dereferencing */
@@ -410,7 +414,7 @@ struct DdManager {    /* specialized DD symbol table */
     double cacheLastInserts;    /* insertions at the last cache resizing */
     double cachedeletions;    /* number of deletions during garbage coll. */
 #ifdef DD_STATS
-    double nodesFreed;        /* number of nodes returned to the ABC_FREE list */
+    double nodesFreed;        /* number of nodes returned to the free list */
     double nodesDropped;    /* number of nodes killed by dereferencing */
 #endif
     unsigned int peakLiveNodes;    /* maximum number of live nodes */
@@ -435,6 +439,7 @@ struct DdManager {    /* specialized DD symbol table */
     int nvars;            /* variables used so far */
     int threshold;        /* for pseudo var threshold value*/
 #endif
+    DdNode * bReached;
 };
 
 typedef struct Move {
@@ -481,10 +486,10 @@ typedef struct DdLevelQueue {
 
 /**Macro***********************************************************************
 
-  Synopsis    [Adds node to the head of the ABC_FREE list.]
+  Synopsis    [Adds node to the head of the free list.]
 
-  Description [Adds node to the head of the ABC_FREE list.  Does not
-  deallocate memory chunks that become ABC_FREE.  This function is also
+  Description [Adds node to the head of the free list.  Does not
+  deallocate memory chunks that become free.  This function is also
   used by the dynamic reordering functions.]
 
   SideEffects [None]
@@ -1128,6 +1133,12 @@ EXTERN int cuddZddSymmSifting ARGS((DdManager *table, int lower, int upper));
 EXTERN int cuddZddSymmSiftingConv ARGS((DdManager *table, int lower, int upper));
 EXTERN int cuddZddP ARGS((DdManager *zdd, DdNode *f));
 
+EXTERN void (*MMoutOfMemory)(long);
+
 /**AutomaticEnd***************************************************************/
 
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif /* _CUDDINT */
diff --git a/src/bdd/cudd/cuddInteract.c b/src/bdd/cudd/cuddInteract.c
index 3745b408..3891e9d0 100644
--- a/src/bdd/cudd/cuddInteract.c
+++ b/src/bdd/cudd/cuddInteract.c
@@ -50,6 +50,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -400,3 +403,5 @@ ddClearGlobal(
 
 } /* end of ddClearGlobal */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c
index 97546cda..bf6af8bd 100644
--- a/src/bdd/cudd/cuddLCache.c
+++ b/src/bdd/cudd/cuddLCache.c
@@ -48,6 +48,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -658,7 +661,7 @@ cuddHashTableInsert(
   is an entry for the given key in the table; NULL otherwise. If the
   entry is present, its reference counter is decremented if not
   saturated. If the counter reaches 0, the value of the entry is
-  dereferenced, and the entry is returned to the ABC_FREE list.]
+  dereferenced, and the entry is returned to the free list.]
 
   SideEffects [None]
 
@@ -1071,7 +1074,7 @@ cuddLocalCacheResize(
     int i, shift;
     unsigned int posn;
     unsigned int slots, oldslots;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     olditem = cache->item;
@@ -1261,7 +1264,7 @@ cuddHashTableResize(
 #endif
     int shift;
     int oldNumBuckets = hash->numBuckets;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     /* Compute the new size of the table. */
@@ -1362,7 +1365,7 @@ cuddHashTableAlloc(
 {
     int i;
     unsigned int itemsize = hash->itemsize;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 #ifdef __osf__
 #pragma pointer_size save
@@ -1384,7 +1387,7 @@ cuddHashTableAlloc(
         hash->manager->stash = NULL;
         /* Inhibit resizing of tables. */
         hash->manager->maxCacheHard = hash->manager->cacheSlots - 1;
-        hash->manager->cacheSlack = -(hash->manager->cacheSlots + 1);
+        hash->manager->cacheSlack = -(int)(hash->manager->cacheSlots + 1);
         for (i = 0; i < hash->manager->size; i++) {
             hash->manager->subtables[i].maxKeys <<= 2;
         }
@@ -1426,3 +1429,5 @@ cuddHashTableAlloc(
     return(item);
 
 } /* end of cuddHashTableAlloc */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddLevelQ.c b/src/bdd/cudd/cuddLevelQ.c
index 28823a83..1a09820a 100644
--- a/src/bdd/cudd/cuddLevelQ.c
+++ b/src/bdd/cudd/cuddLevelQ.c
@@ -21,7 +21,7 @@
   pointers.  The level queue functions make sure that each node
   appears at most once in the queue. They do so by keeping a hash
   table where the node is used as key.  Queue items are recycled via a
-  ABC_FREE list for efficiency.
+  free list for efficiency.
   
   Internal procedures provided by this module:
                 <ul>
@@ -53,6 +53,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -125,7 +128,7 @@ static int hashResize ARGS((DdLevelQueue *queue));
   Description [Initializes a level queue. A level queue is a queue
   where inserts are based on the levels of the nodes. Within each
   level the policy is FIFO. Level queues are useful in traversing a
-  BDD top-down. Queue items are kept in a ABC_FREE list when dequeued for
+  BDD top-down. Queue items are kept in a free list when dequeued for
   efficiency. Returns a pointer to the new queue if successful; NULL
   otherwise.]
 
@@ -263,7 +266,7 @@ cuddLevelQueueEnqueue(
     item = hashLookup(queue,key);
     if (item != NULL) return(item);
 
-    /* Get a ABC_FREE item from either the ABC_FREE list or the memory manager. */
+    /* Get a free item from either the free list or the memory manager. */
     if (queue->freelist == NULL) {
     item = (DdQueueItem *) ABC_ALLOC(char, queue->itemsize);
     if (item == NULL)
@@ -335,7 +338,7 @@ cuddLevelQueueDequeue(
     queue->last[level] = NULL;
 
     queue->first = item->next;
-    /* Put item on the ABC_FREE list. */
+    /* Put item on the free list. */
     item->next = queue->freelist;
     queue->freelist = item;
     /* Update stats. */
@@ -493,7 +496,7 @@ hashResize(
 #endif
     int shift;
     int oldNumBuckets = queue->numBuckets;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     /* Compute the new size of the subtable. */
@@ -531,3 +534,5 @@ hashResize(
     return(1);
 
 } /* end of hashResize */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
index 30537e6c..9cb19e95 100644
--- a/src/bdd/cudd/cuddLinear.c
+++ b/src/bdd/cudd/cuddLinear.c
@@ -37,6 +37,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1331,3 +1334,5 @@ cuddXorLinear(
 
 } /* end of cuddXorLinear */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddLiteral.c b/src/bdd/cudd/cuddLiteral.c
index 43740690..c5684e9b 100644
--- a/src/bdd/cudd/cuddLiteral.c
+++ b/src/bdd/cudd/cuddLiteral.c
@@ -28,6 +28,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -235,3 +238,5 @@ cuddBddLiteralSetIntersectionRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c
index 75e5a732..b4ec5c6a 100644
--- a/src/bdd/cudd/cuddMatMult.c
+++ b/src/bdd/cudd/cuddMatMult.c
@@ -32,6 +32,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -678,3 +681,5 @@ cuddAddOuterSumRecur(
     return(R);
 
 } /* end of cuddAddOuterSumRecur */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c
index af07c7f0..f67fb88a 100644
--- a/src/bdd/cudd/cuddPriority.c
+++ b/src/bdd/cudd/cuddPriority.c
@@ -46,6 +46,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -1474,3 +1477,5 @@ createResult(
     return(res);
 
 } /* end of createResult */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddRead.c b/src/bdd/cudd/cuddRead.c
index 8e4ea60c..52670a6c 100644
--- a/src/bdd/cudd/cuddRead.c
+++ b/src/bdd/cudd/cuddRead.c
@@ -26,6 +26,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -488,3 +491,5 @@ Cudd_bddRead(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddRef.c b/src/bdd/cudd/cuddRef.c
index 7cb5d41b..a8f654af 100644
--- a/src/bdd/cudd/cuddRef.c
+++ b/src/bdd/cudd/cuddRef.c
@@ -41,6 +41,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -308,7 +311,7 @@ Cudd_DelayedDerefBdd(
 #if 0
     if (table->nextDead == table->deathRowDepth) {
     if (table->deathRowDepth < table->looseUpTo / 2) {
-        extern void (*MMoutOfMemory)(long);
+//        extern void (*MMoutOfMemory)(long);
         void (*saveHandler)(long) = MMoutOfMemory;
         DdNodePtr *newRow;
         MMoutOfMemory = Cudd_OutOfMem;
@@ -779,3 +782,5 @@ cuddTimesInDeathRow(
 /*---------------------------------------------------------------------------*/
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index 7c2fac39..93bbb10b 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -48,6 +48,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -378,10 +381,10 @@ cuddDynamicAllocNode(
     int     i;
     DdNodePtr *mem;
     DdNode *list, *node;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
-    if (table->nextFree == NULL) {        /* ABC_FREE list is empty */
+    if (table->nextFree == NULL) {        /* free list is empty */
     /* Try to allocate a new block. */
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
@@ -392,7 +395,7 @@ cuddDynamicAllocNode(
         table->stash = NULL;
         /* Inhibit resizing of tables. */
         table->maxCacheHard = table->cacheSlots - 1;
-        table->cacheSlack = -(table->cacheSlots + 1);
+        table->cacheSlack = -(int)(table->cacheSlots + 1);
         for (i = 0; i < table->size; i++) {
         table->subtables[i].maxKeys <<= 2;
         }
@@ -438,7 +441,7 @@ cuddDynamicAllocNode(
 
         table->nextFree = &list[0];
     }
-    } /* if ABC_FREE list empty */
+    } /* if free list empty */
 
     node = table->nextFree;
     table->nextFree = node->next;
@@ -742,7 +745,7 @@ cuddSwapInPlace(
     DdNodePtr *previousP;
     DdNode *tmp;
     DdNode *sentinel = &(table->sentinel);
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
 #if DD_DEBUG
@@ -2088,3 +2091,5 @@ ddCheckPermuation(
     }
     return(1);
 }
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c
index a1fb79f7..cb0534c3 100644
--- a/src/bdd/cudd/cuddSat.c
+++ b/src/bdd/cudd/cuddSat.c
@@ -45,6 +45,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -214,7 +217,7 @@ Cudd_ShortestPath(
     sol = getPath(manager,visited,f,weight,cost);
     } while (manager->reordered == 1);
 
-    st_foreach(visited, freePathPair, NULL);
+    st_foreach(visited, (ST_PFSR)freePathPair, NULL);
     st_free_table(visited);
 
     *length = cost;
@@ -284,7 +287,7 @@ Cudd_LargestCube(
     sol = getCube(manager,visited,f,cost);
     } while (manager->reordered == 1);
 
-    st_foreach(visited, freePathPair, NULL);
+    st_foreach(visited, (ST_PFSR)freePathPair, NULL);
     st_free_table(visited);
 
     *length = cost;
@@ -345,7 +348,7 @@ Cudd_ShortestLength(
     cost = my_pair->pos;
     }
 
-    st_foreach(visited, freePathPair, NULL);
+    st_foreach(visited, (ST_PFSR)freePathPair, NULL);
     st_free_table(visited);
 
     return(cost);
@@ -1303,3 +1306,5 @@ getCube(
     return(sol);
 
 } /* end of getCube */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSign.c b/src/bdd/cudd/cuddSign.c
index d58c1b43..b2b043a4 100644
--- a/src/bdd/cudd/cuddSign.c
+++ b/src/bdd/cudd/cuddSign.c
@@ -28,6 +28,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -149,7 +152,7 @@ Cudd_CofMinterm(
     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_foreach(table, (ST_PFSR)cuddStCountfree, NULL);
     st_free_table(table);
 #ifdef DD_STATS
     (void) fprintf(dd->out,"Number of calls: %d\tTable memory: %d bytes\n",
@@ -290,3 +293,5 @@ ddCofMintermAux(
 
 } /* end of ddCofMintermAux */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c
index a78055f3..18d29dac 100644
--- a/src/bdd/cudd/cuddSolve.c
+++ b/src/bdd/cudd/cuddSolve.c
@@ -31,6 +31,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -337,3 +340,5 @@ cuddVerifySol(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSplit.c b/src/bdd/cudd/cuddSplit.c
index 1f9a0425..bad35d60 100644
--- a/src/bdd/cudd/cuddSplit.c
+++ b/src/bdd/cudd/cuddSplit.c
@@ -35,6 +35,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -150,7 +153,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");
@@ -164,7 +167,7 @@ Cudd_SplitSet(
         */
         num = bddAnnotateMintermCount(manager,S,max,mtable);
         if (m == num) {
-        st_foreach(mtable,cuddStCountfree,NIL(char));
+        st_foreach(mtable,(ST_PFSR)cuddStCountfree,NIL(char));
         st_free_table(mtable);
         ABC_FREE(varSeen);
         return(S);
@@ -173,7 +176,7 @@ Cudd_SplitSet(
         result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0);
         if (result)
         cuddRef(result);
-        st_foreach(mtable,cuddStCountfree,NULL);
+        st_foreach(mtable,(ST_PFSR)cuddStCountfree,NULL);
         st_free_table(mtable);
         ABC_FREE(varSeen);
     }
@@ -655,3 +658,5 @@ bddAnnotateMintermCount(
     return(min_N);
 
 } /* end of bddAnnotateMintermCount */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSubsetHB.c b/src/bdd/cudd/cuddSubsetHB.c
index 59f8e6d2..86ed380f 100644
--- a/src/bdd/cudd/cuddSubsetHB.c
+++ b/src/bdd/cudd/cuddSubsetHB.c
@@ -49,6 +49,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -367,7 +370,7 @@ cuddSubsetHeavyBranch(
     st_free_table(approxTable);
     return(NULL);
     }
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
     Cudd_RecursiveDeref(dd, (DdNode *)value);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -378,7 +381,7 @@ cuddSubsetHeavyBranch(
     st_free_table(storeTable);
     return(NULL);
     }
-    while(st_gen(stGen, (char **)&key, (char **)&value)) {
+    while(st_gen(stGen, (const char **)&key, (char **)&value)) {
     Cudd_RecursiveDeref(dd, (DdNode *)key);
     }
     st_free_gen(stGen); stGen = NULL;
@@ -777,7 +780,7 @@ 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);
@@ -1309,3 +1312,5 @@ BuildSubsetBdd(
     }
 } /* end of BuildSubsetBdd */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index 25c22b88..d336187b 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -44,6 +44,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -410,7 +413,7 @@ cuddSubsetShortPaths(
         st_free_table(subsetNodeTable);
     }
     st_free_table(info->maxpathTable);
-    st_foreach(pathTable, stPathTableDdFree, (char *)dd);
+    st_foreach(pathTable, (ST_PFSR)stPathTableDdFree, (char *)dd);
 
     ABC_FREE(info);
 
@@ -996,7 +999,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;
@@ -1101,7 +1104,7 @@ CreatePathTable(
      */
     if (!CreateBotDist(node, pathTable, pathLengthArray, fp)) return(NULL);
 
-    /* ABC_FREE BFS queue pages as no longer required */
+    /* free BFS queue pages as no longer required */
     for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
     ABC_FREE(queuePages);
     return(pathTable);
@@ -1595,7 +1598,7 @@ BuildSubsetBdd(
 
 /**Function********************************************************************
 
-  Synopsis     [Procedure to ABC_FREE te result dds stored in the NodeDist pages.]
+  Synopsis     [Procedure to free the result dds stored in the NodeDist pages.]
 
   Description [None]
 
@@ -1624,3 +1627,5 @@ stPathTableDdFree(
     return(ST_CONTINUE);
 
 } /* end of stPathTableFree */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index a608a21f..88e607e5 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -41,6 +41,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1666,3 +1669,5 @@ ddSymmSummary(
     return;
 
 } /* end of ddSymmSummary */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c
index 3c76c1af..6ec6f6e7 100644
--- a/src/bdd/cudd/cuddTable.c
+++ b/src/bdd/cudd/cuddTable.c
@@ -57,6 +57,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -202,10 +205,10 @@ cuddAllocNode(
     int i;
     DdNodePtr *mem;
     DdNode *list, *node;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
-    if (unique->nextFree == NULL) {    /* ABC_FREE list is empty */
+    if (unique->nextFree == NULL) {    /* free list is empty */
     /* Check for exceeded limits. */
     if ((unique->keys - unique->dead) + (unique->keysZ - unique->deadZ) >
         unique->maxLive) {
@@ -699,7 +702,7 @@ cuddGarbageCollect(
     cuddLocalCacheClearDead(unique);
     }
 
-    /* Now return dead nodes to ABC_FREE list. Count them for sanity check. */
+    /* Now return dead nodes to free list. Count them for sanity check. */
     totalDeleted = 0;
 #ifndef DD_UNSORTED_FREE_LIST
     tree = NULL;
@@ -905,7 +908,7 @@ cuddGarbageCollectZdd(
     }
     }
 
-    /* Now return dead nodes to ABC_FREE list. Count them for sanity check. */
+    /* Now return dead nodes to free list. Count them for sanity check. */
     totalDeleted = 0;
 #ifndef DD_UNSORTED_FREE_LIST
     tree = NULL;
@@ -1501,7 +1504,7 @@ cuddRehash(
     DdNode *node, *next;
     DdNode *sentinel = &(unique->sentinel);
     hack split;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     if (unique->gcFrac == DD_GC_FRAC_HI && unique->slots > unique->looseUpTo) {
@@ -1673,7 +1676,7 @@ cuddShrinkSubtable(
     DdNode *node, *next;
     DdNode *sentinel = &(unique->sentinel);
     unsigned int slots, oldslots;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     oldnodelist = unique->subtables[i].nodelist;
@@ -1820,7 +1823,7 @@ cuddInsertSubtables(
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
-        for (j = 0; j < numSlots; j++) {
+        for (j = 0; j < (int)numSlots; j++) {
         newnodelist[j] = sentinel;
         }
     }
@@ -1925,7 +1928,7 @@ cuddInsertSubtables(
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
-        for (j = 0; j < numSlots; j++) {
+        for (j = 0; j < (int)numSlots; j++) {
         newnodelist[j] = sentinel;
         }
     }
@@ -1960,7 +1963,7 @@ cuddInsertSubtables(
         ABC_FREE(unique->map);
         unique->map = newmap;
     }
-    /* Install the new tables and ABC_FREE the old ones. */
+    /* Install the new tables and free the old ones. */
     ABC_FREE(unique->subtables);
     unique->subtables = newsubtables;
     unique->maxSize = newsize;
@@ -2233,7 +2236,7 @@ cuddResizeTableZdd(
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
-        for (j = 0; j < numSlots; j++) {
+        for (j = 0; j < (int)numSlots; j++) {
         newnodelist[j] = NULL;
         }
     }
@@ -2301,7 +2304,7 @@ cuddResizeTableZdd(
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
-        for (j = 0; j < numSlots; j++) {
+        for (j = 0; j < (int)numSlots; j++) {
         newnodelist[j] = NULL;
         }
     }
@@ -2356,7 +2359,7 @@ cuddSlowTableGrowth(
     int i;
 
     unique->maxCacheHard = unique->cacheSlots - 1;
-    unique->cacheSlack = -(unique->cacheSlots + 1);
+    unique->cacheSlack = -(int)(unique->cacheSlots + 1);
     for (i = 0; i < unique->size; i++) {
     unique->subtables[i].maxKeys <<= 2;
     }
@@ -2396,7 +2399,7 @@ ddRehashZdd(
     int j, pos;
     DdNodePtr *nodelist, *oldnodelist;
     DdNode *node, *next;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
     if (unique->slots > unique->looseUpTo) {
@@ -3141,3 +3144,5 @@ See the CUDD Programmer's Guide for additional details.");
     abort();
 
 } /* end of ddReportRefMess */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c
index 7e0eb22a..cbaafb5a 100644
--- a/src/bdd/cudd/cuddUtil.c
+++ b/src/bdd/cudd/cuddUtil.c
@@ -79,6 +79,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -444,7 +447,7 @@ Cudd_EstimateCofactor(
     DdNode *ptr;
     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));
@@ -586,12 +589,12 @@ Cudd_CountPath(
     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_foreach(table, (ST_PFSR)cuddStCountfree, NULL);
     st_free_table(table);
     return(i);
 
@@ -633,7 +636,7 @@ Cudd_EpdCountMinterm(
     return(CUDD_OUT_OF_MEM);
     }
     status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
-    st_foreach(table, ddEpdFree, NULL);
+    st_foreach(table, (ST_PFSR)ddEpdFree, NULL);
     st_free_table(table);
     if (status == CUDD_OUT_OF_MEM) {
     EpdMakeZero(epd, 0);
@@ -670,12 +673,12 @@ Cudd_CountPathsToNonZero(
     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_foreach(table, (ST_PFSR)cuddStCountfree, NULL);
     st_free_table(table);
     return(i);
 
@@ -2187,7 +2190,7 @@ Cudd_FirstNode(
     gen->stack.stack = NULL;
     gen->node = NULL;
 
-    gen->gen.nodes.visited = st_init_table(st_ptrcmp,st_ptrhash);
+    gen->gen.nodes.visited = st_init_table(st_ptrcmp, st_ptrhash);;
     if (gen->gen.nodes.visited == NULL) {
     ABC_FREE(gen);
     return(NULL);
@@ -2210,7 +2213,7 @@ Cudd_FirstNode(
     }
 
     /* Find the first node. */
-    retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
+    retval = st_gen(gen->gen.nodes.stGen, (const char **) &(gen->node), NULL);
     if (retval != 0) {
     gen->status = CUDD_GEN_NONEMPTY;
     *node = gen->node;
@@ -2242,7 +2245,7 @@ Cudd_NextNode(
     int retval;
 
     /* Find the next node. */
-    retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
+    retval = st_gen(gen->gen.nodes.stGen, (const char **) &(gen->node), NULL);
     if (retval == 0) {
     gen->status = CUDD_GEN_EMPTY;
     } else {
@@ -2647,7 +2650,7 @@ 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);
 
@@ -3632,3 +3635,5 @@ ddEpdFree(
     return(ST_CONTINUE);
 
 } /* end of ddEpdFree */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddWindow.c b/src/bdd/cudd/cuddWindow.c
index b97e3358..62c92ff2 100644
--- a/src/bdd/cudd/cuddWindow.c
+++ b/src/bdd/cudd/cuddWindow.c
@@ -34,6 +34,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -995,3 +998,5 @@ ddWindowConv4(
 
 } /* end of ddWindowConv4 */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddCount.c b/src/bdd/cudd/cuddZddCount.c
index bc8a1ee4..8f974e5e 100644
--- a/src/bdd/cudd/cuddZddCount.c
+++ b/src/bdd/cudd/cuddZddCount.c
@@ -37,6 +37,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -113,7 +116,7 @@ Cudd_zddCount(
     if (res == CUDD_OUT_OF_MEM) {
     zdd->errorCode = CUDD_MEMORY_OUT;
     }
-    st_foreach(table, st_zdd_countfree, NIL(char));
+    st_foreach(table, (ST_PFSR)st_zdd_countfree, NIL(char));
     st_free_table(table);
 
     return(res);
@@ -152,7 +155,7 @@ Cudd_zddCountDouble(
     if (res == (double)CUDD_OUT_OF_MEM) {
     zdd->errorCode = CUDD_MEMORY_OUT;
     }
-    st_foreach(table, st_zdd_count_dbl_free, NIL(char));
+    st_foreach(table, (ST_PFSR)st_zdd_count_dbl_free, NIL(char));
     st_free_table(table);
 
     return(res);
@@ -322,3 +325,5 @@ st_zdd_count_dbl_free(
     return(ST_CONTINUE);
 
 } /* end of st_zdd_count_dbl_free */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddFuncs.c b/src/bdd/cudd/cuddZddFuncs.c
index 9dc27a95..2560159c 100644
--- a/src/bdd/cudd/cuddZddFuncs.c
+++ b/src/bdd/cudd/cuddZddFuncs.c
@@ -51,6 +51,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1601,3 +1604,5 @@ cuddZddGetNegVarLevel(
     int    nv = cuddZddGetNegVarIndex(dd, index);
     return(dd->permZ[nv]);
 } /* end of cuddZddGetNegVarLevel */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c
index 8845dc49..0bf611e5 100644
--- a/src/bdd/cudd/cuddZddGroup.c
+++ b/src/bdd/cudd/cuddZddGroup.c
@@ -43,6 +43,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1315,3 +1318,5 @@ zddMergeGroups(
 
 } /* end of zddMergeGroups */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddIsop.c b/src/bdd/cudd/cuddZddIsop.c
index f4b057ea..cd7c16bf 100644
--- a/src/bdd/cudd/cuddZddIsop.c
+++ b/src/bdd/cudd/cuddZddIsop.c
@@ -37,6 +37,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -883,3 +886,5 @@ cuddMakeBddFromZddCover(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddLin.c b/src/bdd/cudd/cuddZddLin.c
index 4d4135d1..14cad0b1 100644
--- a/src/bdd/cudd/cuddZddLin.c
+++ b/src/bdd/cudd/cuddZddLin.c
@@ -35,6 +35,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -937,3 +940,5 @@ cuddZddUndoMovesOutOfMem:
 
 } /* end of cuddZddUndoMoves */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddMisc.c b/src/bdd/cudd/cuddZddMisc.c
index 6a4ddd09..b78faea1 100644
--- a/src/bdd/cudd/cuddZddMisc.c
+++ b/src/bdd/cudd/cuddZddMisc.c
@@ -36,6 +36,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -250,3 +253,5 @@ cuddZddDagInt(
 
 } /* cuddZddDagInt */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddPort.c b/src/bdd/cudd/cuddZddPort.c
index 6d4a3236..dfefece1 100644
--- a/src/bdd/cudd/cuddZddPort.c
+++ b/src/bdd/cudd/cuddZddPort.c
@@ -35,6 +35,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -352,3 +355,5 @@ zddPortToBddStep(
 
 } /* end of zddPortToBddStep */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c
index 4c6e394b..1d73721c 100644
--- a/src/bdd/cudd/cuddZddReord.c
+++ b/src/bdd/cudd/cuddZddReord.c
@@ -49,6 +49,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1413,7 +1416,7 @@ zddReorderPostprocess(
     DdNodePtr *nodelist, *oldnodelist;
     DdNode *node, *next;
     unsigned int slots, oldslots;
-    extern void (*MMoutOfMemory)(long);
+//    extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
 #ifdef DD_VERBOSE
@@ -1632,3 +1635,5 @@ zddFixTree(
 
 } /* end of zddFixTree */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddSetop.c b/src/bdd/cudd/cuddZddSetop.c
index f1bd72f3..566c610b 100644
--- a/src/bdd/cudd/cuddZddSetop.c
+++ b/src/bdd/cudd/cuddZddSetop.c
@@ -49,6 +49,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1135,3 +1138,5 @@ zddVarToConst(
 
 } /* end of zddVarToConst */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c
index c752c394..644673cd 100644
--- a/src/bdd/cudd/cuddZddSymm.c
+++ b/src/bdd/cudd/cuddZddSymm.c
@@ -43,6 +43,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -1675,3 +1678,5 @@ cuddZddSymmSummary(
 
 } /* end of cuddZddSymmSummary */
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c
index efa73d15..72ee639a 100644
--- a/src/bdd/cudd/cuddZddUtil.c
+++ b/src/bdd/cudd/cuddZddUtil.c
@@ -38,6 +38,9 @@
 #include    "util_hack.h"
 #include    "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -551,7 +554,7 @@ Cudd_zddDumpDot(
     }
     Cudd_RecursiveDeref(dd,support);
     }
-    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
+    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);
@@ -578,7 +581,7 @@ Cudd_zddDumpDot(
     refAddr = (long) f[0];
     diff = 0;
     gen = st_init_gen(visited);
-    while (st_gen(gen, (char **) &scan, NULL)) {
+    while (st_gen(gen, (const char **) &scan, NULL)) {
     diff |= refAddr ^ (long) scan;
     }
     st_free_gen(gen);
@@ -1019,3 +1022,5 @@ zddPrintCoverAux(
     return;
 
 } /* end of zddPrintCoverAux */
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/testcudd.c b/src/bdd/cudd/testcudd.c
index d8affadc..1b6de5aa 100644
--- a/src/bdd/cudd/testcudd.c
+++ b/src/bdd/cudd/testcudd.c
@@ -26,6 +26,9 @@
 #include "util_hack.h"
 #include "cuddInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -986,3 +989,5 @@ testHamming(
     return(1);
 
 } /* end of testHamming */
+ABC_NAMESPACE_IMPL_END
+
author	Alan Mishchenko <alanmi@berkeley.edu>	2010-11-01 01:35:04 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2010-11-01 01:35:04 -0700
commit	6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch)
tree	0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/bdd/cudd
parent	f0e77f6797c0504b0da25a56152b707d3357f386 (diff)
download	abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2 abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip