Major restructuring of the code.

84 files changed, 4333 insertions, 491 deletions

diff --git a/src/misc/avl/avl.h b/src/misc/avl/avl.h
index 50a06b69..141e4f56 100644
--- a/src/misc/avl/avl.h
+++ b/src/misc/avl/avl.h
@@ -7,8 +7,8 @@
  * $Date: 1994/07/15 23:00:40 $
  *
  */
-#ifndef AVL_INCLUDED
-#define AVL_INCLUDED
+#ifndef ABC__misc__avl__avl_h
+#define ABC__misc__avl__avl_h
 
 
 ABC_NAMESPACE_HEADER_START
diff --git a/src/misc/bar/bar.c b/src/misc/bar/bar.c
new file mode 100644
index 00000000..565a969e
--- /dev/null
+++ b/src/misc/bar/bar.c
@@ -0,0 +1,187 @@
+/**CFile****************************************************************
+
+  FileName    [bar.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Progress bar.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bar.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include "src/misc/util/abc_global.h"
+#include "src/base/main/main.h"
+#include "bar.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Bar_Progress_t_
+{
+    int              nItemsNext;   // the number of items for the next update of the progress bar
+    int              nItemsTotal;  // the total number of items
+    int              posTotal;     // the total number of positions
+    int              posCur;       // the current position
+    FILE *           pFile;        // the output stream 
+};
+
+static void Bar_ProgressShow( Bar_Progress_t * p, char * pString );
+static void Bar_ProgressClean( Bar_Progress_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the progress bar.]
+
+  Description [The first parameter is the output stream (pFile), where
+  the progress is printed. The current printing position should be the
+  first one on the given line. The second parameters is the total
+  number of items that correspond to 100% position of the progress bar.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal )
+{
+    Bar_Progress_t * p;
+    Abc_Frame_t * pFrame;
+    pFrame = Abc_FrameReadGlobalFrame();
+    if ( pFrame == NULL )
+        return NULL;
+    if ( !Abc_FrameShowProgress(pFrame) ) return NULL;
+    p = ABC_ALLOC( Bar_Progress_t, 1 );
+    memset( p, 0, sizeof(Bar_Progress_t) );
+    p->pFile       = pFile;
+    p->nItemsTotal = nItemsTotal;
+    p->posTotal    = 78;
+    p->posCur      = 1;
+    p->nItemsNext  = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
+    Bar_ProgressShow( p, NULL );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the progress bar.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString )
+{
+    if ( p == NULL ) return;
+    if ( nItemsCur < p->nItemsNext )
+        return;
+    if ( nItemsCur >= p->nItemsTotal )
+    {
+        p->posCur = 78;
+        p->nItemsNext = 0x7FFFFFFF;
+    }
+    else
+    {
+        p->posCur += 7;
+        p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
+    }
+    Bar_ProgressShow( p, pString );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the progress bar.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bar_ProgressStop( Bar_Progress_t * p )
+{
+    if ( p == NULL ) return;
+    Bar_ProgressClean( p );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the progress bar of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
+{
+    int i;
+    if ( p == NULL ) return;
+    if ( pString )
+        fprintf( p->pFile, "%s ", pString );
+    for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
+        fprintf( p->pFile, "-" );
+    if ( i == p->posCur )
+        fprintf( p->pFile, ">" );
+    for ( i++  ; i <= p->posTotal; i++ )
+        fprintf( p->pFile, " " );
+    fprintf( p->pFile, "\r" );
+    fflush( stdout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the progress bar before quitting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bar_ProgressClean( Bar_Progress_t * p )
+{
+    int i;
+    if ( p == NULL ) return;
+    for ( i = 0; i <= p->posTotal; i++ )
+        fprintf( p->pFile, " " );
+    fprintf( p->pFile, "\r" );
+    fflush( stdout );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/bar/bar.h b/src/misc/bar/bar.h
new file mode 100644
index 00000000..c66e302e
--- /dev/null
+++ b/src/misc/bar/bar.h
@@ -0,0 +1,78 @@
+/**CFile****************************************************************
+
+  FileName    [bar.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Progress bar.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bar.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__bar__bar_h
+#define ABC__aig__bar__bar_h
+
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+#define BAR_PROGRESS_USE   1
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+typedef struct Bar_Progress_t_ Bar_Progress_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bar.c ==========================================================*/
+extern Bar_Progress_t *  Bar_ProgressStart( FILE * pFile, int nItemsTotal );
+extern void              Bar_ProgressStop( Bar_Progress_t * p );
+extern void              Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString );
+
+static inline void       Bar_ProgressUpdate( Bar_Progress_t * p, int nItemsCur, char * pString ) {  
+    if ( BAR_PROGRESS_USE && p && (nItemsCur < *((int*)p)) ) return; Bar_ProgressUpdate_int(p, nItemsCur, pString); }
+
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/misc/bar/module.make b/src/misc/bar/module.make
new file mode 100644
index 00000000..7234e386
--- /dev/null
+++ b/src/misc/bar/module.make
@@ -0,0 +1 @@
+SRC +=    src/misc/bar/bar.c 
diff --git a/src/misc/bbl/bblif.c b/src/misc/bbl/bblif.c
new file mode 100644
index 00000000..fc227760
--- /dev/null
+++ b/src/misc/bbl/bblif.c
@@ -0,0 +1,1518 @@
+/**CFile****************************************************************
+
+  FileName    [bblif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Binary BLIF representation for logic networks.]
+
+  Synopsis    [Main implementation module.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 28, 2009.]
+
+  Revision    [$Id: bblif.c,v 1.00 2009/02/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "src/misc/util/abc_global.h"
+#include "bblif.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// vector of integers
+typedef struct Vec_Int_t_ Vec_Int_t;
+struct Vec_Int_t_ 
+{
+    int         nCap;
+    int         nSize;
+    int *       pArray;
+};
+
+// vector of characters
+typedef struct Vec_Str_t_ Vec_Str_t;
+struct Vec_Str_t_ 
+{
+    int         nCap;
+    int         nSize;
+    char *      pArray;
+};
+
+// network object
+struct Bbl_Obj_t_
+{
+    int         Id;              // user ID
+    int         Fnc;             // functionality
+    unsigned    fCi     :  1;    // combinational input
+    unsigned    fCo     :  1;    // combinational output
+    unsigned    fBox    :  1;    // subcircuit
+    unsigned    fMark   :  1;    // temporary mark
+    unsigned    nFanins : 28;    // fanin number
+    int         pFanins[0];      // fanin array
+};
+
+// object function
+typedef struct Bbl_Fnc_t_ Bbl_Fnc_t;
+struct Bbl_Fnc_t_
+{
+    int         nWords;          // word number
+    int         pWords[0];       // word array
+};
+
+// object function
+typedef struct Bbl_Ent_t_ Bbl_Ent_t;
+struct Bbl_Ent_t_
+{
+    int         iFunc;           // function handle
+    int         iNext;           // next entry handle
+};
+
+// data manager
+struct Bbl_Man_t_
+{
+    // data pool
+    Vec_Str_t * pName;           // design name
+    Vec_Str_t * pObjs;           // vector of objects
+    Vec_Str_t * pFncs;           // vector of functions
+    // construction
+    Vec_Int_t * vId2Obj;         // mapping user IDs into objects
+    Vec_Int_t * vObj2Id;         // mapping objects into user IDs
+    Vec_Int_t * vFaninNums;      // mapping user IDs into fanin number
+    // file contents
+    int         nFileSize;       // file size
+    char *      pFileData;       // file contents
+    // other data
+    Vec_Str_t * pEnts;           // vector of entries
+    int         SopMap[17][17];  // mapping vars x cubes into entry handles
+};
+
+static inline int         Bbl_ObjIsCi( Bbl_Obj_t * pObj )          { return pObj->fCi;                                        } 
+static inline int         Bbl_ObjIsCo( Bbl_Obj_t * pObj )          { return pObj->fCo;                                        } 
+static inline int         Bbl_ObjIsNode( Bbl_Obj_t * pObj )        { return!pObj->fCi && !pObj->fCo;                          } 
+
+static inline int         Bbl_ObjFaninNum( Bbl_Obj_t * pObj )      { return pObj->nFanins;                                    } 
+static inline Bbl_Obj_t * Bbl_ObjFanin( Bbl_Obj_t * pObj, int i )  { return (Bbl_Obj_t *)(((char *)pObj) - pObj->pFanins[i]); } 
+
+static inline int         Bbl_ObjSize( Bbl_Obj_t * pObj )          { return sizeof(Bbl_Obj_t) + sizeof(int) * pObj->nFanins;  } 
+static inline int         Bbl_FncSize( Bbl_Fnc_t * pFnc )          { return sizeof(Bbl_Fnc_t) + sizeof(int) * pFnc->nWords;   } 
+
+static inline Bbl_Obj_t * Bbl_VecObj( Vec_Str_t * p, int h )       { return (Bbl_Obj_t *)(p->pArray + h);                     } 
+static inline Bbl_Fnc_t * Bbl_VecFnc( Vec_Str_t * p, int h )       { return (Bbl_Fnc_t *)(p->pArray + h);                     } 
+static inline Bbl_Ent_t * Bbl_VecEnt( Vec_Str_t * p, int h )       { return (Bbl_Ent_t *)(p->pArray + h);                     } 
+
+static inline char *      Bbl_ManSop( Bbl_Man_t * p, int h )       { return (char *)Bbl_VecFnc(p->pFncs, h)->pWords;          } 
+static inline Bbl_Obj_t * Bbl_ManObj( Bbl_Man_t * p, int Id )      { return Bbl_VecObj(p->pObjs, p->vId2Obj->pArray[Id]);     } 
+
+#define Bbl_ManForEachObj_int( p, pObj, h )                \
+    for ( h = 0; (h < p->nSize) && (pObj = Bbl_VecObj(p,h)); h += Bbl_ObjSize(pObj) )
+#define Bbl_ManForEachFnc_int( p, pObj, h )                \
+    for ( h = 0; (h < p->nSize) && (pObj = Bbl_VecFnc(p,h)); h += Bbl_FncSize(pObj) )
+#define Bbl_ObjForEachFanin_int( pObj, pFanin, i )         \
+    for ( i = 0; (i < (int)pObj->nFanins) && (pFanin = Bbl_ObjFanin(pObj,i)); i++ )
+
+#define BBLIF_ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
+#define BBLIF_CALLOC(type, num)     ((type *) calloc((num), sizeof(type)))
+#define BBLIF_FALLOC(type, num)     ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
+#define BBLIF_FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#define BBLIF_REALLOC(type, obj, num)    \
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+         ((type *) malloc(sizeof(type) * (num))))
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntAlloc( int nCap )
+{
+    Vec_Int_t * p;
+    p = BBLIF_ALLOC( Vec_Int_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? BBLIF_ALLOC( int, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given size and cleans it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntStart( int nSize )
+{
+    Vec_Int_t * p;
+    p = Vec_IntAlloc( nSize );
+    p->nSize = nSize;
+    memset( p->pArray, 0, sizeof(int) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given size and cleans it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntStartNatural( int nSize )
+{
+    Vec_Int_t * p;
+    int i;
+    p = Vec_IntAlloc( nSize );
+    p->nSize = nSize;
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = i;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
+{
+    Vec_Int_t * p;
+    p = BBLIF_ALLOC( Vec_Int_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFree( Vec_Int_t * p )
+{
+    BBLIF_FREE( p->pArray );
+    BBLIF_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSize( Vec_Int_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntEntry( Vec_Int_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] += Addition;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntEntryLast( Vec_Int_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = BBLIF_REALLOC( int, p->pArray, nCapMin ); 
+    assert( p->pArray );
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Fill )
+{
+    int i;
+    Vec_IntGrow( p, nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Fill;
+    p->nSize = nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Fill )
+{
+    int i;
+    if ( p->nSize >= nSize )
+        return;
+    if ( nSize > 2 * p->nCap )
+        Vec_IntGrow( p, nSize );
+    else if ( nSize > p->nCap )
+        Vec_IntGrow( p, 2 * p->nCap );
+    for ( i = p->nSize; i < nSize; i++ )
+        p->pArray[i] = Fill;
+    p->nSize = nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the entry even if the place not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntGetEntry( Vec_Int_t * p, int i )
+{
+    Vec_IntFillExtra( p, i + 1, 0 );
+    return Vec_IntEntry( p, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the entry even if the place does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSetEntry( Vec_Int_t * p, int i, int Entry )
+{
+    Vec_IntFillExtra( p, i + 1, 0 );
+    Vec_IntWriteEntry( p, i, Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntClear( Vec_Int_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAlloc( int nCap )
+{
+    Vec_Str_t * p;
+    p = BBLIF_ALLOC( Vec_Str_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? BBLIF_ALLOC( char, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
+{
+    Vec_Str_t * p;
+    p = BBLIF_ALLOC( Vec_Str_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns a piece of memory.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Vec_StrFetch( Vec_Str_t * p, int nBytes )
+{
+    while ( p->nSize + nBytes > p->nCap )
+    {
+        p->pArray = BBLIF_REALLOC( char, p->pArray, 3 * p->nCap );
+        p->nCap *= 3;
+    }
+    p->nSize += nBytes;
+    return p->pArray + p->nSize - nBytes;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Write vector into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Vec_StrWrite( FILE * pFile, Vec_Str_t * p )
+{
+    fwrite( &p->nSize, sizeof(int), 1, pFile );
+    fwrite( p->pArray, sizeof(char), p->nSize, pFile );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Write vector into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Vec_StrRead( char ** ppStr )
+{
+    Vec_Str_t * p;
+    char * pStr = *ppStr;
+    p = Vec_StrAlloc( 0 );
+    p->nSize = *(int *)pStr;
+    p->pArray = pStr + sizeof(int);
+    *ppStr = pStr + sizeof(int) + p->nSize * sizeof(char);
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSize( Vec_Str_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrFree( Vec_Str_t * p )
+{
+    BBLIF_FREE( p->pArray );
+    BBLIF_FREE( p );
+}
+
+
+
+
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbl_ManFileSize( char * pFileName )
+{
+    FILE * pFile;
+    int nFileSize;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Bbl_ManFileSize(): The file is unavailable (absent or open).\n" );
+        return 0;
+    }
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile ); 
+    fclose( pFile );
+    return nFileSize;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Read data from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Bbl_ManFileRead( char * pFileName )
+{
+    FILE * pFile;
+    char * pContents;
+    int nFileSize;
+    nFileSize = Bbl_ManFileSize( pFileName );
+    pFile = fopen( pFileName, "rb" );
+    pContents = BBLIF_ALLOC( char, nFileSize );
+    fread( pContents, nFileSize, 1, pFile );
+    fclose( pFile );
+    return pContents;
+}
+
+
+
+/**Fnction*************************************************************
+
+  Synopsis    [Writes data into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManDumpBinaryBlif( Bbl_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    pFile = fopen( pFileName, "wb" );
+    Vec_StrWrite( pFile, p->pName );
+    Vec_StrWrite( pFile, p->pObjs );
+    Vec_StrWrite( pFile, p->pFncs );
+    fclose( pFile );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Creates manager after reading.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbl_Man_t * Bbl_ManReadBinaryBlif( char * pFileName )
+{
+    Bbl_Man_t * p;
+    Bbl_Obj_t * pObj;
+    char * pBuffer;
+    int h;
+    p = BBLIF_ALLOC( Bbl_Man_t, 1 );
+    memset( p, 0, sizeof(Bbl_Man_t) );
+    p->nFileSize = Bbl_ManFileSize( pFileName );
+    p->pFileData = Bbl_ManFileRead( pFileName );
+    // extract three managers
+    pBuffer = p->pFileData;
+    p->pName = Vec_StrRead( &pBuffer );
+    p->pObjs = Vec_StrRead( &pBuffer );
+    p->pFncs = Vec_StrRead( &pBuffer );
+    assert( pBuffer - p->pFileData == p->nFileSize );
+    // remember original IDs in the objects
+    p->vObj2Id = Vec_IntAlloc( 1000 );
+    Bbl_ManForEachObj_int( p->pObjs, pObj, h )
+    {
+        Vec_IntPush( p->vObj2Id, pObj->Id );
+        pObj->Id = Vec_IntSize(p->vObj2Id) - 1; 
+    }
+    return p;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManPrintStats( Bbl_Man_t * p )
+{
+    Bbl_Obj_t * pObj;
+    Bbl_Fnc_t * pFnc;
+    int h, nFuncs = 0, nNodes = 0, nObjs = 0;
+    Bbl_ManForEachObj_int( p->pObjs, pObj, h )
+        nObjs++, nNodes += Bbl_ObjIsNode(pObj);
+    Bbl_ManForEachFnc_int( p->pFncs, pFnc, h )
+        nFuncs++;
+    printf( "Total objects = %7d.  Total nodes = %7d. Unique functions = %7d.\n", nObjs, nNodes, nFuncs );
+    printf( "Name manager = %5.2f Mb\n", 1.0*Vec_StrSize(p->pName)/(1 << 20) );
+    printf( "Objs manager = %5.2f Mb\n", 1.0*Vec_StrSize(p->pObjs)/(1 << 20) );
+    printf( "Fncs manager = %5.2f Mb\n", 1.0*Vec_StrSize(p->pFncs)/(1 << 20) );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Deletes the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManStop( Bbl_Man_t * p )
+{
+    if ( p->vId2Obj )    Vec_IntFree( p->vId2Obj );
+    if ( p->vObj2Id )    Vec_IntFree( p->vObj2Id );
+    if ( p->vFaninNums ) Vec_IntFree( p->vFaninNums );
+    if ( p->pFileData )
+    {
+        BBLIF_FREE( p->pFileData );
+        p->pName->pArray = NULL;
+        p->pObjs->pArray = NULL;
+        p->pFncs->pArray = NULL;
+    }
+    if ( p->pEnts )
+    Vec_StrFree( p->pEnts );
+    Vec_StrFree( p->pName );
+    Vec_StrFree( p->pObjs );
+    Vec_StrFree( p->pFncs );
+    BBLIF_FREE( p );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Creates manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbl_Man_t * Bbl_ManStart( char * pName )
+{
+    Bbl_Man_t * p;
+    int nLength;
+    p = BBLIF_ALLOC( Bbl_Man_t, 1 );
+    memset( p, 0, sizeof(Bbl_Man_t) );
+    nLength = pName? 4 * ((strlen(pName) + 1) / 4 + 1) : 0;
+    p->pName  = Vec_StrAlloc( nLength );
+    p->pName->nSize = p->pName->nCap;
+    if ( pName )
+        strcpy( p->pName->pArray, pName );
+    p->pObjs = Vec_StrAlloc( 1 << 16 );
+    p->pFncs = Vec_StrAlloc( 1 << 16 );
+    p->pEnts = Vec_StrAlloc( 1 << 16 ); p->pEnts->nSize = 1;
+    p->vId2Obj = Vec_IntStart( 1 << 10 );
+    p->vFaninNums = Vec_IntStart( 1 << 10 );
+    return p;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs selection sort on the array of cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManSortCubes( char ** pCubes, int nCubes, int nVars )
+{
+    char * pTemp;
+    int i, j, best_i;
+    for ( i = 0; i < nCubes-1; i++ )
+    {
+        best_i = i;
+        for (j = i+1; j < nCubes; j++)
+            if ( memcmp( pCubes[j], pCubes[best_i], nVars ) < 0 )
+                best_i = j;
+        pTemp = pCubes[i]; pCubes[i] = pCubes[best_i]; pCubes[best_i] = pTemp;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cubes in the SOP to uniqify them to some extent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Bbl_ManSortSop( char * pSop, int nVars )
+{
+    char ** pCubes, * pSopNew;
+    int c, Length, nCubes;
+    Length = strlen(pSop);
+    assert( Length % (nVars + 3) == 0 );
+    nCubes = Length / (nVars + 3);
+    if ( nCubes < 2 )
+    {
+        pSopNew = BBLIF_ALLOC( char, Length + 1 );
+        memcpy( pSopNew, pSop, Length + 1 );
+        return pSopNew;
+    }
+    pCubes = BBLIF_ALLOC( char *, nCubes );
+    for ( c = 0; c < nCubes; c++ )
+        pCubes[c] = pSop + c * (nVars + 3);
+    if ( nCubes < 300 )
+        Bbl_ManSortCubes( pCubes, nCubes, nVars );
+    pSopNew = BBLIF_ALLOC( char, Length + 1 );
+    for ( c = 0; c < nCubes; c++ )
+        memcpy( pSopNew + c * (nVars + 3), pCubes[c], nVars + 3 );
+    BBLIF_FREE( pCubes );
+    pSopNew[nCubes * (nVars + 3)] = 0;
+    return pSopNew;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Saves one entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbl_ManCreateEntry( Bbl_Man_t * p, int iFunc, int iNext )
+{
+    Bbl_Ent_t * pEnt;
+    pEnt = (Bbl_Ent_t *)Vec_StrFetch( p->pEnts, 2 * sizeof(int) );
+    pEnt->iFunc = iFunc;
+    pEnt->iNext = iNext;
+    return (char *)pEnt - p->pEnts->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cubes in the SOP to uniqify them to some extent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbl_ManSopCheckUnique( Bbl_Man_t * p, char * pSop, int nVars, int nCubes, int iFunc )
+{
+    Bbl_Fnc_t * pFnc;
+    Bbl_Ent_t * pEnt;
+    int h, Length = strlen(pSop) + 1;
+    int nWords = (Length / 4 + (Length % 4 > 0));
+    if ( nVars > 16 )   nVars = 16;
+    if ( nCubes > 16 )  nCubes = 16;
+//    if ( nVars == 16 && nCubes == 16 )
+//        return iFunc;
+    for ( h = p->SopMap[nVars][nCubes]; h; h = pEnt->iNext )
+    {
+        pEnt = Bbl_VecEnt( p->pEnts, h );
+        pFnc = Bbl_VecFnc( p->pFncs, pEnt->iFunc );
+        assert( nVars == 16 || nCubes == 16 || pFnc->nWords == nWords );
+        if ( pFnc->nWords == nWords && memcmp( pFnc->pWords, pSop, Length ) == 0 )
+            return pEnt->iFunc;
+    }
+    p->SopMap[nVars][nCubes] = Bbl_ManCreateEntry( p, iFunc, p->SopMap[nVars][nCubes] );
+    return iFunc;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Saves one SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbl_ManSaveSop( Bbl_Man_t * p, char * pSop, int nVars )
+{
+    Bbl_Fnc_t * pFnc;
+    char * pSopNew;
+    int iFunc, Length = strlen(pSop) + 1;
+    int nWords = Length / 4 + (Length % 4 > 0);
+    // reorder cubes to semi-canicize SOPs
+    pSopNew = Bbl_ManSortSop( pSop, nVars );
+    // get the candidate location
+    iFunc = Bbl_ManSopCheckUnique( p, pSopNew, nVars, Length / (nVars + 3), Vec_StrSize(p->pFncs) );
+//    iFunc = Vec_StrSize(p->pFncs);
+    if ( iFunc == Vec_StrSize(p->pFncs) )
+    { // store this SOP
+        pFnc = (Bbl_Fnc_t *)Vec_StrFetch( p->pFncs, sizeof(Bbl_Fnc_t) + nWords * sizeof(int) );
+        pFnc->pWords[nWords-1] = 0;
+        pFnc->nWords = nWords;
+        strcpy( (char *)pFnc->pWords, pSopNew );
+        assert( iFunc == (char *)pFnc - p->pFncs->pArray );
+    }
+    BBLIF_FREE( pSopNew );
+    return iFunc;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Adds one object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManCreateObject( Bbl_Man_t * p, Bbl_Type_t Type, int ObjId, int nFanins, char * pSop )
+{
+    Bbl_Obj_t * pObj;
+    if ( Type == BBL_OBJ_CI && nFanins != 0 )
+    {
+        printf( "Attempting to create a combinational input with %d fanins (should be 0).\n", nFanins );
+        return;
+    }
+    if ( Type == BBL_OBJ_CO && nFanins != 1 )
+    {
+        printf( "Attempting to create a combinational output with %d fanins (should be 1).\n", nFanins );
+        return;
+    }
+    pObj = (Bbl_Obj_t *)Vec_StrFetch( p->pObjs, sizeof(Bbl_Obj_t) + nFanins * sizeof(int) );
+    memset( pObj, 0, sizeof(Bbl_Obj_t) );
+    Vec_IntSetEntry( p->vId2Obj, ObjId, (char *)pObj - p->pObjs->pArray );
+    Vec_IntSetEntry( p->vFaninNums, ObjId, 0 );
+    pObj->fCi = (Type == BBL_OBJ_CI);
+    pObj->fCo = (Type == BBL_OBJ_CO);
+    pObj->Id  = ObjId;
+    pObj->Fnc = pSop? Bbl_ManSaveSop(p, pSop, nFanins) : -1;
+    pObj->nFanins = nFanins;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Creates fanin/fanout relationship between two objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManAddFanin( Bbl_Man_t * p, int ObjId, int FaninId )
+{
+    Bbl_Obj_t * pObj, * pFanin;
+    int iFanin;
+    pObj   = Bbl_ManObj( p, ObjId );
+    if ( Bbl_ObjIsCi(pObj) )
+    {
+        printf( "Bbl_ManAddFanin(): Cannot add fanin of the combinational input (Id = %d).\n", ObjId );
+        return;
+    }
+    pFanin = Bbl_ManObj( p, FaninId );
+    if ( Bbl_ObjIsCo(pFanin) )
+    {
+        printf( "Bbl_ManAddFanin(): Cannot add fanout of the combinational output (Id = %d).\n", FaninId );
+        return;
+    }
+    iFanin = Vec_IntEntry( p->vFaninNums, ObjId );
+    if ( iFanin >= (int)pObj->nFanins )
+    {
+        printf( "Bbl_ManAddFanin(): Trying to add more fanins to object (Id = %d) than declared (%d).\n", ObjId, pObj->nFanins );
+        return;
+    }
+    assert( iFanin < (int)pObj->nFanins );
+    Vec_IntWriteEntry( p->vFaninNums, ObjId, iFanin+1 );
+    pObj->pFanins[iFanin] = (char *)pObj - (char *)pFanin;
+}
+
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns 1 if the manager was created correctly.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbl_ManCheck( Bbl_Man_t * p )
+{
+    Bbl_Obj_t * pObj;
+    int h, RetValue = 1;
+    Bbl_ManForEachObj_int( p->pObjs, pObj, h )
+    {
+        if ( Bbl_ObjIsNode(pObj) && pObj->Fnc == -1 )
+            RetValue = 0, printf( "Bbl_ManCheck(): Node %d does not have function specified.\n", pObj->Id );
+        if ( Bbl_ObjIsCi(pObj) && pObj->Fnc != -1 )
+            RetValue = 0, printf( "Bbl_ManCheck(): CI with %d has function specified.\n", pObj->Id );
+        if ( Bbl_ObjIsCo(pObj) && pObj->Fnc != -1 )
+            RetValue = 0, printf( "Bbl_ManCheck(): CO with %d has function specified.\n", pObj->Id );
+        if ( Vec_IntEntry(p->vFaninNums, pObj->Id) != (int)pObj->nFanins )
+            RetValue = 0, printf( "Bbl_ManCheck(): Object %d has less fanins (%d) than declared (%d).\n", 
+                pObj->Id, Vec_IntEntry(p->vFaninNums, pObj->Id), pObj->nFanins );
+    }
+    return RetValue;
+}
+
+
+/**Fnction*************************************************************
+
+  Synopsis    [Misc APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int         Bbl_ObjIsInput( Bbl_Obj_t * p )                      { return Bbl_ObjIsCi(p);                      }
+int         Bbl_ObjIsOutput( Bbl_Obj_t * p )                     { return Bbl_ObjIsCo(p);                      }
+int         Bbl_ObjIsLut( Bbl_Obj_t * p )                        { return Bbl_ObjIsNode(p);                    }
+int         Bbl_ObjId( Bbl_Obj_t * p )                           { return p->Id;                               }
+int         Bbl_ObjIdOriginal( Bbl_Man_t * pMan, Bbl_Obj_t * p ) { assert(0); return Vec_IntEntry(pMan->vObj2Id, p->Id);  }
+int         Bbl_ObjFaninNumber( Bbl_Obj_t * p )                  { return Bbl_ObjFaninNum(p);                  }
+char *      Bbl_ObjSop( Bbl_Man_t * pMan, Bbl_Obj_t * p )        { return Bbl_ManSop(pMan, p->Fnc);            }
+int         Bbl_ObjIsMarked( Bbl_Obj_t * p )                     { return p->fMark;                            }
+void        Bbl_ObjMark( Bbl_Obj_t * p )                         { p->fMark = 1;                               }
+int         Bbl_ObjFncHandle( Bbl_Obj_t * p )                    { return p->Fnc;                              }
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the name of the design.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Bbl_ManName( Bbl_Man_t * p )
+{
+    return p->pName->pArray;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the maximum handle of the SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbl_ManFncSize( Bbl_Man_t * p )
+{
+    return p->pFncs->nSize;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the first object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbl_Obj_t * Bbl_ManObjFirst( Bbl_Man_t * p )
+{
+    return Bbl_VecObj( p->pObjs, 0 );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the next object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbl_Obj_t * Bbl_ManObjNext( Bbl_Man_t * p, Bbl_Obj_t * pObj )
+{
+    char * pNext = (char *)pObj + Bbl_ObjSize(pObj);
+    char * pEdge = p->pObjs->pArray + p->pObjs->nSize;
+    return (Bbl_Obj_t *)(pNext < pEdge ? pNext : NULL);
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the first fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbl_Obj_t * Bbl_ObjFaninFirst( Bbl_Obj_t * p )
+{
+    return Bbl_ObjFaninNum(p) ? Bbl_ObjFanin( p, 0 ) : NULL;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Returns the next fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbl_Obj_t * Bbl_ObjFaninNext( Bbl_Obj_t * p, Bbl_Obj_t * pPrev )
+{
+    Bbl_Obj_t * pFanin;
+    int i;
+    Bbl_ObjForEachFanin_int( p, pFanin, i )
+        if ( pFanin == pPrev )
+            break;
+    return i < Bbl_ObjFaninNum(p) - 1 ? Bbl_ObjFanin( p, i+1 ) : NULL;
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Drives text BLIF file for debugging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManDumpBlif( Bbl_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Bbl_Obj_t * pObj, * pFanin;
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# Test file written by Bbl_ManDumpBlif() in ABC.\n" );
+    fprintf( pFile, ".model %s\n", Bbl_ManName(p) );
+    // write objects
+    Bbl_ManForEachObj( p, pObj )
+    {
+        if ( Bbl_ObjIsInput(pObj) )
+            fprintf( pFile, ".inputs %d\n", Bbl_ObjId(pObj) );
+        else if ( Bbl_ObjIsOutput(pObj) )
+            fprintf( pFile, ".outputs %d\n", Bbl_ObjId(pObj) );
+        else if ( Bbl_ObjIsLut(pObj) )
+        {
+            fprintf( pFile, ".names" );
+            Bbl_ObjForEachFanin( pObj, pFanin )
+                fprintf( pFile, " %d", Bbl_ObjId(pFanin) );
+            fprintf( pFile, " %d\n", Bbl_ObjId(pObj) );
+            fprintf( pFile, "%s", Bbl_ObjSop(p, pObj) );
+        }
+        else assert( 0 );
+    }
+    // write output drivers
+    Bbl_ManForEachObj( p, pObj )
+    {
+        if ( !Bbl_ObjIsOutput(pObj) )
+            continue;
+        fprintf( pFile, ".names" );
+        Bbl_ObjForEachFanin( pObj, pFanin )
+            fprintf( pFile, " %d", Bbl_ObjId(pFanin) );
+        fprintf( pFile, " %d\n", Bbl_ObjId(pObj) );
+        fprintf( pFile, "1 1\n" );
+    }
+    fprintf( pFile, ".end\n" );
+    fclose( pFile );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Converting truth table into an SOP.]
+
+  Description [The truth table is given as a bit-string pTruth
+  composed of 2^nVars bits. The result is an SOP derived by
+  collecting minterms appearing in the truth table. The SOP is 
+  represented as a C-string, as documented in file "bblif.h".
+  It is recommended to limit the use of this procedure to Boolean 
+  functions up to 6 inputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Bbl_ManTruthToSop( unsigned * pTruth, int nVars )
+{
+    char * pResult, * pTemp;
+    int nMints, nOnes, b, v;
+    assert( nVars >= 0 && nVars <= 16 );
+    nMints = (1 << nVars);
+    // count the number of ones
+    nOnes = 0;
+    for ( b = 0; b < nMints; b++ )
+        nOnes += ((pTruth[b>>5] >> (b&31)) & 1);
+    // handle constants
+    if ( nOnes == 0 || nOnes == nMints )
+    {
+        pResult = pTemp = BBLIF_ALLOC( char, nVars + 4 );        
+        for ( v = 0; v < nVars; v++ )
+            *pTemp++ = '-';
+        *pTemp++ = ' ';
+        *pTemp++ = nOnes? '1' : '0';
+        *pTemp++ = '\n';
+        *pTemp++ = 0;
+        assert( pTemp - pResult == nVars + 4 );
+        return pResult;
+    }
+    pResult = pTemp = BBLIF_ALLOC( char, nOnes * (nVars + 3) + 1 );        
+    for ( b = 0; b < nMints; b++ )
+    {
+        if ( ((pTruth[b>>5] >> (b&31)) & 1) == 0 )
+            continue;
+        for ( v = 0; v < nVars; v++ )
+            *pTemp++ = ((b >> v) & 1)? '1' : '0';
+        *pTemp++ = ' ';
+        *pTemp++ = '1';
+        *pTemp++ = '\n';
+    }
+    *pTemp++ = 0;
+    assert( pTemp - pResult == nOnes * (nVars + 3) + 1 );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the array of truth tables for the given number of vars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Bbl_ManSopToTruthElem( int nVars, unsigned ** pVars )
+{
+    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    int i, k, nWords;
+    nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( i < 5 )
+        {
+            for ( k = 0; k < nWords; k++ )
+                pVars[i][k] = Masks[i];
+        }
+        else
+        {
+            for ( k = 0; k < nWords; k++ )
+                if ( k & (1 << (i-5)) )
+                    pVars[i][k] = ~(unsigned)0;
+                else
+                    pVars[i][k] = 0;
+        }
+    }
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [Converting SOP into a truth table.]
+
+  Description [The SOP is represented as a C-string, as documented in 
+  file "bblif.h". The truth table is returned as a bit-string composed 
+  of 2^nVars bits. For functions of less than 6 variables, the full
+  machine word is returned. (The truth table looks as if the function
+  had 5 variables.) The use of this procedure should be limited to 
+  Boolean functions with no more than 16 inputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Bbl_ManSopToTruth( char * pSop, int nVars )
+{
+    unsigned * pTruth, * pCube, * pVars[16];
+    int nWords = nVars <= 5 ? 1 : (1 << (nVars - 5));
+    int v, c, w, nCubes, fCompl = 0;
+    if ( pSop == NULL )
+        return NULL;
+    if ( strlen(pSop) % (nVars + 3) != 0 )
+    {
+        printf( "Bbl_ManSopToTruth(): SOP is represented incorrectly.\n" );
+        return NULL;
+    }
+    // create storage for TTs of the result, elementary variables and the temp cube
+    pTruth   = BBLIF_ALLOC( unsigned, nWords );   
+    pVars[0] = BBLIF_ALLOC( unsigned, nWords * (nVars+1) );   
+    for ( v = 1; v < nVars; v++ )
+        pVars[v] = pVars[v-1] + nWords;
+    pCube = pVars[v-1] + nWords;
+    Bbl_ManSopToTruthElem( nVars, pVars );
+    // iterate through the cubes
+    memset( pTruth, 0, sizeof(unsigned) * nWords );
+    nCubes =  strlen(pSop) / (nVars + 3);
+    for ( c = 0; c < nCubes; c++ )
+    {
+        fCompl = (pSop[nVars+1] == '0');
+        memset( pCube, 0xff, sizeof(unsigned) * nWords );
+        // iterate through the literals of the cube
+        for ( v = 0; v < nVars; v++ )
+            if ( pSop[v] == '1' )
+                for ( w = 0; w < nWords; w++ )
+                    pCube[w] &= pVars[v][w];
+            else if ( pSop[v] == '0' )
+                for ( w = 0; w < nWords; w++ )
+                    pCube[w] &= ~pVars[v][w];
+        // add cube to storage
+        for ( w = 0; w < nWords; w++ )
+            pTruth[w] |= pCube[w];
+        // go to the next cube
+        pSop += (nVars + 3);
+    }
+    BBLIF_FREE( pVars[0] );
+    if ( fCompl )
+        for ( w = 0; w < nWords; w++ )
+            pTruth[w] = ~pTruth[w];
+    return pTruth;
+}
+
+
+/**Fnction*************************************************************
+
+  Synopsis    [Checks the truth table computation.]
+
+  Description [We construct the logic network for the half-adder represnted
+  using the BLIF file below]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManTestTruth( char * pSop, int nVars )
+{
+    unsigned * pTruth;
+    char * pSopNew;
+    pTruth = Bbl_ManSopToTruth( pSop, nVars );
+    pSopNew = Bbl_ManTruthToSop( pTruth, nVars );
+    printf( "Old SOP:\n%s\n", pSop );
+    printf( "New SOP:\n%s\n", pSopNew );
+    BBLIF_FREE( pSopNew );
+    BBLIF_FREE( pTruth );
+}
+
+/**Fnction*************************************************************
+
+  Synopsis    [This demo shows using the internal to construct a half-adder.]
+
+  Description [We construct the logic network for the half-adder represnted
+  using the BLIF file below]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbl_ManSimpleDemo()
+{
+/*
+    # There are contents of a BLIF file representing a half-adder:
+    .model hadder
+    .inputs a     // ID = 1
+    .inputs b     // ID = 2
+    .inputs cin   // ID = 3
+    .outputs s    // ID = 4
+    .outputs cout // ID = 5
+    .names a b cin s_driver   // ID = 6
+    100 1
+    010 1
+    001 1
+    111 1
+    .names a b cin cout_driver // ID = 7
+    -11 1
+    1-1 1
+    11- 1
+    .names s_driver s
+    1 1
+    .names cout_driver cout
+    1 1
+    .end
+*/
+    Bbl_Man_t * p;
+    // start the data manager
+    p = Bbl_ManStart( "hadder" );
+    // create CIs
+    Bbl_ManCreateObject( p, BBL_OBJ_CI, 1, 0, NULL ); // a
+    Bbl_ManCreateObject( p, BBL_OBJ_CI, 2, 0, NULL ); // b
+    Bbl_ManCreateObject( p, BBL_OBJ_CI, 3, 0, NULL ); // cin
+    // create COs
+    Bbl_ManCreateObject( p, BBL_OBJ_CO, 4, 1, NULL ); // s
+    Bbl_ManCreateObject( p, BBL_OBJ_CO, 5, 1, NULL ); // cout
+    // create internal nodes
+    Bbl_ManCreateObject( p, BBL_OBJ_NODE, 6, 3, "100 1\n010 1\n001 1\n111 1\n" ); // s_driver
+    Bbl_ManCreateObject( p, BBL_OBJ_NODE, 7, 3, "-11 1\n1-1 1\n11- 1\n" );        // cout_driver
+    // add fanins of node 6
+    Bbl_ManAddFanin( p, 6, 1 ); // s_driver <- a
+    Bbl_ManAddFanin( p, 6, 2 ); // s_driver <- b
+    Bbl_ManAddFanin( p, 6, 3 ); // s_driver <- cin
+    // add fanins of node 7
+    Bbl_ManAddFanin( p, 7, 1 ); // cout_driver <- a
+    Bbl_ManAddFanin( p, 7, 2 ); // cout_driver <- b
+    Bbl_ManAddFanin( p, 7, 3 ); // cout_driver <- cin
+    // add fanins of COs
+    Bbl_ManAddFanin( p, 4, 6 ); // s <- s_driver
+    Bbl_ManAddFanin( p, 5, 7 ); // cout <- cout_driver
+    // sanity check
+    Bbl_ManCheck( p );
+    // write BLIF file as a sanity check
+    Bbl_ManDumpBlif( p, "hadder.blif" );
+    // write binary BLIF file
+    Bbl_ManDumpBinaryBlif( p, "hadder.bblif" );
+    // remove the manager
+    Bbl_ManStop( p );
+
+
+//    Bbl_ManTestTruth( "100 1\n010 1\n001 1\n111 1\n", 3 );
+//    Bbl_ManTestTruth( "-11 0\n1-1 0\n11- 0\n", 3 );
+//    Bbl_ManTestTruth( "--- 1\n", 3 );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/bbl/bblif.h b/src/misc/bbl/bblif.h
new file mode 100644
index 00000000..b4859370
--- /dev/null
+++ b/src/misc/bbl/bblif.h
@@ -0,0 +1,285 @@
+/**CFile****************************************************************
+
+  FileName    [bblif.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Binary BLIF representation for logic networks.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 28, 2009.]
+
+  Revision    [$Id: bblif.h,v 1.00 2009/02/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__bbl__bblif_h
+#define ABC__aig__bbl__bblif_h
+
+
+/*
+    This file (taken together with "bblif.c") implements a stand-alone 
+    interface between ABC and an application that uses ABC. 
+    
+    The interface is designed to pass a combinational logic network 
+    from the calling application to ABC using a binary BLIF format (BBLIF) 
+    and return the network after synthesis/mapping/verification in ABC 
+    back to the caller.
+
+    The interface can do the following:
+    (1) accept a combinational logic network via a set of APIs
+    (2) write the logic network into a binary BLIF file readable by ABC
+    (3) read a binary BLIF file with a mapped network produced by ABC
+    (4) return the mapped network to the caller through a set of APIs
+
+    It should be noted that the BBLIF interface can be used to pass
+    the network from the calling application into ABC without writing it
+    into a file. In this case, ABC should be compiled as a library and
+    linked to the calling application. The BBLIF manager can be given
+    directly to the procedure Bbl_ManToAbc() to convert it into an AIG.
+    Similarly, the resulting mapped network can be converted into
+    BBLIF manager and passed back after the call to Bbl_ManFromAbc().
+
+    Here these steps are described in more detail:
+
+    (1) The BBLIF manager is allocated by calling Bbl_ManStart() and 
+        deallocated by calling Bbl_ManStop(). 
+    
+        The combinational network is composed of three types of objects:
+        (a) combinational inputs (CIs), (b) combinational outputs (COs), 
+        (c) internal logic nodes represented using Sum-of-Products (SOPs)
+        similar to the way logic nodes are represented in SIS. Sequential 
+        elements (flops) are currently not supported.   A CI has no fanins. 
+        A CO has exactly one fanin and no fanouts. Internal nodes can 
+        have any number of fanins and fanouts. Only an internal node can 
+        have a logic function.
+
+        Before constructing the BBLIF manager, each object should be 
+        assigned a unique non-negative (0-based) integer ID. The sequence
+        of ID numbers may have gaps in it (for example, 0, 1, 2, 5, 6, etc)
+        but care should be taken that the ID numbers do not grow too large
+        because internally they are used to index the objects. So if 
+        the largest given ID has value N, an array of 4*N bytes will be 
+        allocated internally by the BBLIF manager. Obviously if N = 1M, 
+        the array will use 4Mb, but if N = 100M, it will use 0.4Gb.
+
+        This object ID (called also "the original ID of the object") is 
+        given to Bbl_ManCreateObject(), which construct the BBLIF objects 
+        and to the procedure Bbl_ManAddFanin(), which creates fanin/fanout
+        relations between two objects.  The exact number of fanins of an
+        object should be declared when calling Bbl_ManCreateObject(). 
+        Later on, each node should be assigned as many fanins using 
+        Bbl_ManAddFanin(). The order/number of fanins corresponds to the 
+        order/number of variables in the SOP of the logic function of the 
+        node. The declared and actual number of fanins should be the same.
+        otherwise the interface will not function correctly. This is checked
+        by the procedure Bbl_ManCheck(), which should be called when 
+        constructing all objects and their fanins is finished.
+
+        The SOP representation of the logic function should be given to
+        every internal node. It is given as a C-string, showing the SOP
+        as it would appear in a BLIF or PLA file. Each cube is composed
+        of characters '0', '1', and '-', and ended by a seqence of three
+        characters: space ' ', followed by '0' or '1' (depending on whether 
+        on- or off-set is used), followed by the new line character '\n'. 
+        For example, a two-input OR has the following SOP representation: 
+        "1- 1\n-1 1\n", or equivalently, "00 0\n". The SOP for a constant 
+        function with no fanins is represented as " 0\n" (constant 0) and
+        " 1\n" (constant 1). SOP for a constant node with some fanins
+        may also be represented. For example, constant 0 node with three 
+        fanins will have SOP representation as follows: "--- 0\n".
+
+        The objects can be added to the BBLIF manager in any order, but 
+        by the time the fanin/fanout connections are created, corresponding 
+        objects should be already created.
+
+        The number of objects is limited by 2^31. The number of fanins
+        of one object is restricted to 2^28. The SOP representation can 
+        have arbitrary many products (cubes), as long as memory is enough
+        to represent them in the C-string form, as described above.
+
+    (2) To write the manager into a file, call procedure Bbl_ManDumpBinaryBlif().
+        It is recommended to use files with extension ".bblif" because it
+        will allow ABC to call the approapriate reader in command "read".
+
+    (3) To read the network from file, call procedure Bbl_ManReadBinaryBlif().
+
+    (4) It is assumed that ABC will return the network after mapping.
+        This network will arrive in a BBLIF file, from which the BBLIF 
+        manager is created by the call to Bbl_ManReadBinaryBlif(). The 
+        following APIs are useful to extract the mapped network from the manager:
+        
+        Iterator Bbl_ManForEachObj() iterates through the pointers to the
+        BBLIF objects, which are guaranteed to be in a topological order. 
+
+        For each object, the following APIs can be used:
+        Bbl_ObjIsInput() returns 1 if the object is a CI
+        Bbl_ObjIsOutput() returns 1 if the object is a CO
+        Bbl_ObjIsLut() returns 1 if the object is a logic node (lookup table)
+        Bbl_ObjFaninNumber() returns the number of fanins of the node
+        Bbl_ObjSop() returns the SOP representation of the node, as described above.
+
+        A special attention should be given to the representation of object IDs
+        after mapping. Recall that when the outgoing BBLIF network is constructed, 
+        the IDs of objects are assigned by the calling application and given to 
+        the BBLIF manager when procedure Bbl_ManCreateObject() is called.  
+        We refer to these object IDs as "original IDs of the objects". 
+        
+        When the network has been given to ABC, mapped, and returned to the 
+        calling application in the incoming BBLIF file, only CIs and COs are 
+        guaranteed to preserve their "original IDs". Other objects may be created 
+        during synthesis/mapping. The original IDs of these objects are set to -1. 
+
+        The following two APIs are used to return the IDs of objects after mapping:
+        Bbl_ObjId() returns the new ID (useful to construct network after mapping)
+        Bbl_ObjIdOriginal() returns the original ID (or -1 if this is a new object).
+
+        !!!***!!!
+        Note: The original ID currently cannot be returned by Bbl_ObjIdOriginal().
+        It is recommended to use the work-around described below.
+        !!!***!!!
+
+        The original ID is useful to map CIs/COs after mapping into CIs/COs before
+        mapping. However, the order of CIs/COs after mapping in the incoming network 
+        is the same as the order of their creation by the calling application 
+        in the outgoing network. This allows for a workaround that does not have 
+        the need for the original IDs.  We can simply iterate through the objects 
+        after mapping, and create CIs and COs in the order of their appearance, 
+        and this order is guaranteed to be the same as the order of their 
+        construction by the calling application.
+
+        It is also worth noting that currently the internal node names are not 
+        preserved by ABC during synthesis. This may change in the future. and then 
+        some of the internal nodes will preserve their IDs, which may allow the 
+        calling application to reconstruct the names of some of the nodes after 
+        synthesis/mapping in ABC using their original IDs whenever available.
+
+        Finally, iterator Bbl_ObjForEachFanin() can be used to iterate through 
+        the fanins of each mapped object. For CIs, there will be no fanins. 
+        For COs, there will be exactly one fanin. For the internal nodes (LUTs)
+        the number of fanins is the number of inputs of these nodes.
+
+    A demo of using this interface is included at the bottom of file "bblif.c" in 
+    procedure Bbl_ManSimpleDemo(). Additional examples can be found in the files
+    "abc\src\base\io\ioReadBblif.c" and "abc\src\base\io\ioWriteBblif.c". These
+    files illustrate how an ABC network is created from the BBLIF data manager 
+    and how the data manager is created from the ABC network. 
+    
+    Note that only the files "bblif.h" and "bblif.c" are needed for interfacing
+    the user's application with ABC, while other files should not be compiled 
+    as part of the application code.
+
+    Finally, a warning regarding endianness. The interface may not work 
+    if the BBLIF file is produced on a machine whose engianness is different 
+    from the machine, which is reading this file.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+#ifdef _WIN32
+#define inline __inline
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// object types
+typedef enum { 
+    BBL_OBJ_NONE,                // 0: non-existent object
+    BBL_OBJ_CI,                  // 1: primary input
+    BBL_OBJ_CO,                  // 2: primary output
+    BBL_OBJ_NODE,                // 3: buffer node
+    BBL_OBJ_VOID                 // 4: unused object
+} Bbl_Type_t;
+
+// data manager
+typedef struct Bbl_Man_t_ Bbl_Man_t;
+
+// data object
+typedef struct Bbl_Obj_t_ Bbl_Obj_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// (1) creating the data manager in the application code
+extern Bbl_Man_t * Bbl_ManStart( char * pName );
+extern void        Bbl_ManCreateObject( Bbl_Man_t * p, Bbl_Type_t Type, int ObjId, int nFanins, char * pSop );
+extern void        Bbl_ManAddFanin( Bbl_Man_t * p, int ObjId, int FaninId );
+extern int         Bbl_ManCheck( Bbl_Man_t * p );
+extern void        Bbl_ManPrintStats( Bbl_Man_t * p );
+extern void        Bbl_ManStop( Bbl_Man_t * p );
+
+// (2) writing the data manager into file
+extern void        Bbl_ManDumpBinaryBlif( Bbl_Man_t * p, char * pFileName );
+
+// (3) reading the data manager from file
+extern Bbl_Man_t * Bbl_ManReadBinaryBlif( char * pFileName );
+
+// (4) returning the mapped network after reading the data manaager from file
+extern char *      Bbl_ManName( Bbl_Man_t * p );
+extern int         Bbl_ObjIsInput( Bbl_Obj_t * p );
+extern int         Bbl_ObjIsOutput( Bbl_Obj_t * p );
+extern int         Bbl_ObjIsLut( Bbl_Obj_t * p );
+extern int         Bbl_ObjId( Bbl_Obj_t * p );
+extern int         Bbl_ObjIdOriginal( Bbl_Man_t * pMan, Bbl_Obj_t * p );
+extern int         Bbl_ObjFaninNumber( Bbl_Obj_t * p );
+extern char *      Bbl_ObjSop( Bbl_Man_t * pMan, Bbl_Obj_t * p );
+
+// for the use in iterators only
+extern Bbl_Obj_t * Bbl_ManObjFirst( Bbl_Man_t * p );
+extern Bbl_Obj_t * Bbl_ManObjNext( Bbl_Man_t * p, Bbl_Obj_t * pObj );
+extern Bbl_Obj_t * Bbl_ObjFaninFirst( Bbl_Obj_t * p );
+extern Bbl_Obj_t * Bbl_ObjFaninNext( Bbl_Obj_t * p, Bbl_Obj_t * pPrev );
+
+// iterator through the objects
+#define Bbl_ManForEachObj( p, pObj )                \
+    for ( pObj = Bbl_ManObjFirst(p); pObj; pObj = Bbl_ManObjNext(p, pObj) )
+// iterator through the fanins fo the an object
+#define Bbl_ObjForEachFanin( pObj, pFanin )         \
+    for ( pFanin = Bbl_ObjFaninFirst(pObj); pFanin; pFanin = Bbl_ObjFaninNext(pObj, pFanin) )
+
+// these additional procedures are provided to transform truth tables into SOPs, and vice versa
+extern char *      Bbl_ManTruthToSop( unsigned * pTruth, int nVars );
+extern unsigned *  Bbl_ManSopToTruth( char * pSop, int nVars );
+
+// write text BLIF file for debugging
+extern void        Bbl_ManDumpBlif( Bbl_Man_t * p, char * pFileName );
+
+// a simple demo procedure
+extern void        Bbl_ManSimpleDemo();
+
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/misc/bbl/module.make b/src/misc/bbl/module.make
new file mode 100644
index 00000000..187e570b
--- /dev/null
+++ b/src/misc/bbl/module.make
@@ -0,0 +1 @@
+SRC +=    src/misc/bbl/bblif.c 
diff --git a/src/misc/bzlib/bzlib.h b/src/misc/bzlib/bzlib.h
index 68a6cd01..30487828 100644
--- a/src/misc/bzlib/bzlib.h
+++ b/src/misc/bzlib/bzlib.h
@@ -24,8 +24,8 @@
 #endif
 #endif
 
-#ifndef _BZLIB_H
-#define _BZLIB_H
+#ifndef ABC__misc__bzlib__bzlib_h
+#define ABC__misc__bzlib__bzlib_h
 
 #define BZ_RUN               0
 #define BZ_FLUSH             1
@@ -96,7 +96,7 @@ typedef
 #endif
 
 #include <stdio.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/bzlib/bzlib_private.h b/src/misc/bzlib/bzlib_private.h
index 072f0486..229ed386 100644
--- a/src/misc/bzlib/bzlib_private.h
+++ b/src/misc/bzlib/bzlib_private.h
@@ -19,8 +19,8 @@
    ------------------------------------------------------------------ */
 
 
-#ifndef _BZLIB_PRIVATE_H
-#define _BZLIB_PRIVATE_H
+#ifndef ABC__misc__bzlib__bzlib_private_h
+#define ABC__misc__bzlib__bzlib_private_h
 
 
 #include <stdlib.h>
diff --git a/src/misc/espresso/espresso.h b/src/misc/espresso/espresso.h
index 27d1c124..8b54fab5 100644
--- a/src/misc/espresso/espresso.h
+++ b/src/misc/espresso/espresso.h
@@ -18,7 +18,7 @@
 
 #include "util_hack.h" // added
 
-#define ptime()            util_cpu_time()
+#define ABC__misc__espresso__espresso_h
 #define print_time(t)    util_print_time(t)
 
 #ifdef IBM_WATC
@@ -55,7 +55,7 @@
 
 
 /* Define host machine characteristics of "unsigned int" */
-#ifndef BPI
+#ifndef ABC__misc__espresso__espresso_h
 #define BPI
 
 
diff --git a/src/misc/espresso/main.c b/src/misc/espresso/main.c
index 157ef5a0..76c5fb79 100644
--- a/src/misc/espresso/main.c
+++ b/src/misc/espresso/main.c
@@ -14,7 +14,7 @@
  */
 
 #include "espresso.h"
-#include "main.h"
+#include "base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
         /* table definitions for options */
diff --git a/src/misc/espresso/mincov_int.h b/src/misc/espresso/mincov_int.h
index e81850f2..4b61be17 100644
--- a/src/misc/espresso/mincov_int.h
+++ b/src/misc/espresso/mincov_int.h
@@ -52,4 +52,4 @@ extern solution_t *sm_mincov();
 extern int gimpel_reduce();
 
 
-#define WEIGHT(weight, col)    (weight == NIL(int) ? 1 : weight[col])
+#define ABC__misc__espresso__mincov_int_h
diff --git a/src/misc/espresso/sparse.h b/src/misc/espresso/sparse.h
index 9a15fc65..dda0a7ed 100644
--- a/src/misc/espresso/sparse.h
+++ b/src/misc/espresso/sparse.h
@@ -7,8 +7,8 @@
  * $Date$
  *
  */
-#ifndef SPARSE_H
-#define SPARSE_H
+#ifndef ABC__misc__espresso__sparse_h
+#define ABC__misc__espresso__sparse_h
 
 
 ABC_NAMESPACE_HEADER_START
diff --git a/src/misc/espresso/sparse_int.h b/src/misc/espresso/sparse_int.h
index 49b2509a..c567afde 100644
--- a/src/misc/espresso/sparse_int.h
+++ b/src/misc/espresso/sparse_int.h
@@ -30,7 +30,7 @@
  *  e: an object to use if insertion needed (set to actual value used)
  */
 
-#define sorted_insert(type, first, last, count, next, prev, value, newval, e) \
+#define ABC__misc__espresso__sparse_int_h
     if (last == 0) { \
     e->value = newval; \
     first = e; \
diff --git a/src/misc/espresso/util_old.h b/src/misc/espresso/util_old.h
index 32be6ffa..d60790d3 100644
--- a/src/misc/espresso/util_old.h
+++ b/src/misc/espresso/util_old.h
@@ -7,8 +7,8 @@
  * $Date: 1993/06/07 21:04:07 $
  *
  */
-#ifndef UTIL_H
-#define UTIL_H
+#ifndef ABC__misc__espresso__util_old_h
+#define ABC__misc__espresso__util_old_h
 
 #if defined(_IBMR2)
 #ifndef _POSIX_SOURCE
diff --git a/src/misc/ext/ext.h b/src/misc/ext/ext.h
index 8db5a056..86601e52 100644
--- a/src/misc/ext/ext.h
+++ b/src/misc/ext/ext.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __EXT_H__
-#define __EXT_H__
+#ifndef ABC__misc__ext__ext_h
+#define ABC__misc__ext__ext_h
 
 #define EXT_ABC_FRAME
 #define EXT_ABC_INIT(pAbc)
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 693c25bd..0bef042c 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -26,8 +26,8 @@
 
 ***********************************************************************/
 
-#ifndef __EXTRA_H__
-#define __EXTRA_H__
+#ifndef ABC__misc__extra__extra_h
+#define ABC__misc__extra__extra_h
 
 
 #ifdef _WIN32
@@ -44,10 +44,7 @@
 #include <assert.h>
 #include <time.h>
 
-#include "st.h"
-#include "cuddInt.h"
-
-
+#include "src/misc/st/st.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -76,239 +73,10 @@ typedef unsigned char      uint8;
 typedef unsigned short     uint16;
 typedef unsigned int       uint32;
 
-/* constants of the manager */
-#define     b0     Cudd_Not((dd)->one)
-#define     b1              (dd)->one
-#define     z0              (dd)->zero
-#define     z1              (dd)->one
-#define     a0              (dd)->zero
-#define     a1              (dd)->one
-
-// hash key macros
-#define hashKey1(a,TSIZE) \
-((ABC_PTRUINT_T)(a) % TSIZE)
-
-#define hashKey2(a,b,TSIZE) \
-(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
-
-#define hashKey3(a,b,c,TSIZE) \
-(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
-
-#define hashKey4(a,b,c,d,TSIZE) \
-((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
-   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
-
-#define hashKey5(a,b,c,d,e,TSIZE) \
-(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
-   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
-
 /*===========================================================================*/
 /*     Various Utilities                                                     */
 /*===========================================================================*/
 
-/*=== extraBddAuto.c ========================================================*/
-
-extern DdNode *     Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc );
-extern DdNode *     Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
-extern DdNode *      extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
-extern DdNode *     Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
-extern DdNode *      extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
-extern DdNode *     Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
-extern DdNode *      extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
-
-extern DdNode *     Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
-extern DdNode *      extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
-
-extern DdNode *     Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace );
-extern DdNode *     Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
-extern DdNode *      extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
-extern DdNode *     Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
-extern DdNode *      extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
-
-extern DdNode *     Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
-extern DdNode *      extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
-extern DdNode *     Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
-extern DdNode *      extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
-
-extern DdNode *     Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
-extern DdNode **    Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
-
-/*=== extraBddCas.c =============================================================*/
-
-/* performs the binary encoding of the set of function using the given vars */
-extern DdNode *     Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
-/* solves the column encoding problem using a sophisticated method */
-extern DdNode *     Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
-/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
-extern st_table *   Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
-/* collects the nodes under the cut starting from the given set of ADD nodes */
-extern int          Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
-/* find the profile of a DD (the number of edges crossing each level) */
-extern int          Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
-
-/*=== extraBddImage.c ================================================================*/
-
-typedef struct Extra_ImageTree_t_  Extra_ImageTree_t;
-extern Extra_ImageTree_t * Extra_bddImageStart( 
-    DdManager * dd, DdNode * bCare,
-    int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int fVerbose );
-extern DdNode *    Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
-extern void        Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
-extern DdNode *    Extra_bddImageRead( Extra_ImageTree_t * pTree );
-
-typedef struct Extra_ImageTree2_t_  Extra_ImageTree2_t;
-extern Extra_ImageTree2_t * Extra_bddImageStart2( 
-    DdManager * dd, DdNode * bCare,
-    int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int fVerbose );
-extern DdNode *    Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
-extern void        Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
-extern DdNode *    Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
-
-/*=== extraBddMisc.c ========================================================*/
-
-extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
-extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
-extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
-extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int nVars );
-extern DdNode *     extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
-extern void         Extra_StopManager( DdManager * dd );
-extern void         Extra_bddPrint( DdManager * dd, DdNode * F );
-extern void         Extra_bddPrintSupport( DdManager * dd, DdNode * F );
-extern void         extraDecomposeCover( DdManager* dd, DdNode*  zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 );
-extern int          Extra_bddSuppSize( DdManager * dd, DdNode * bSupp );
-extern int          Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar );
-extern int          Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 );
-extern int          Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax );
-extern int          Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall );
-extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * support );
-extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
-extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
-extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
-extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
-extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
-extern DdNode *     Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f );
-extern int          Extra_bddIsVar( DdNode * bFunc );
-extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
-extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
-extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
-extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
-extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
-extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
-extern DdNode *     Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
-extern DdNode *     extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
-extern int          Extra_bddVarIsInCube( DdNode * bCube, int iVar );
-extern DdNode *     Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
-
-#ifndef ABC_PRB
-#define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
-#endif
-
-/*=== extraBddKmap.c ================================================================*/
-
-/* displays the Karnaugh Map of a function */
-extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
-/* displays the Karnaugh Map of a relation */
-extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
-
-/*=== extraBddSymm.c =================================================================*/
-
-typedef struct Extra_SymmInfo_t_  Extra_SymmInfo_t;
-struct Extra_SymmInfo_t_ {
-    int nVars;      // the number of variables in the support
-    int nVarsMax;   // the number of variables in the DD manager
-    int nSymms;     // the number of pair-wise symmetries
-    int nNodes;     // the number of nodes in a ZDD (if applicable)
-    int * pVars;    // the list of all variables present in the support
-    char ** pSymms; // the symmetry information
-};
-
-/* computes the classical symmetry information for the function - recursive */
-extern Extra_SymmInfo_t *  Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
-/* computes the classical symmetry information for the function - using naive approach */
-extern Extra_SymmInfo_t *  Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
-extern int         Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
-
-/* allocates the data structure */
-extern Extra_SymmInfo_t *  Extra_SymmPairsAllocate( int nVars );
-/* deallocates the data structure */
-extern void        Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
-/* print the contents the data structure */
-extern void        Extra_SymmPairsPrint( Extra_SymmInfo_t * );
-/* converts the ZDD into the Extra_SymmInfo_t structure */
-extern Extra_SymmInfo_t *  Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
-
-/* computes the classical symmetry information as a ZDD */
-extern DdNode *    Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-extern DdNode *     extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
-extern DdNode *    Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
-extern DdNode *     extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
-/* converts a set of variables into a set of singleton subsets */
-extern DdNode *    Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
-extern DdNode *     extraZddGetSingletons( DdManager * dd, DdNode * bVars );
-/* filters the set of variables using the support of the function */
-extern DdNode *    Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
-extern DdNode *     extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
-
-/* checks the possibility that the two vars are symmetric */
-extern int         Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
-extern DdNode *     extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
-
-/* build the set of all tuples of K variables out of N from the BDD cube */
-extern DdNode *    Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
-extern DdNode *     extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
-/* selects one subset from a ZDD representing the set of subsets */
-extern DdNode *    Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
-extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
-
-/*=== extraBddUnate.c =================================================================*/
-
-extern DdNode *    Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut );
-extern DdNode *    Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut );
-extern DdNode *    Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut );
-
-/*=== extraBddUnate.c =================================================================*/
-
-typedef struct Extra_UnateVar_t_  Extra_UnateVar_t;
-struct Extra_UnateVar_t_ {
-    unsigned    iVar : 30;  // index of the variable
-    unsigned    Pos  :  1;  // 1 if positive unate
-    unsigned    Neg  :  1;  // 1 if negative unate
-};
-
-typedef struct Extra_UnateInfo_t_  Extra_UnateInfo_t;
-struct Extra_UnateInfo_t_ {
-    int nVars;      // the number of variables in the support
-    int nVarsMax;   // the number of variables in the DD manager
-    int nUnate;     // the number of unate variables
-    Extra_UnateVar_t * pVars;    // the array of variables present in the support
-};
-
-/* allocates the data structure */
-extern Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars );
-/* deallocates the data structure */
-extern void        Extra_UnateInfoDissolve( Extra_UnateInfo_t * );
-/* print the contents the data structure */
-extern void        Extra_UnateInfoPrint( Extra_UnateInfo_t * );
-/* converts the ZDD into the Extra_SymmInfo_t structure */
-extern Extra_UnateInfo_t *  Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars );
-/* naive check of unateness of one variable */
-extern int         Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar );
-
-/* computes the unateness information for the function */
-extern Extra_UnateInfo_t *  Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc );
-extern Extra_UnateInfo_t *  Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc );
-
-/* computes the classical symmetry information as a ZDD */
-extern DdNode *    Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-extern DdNode *     extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-
-/* converts a set of variables into a set of singleton subsets */
-extern DdNode *    Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
-extern DdNode *     extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
-
 /*=== extraUtilBitMatrix.c ================================================================*/
 
 typedef struct Extra_BitMat_t_ Extra_BitMat_t;
@@ -391,9 +159,7 @@ extern int         Extra_MmStepReadMemUsage( Extra_MmStep_t * p );
 /*=== extraUtilMisc.c ========================================================*/
 
 /* finds the smallest integer larger or equal than the logarithm */
-extern int         Extra_Base2Log( unsigned Num );
 extern int         Extra_Base2LogDouble( double Num );
-extern int         Extra_Base10Log( unsigned Num );
 /* returns the power of two as a double */
 extern double      Extra_Power2( int Num );
 extern int         Extra_Power3( int Num );
@@ -430,8 +196,6 @@ extern unsigned ** Extra_TruthPerm53();
 extern unsigned ** Extra_TruthPerm54();
 /* bubble sort for small number of entries */
 extern void        Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing );
-/* for independence from CUDD */
-extern unsigned int Cudd_PrimeCopy( unsigned int  p );
 
 /*=== extraUtilCanon.c ========================================================*/
 
@@ -451,10 +215,6 @@ static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char
 
 /*=== extraUtilTruth.c ================================================================*/
 
-//static inline int   Extra_Float2Int( float Val )     { return *((int *)&Val);               }
-//static inline float Extra_Int2Float( int Num )       { return *((float *)&Num);             }
-static inline int   Extra_Float2Int( float Val )     { union { int x; float y; } v; v.y = Val; return v.x;     }
-static inline float Extra_Int2Float( int Num )       { union { int x; float y; } v; v.x = Num; return v.y;     }
 static inline int   Extra_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
 static inline int   Extra_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
 
diff --git a/src/misc/extra/extraBdd.h b/src/misc/extra/extraBdd.h
new file mode 100644
index 00000000..25df14bb
--- /dev/null
+++ b/src/misc/extra/extraBdd.h
@@ -0,0 +1,316 @@
+/**CFile****************************************************************
+
+  FileName    [extraBdd.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Various reusable software utilities.]
+
+  Description [This library contains a number of operators and 
+  traversal routines developed to extend the functionality of 
+  CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/)
+  To compile your code with the library, #include "extra.h" 
+  in your source files and link your project to CUDD and this 
+  library. Use the library at your own risk and with caution. 
+  Note that debugging of some operators still continues.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraBdd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__misc__extra__extra_bdd_h
+#define ABC__misc__extra__extra_bdd_h
+
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "src/misc/st/st.h"
+#include "src/bdd/cudd/cuddInt.h"
+#include "src/misc/extra/extra.h"
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/* constants of the manager */
+#define     b0     Cudd_Not((dd)->one)
+#define     b1              (dd)->one
+#define     z0              (dd)->zero
+#define     z1              (dd)->one
+#define     a0              (dd)->zero
+#define     a1              (dd)->one
+
+// hash key macros
+#define hashKey1(a,TSIZE) \
+((ABC_PTRUINT_T)(a) % TSIZE)
+
+#define hashKey2(a,b,TSIZE) \
+(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
+
+#define hashKey3(a,b,c,TSIZE) \
+(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
+
+#define hashKey4(a,b,c,d,TSIZE) \
+((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
+
+#define hashKey5(a,b,c,d,e,TSIZE) \
+(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
+
+/*===========================================================================*/
+/*     Various Utilities                                                     */
+/*===========================================================================*/
+
+/*=== extraBddAuto.c ========================================================*/
+
+extern DdNode *     Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
+extern DdNode *      extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
+extern DdNode *     Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
+extern DdNode *      extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
+extern DdNode *      extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
+
+extern DdNode *     Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
+extern DdNode *      extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
+
+extern DdNode *     Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace );
+extern DdNode *     Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
+extern DdNode *      extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
+extern DdNode *     Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
+extern DdNode *      extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
+
+extern DdNode *     Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
+extern DdNode *      extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
+extern DdNode *     Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
+extern DdNode *      extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
+
+extern DdNode *     Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
+extern DdNode **    Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
+
+/*=== extraBddCas.c =============================================================*/
+
+/* performs the binary encoding of the set of function using the given vars */
+extern DdNode *     Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
+/* solves the column encoding problem using a sophisticated method */
+extern DdNode *     Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
+/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
+extern st_table *   Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
+/* collects the nodes under the cut starting from the given set of ADD nodes */
+extern int          Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
+/* find the profile of a DD (the number of edges crossing each level) */
+extern int          Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
+
+/*=== extraBddImage.c ================================================================*/
+
+typedef struct Extra_ImageTree_t_  Extra_ImageTree_t;
+extern Extra_ImageTree_t * Extra_bddImageStart( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
+extern void        Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
+extern DdNode *    Extra_bddImageRead( Extra_ImageTree_t * pTree );
+
+typedef struct Extra_ImageTree2_t_  Extra_ImageTree2_t;
+extern Extra_ImageTree2_t * Extra_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
+extern void        Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
+extern DdNode *    Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
+
+/*=== extraBddMisc.c ========================================================*/
+
+extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
+extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
+extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
+extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int nVars );
+extern DdNode *     extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
+extern void         Extra_StopManager( DdManager * dd );
+extern void         Extra_bddPrint( DdManager * dd, DdNode * F );
+extern void         Extra_bddPrintSupport( DdManager * dd, DdNode * F );
+extern void         extraDecomposeCover( DdManager* dd, DdNode*  zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 );
+extern int          Extra_bddSuppSize( DdManager * dd, DdNode * bSupp );
+extern int          Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar );
+extern int          Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 );
+extern int          Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax );
+extern int          Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall );
+extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * support );
+extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
+extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
+extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
+extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
+extern DdNode *     Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f );
+extern int          Extra_bddIsVar( DdNode * bFunc );
+extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
+extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
+extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
+extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
+extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
+extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
+extern DdNode *     Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern DdNode *     extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern int          Extra_bddVarIsInCube( DdNode * bCube, int iVar );
+extern DdNode *     Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
+
+#ifndef ABC_PRB
+#define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
+#endif
+
+/*=== extraBddKmap.c ================================================================*/
+
+/* displays the Karnaugh Map of a function */
+extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
+/* displays the Karnaugh Map of a relation */
+extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
+
+/*=== extraBddSymm.c =================================================================*/
+
+typedef struct Extra_SymmInfo_t_  Extra_SymmInfo_t;
+struct Extra_SymmInfo_t_ {
+    int nVars;      // the number of variables in the support
+    int nVarsMax;   // the number of variables in the DD manager
+    int nSymms;     // the number of pair-wise symmetries
+    int nNodes;     // the number of nodes in a ZDD (if applicable)
+    int * pVars;    // the list of all variables present in the support
+    char ** pSymms; // the symmetry information
+};
+
+/* computes the classical symmetry information for the function - recursive */
+extern Extra_SymmInfo_t *  Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
+/* computes the classical symmetry information for the function - using naive approach */
+extern Extra_SymmInfo_t *  Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
+extern int         Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
+
+/* allocates the data structure */
+extern Extra_SymmInfo_t *  Extra_SymmPairsAllocate( int nVars );
+/* deallocates the data structure */
+extern void        Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
+/* print the contents the data structure */
+extern void        Extra_SymmPairsPrint( Extra_SymmInfo_t * );
+/* converts the ZDD into the Extra_SymmInfo_t structure */
+extern Extra_SymmInfo_t *  Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
+
+/* computes the classical symmetry information as a ZDD */
+extern DdNode *    Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+extern DdNode *     extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
+extern DdNode *    Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
+extern DdNode *     extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
+/* converts a set of variables into a set of singleton subsets */
+extern DdNode *    Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
+extern DdNode *     extraZddGetSingletons( DdManager * dd, DdNode * bVars );
+/* filters the set of variables using the support of the function */
+extern DdNode *    Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
+extern DdNode *     extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
+
+/* checks the possibility that the two vars are symmetric */
+extern int         Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
+extern DdNode *     extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
+
+/* build the set of all tuples of K variables out of N from the BDD cube */
+extern DdNode *    Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
+extern DdNode *     extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
+/* selects one subset from a ZDD representing the set of subsets */
+extern DdNode *    Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
+extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
+
+/*=== extraBddUnate.c =================================================================*/
+
+extern DdNode *    Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut );
+extern DdNode *    Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut );
+extern DdNode *    Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut );
+
+/*=== extraBddUnate.c =================================================================*/
+
+typedef struct Extra_UnateVar_t_  Extra_UnateVar_t;
+struct Extra_UnateVar_t_ {
+    unsigned    iVar : 30;  // index of the variable
+    unsigned    Pos  :  1;  // 1 if positive unate
+    unsigned    Neg  :  1;  // 1 if negative unate
+};
+
+typedef struct Extra_UnateInfo_t_  Extra_UnateInfo_t;
+struct Extra_UnateInfo_t_ {
+    int nVars;      // the number of variables in the support
+    int nVarsMax;   // the number of variables in the DD manager
+    int nUnate;     // the number of unate variables
+    Extra_UnateVar_t * pVars;    // the array of variables present in the support
+};
+
+/* allocates the data structure */
+extern Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars );
+/* deallocates the data structure */
+extern void        Extra_UnateInfoDissolve( Extra_UnateInfo_t * );
+/* print the contents the data structure */
+extern void        Extra_UnateInfoPrint( Extra_UnateInfo_t * );
+/* converts the ZDD into the Extra_SymmInfo_t structure */
+extern Extra_UnateInfo_t *  Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars );
+/* naive check of unateness of one variable */
+extern int         Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar );
+
+/* computes the unateness information for the function */
+extern Extra_UnateInfo_t *  Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc );
+extern Extra_UnateInfo_t *  Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc );
+
+/* computes the classical symmetry information as a ZDD */
+extern DdNode *    Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+extern DdNode *     extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+
+/* converts a set of variables into a set of singleton subsets */
+extern DdNode *    Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
+extern DdNode *     extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
+
+/**AutomaticEnd***************************************************************/
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif /* __EXTRA_H__ */
diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c
index 3b0e2aa0..5fb38aec 100644
--- a/src/misc/extra/extraBddAuto.c
+++ b/src/misc/extra/extraBddAuto.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
index 14de2d2b..0416a0d2 100644
--- a/src/misc/extra/extraBddCas.c
+++ b/src/misc/extra/extraBddCas.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -146,7 +146,7 @@ Extra_bddEncodingBinary(
     DdNode * bResult;
     DdNode * bCube, * bTemp, * bProd;
 
-    assert( nVars >= Extra_Base2Log(nFuncs) );
+    assert( nVars >= Abc_Base2Log(nFuncs) );
 
     bResult = b0;   Cudd_Ref( bResult );
     for ( i = 0; i < nFuncs; i++ )
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
index 38c18f63..46afb4f2 100644
--- a/src/misc/extra/extraBddImage.c
+++ b/src/misc/extra/extraBddImage.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddKmap.c b/src/misc/extra/extraBddKmap.c
index aa8e3764..23bf2224 100644
--- a/src/misc/extra/extraBddKmap.c
+++ b/src/misc/extra/extraBddKmap.c
@@ -20,7 +20,7 @@
 ///       Version 1.0. Started - August 20, 2000        ///
 ///     Version 2.0. Added to EXTRA - July 17, 2001     ///
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 3af9c81e..4512572d 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1917,7 +1917,7 @@ DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF,
     // find the topmost variable in F and G using var order of F
     LevF = cuddI( ddF, Cudd_Regular(bF)->index );
     LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index );
-    Lev  = ABC_MIN( LevF, LevG );
+    Lev  = Abc_MinInt( LevF, LevG );
     assert( Lev < ddF->size );
     bVar = ddF->vars[ddF->invperm[Lev]];
 
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
index 0adcbd2a..9dd2c8e5 100644
--- a/src/misc/extra/extraBddSymm.c
+++ b/src/misc/extra/extraBddSymm.c
@@ -19,7 +19,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddTime.c b/src/misc/extra/extraBddTime.c
index b861d51a..853f8a64 100644
--- a/src/misc/extra/extraBddTime.c
+++ b/src/misc/extra/extraBddTime.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddUnate.c b/src/misc/extra/extraBddUnate.c
index 3aa18e51..9ebdd4e5 100644
--- a/src/misc/extra/extraBddUnate.c
+++ b/src/misc/extra/extraBddUnate.c
@@ -20,7 +20,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index a8542da4..b38befd6 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -580,7 +580,7 @@ void Extra_FileSort( char * pFileName, char * pFileNameOut )
             Begin = i + 1;
         }
     // sort the lines
-    qsort( pLines, nLines, sizeof(char *), Extra_StringCompare );
+    qsort( pLines, nLines, sizeof(char *), (int(*)(const void *,const void *))Extra_StringCompare );
     // write a new file
     pFile = fopen( pFileNameOut, "wb" );
     for ( i = 0; i < nLines; i++ )
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index e4c5acd5..b910f209 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -18,6 +18,8 @@
 
 ***********************************************************************/
 
+#include <math.h>
+
 #include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -58,27 +60,6 @@ static void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[]
 /* Definition of exported functions                                          */
 /*---------------------------------------------------------------------------*/
 
-
-/**Function********************************************************************
-
-  Synopsis    [Finds the smallest integer larger of equal than the logarithm.]
-
-  Description [Returns [Log2(Num)].]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int Extra_Base2Log( unsigned Num )
-{
-    int Res;
-    if ( Num == 0 ) return 0;
-    if ( Num == 1 ) return 1;
-    for ( Res = 0, Num--; Num; Num >>= 1, Res++ );
-    return Res;
-} /* end of Extra_Base2Log */
-
 /**Function********************************************************************
 
   Synopsis    [Finds the smallest integer larger of equal than the logarithm.]
@@ -105,26 +86,6 @@ int Extra_Base2LogDouble( double Num )
 
 /**Function********************************************************************
 
-  Synopsis    [Finds the smallest integer larger of equal than the logarithm.]
-
-  Description [Returns [Log10(Num)].]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int Extra_Base10Log( unsigned Num )
-{
-    int Res;
-    if ( Num == 0 ) return 0;
-    if ( Num == 1 ) return 1;
-    for ( Res = 0, Num--;  Num;  Num /= 10,  Res++ );
-    return Res;
-} /* end of Extra_Base2Log */
-
-/**Function********************************************************************
-
   Synopsis    [Returns the power of two as a double.]
 
   Description []
@@ -2118,41 +2079,6 @@ void Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing )
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Returns the smallest prime larger than the number.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned int Cudd_PrimeCopy( unsigned int  p)
-{
-    int i,pn;
-
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
 
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c
index e7add47f..ab0f5849 100644
--- a/src/misc/extra/extraUtilProgress.c
+++ b/src/misc/extra/extraUtilProgress.c
@@ -20,7 +20,7 @@
 
 #include <stdio.h>
 #include "extra.h"
-#include "main.h"
+#include "src/base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
index bcf3da37..41e02a27 100644
--- a/src/misc/extra/extraUtilReader.c
+++ b/src/misc/extra/extraUtilReader.c
@@ -20,7 +20,7 @@
 
 #include <stdio.h>
 #include "extra.h"
-#include "vec.h"
+#include "src/misc/vec/vec.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/hash/hash.h b/src/misc/hash/hash.h
index 9b5b25d6..6e6c637c 100644
--- a/src/misc/hash/hash.h
+++ b/src/misc/hash/hash.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __HASH_H__
-#define __HASH_H__
+#ifndef ABC__misc__hash__hash_h
+#define ABC__misc__hash__hash_h
 
 
 #ifdef _WIN32
@@ -29,7 +29,7 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "hashInt.h"
 #include "hashFlt.h"
@@ -55,7 +55,7 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 
 int Hash_DefaultHashFunc(int key, int nBins) {
-  return ABC_ABS( ( (key+11)*(key)*7+3 ) % nBins );
+  return Abc_AbsInt( ( (key+11)*(key)*7+3 ) % nBins );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashFlt.h b/src/misc/hash/hashFlt.h
index 74e8503d..c5776b46 100644
--- a/src/misc/hash/hashFlt.h
+++ b/src/misc/hash/hashFlt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __HASH_FLT_H__
-#define __HASH_FLT_H__
+#ifndef ABC__misc__hash__hashFlt_h
+#define ABC__misc__hash__hashFlt_h
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
-#include "extra.h"
+#include "src/misc/extra/extra.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/hash/hashGen.h b/src/misc/hash/hashGen.h
index e26a3c84..eaeef6fd 100644
--- a/src/misc/hash/hashGen.h
+++ b/src/misc/hash/hashGen.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __HASH_GEN_H__
-#define __HASH_GEN_H__
+#ifndef ABC__misc__hash__hashGen_h
+#define ABC__misc__hash__hashGen_h
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
-#include "extra.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/hash/hashInt.h b/src/misc/hash/hashInt.h
index 23947946..81a338fc 100644
--- a/src/misc/hash/hashInt.h
+++ b/src/misc/hash/hashInt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __HASH_INT_H__
-#define __HASH_INT_H__
+#ifndef ABC__misc__hash__hashInt_h
+#define ABC__misc__hash__hashInt_h
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
-#include "extra.h"
+#include "src/misc/extra/extra.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/hash/hashPtr.h b/src/misc/hash/hashPtr.h
index a10fb548..72e2f394 100644
--- a/src/misc/hash/hashPtr.h
+++ b/src/misc/hash/hashPtr.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __HASH_PTR_H__
-#define __HASH_PTR_H__
+#ifndef ABC__misc__hash__hashPtr_h
+#define ABC__misc__hash__hashPtr_h
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
-#include "extra.h"
+#include "src/misc/extra/extra.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/mem/mem.c b/src/misc/mem/mem.c
new file mode 100644
index 00000000..23d8d7ec
--- /dev/null
+++ b/src/misc/mem/mem.c
@@ -0,0 +1,605 @@
+/**CFile****************************************************************
+
+  FileName    [esopMem.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Memory managers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: esopMem.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "mem.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Mem_Fixed_t_
+{
+    // information about individual entries
+    int           nEntrySize;    // the size of one entry
+    int           nEntriesAlloc; // the total number of entries allocated
+    int           nEntriesUsed;  // the number of entries in use
+    int           nEntriesMax;   // the max number of entries in use
+    char *        pEntriesFree;  // the linked list of free entries
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+struct Mem_Flex_t_
+{
+    // information about individual entries
+    int           nEntriesUsed;  // the number of entries allocated
+    char *        pCurrent;      // the current pointer to free memory
+    char *        pEnd;          // the first entry outside the free memory
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+struct Mem_Step_t_
+{
+    int             nMems;              // the number of fixed memory managers employed
+    Mem_Fixed_t **  pMems;              // memory managers: 2^1 words, 2^2 words, etc
+    int             nMapSize;           // the size of the memory array
+    Mem_Fixed_t **  pMap;               // maps the number of bytes into its memory manager
+    int             nLargeChunksAlloc;  // the maximum number of large memory chunks
+    int             nLargeChunks;       // the current number of large memory chunks
+    void **         pLargeChunks;       // the allocated large memory chunks
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory pieces of fixed size.]
+
+  Description [The size of the chunk is computed as the minimum of
+  1024 entries and 64K. Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mem_Fixed_t * Mem_FixedStart( int nEntrySize )
+{
+    Mem_Fixed_t * p;
+
+    p = ABC_ALLOC( Mem_Fixed_t, 1 );
+    memset( p, 0, sizeof(Mem_Fixed_t) );
+
+    p->nEntrySize    = nEntrySize;
+    p->nEntriesAlloc = 0;
+    p->nEntriesUsed  = 0;
+    p->pEntriesFree  = NULL;
+
+    if ( nEntrySize * (1 << 10) < (1<<16) )
+        p->nChunkSize = (1 << 10);
+    else
+        p->nChunkSize = (1<<16) / nEntrySize;
+    if ( p->nChunkSize < 8 )
+        p->nChunkSize = 8;
+
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FixedStop( Mem_Fixed_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+            p->nEntrySize, p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Mem_FixedEntryFetch( Mem_Fixed_t * p )
+{
+    char * pTemp;
+    int i;
+
+    // check if there are still free entries
+    if ( p->nEntriesUsed == p->nEntriesAlloc )
+    { // need to allocate more entries
+        assert( p->pEntriesFree == NULL );
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+        // transform these entries into a linked list
+        pTemp = p->pEntriesFree;
+        for ( i = 1; i < p->nChunkSize; i++ )
+        {
+            *((char **)pTemp) = pTemp + p->nEntrySize;
+            pTemp += p->nEntrySize;
+        }
+        // set the last link
+        *((char **)pTemp) = NULL;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+        // add to the number of entries allocated
+        p->nEntriesAlloc += p->nChunkSize;
+    }
+    // incrememt the counter of used entries
+    p->nEntriesUsed++;
+    if ( p->nEntriesMax < p->nEntriesUsed )
+        p->nEntriesMax = p->nEntriesUsed;
+    // return the first entry in the free entry list
+    pTemp = p->pEntriesFree;
+    p->pEntriesFree = *((char **)pTemp);
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FixedEntryRecycle( Mem_Fixed_t * p, char * pEntry )
+{
+    // decrement the counter of used entries
+    p->nEntriesUsed--;
+    // add the entry to the linked list of free entries
+    *((char **)pEntry) = p->pEntriesFree;
+    p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FixedRestart( Mem_Fixed_t * p )
+{
+    int i;
+    char * pTemp;
+
+    // deallocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        ABC_FREE( p->pChunks[i] );
+    p->nChunks = 1;
+    // transform these entries into a linked list
+    pTemp = p->pChunks[0];
+    for ( i = 1; i < p->nChunkSize; i++ )
+    {
+        *((char **)pTemp) = pTemp + p->nEntrySize;
+        pTemp += p->nEntrySize;
+    }
+    // set the last link
+    *((char **)pTemp) = NULL;
+    // set the free entry list
+    p->pEntriesFree  = p->pChunks[0];
+    // set the correct statistics
+    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
+    p->nMemoryUsed   = 0;
+    p->nEntriesAlloc = p->nChunkSize;
+    p->nEntriesUsed  = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mem_FixedReadMemUsage( Mem_Fixed_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mem_FixedReadMaxEntriesUsed( Mem_Fixed_t * p )
+{
+    return p->nEntriesMax;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates entries of flexible size.]
+
+  Description [Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mem_Flex_t * Mem_FlexStart()
+{
+    Mem_Flex_t * p;
+
+    p = ABC_ALLOC( Mem_Flex_t, 1 );
+    memset( p, 0, sizeof(Mem_Flex_t) );
+
+    p->nEntriesUsed  = 0;
+    p->pCurrent      = NULL;
+    p->pEnd          = NULL;
+
+    p->nChunkSize    = (1 << 12);
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FlexStop( Mem_Flex_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
+            p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
+            p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Mem_FlexEntryFetch( Mem_Flex_t * p, int nBytes )
+{
+    char * pTemp;
+    // check if there are still free entries
+    if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
+    { // need to allocate more entries
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        if ( nBytes > p->nChunkSize )
+        {
+            // resize the chunk size if more memory is requested than it can give
+            // (ideally, this should never happen)
+            p->nChunkSize = 2 * nBytes;
+        }
+        p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
+        p->pEnd     = p->pCurrent + p->nChunkSize;
+        p->nMemoryAlloc += p->nChunkSize;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pCurrent;
+    }
+    assert( p->pCurrent + nBytes <= p->pEnd );
+    // increment the counter of used entries
+    p->nEntriesUsed++;
+    // keep track of the memory used
+    p->nMemoryUsed += nBytes;
+    // return the next entry
+    pTemp = p->pCurrent;
+    p->pCurrent += nBytes;
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FlexRestart( Mem_Flex_t * p )
+{
+    int i;
+    if ( p->nChunks == 0 )
+        return;
+    // deallocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        ABC_FREE( p->pChunks[i] );
+    p->nChunks  = 1;
+    p->nMemoryAlloc = p->nChunkSize;
+    // transform these entries into a linked list
+    p->pCurrent = p->pChunks[0];
+    p->pEnd     = p->pCurrent + p->nChunkSize;
+    p->nEntriesUsed = 0;
+    p->nMemoryUsed = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mem_FlexReadMemUsage( Mem_Flex_t * p )
+{
+    return p->nMemoryUsed;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the hierarchical memory manager.]
+
+  Description [This manager can allocate entries of any size.
+  Iternally they are mapped into the entries with the number of bytes
+  equal to the power of 2. The smallest entry size is 8 bytes. The
+  next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 
+  8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
+  The input parameters "nSteps" says how many fixed memory managers
+  are employed internally. Calling this procedure with nSteps equal
+  to 10 results in 10 hierarchically arranged internal memory managers, 
+  which can allocate up to 4096 (1Kb) entries. Requests for larger 
+  entries are handed over to malloc() and then ABC_FREE()ed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mem_Step_t * Mem_StepStart( int nSteps )
+{
+    Mem_Step_t * p;
+    int i, k;
+    p = ABC_ALLOC( Mem_Step_t, 1 );
+    memset( p, 0, sizeof(Mem_Step_t) );
+    p->nMems = nSteps;
+    // start the fixed memory managers
+    p->pMems = ABC_ALLOC( Mem_Fixed_t *, p->nMems );
+    for ( i = 0; i < p->nMems; i++ )
+        p->pMems[i] = Mem_FixedStart( (8<<i) );
+    // set up the mapping of the required memory size into the corresponding manager
+    p->nMapSize = (4<<p->nMems);
+    p->pMap = ABC_ALLOC( Mem_Fixed_t *, p->nMapSize+1 );
+    p->pMap[0] = NULL;
+    for ( k = 1; k <= 4; k++ )
+        p->pMap[k] = p->pMems[0];
+    for ( i = 0; i < p->nMems; i++ )
+        for ( k = (4<<i)+1; k <= (8<<i); k++ )
+            p->pMap[k] = p->pMems[i];
+//for ( i = 1; i < 100; i ++ )
+//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_StepStop( Mem_Step_t * p, int fVerbose )
+{
+    int i;
+    for ( i = 0; i < p->nMems; i++ )
+        Mem_FixedStop( p->pMems[i], fVerbose );
+    if ( p->pLargeChunks ) 
+    {
+        for ( i = 0; i < p->nLargeChunks; i++ )
+            ABC_FREE( p->pLargeChunks[i] );
+        ABC_FREE( p->pLargeChunks );
+    }
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pMap );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Mem_StepEntryFetch( Mem_Step_t * p, int nBytes )
+{
+    if ( nBytes == 0 )
+        return NULL;
+    if ( nBytes > p->nMapSize )
+    {
+//        printf( "Allocating %d bytes.\n", nBytes );
+//        return ABC_ALLOC( char, nBytes );
+        if ( p->nLargeChunks == p->nLargeChunksAlloc )
+        {
+            if ( p->nLargeChunksAlloc == 0 )
+                p->nLargeChunksAlloc = 32;
+            p->nLargeChunksAlloc *= 2;
+            p->pLargeChunks = (void **)ABC_REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); 
+        }
+        p->pLargeChunks[ p->nLargeChunks++ ] = ABC_ALLOC( char, nBytes );
+        return (char *)p->pLargeChunks[ p->nLargeChunks - 1 ];
+    }
+    return Mem_FixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_StepEntryRecycle( Mem_Step_t * p, char * pEntry, int nBytes )
+{
+    if ( nBytes == 0 )
+        return;
+    if ( nBytes > p->nMapSize )
+    {
+//        ABC_FREE( pEntry );
+        return;
+    }
+    Mem_FixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mem_StepReadMemUsage( Mem_Step_t * p )
+{
+    int i, nMemTotal = 0;
+    for ( i = 0; i < p->nMems; i++ )
+        nMemTotal += p->pMems[i]->nMemoryAlloc;
+    return nMemTotal;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/mem/mem.h b/src/misc/mem/mem.h
new file mode 100644
index 00000000..0f04c160
--- /dev/null
+++ b/src/misc/mem/mem.h
@@ -0,0 +1,75 @@
+/**CFile****************************************************************
+
+  FileName    [mem.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Memory management.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mem.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__aig__mem__mem_h
+#define ABC__aig__mem__mem_h
+
+#include "src/misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Mem_Fixed_t_    Mem_Fixed_t;    
+typedef struct Mem_Flex_t_     Mem_Flex_t;     
+typedef struct Mem_Step_t_     Mem_Step_t;     
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/*=== mem.c ===========================================================*/
+// fixed-size-block memory manager
+extern Mem_Fixed_t * Mem_FixedStart( int nEntrySize );
+extern void          Mem_FixedStop( Mem_Fixed_t * p, int fVerbose );
+extern char *        Mem_FixedEntryFetch( Mem_Fixed_t * p );
+extern void          Mem_FixedEntryRecycle( Mem_Fixed_t * p, char * pEntry );
+extern void          Mem_FixedRestart( Mem_Fixed_t * p );
+extern int           Mem_FixedReadMemUsage( Mem_Fixed_t * p );
+extern int           Mem_FixedReadMaxEntriesUsed( Mem_Fixed_t * p );
+// flexible-size-block memory manager
+extern Mem_Flex_t *  Mem_FlexStart();
+extern void          Mem_FlexStop( Mem_Flex_t * p, int fVerbose );
+extern char *        Mem_FlexEntryFetch( Mem_Flex_t * p, int nBytes );
+extern void          Mem_FlexRestart( Mem_Flex_t * p );
+extern int           Mem_FlexReadMemUsage( Mem_Flex_t * p );
+// hierarchical memory manager
+extern Mem_Step_t *  Mem_StepStart( int nSteps );
+extern void          Mem_StepStop( Mem_Step_t * p, int fVerbose );
+extern char *        Mem_StepEntryFetch( Mem_Step_t * p, int nBytes );
+extern void          Mem_StepEntryRecycle( Mem_Step_t * p, char * pEntry, int nBytes );
+extern int           Mem_StepReadMemUsage( Mem_Step_t * p );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mem/module.make b/src/misc/mem/module.make
new file mode 100644
index 00000000..53d76603
--- /dev/null
+++ b/src/misc/mem/module.make
@@ -0,0 +1 @@
+SRC +=    src/misc/mem/mem.c 
diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h
index 93229470..94b9acd9 100644
--- a/src/misc/mvc/mvc.h
+++ b/src/misc/mvc/mvc.h
@@ -16,8 +16,8 @@
 
 ***********************************************************************/
 
-#ifndef __MVC_H__
-#define __MVC_H__
+#ifndef ABC__misc__mvc__mvc_h
+#define ABC__misc__mvc__mvc_h
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -25,8 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
-#include "extra.h"
-#include "extra.h"
+#include "src/misc/extra/extra.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/nm/nm.h b/src/misc/nm/nm.h
index 015b4ef4..2fa46d73 100644
--- a/src/misc/nm/nm.h
+++ b/src/misc/nm/nm.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __NM_H__
-#define __NM_H__
+#ifndef ABC__misc__nm__nm_h
+#define ABC__misc__nm__nm_h
 
 
 /*
diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c
index e6bfb069..ab334032 100644
--- a/src/misc/nm/nmApi.c
+++ b/src/misc/nm/nmApi.c
@@ -52,7 +52,7 @@ Nm_Man_t * Nm_ManCreate( int nSize )
     p->nSizeFactor   = 2; // determined the limit on the grow of data before the table resizes
     p->nGrowthFactor = 3; // determined how much the table grows after resizing
     // allocate and clean the bins
-    p->nBins = Cudd_PrimeNm(nSize);
+    p->nBins = Abc_PrimeCudd(nSize);
     p->pBinsI2N = ABC_ALLOC( Nm_Entry_t *, p->nBins );
     p->pBinsN2I = ABC_ALLOC( Nm_Entry_t *, p->nBins );
     memset( p->pBinsI2N, 0, sizeof(Nm_Entry_t *) * p->nBins );
diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h
index 0978c6b6..4463b276 100644
--- a/src/misc/nm/nmInt.h
+++ b/src/misc/nm/nmInt.h
@@ -18,16 +18,16 @@
 
 ***********************************************************************/
  
-#ifndef __NM_INT_H__
-#define __NM_INT_H__
+#ifndef ABC__misc__nm__nmInt_h
+#define ABC__misc__nm__nmInt_h
 
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "extra.h"
-#include "vec.h"
+#include "src/misc/extra/extra.h"
+#include "src/misc/vec/vec.h"
 #include "nm.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -78,7 +78,6 @@ extern int              Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry );
 extern int              Nm_ManTableDelete( Nm_Man_t * p, int ObjId );
 extern Nm_Entry_t *     Nm_ManTableLookupId( Nm_Man_t * p, int ObjId );
 extern Nm_Entry_t *     Nm_ManTableLookupName( Nm_Man_t * p, char * pName, int Type );
-extern unsigned int     Cudd_PrimeNm( unsigned int p );
 
 
 
diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c
index 29c751a6..4c2b7a0a 100644
--- a/src/misc/nm/nmTable.c
+++ b/src/misc/nm/nmTable.c
@@ -260,7 +260,7 @@ void Nm_ManResize( Nm_Man_t * p )
 
 clk = clock();
     // get the new table size
-    nBinsNew = Cudd_PrimeCopy( p->nGrowthFactor * p->nBins ); 
+    nBinsNew = Abc_PrimeCudd( p->nGrowthFactor * p->nBins ); 
     // allocate a new array
     pBinsNewI2N = ABC_ALLOC( Nm_Entry_t *, nBinsNew );
     pBinsNewN2I = ABC_ALLOC( Nm_Entry_t *, nBinsNew );
@@ -299,41 +299,6 @@ clk = clock();
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    [Returns the smallest prime larger than the number.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned int Cudd_PrimeNm( unsigned int  p)
-{
-    int i,pn;
-
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/misc/st/st.c b/src/misc/st/st.c
index cadddb0b..2e2edc53 100644
--- a/src/misc/st/st.c
+++ b/src/misc/st/st.c
@@ -9,6 +9,7 @@
  */
 #include <stdio.h>
 #include <stdlib.h>
+#include <string.h>
 
 #include "st.h"
 
@@ -16,7 +17,7 @@ ABC_NAMESPACE_IMPL_START
 
 
 #define ST_NUMCMP(x,y) ((x) != (y))
-#define ST_NUMHASH(x,size) (ABC_ABS((long)x)%(size))
+#define ST_NUMHASH(x,size) (Abc_AbsInt((long)x)%(size))
 //#define ST_PTRHASH(x,size) ((int)((ABC_PTRUINT_T)(x)>>2)%size)  // 64-bit bug fix 9/17/2007
 #define ST_PTRHASH(x,size) ((int)(((ABC_PTRUINT_T)(x)>>2)%size))
 #define EQUAL(func, x, y) \
diff --git a/src/misc/st/st.h b/src/misc/st/st.h
index d16fc4b6..50a8440e 100644
--- a/src/misc/st/st.h
+++ b/src/misc/st/st.h
@@ -11,10 +11,11 @@
 
 /* /projects/hsis/CVS/utilities/st/st.h,v 1.1 1993/07/29 01:00:21 serdar Exp */
 
-#ifndef ST_INCLUDED
+#ifndef ABC__misc__st__st_h
+#define ABC__misc__st__st_h
 #define ST_INCLUDED
 
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c
index 1305d5b0..dc883a67 100644
--- a/src/misc/st/stmm.c
+++ b/src/misc/st/stmm.c
@@ -8,14 +8,14 @@
  *
  */
 #include <stdio.h>
-#include "extra.h"
+#include "src/misc/extra/extra.h"
 #include "stmm.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
 #define STMM_NUMCMP(x,y) ((x) != (y))
-#define STMM_NUMHASH(x,size) (ABC_ABS((long)x)%(size))
+#define STMM_NUMHASH(x,size) (Abc_AbsInt((long)x)%(size))
 //#define STMM_PTRHASH(x,size) ((int)((ABC_PTRUINT_T)(x)>>2)%size) //  64-bit bug fix 9/17/2007
 #define STMM_PTRHASH(x,size) ((int)(((ABC_PTRUINT_T)(x)>>2)%size))
 #define EQUAL(func, x, y) \
diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h
index eee90073..1853ce36 100644
--- a/src/misc/st/stmm.h
+++ b/src/misc/st/stmm.h
@@ -11,10 +11,10 @@
 
 /* /projects/hsis/CVS/utilities/st/st.h,v 1.1 1993/07/29 01:00:21 serdar Exp */
 
-#ifndef STMM_INCLUDED
-#define STMM_INCLUDED
+#ifndef ABC__misc__st__stmm_h
+#define ABC__misc__st__stmm_h
 
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/tim/module.make b/src/misc/tim/module.make
new file mode 100644
index 00000000..62a3ede5
--- /dev/null
+++ b/src/misc/tim/module.make
@@ -0,0 +1 @@
+SRC +=    src/misc/tim/tim.c
diff --git a/src/misc/tim/tim.c b/src/misc/tim/tim.c
new file mode 100644
index 00000000..fe5f214d
--- /dev/null
+++ b/src/misc/tim/tim.c
@@ -0,0 +1,996 @@
+/**CFile****************************************************************
+
+  FileName    [tim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [A timing manager.]
+
+  Synopsis    [Representation of timing information.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: tim.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "src/misc/vec/vec.h"
+#include "src/misc/mem/mem.h"
+#include "tim.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Tim_Box_t_           Tim_Box_t;
+typedef struct Tim_Obj_t_           Tim_Obj_t;
+
+// timing manager
+struct Tim_Man_t_
+{
+    Vec_Ptr_t *      vBoxes;         // the timing boxes
+    Vec_Ptr_t *      vDelayTables;   // pointers to the delay tables
+    Mem_Flex_t *     pMemObj;        // memory manager for boxes
+    int              nTravIds;       // traversal ID of the manager
+    int              fUseTravId;     // enables the use of traversal ID
+    int              nCis;           // the number of PIs
+    int              nCos;           // the number of POs
+    Tim_Obj_t *      pCis;           // timing info for the PIs
+    Tim_Obj_t *      pCos;           // timing info for the POs
+};
+
+// timing box
+struct Tim_Box_t_
+{
+    int              iBox;           // the unique ID of this box
+    int              TravId;         // traversal ID of this box
+    int              nInputs;        // the number of box inputs (POs)
+    int              nOutputs;       // the number of box outputs (PIs)
+    float *          pDelayTable;    // delay for each input->output path
+    int              Inouts[0];      // the int numbers of PIs and POs
+};
+
+// timing object
+struct Tim_Obj_t_
+{
+    int              Id;             // the ID of this object
+    int              TravId;         // traversal ID of this object
+    int              iObj2Box;       // mapping of the object into its box
+    int              iObj2Num;       // mapping of the object into its number in the box
+    float            timeArr;        // arrival time of the object
+    float            timeReq;        // required time of the object
+};
+
+static inline Tim_Obj_t * Tim_ManCi( Tim_Man_t * p, int i )                           { assert( i < p->nCis ); return p->pCis + i;      }
+static inline Tim_Obj_t * Tim_ManCo( Tim_Man_t * p, int i )                           { assert( i < p->nCos ); return p->pCos + i;      }
+static inline Tim_Box_t * Tim_ManBox( Tim_Man_t * p, int i )                          { return (Tim_Box_t *)Vec_PtrEntry(p->vBoxes, i); }
+
+static inline Tim_Box_t * Tim_ManCiBox( Tim_Man_t * p, int i )                        { return Tim_ManCi(p,i)->iObj2Box < 0 ? NULL : (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, Tim_ManCi(p,i)->iObj2Box ); }
+static inline Tim_Box_t * Tim_ManCoBox( Tim_Man_t * p, int i )                        { return Tim_ManCo(p,i)->iObj2Box < 0 ? NULL : (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, Tim_ManCo(p,i)->iObj2Box ); }
+
+static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i )   { assert( i < pBox->nInputs  ); return p->pCos + pBox->Inouts[i];               }
+static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i )  { assert( i < pBox->nOutputs ); return p->pCis + pBox->Inouts[pBox->nInputs+i]; }
+
+#define Tim_ManBoxForEachInput( p, pBox, pObj, i )                               \
+    for ( i = 0; (i < (pBox)->nInputs) && ((pObj) = Tim_ManBoxInput(p, pBox, i)); i++ )
+#define Tim_ManBoxForEachOutput( p, pBox, pObj, i )                              \
+    for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ )
+
+#define Tim_ManForEachCi( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nCis) && ((pObj) = (p)->pCis + i); i++ )              \
+        if ( pObj->iObj2Box >= 0 ) {} else 
+#define Tim_ManForEachCo( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nCos) && ((pObj) = (p)->pCos + i); i++ )              \
+        if ( pObj->iObj2Box >= 0 ) {} else 
+#define Tim_ManForEachBox( p, pBox, i )                                          \
+    Vec_PtrForEachEntry( Tim_Box_t *, p->vBoxes, pBox, i )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManStart( int nCis, int nCos )
+{
+    Tim_Man_t * p;
+    int i;
+    p = ABC_ALLOC( Tim_Man_t, 1 );
+    memset( p, 0, sizeof(Tim_Man_t) );
+    p->pMemObj = Mem_FlexStart();
+    p->vBoxes  = Vec_PtrAlloc( 100 );
+    p->nCis = nCis;
+    p->nCos = nCos;
+    p->pCis = ABC_ALLOC( Tim_Obj_t, nCis );
+    memset( p->pCis, 0, sizeof(Tim_Obj_t) * nCis );
+    p->pCos = ABC_ALLOC( Tim_Obj_t, nCos );
+    memset( p->pCos, 0, sizeof(Tim_Obj_t) * nCos );
+    for ( i = 0; i < nCis; i++ )
+    {
+        p->pCis[i].Id = i;
+        p->pCis[i].iObj2Box = p->pCis[i].iObj2Num = -1;
+        p->pCis[i].timeReq = TIM_ETERNITY;
+        p->pCis[i].timeArr = 0.0;
+        p->pCis[i].TravId = 0;
+    }
+    for ( i = 0; i < nCos; i++ )
+    {
+        p->pCos[i].Id = i;
+        p->pCos[i].iObj2Box = p->pCos[i].iObj2Num = -1;
+        p->pCos[i].timeReq = TIM_ETERNITY;
+        p->pCos[i].timeArr = 0.0;
+        p->pCos[i].TravId = 0;
+    }
+    p->fUseTravId = 1;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the timing manager.]
+
+  Description [Derives discrete-delay-model timing manager. 
+  Useful for AIG optimization with approximate timing information.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    float * pDelayTableNew;
+    int i, k;
+    pNew = Tim_ManStart( p->nCis, p->nCos );
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis );
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos );
+    for ( k = 0; k < p->nCis; k++ )
+        pNew->pCis[k].TravId = 0;
+    for ( k = 0; k < p->nCos; k++ )
+        pNew->pCos[k].TravId = 0;
+    if ( fDiscrete )
+    {
+        for ( k = 0; k < p->nCis; k++ )
+            pNew->pCis[k].timeArr = 0.0; // modify here
+        // modify the required times
+    }
+    pNew->vDelayTables = Vec_PtrAlloc( 100 );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+//printf( "%d %d\n", pBox->nInputs, pBox->nOutputs );
+        pDelayTableNew = ABC_ALLOC( float, pBox->nInputs * pBox->nOutputs );
+        Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+        if ( fDiscrete )
+        {
+            for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
+                pDelayTableNew[k] = 1.0; // modify here
+
+///// begin part of improved CIN/COUT propagation
+            for ( k = 0; k < pBox->nInputs; k++ )  // fill in the first row
+               pDelayTableNew[k] = 0.5;
+            for ( k = 0; k < pBox->nOutputs; k++ ) // fill in the first column
+               pDelayTableNew[k*pBox->nInputs] = 0.5;
+            pDelayTableNew[0] = 0.0; // fill in the first entry 
+///// end part of improved CIN/COUT propagation
+
+            /// change
+//            pDelayTableNew[0] = 0.0;
+            /// change
+        }
+        else
+            memcpy( pDelayTableNew, pBox->pDelayTable, sizeof(float) * pBox->nInputs * pBox->nOutputs );
+        Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
+            pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the timing manager.]
+
+  Description [Derives unit-delay-model timing manager. 
+  Useful for levelizing the network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    float * pDelayTableNew;
+    int i, k;
+    pNew = Tim_ManStart( p->nCis, p->nCos );
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis );
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos );
+    for ( k = 0; k < p->nCis; k++ )
+    {
+        pNew->pCis[k].TravId = 0;
+        pNew->pCis[k].timeArr = 0.0; 
+    }
+    for ( k = 0; k < p->nCos; k++ )
+        pNew->pCos[k].TravId = 0;
+    pNew->vDelayTables = Vec_PtrAlloc( 100 );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+        pDelayTableNew = ABC_ALLOC( float, pBox->nInputs * pBox->nOutputs );
+        Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+        for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
+            pDelayTableNew[k] = 1.0;
+        Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
+            pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the timing manager.]
+
+  Description [Derives the approximate timing manager with realistic delays
+  but without white-boxes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDupApprox( Tim_Man_t * p )
+{
+    Tim_Man_t * pNew;
+    int k;
+    pNew = Tim_ManStart( p->nCis, p->nCos );
+    for ( k = 0; k < p->nCis; k++ )
+        if ( p->pCis[k].iObj2Box == -1 )
+            pNew->pCis[k].timeArr = p->pCis[k].timeArr;
+        else
+            pNew->pCis[k].timeArr = p->pCis[k].timeReq;
+    for ( k = 0; k < p->nCos; k++ )
+        pNew->pCos[k].timeReq = p->pCos[k].timeReq;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManStop( Tim_Man_t * p )
+{
+    float * pTable;
+    int i;
+    if ( p->vDelayTables )
+    {
+        Vec_PtrForEachEntry( float *, p->vDelayTables, pTable, i )
+            ABC_FREE( pTable );
+        Vec_PtrFree( p->vDelayTables );
+    }
+    Vec_PtrFree( p->vBoxes );
+    Mem_FlexStop( p->pMemObj, 0 );
+    ABC_FREE( p->pCis );
+    ABC_FREE( p->pCos );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManStopP( Tim_Man_t ** p )
+{
+    if ( *p == NULL )
+        return;
+    Tim_ManStop( *p );
+    *p = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManPrint( Tim_Man_t * p )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    printf( "TIMING INFORMATION:\n" );
+    Tim_ManForEachCi( p, pObj, i )
+        printf( "pi%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+    Tim_ManForEachCo( p, pObj, i )
+        printf( "po%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+        printf( "*** Box %3d :  Ins = %d. Outs = %d.\n", i, pBox->nInputs, pBox->nOutputs );
+        printf( "Delay table:" );
+        for ( i = 0; i < pBox->nInputs * pBox->nOutputs; i++ )
+            printf( " %5.3f", pBox->pDelayTable[i] );
+        printf( "\n" );
+        Tim_ManBoxForEachInput( p, pBox, pObj, i )
+            printf( "box-inp%3d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+        Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+            printf( "box-out%3d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Disables the use of the traversal ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManTravIdDisable( Tim_Man_t * p )
+{
+    p->fUseTravId = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Enables the use of the traversal ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManTravIdEnable( Tim_Man_t * p )
+{
+    p->fUseTravId = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Label box inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Label box outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Label box inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetPreviousTravIdBoxInputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Label box outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetPreviousTravIdBoxOutputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManIsCiTravIdCurrent( Tim_Man_t * p, int iCi )
+{
+    assert( iCi < p->nCis );
+    assert( p->fUseTravId );
+    return p->pCis[iCi].TravId == p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManIsCoTravIdCurrent( Tim_Man_t * p, int iCo )
+{
+    assert( iCo < p->nCos );
+    assert( p->fUseTravId );
+    return p->pCos[iCo].TravId == p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the vector of timing tables associated with the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables )
+{
+    assert( p->vDelayTables == NULL );
+    p->vDelayTables = vDelayTables;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable )
+{
+    Tim_Box_t * pBox;
+    int i;
+    pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
+    memset( pBox, 0, sizeof(Tim_Box_t) );
+    pBox->iBox = Vec_PtrSize( p->vBoxes );
+    Vec_PtrPush( p->vBoxes, pBox );
+    pBox->pDelayTable = pDelayTable;
+    pBox->nInputs  = nIns;
+    pBox->nOutputs = nOuts;
+    for ( i = 0; i < nIns; i++ )
+    {
+        assert( pIns[i] < p->nCos );
+        pBox->Inouts[i] = pIns[i];
+        p->pCos[pIns[i]].iObj2Box = pBox->iBox;
+        p->pCos[pIns[i]].iObj2Num = i;
+    }
+    for ( i = 0; i < nOuts; i++ )
+    {
+        assert( pOuts[i] < p->nCis );
+        pBox->Inouts[nIns+i] = pOuts[i];
+        p->pCis[pOuts[i]].iObj2Box = pBox->iBox;
+        p->pCis[pOuts[i]].iObj2Num = i;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable )
+{
+    Tim_Box_t * pBox;
+    int i;
+
+    pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
+    memset( pBox, 0, sizeof(Tim_Box_t) );
+    pBox->iBox = Vec_PtrSize( p->vBoxes );
+    Vec_PtrPush( p->vBoxes, pBox );
+    pBox->pDelayTable = pDelayTable;
+    pBox->nInputs  = nIns;
+    pBox->nOutputs = nOuts;
+    for ( i = 0; i < nIns; i++ )
+    {
+        assert( firstIn+i < p->nCos );
+        pBox->Inouts[i] = firstIn+i;
+        p->pCos[firstIn+i].iObj2Box = pBox->iBox;
+        p->pCos[firstIn+i].iObj2Num = i;
+    }
+    for ( i = 0; i < nOuts; i++ )
+    {
+        assert( firstOut+i < p->nCis );
+        pBox->Inouts[nIns+i] = firstOut+i;
+        p->pCis[firstOut+i].iObj2Box = pBox->iBox;
+        p->pCis[firstOut+i].iObj2Num = i;
+    }
+//    if ( pBox->iBox < 50 )
+//    printf( "%4d  %4d  %4d  %4d  \n", firstIn, nIns, firstOut, nOuts );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the trav ID of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManIncrementTravId( Tim_Man_t * p )
+{
+    int i;
+    if ( p->nTravIds >= (1<<30)-1 )
+    {
+        p->nTravIds = 0;
+        for ( i = 0; i < p->nCis; i++ )
+            p->pCis[i].TravId = 0;
+        for ( i = 0; i < p->nCos; i++ )
+            p->pCos[i].TravId = 0;
+    }
+    assert( p->nTravIds < (1<<30)-1 );
+    p->nTravIds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes arrival time of the PI.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManInitCiArrival( Tim_Man_t * p, int iCi, float Delay )
+{
+    assert( iCi < p->nCis );
+    p->pCis[iCi].timeArr = Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Delay )
+{
+    assert( iCo < p->nCos );
+    p->pCos[iCo].timeReq = Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay )
+{
+    assert( iCo < p->nCos );
+    assert( !p->fUseTravId || p->pCos[iCo].TravId != p->nTravIds );
+    p->pCos[iCo].timeArr = Delay;
+    p->pCos[iCo].TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates arrival time of the PI.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay )
+{
+    assert( iCi < p->nCis );
+    assert( !p->fUseTravId || p->pCis[iCi].TravId != p->nTravIds );
+    p->pCis[iCi].timeReq = Delay;
+    p->pCis[iCi].TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay )
+{
+    assert( iCo < p->nCos );
+    assert( !p->fUseTravId || p->pCos[iCo].TravId != p->nTravIds );
+    p->pCos[iCo].timeReq = Delay;
+    p->pCos[iCo].TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the correct required times for all POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay )
+{
+    Tim_Obj_t * pObj;
+    int i;
+    Tim_ManForEachCi( p, pObj, i )
+        Tim_ManInitCiArrival( p, i, Delay );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the correct required times for all POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay )
+{
+    Tim_Obj_t * pObj;
+    int i;
+    Tim_ManForEachCo( p, pObj, i )
+    {
+        Tim_ManSetCoRequired( p, i, Delay );
+//printf( "%d ", i );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns PI arrival time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObjThis, * pObj, * pObjRes;
+    float * pDelays, DelayBest;
+    int i, k;
+    // consider the already processed PI
+    pObjThis = Tim_ManCi( p, iCi );
+    if ( p->fUseTravId && pObjThis->TravId == p->nTravIds )
+        return pObjThis->timeArr;
+    pObjThis->TravId = p->nTravIds;
+    // consider the main PI
+    pBox = Tim_ManCiBox( p, iCi );
+    if ( pBox == NULL )
+        return pObjThis->timeArr;
+    // update box timing
+    pBox->TravId = p->nTravIds;
+    // get the arrival times of the inputs of the box (POs)
+    if ( p->fUseTravId )
+    Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        if ( pObj->TravId != p->nTravIds )
+            printf( "Tim_ManGetCiArrival(): Input arrival times of the box are not up to date!\n" );
+    // compute the arrival times for each output of the box (PIs)
+    Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
+    {
+        pDelays = pBox->pDelayTable + i * pBox->nInputs;
+        DelayBest = -TIM_ETERNITY;
+        Tim_ManBoxForEachInput( p, pBox, pObj, k )
+            DelayBest = Abc_MaxInt( DelayBest, pObj->timeArr + pDelays[k] );
+        pObjRes->timeArr = DelayBest;
+        pObjRes->TravId = p->nTravIds;
+    }
+    return pObjThis->timeArr;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns PO required time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObjThis, * pObj, * pObjRes;
+    float * pDelays, DelayBest;
+    int i, k;
+    // consider the already processed PO
+    pObjThis = Tim_ManCo( p, iCo );
+    if ( p->fUseTravId && pObjThis->TravId == p->nTravIds )
+        return pObjThis->timeReq;
+    pObjThis->TravId = p->nTravIds;
+    // consider the main PO
+    pBox = Tim_ManCoBox( p, iCo );
+    if ( pBox == NULL )
+        return pObjThis->timeReq;
+    // update box timing
+    pBox->TravId = p->nTravIds;
+    // get the required times of the outputs of the box (PIs)
+    if ( p->fUseTravId )
+    Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        if ( pObj->TravId != p->nTravIds )
+            printf( "Tim_ManGetCoRequired(): Output required times of the box are not up to date!\n" );
+    // compute the required times for each input of the box (POs)
+    Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
+    {
+        DelayBest = TIM_ETERNITY;
+        Tim_ManBoxForEachOutput( p, pBox, pObj, k )
+        {
+            pDelays = pBox->pDelayTable + k * pBox->nInputs;
+            DelayBest = Abc_MinInt( DelayBest, pObj->timeReq - pDelays[i] );
+        }
+        pObjRes->timeReq = DelayBest;
+        pObjRes->TravId = p->nTravIds;
+    }
+    return pObjThis->timeReq;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the box number for the given input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxForCi( Tim_Man_t * p, int iCi )
+{
+    if ( iCi >= p->nCis )
+        return -1;
+    return p->pCis[iCi].iObj2Box;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the box number for the given output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxForCo( Tim_Man_t * p, int iCo )
+{
+    if ( iCo >= p->nCos )
+        return -1;
+    return p->pCos[iCo].iObj2Box;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->Inouts[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->Inouts[pBox->nInputs];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->nInputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->nOutputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManChangeForAdders( Tim_Man_t * p )
+{
+    Tim_Box_t * pBox;
+    int i;
+    Tim_ManForEachBox( p, pBox, i )
+        pBox->pDelayTable[0] = 0.0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h
new file mode 100644
index 00000000..d921bcc5
--- /dev/null
+++ b/src/misc/tim/tim.h
@@ -0,0 +1,110 @@
+/**CFile****************************************************************
+
+  FileName    [tim.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [A timing manager.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: tim.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__aig__tim__tim_h
+#define ABC__aig__tim__tim_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Tim_Man_t_           Tim_Man_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define TIM_ETERNITY 10000
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     SEQUENTIAL ITERATORS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== time.c ===========================================================*/
+extern Tim_Man_t *     Tim_ManStart( int nCis, int nCos );
+extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fDiscrete );
+extern Tim_Man_t *     Tim_ManDupUnit( Tim_Man_t * p );
+extern Tim_Man_t *     Tim_ManDupApprox( Tim_Man_t * p );
+extern void            Tim_ManStop( Tim_Man_t * p );
+extern void            Tim_ManStopP( Tim_Man_t ** p );
+extern void            Tim_ManPrint( Tim_Man_t * p );
+extern void            Tim_ManTravIdDisable( Tim_Man_t * p );
+extern void            Tim_ManTravIdEnable( Tim_Man_t * p );
+extern void            Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox );
+extern void            Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox );
+extern void            Tim_ManSetPreviousTravIdBoxInputs( Tim_Man_t * p, int iBox );
+extern void            Tim_ManSetPreviousTravIdBoxOutputs( Tim_Man_t * p, int iBox );
+extern int             Tim_ManIsCiTravIdCurrent( Tim_Man_t * p, int iCi );
+extern int             Tim_ManIsCoTravIdCurrent( Tim_Man_t * p, int iCo );
+extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
+extern void            Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
+extern void            Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
+extern void            Tim_ManIncrementTravId( Tim_Man_t * p );
+extern void            Tim_ManInitCiArrival( Tim_Man_t * p, int iCi, float Delay );
+extern void            Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay );
+extern void            Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay );
+extern void            Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay );
+extern float           Tim_ManGetCiArrival( Tim_Man_t * p, int iCi );
+extern float           Tim_ManGetCoRequired( Tim_Man_t * p, int iCo );
+extern int             Tim_ManBoxForCi( Tim_Man_t * p, int iCo );
+extern int             Tim_ManBoxForCo( Tim_Man_t * p, int iCi );
+extern int             Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxInputNum( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox );
+extern void            Tim_ManChangeForAdders( Tim_Man_t * p );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 61aa9327..83c86f28 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __ABC_GLOBAL_H__
-#define __ABC_GLOBAL_H__
+#ifndef ABC__misc__util__abc_global_h
+#define ABC__misc__util__abc_global_h
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
@@ -200,11 +200,7 @@ typedef ABC_UINT64_T word;
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-
-#define ABC_ABS(a)            ((a) < 0 ? -(a) : (a))
-#define ABC_MAX(a,b)        ((a) > (b) ? (a) : (b))
-#define ABC_MIN(a,b)        ((a) < (b) ? (a) : (b))
-#define ABC_INFINITY        (100000000)
+#define ABC_INFINITY    (100000000)
 
 #define ABC_PRT(a,t)    (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
 #define ABC_PRTr(a,t)   (printf("%s = ", (a)), printf("%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
@@ -236,17 +232,37 @@ ABC_NAMESPACE_HEADER_START
          ((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num)))))
 #endif
 
-static inline int    Abc_AbsInt( int a        )          { return a < 0 ? -a : a; }
-static inline int    Abc_MaxInt( int a, int b )          { return a > b ?  a : b; }
-static inline int    Abc_MinInt( int a, int b )          { return a < b ?  a : b; }
-static inline word   Abc_MaxWord( word a, word b )       { return a > b ?  a : b; }
-static inline word   Abc_MinWord( word a, word b )       { return a < b ?  a : b; }
-static inline float  Abc_AbsFloat( float a          )    { return a < 0 ? -a : a; }
-static inline float  Abc_MaxFloat( float a, float b )    { return a > b ?  a : b; }
-static inline float  Abc_MinFloat( float a, float b )    { return a < b ?  a : b; }
-static inline double Abc_AbsDouble( double a           ) { return a < 0 ? -a : a; }
-static inline double Abc_MaxDouble( double a, double b ) { return a > b ?  a : b; }
-static inline double Abc_MinDouble( double a, double b ) { return a < b ?  a : b; }
+static inline int      Abc_AbsInt( int a        )             { return a < 0 ? -a : a; }
+static inline int      Abc_MaxInt( int a, int b )             { return a > b ?  a : b; }
+static inline int      Abc_MinInt( int a, int b )             { return a < b ?  a : b; }
+static inline word     Abc_MaxWord( word a, word b )          { return a > b ?  a : b; }
+static inline word     Abc_MinWord( word a, word b )          { return a < b ?  a : b; }
+static inline float    Abc_AbsFloat( float a          )       { return a < 0 ? -a : a; }
+static inline float    Abc_MaxFloat( float a, float b )       { return a > b ?  a : b; }
+static inline float    Abc_MinFloat( float a, float b )       { return a < b ?  a : b; }
+static inline double   Abc_AbsDouble( double a           )    { return a < 0 ? -a : a; }
+static inline double   Abc_MaxDouble( double a, double b )    { return a > b ?  a : b; }
+static inline double   Abc_MinDouble( double a, double b )    { return a < b ?  a : b; }
+
+static inline int      Abc_Float2Int( float Val )             { union { int x; float y; } v; v.y = Val; return v.x;         }
+static inline float    Abc_Int2Float( int Num )               { union { int x; float y; } v; v.x = Num; return v.y;         }
+static inline int      Abc_Base2Log( unsigned n )             { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
+static inline int      Abc_Base10Log( unsigned n )            { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
+static inline int      Abc_Base16Log( unsigned n )            { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ); return r; }
+static inline char *   Abc_UtilStrsav( char * s )             { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL;  }
+static inline int      Abc_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);                       }
+static inline int      Abc_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));                 }
+static inline int      Abc_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;                   }
+static inline void     Abc_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                               }
+static inline void     Abc_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                               }
+static inline unsigned Abc_InfoMask( int nVar )               { return (~(unsigned)0) >> (32-nVar);                         }
+
+static inline int      Abc_Var2Lit( int Var, int fCompl )     { return Var + Var + fCompl; }
+static inline int      Abc_Lit2Var( int Lit )                 { return Lit >> 1;           }
+static inline int      Abc_LitIsCompl( int Lit )              { return Lit & 1;            }
+static inline int      Abc_LitNot( int Lit )                  { return Lit ^ 1;            }
+static inline int      Abc_LitNotCond( int Lit, int c )       { return Lit ^ (int)(c > 0); }
+static inline int      Abc_LitRegular( int Lit )              { return Lit & ~01;          }
 
 enum Abc_VerbLevel 
 {
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 37205543..80d8e141 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -32,10 +32,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int   Abc_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);     }
-static inline int   Abc_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
-static inline void  Abc_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));             }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index 556f2268..b45cd27b 100644
--- a/src/misc/util/utilCex.h
+++ b/src/misc/util/utilCex.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __UTIL_CEX_H__
-#define __UTIL_CEX_H__
+#ifndef ABC__misc__util__utilCex_h
+#define ABC__misc__util__utilCex_h
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
diff --git a/src/misc/util/utilMem.h b/src/misc/util/utilMem.h
index 1f8432c1..af5873c0 100644
--- a/src/misc/util/utilMem.h
+++ b/src/misc/util/utilMem.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __UTIL_INT_H__
-#define __UTIL_INT_H__
+#ifndef ABC__misc__util__utilMem_h
+#define ABC__misc__util__utilMem_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilNam.c b/src/misc/util/utilNam.c
index 79565186..c6399818 100644
--- a/src/misc/util/utilNam.c
+++ b/src/misc/util/utilNam.c
@@ -25,7 +25,7 @@
 #include <assert.h>
 
 #include "abc_global.h"
-#include "vec.h"
+#include "src/misc/vec/vec.h"
 #include "utilNam.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -304,7 +304,7 @@ void Abc_NamStrHashResize( Abc_Nam_t * p )
     char * pThis;
     int * piPlace, * pBinsOld, iHandleOld, i;//, clk = clock();
     assert( p->pBins != NULL );
-//    Abc_Print( 1, "Resizing names manager hash table from %6d to %6d. ", p->nBins, Gia_PrimeCudd( 3 * p->nBins ) );
+//    Abc_Print( 1, "Resizing names manager hash table from %6d to %6d. ", p->nBins, Abc_PrimeCudd( 3 * p->nBins ) );
     // replace the table
     pBinsOld = p->pBins;
     p->nBins = Abc_PrimeCudd( 3 * p->nBins ); 
diff --git a/src/misc/util/utilNam.h b/src/misc/util/utilNam.h
index ae2c099c..fd29e537 100644
--- a/src/misc/util/utilNam.h
+++ b/src/misc/util/utilNam.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __UTIL_NAM_H__
-#define __UTIL_NAM_H__
+#ifndef ABC__misc__util__utilNam_h
+#define ABC__misc__util__utilNam_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilSignal.c b/src/misc/util/utilSignal.c
index 2886f69b..af0948bd 100644
--- a/src/misc/util/utilSignal.c
+++ b/src/misc/util/utilSignal.c
@@ -20,6 +20,8 @@
 
 #include <stdio.h>
 #include <stdlib.h>
+#include <string.h>
+
 #include "abc_global.h"
 #include "utilSignal.h"
 
diff --git a/src/misc/util/utilSignal.h b/src/misc/util/utilSignal.h
index 0ac87290..b29def80 100644
--- a/src/misc/util/utilSignal.h
+++ b/src/misc/util/utilSignal.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __UTIL_SIGNAL_H__
-#define __UTIL_SIGNAL_H__
+#ifndef ABC__misc__util__utilSignal_h
+#define ABC__misc__util__utilSignal_h
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index 1a734f03..9c702bfe 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __UTIL_HACK_H__
-#define __UTIL_HACK_H__
+#ifndef ABC__misc__util__util_hack_h
+#define ABC__misc__util__util_hack_h
 
 #include <stdio.h>
 #include <stdlib.h>
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index da5fc866..c02cafeb 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -18,15 +18,15 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_H__
-#define __VEC_H__
+#ifndef ABC__misc__vec__vec_h
+#define ABC__misc__vec__vec_h
 
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "vecInt.h"
 #include "vecFlt.h"
diff --git a/src/misc/vec/vecAtt.h b/src/misc/vec/vecAtt.h
index 60b2d17a..63dd4779 100644
--- a/src/misc/vec/vecAtt.h
+++ b/src/misc/vec/vecAtt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_ATT_H__
-#define __VEC_ATT_H__
+#ifndef ABC__misc__vec__vecAtt_h
+#define ABC__misc__vec__vecAtt_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecBit.h b/src/misc/vec/vecBit.h
index 802486d9..7f0d7409 100644
--- a/src/misc/vec/vecBit.h
+++ b/src/misc/vec/vecBit.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_BIT_H__
-#define __VEC_BIT_H__
+#ifndef ABC__misc__vec__vecBit_h
+#define ABC__misc__vec__vecBit_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h
index 8273b033..0ad6da27 100644
--- a/src/misc/vec/vecFlt.h
+++ b/src/misc/vec/vecFlt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_FLT_H__
-#define __VEC_FLT_H__
+#ifndef ABC__misc__vec__vecFlt_h
+#define ABC__misc__vec__vecFlt_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 0d0c24a8..0d18f973 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_INT_H__
-#define __VEC_INT_H__
+#ifndef ABC__misc__vec__vecInt_h
+#define ABC__misc__vec__vecInt_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index fe4b00b2..afad09d1 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_PTR_H__
-#define __VEC_PTR_H__
+#ifndef ABC__misc__vec__vecPtr_h
+#define ABC__misc__vec__vecPtr_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index c92760f2..cec3e7e1 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_STR_H__
-#define __VEC_STR_H__
+#ifndef ABC__misc__vec__vecStr_h
+#define ABC__misc__vec__vecStr_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 91713291..f72bd93c 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_VEC_H__
-#define __VEC_VEC_H__
+#ifndef ABC__misc__vec__vecVec_h
+#define ABC__misc__vec__vecVec_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index 94449262..ab8e8306 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __VEC_WRD_H__
-#define __VEC_WRD_H__
+#ifndef ABC__misc__vec__vecWrd_h
+#define ABC__misc__vec__vecWrd_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/zlib/adler32.c b/src/misc/zlib/adler32.c
index 7783d96c..10208ab4 100644
--- a/src/misc/zlib/adler32.c
+++ b/src/misc/zlib/adler32.c
@@ -8,7 +8,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"
 
diff --git a/src/misc/zlib/crc32.c b/src/misc/zlib/crc32.c
index 749480ef..6c33b549 100644
--- a/src/misc/zlib/crc32.c
+++ b/src/misc/zlib/crc32.c
@@ -29,7 +29,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"      /* for STDC and FAR definitions */
 
diff --git a/src/misc/zlib/deflate.c b/src/misc/zlib/deflate.c
index ceeeed06..e47050bd 100644
--- a/src/misc/zlib/deflate.c
+++ b/src/misc/zlib/deflate.c
@@ -52,7 +52,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "deflate.h"
 
diff --git a/src/misc/zlib/gzclose.c b/src/misc/zlib/gzclose.c
index 07d6e0d9..6cd8dc3d 100644
--- a/src/misc/zlib/gzclose.c
+++ b/src/misc/zlib/gzclose.c
@@ -6,7 +6,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "gzguts.h"
 
diff --git a/src/misc/zlib/gzguts.h b/src/misc/zlib/gzguts.h
index 7334b92e..f95db6c2 100644
--- a/src/misc/zlib/gzguts.h
+++ b/src/misc/zlib/gzguts.h
@@ -61,7 +61,7 @@
 #endif
 
 #include <stdio.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/misc/zlib/gzlib.c b/src/misc/zlib/gzlib.c
index 1d88baa4..4d6fdfd0 100644
--- a/src/misc/zlib/gzlib.c
+++ b/src/misc/zlib/gzlib.c
@@ -6,7 +6,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "gzguts.h"
 
diff --git a/src/misc/zlib/gzread.c b/src/misc/zlib/gzread.c
index 7abe5d9c..6a4d13b6 100644
--- a/src/misc/zlib/gzread.c
+++ b/src/misc/zlib/gzread.c
@@ -6,7 +6,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "gzguts.h"
 
diff --git a/src/misc/zlib/gzwrite.c b/src/misc/zlib/gzwrite.c
index bf96602c..f7482615 100644
--- a/src/misc/zlib/gzwrite.c
+++ b/src/misc/zlib/gzwrite.c
@@ -6,7 +6,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "gzguts.h"
 
diff --git a/src/misc/zlib/infback.c b/src/misc/zlib/infback.c
index 882b2492..7163f99d 100644
--- a/src/misc/zlib/infback.c
+++ b/src/misc/zlib/infback.c
@@ -13,7 +13,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"
 #include "inftrees.h"
diff --git a/src/misc/zlib/inffast.c b/src/misc/zlib/inffast.c
index 22bc98d1..fbdf94d0 100644
--- a/src/misc/zlib/inffast.c
+++ b/src/misc/zlib/inffast.c
@@ -6,7 +6,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"
 #include "inftrees.h"
diff --git a/src/misc/zlib/inflate.c b/src/misc/zlib/inflate.c
index c68c13f5..04feb237 100644
--- a/src/misc/zlib/inflate.c
+++ b/src/misc/zlib/inflate.c
@@ -83,7 +83,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"
 #include "inftrees.h"
diff --git a/src/misc/zlib/inftrees.c b/src/misc/zlib/inftrees.c
index ad631f85..a73e58a8 100644
--- a/src/misc/zlib/inftrees.c
+++ b/src/misc/zlib/inftrees.c
@@ -6,7 +6,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"
 #include "inftrees.h"
diff --git a/src/misc/zlib/trees.c b/src/misc/zlib/trees.c
index e107ba04..a7365594 100644
--- a/src/misc/zlib/trees.c
+++ b/src/misc/zlib/trees.c
@@ -37,7 +37,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "deflate.h"
 
diff --git a/src/misc/zlib/uncompr.c b/src/misc/zlib/uncompr.c
index e195ec3e..cf021273 100644
--- a/src/misc/zlib/uncompr.c
+++ b/src/misc/zlib/uncompr.c
@@ -8,7 +8,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #define ZLIB_INTERNAL
 #include "zlib.h"
diff --git a/src/misc/zlib/zlib.h b/src/misc/zlib/zlib.h
index 58ff1d15..94825b55 100644
--- a/src/misc/zlib/zlib.h
+++ b/src/misc/zlib/zlib.h
@@ -32,7 +32,10 @@
 #define ZLIB_H
 
 #include <stdio.h>
-#include "abc_global.h"
+#include <stdlib.h>
+#include <string.h>
+
+#include "src/misc/util/abc_global.h"
 
 #include "zconf.h"
 
diff --git a/src/misc/zlib/zutil.c b/src/misc/zlib/zutil.c
index 17a906d8..b74b21ea 100644
--- a/src/misc/zlib/zutil.c
+++ b/src/misc/zlib/zutil.c
@@ -8,7 +8,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include "abc_global.h"
+#include "src/misc/util/abc_global.h"
 
 #include "zutil.h"