Version abc50729

31 files changed, 7702 insertions, 0 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
new file mode 100644
index 00000000..ec4023b0
--- /dev/null
+++ b/src/misc/extra/extra.h
@@ -0,0 +1,220 @@
+/**CFile****************************************************************
+
+  FileName    [extra.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: extra.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __EXTRA_H__
+#define __EXTRA_H__
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+
+#include <string.h>
+#include <time.h>
+#include "util.h"
+#include "st.h"
+#include "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* 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) \
+((unsigned)(a) % TSIZE)
+
+#define hashKey2(a,b,TSIZE) \
+(((unsigned)(a) + (unsigned)(b) * DD_P1) % TSIZE)
+
+#define hashKey3(a,b,c,TSIZE) \
+(((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 ) % TSIZE)
+
+#define hashKey4(a,b,c,d,TSIZE) \
+((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
+   (unsigned)(d)) * DD_P3) % TSIZE)
+
+#define hashKey5(a,b,c,d,e,TSIZE) \
+(((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
+   (unsigned)(d)) * DD_P3 + (unsigned)(e)) * DD_P1) % TSIZE)
+
+/*===========================================================================*/
+/*     Various Utilities                                                     */
+/*===========================================================================*/
+
+/*=== extraUtilBdd.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 fShiftUp );
+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         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 );
+
+/*=== extraUtilFile.c ========================================================*/
+
+extern char *       Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, char * pS3, char * pS4, char * pS5 );
+extern int          Extra_FileNameCheckExtension( char * FileName, char * Extension );
+extern char *       Extra_FileNameAppend( char * pBase, char * pSuffix );
+extern char *       Extra_FileNameGeneric( char * FileName );
+extern int          Extra_FileSize( char * pFileName );
+extern char *       Extra_FileRead( FILE * pFile );
+extern char *       Extra_TimeStamp();
+extern char *       Extra_StringAppend( char * pStrGiven, char * pStrAdd );
+extern unsigned     Extra_ReadBinary( char * Buffer );
+extern void         Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
+extern void         Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine );
+
+/*=== extraUtilReader.c ========================================================*/
+
+typedef struct Extra_FileReader_t_ Extra_FileReader_t;
+extern Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName, 
+    char * pCharsComment, char * pCharsStop, char * pCharsClean );
+extern void         Extra_FileReaderFree( Extra_FileReader_t * p );
+extern char *       Extra_FileReaderGetFileName( Extra_FileReader_t * p );
+extern int          Extra_FileReaderGetFileSize( Extra_FileReader_t * p );
+extern int          Extra_FileReaderGetCurPosition( Extra_FileReader_t * p );
+extern void *       Extra_FileReaderGetTokens( Extra_FileReader_t * p );
+extern int          Extra_FileReaderGetLineNumber( Extra_FileReader_t * p, int iToken );
+
+/*=== extraUtilMemory.c ========================================================*/
+
+typedef struct Extra_MmFixed_t_    Extra_MmFixed_t;    
+typedef struct Extra_MmFlex_t_     Extra_MmFlex_t;     
+typedef struct Extra_MmStep_t_     Extra_MmStep_t;     
+
+// fixed-size-block memory manager
+extern Extra_MmFixed_t *  Extra_MmFixedStart( int nEntrySize );
+extern void        Extra_MmFixedStop( Extra_MmFixed_t * p, int fVerbose );
+extern char *      Extra_MmFixedEntryFetch( Extra_MmFixed_t * p );
+extern void        Extra_MmFixedEntryRecycle( Extra_MmFixed_t * p, char * pEntry );
+extern void        Extra_MmFixedRestart( Extra_MmFixed_t * p );
+extern int         Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Extra_MmFlex_t * Extra_MmFlexStart();
+extern void        Extra_MmFlexStop( Extra_MmFlex_t * p, int fVerbose );
+extern char *      Extra_MmFlexEntryFetch( Extra_MmFlex_t * p, int nBytes );
+extern int         Extra_MmFlexReadMemUsage( Extra_MmFlex_t * p );
+// hierarchical memory manager
+extern Extra_MmStep_t * Extra_MmStepStart( int nSteps );
+extern void        Extra_MmStepStop( Extra_MmStep_t * p, int fVerbose );
+extern char *      Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes );
+extern void        Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes );
+extern int         Extra_MmStepReadMemUsage( Extra_MmStep_t * p );
+
+/*=== extraUtilMisc.c ========================================================*/
+
+/* finds the smallest integer larger of 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 );
+/* the number of combinations of k elements out of n */
+extern int         Extra_NumCombinations( int k, int n  );
+extern int *       Extra_DeriveRadixCode( int Number, int Radix, int nDigits );
+/* the factorial of number */
+extern int         Extra_Factorial( int n );
+/* the permutation of the given number of elements */
+extern char **     Extra_Permutations( int n );
+extern unsigned int Cudd_PrimeCopy( unsigned int  p );
+
+/*=== extraUtilProgress.c ================================================================*/
+
+typedef struct ProgressBarStruct ProgressBar;
+
+extern ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal );
+extern void        Extra_ProgressBarStop( ProgressBar * p );
+extern void        Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString );
+
+static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char * pString ) 
+{  if ( nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); }
+
+/*=== extraUtilIntVec.c ================================================================*/
+
+typedef struct Extra_IntVec_t_    Extra_IntVec_t;
+extern Extra_IntVec_t * Extra_IntVecAlloc( int nCap );
+extern Extra_IntVec_t * Extra_IntVecAllocArray( int * pArray, int nSize );
+extern Extra_IntVec_t * Extra_IntVecAllocArrayCopy( int * pArray, int nSize );
+extern Extra_IntVec_t * Extra_IntVecDup( Extra_IntVec_t * pVec );
+extern Extra_IntVec_t * Extra_IntVecDupArray( Extra_IntVec_t * pVec );
+extern void        Extra_IntVecFree( Extra_IntVec_t * p );
+extern void        Extra_IntVecFill( Extra_IntVec_t * p, int nSize, int Entry );
+extern int *       Extra_IntVecReleaseArray( Extra_IntVec_t * p );
+extern int *       Extra_IntVecReadArray( Extra_IntVec_t * p );
+extern int         Extra_IntVecReadSize( Extra_IntVec_t * p );
+extern int         Extra_IntVecReadEntry( Extra_IntVec_t * p, int i );
+extern int         Extra_IntVecReadEntryLast( Extra_IntVec_t * p );
+extern void        Extra_IntVecWriteEntry( Extra_IntVec_t * p, int i, int Entry );
+extern void        Extra_IntVecGrow( Extra_IntVec_t * p, int nCapMin );
+extern void        Extra_IntVecShrink( Extra_IntVec_t * p, int nSizeNew );
+extern void        Extra_IntVecClear( Extra_IntVec_t * p );
+extern void        Extra_IntVecPush( Extra_IntVec_t * p, int Entry );
+extern int         Extra_IntVecPop( Extra_IntVec_t * p );
+extern void        Extra_IntVecSort( Extra_IntVec_t * p );
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* __EXTRA_H__ */
diff --git a/src/misc/extra/extraUtilBdd.c b/src/misc/extra/extraUtilBdd.c
new file mode 100644
index 00000000..32fdca2c
--- /dev/null
+++ b/src/misc/extra/extraUtilBdd.c
@@ -0,0 +1,1018 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilBdd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [DD-based utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilBdd.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+// file "extraDdTransfer.c"
+static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute );
+static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute );
+
+// file "cuddUtils.c"
+static void ddSupportStep ARGS((DdNode *f, int *support));
+static void ddClearFlag ARGS((DdNode *f));
+
+/**AutomaticEnd***************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Convert a {A,B}DD from a manager to another with variable remapping.]
+
+  Description [Convert a {A,B}DD from a manager to another one. The orders of the
+  variables in the two managers may be different. Returns a
+  pointer to the {A,B}DD in the destination manager if successful; NULL
+  otherwise. The i-th entry in the array Permute tells what is the index
+  of the i-th variable from the old manager in the new manager.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute )
+{
+    DdNode * bRes;
+    do
+    {
+        ddDestination->reordered = 0;
+        bRes = extraTransferPermute( ddSource, ddDestination, f, Permute );
+    }
+    while ( ddDestination->reordered == 1 );
+    return ( bRes );
+
+}                               /* end of Extra_TransferPermute */
+
+/**Function********************************************************************
+
+  Synopsis    [Transfers the BDD from one manager into another level by level.]
+
+  Description [Transfers the BDD from one manager into another while
+  preserving the correspondence between variables level by level.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f )
+{
+    DdNode * bRes;
+    int * pPermute;
+    int nMin, nMax, i;
+
+    nMin = ddMin(ddSource->size, ddDestination->size);
+    nMax = ddMax(ddSource->size, ddDestination->size);
+    pPermute = ALLOC( int, nMax );
+    // set up the variable permutation
+    for ( i = 0; i < nMin; i++ )
+        pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i];
+    if ( ddSource->size > ddDestination->size )
+    {
+        for (      ; i < nMax; i++ )
+            pPermute[ ddSource->invperm[i] ] = -1;
+    }
+    bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute );
+    FREE( pPermute );
+    return bRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Remaps the function to depend on the topmost variables on the manager.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddRemapUp(
+  DdManager * dd,
+  DdNode * bF )
+{
+    int * pPermute;
+    DdNode * bSupp, * bTemp, * bRes;
+    int Counter;
+
+    pPermute = ALLOC( int, dd->size );
+
+    // get support
+    bSupp = Cudd_Support( dd, bF );    Cudd_Ref( bSupp );
+
+    // create the variable map
+    // to remap the DD into the upper part of the manager
+    Counter = 0;
+    for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
+        pPermute[bTemp->index] = dd->invperm[Counter++];
+
+    // transfer the BDD and remap it
+    bRes = Cudd_bddPermute( dd, bF, pPermute );  Cudd_Ref( bRes );
+
+    // remove support
+    Cudd_RecursiveDeref( dd, bSupp );
+
+    // return
+    Cudd_Deref( bRes );
+    free( pPermute );
+    return bRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Moves the BDD by the given number of variables up or down.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     [Extra_bddShift]
+
+******************************************************************************/
+DdNode * Extra_bddMove( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * bF,
+  int nVars) 
+{
+    DdNode * res;
+    DdNode * bVars;
+    if ( nVars == 0 )
+        return bF;
+    if ( Cudd_IsConstant(bF) )
+        return bF;
+    assert( nVars <= dd->size );
+    if ( nVars > 0 )
+        bVars = dd->vars[nVars];
+    else
+        bVars = Cudd_Not(dd->vars[-nVars]);
+
+    do {
+        dd->reordered = 0;
+        res = extraBddMove( dd, bF, bVars );
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_bddMove */
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_StopManager( DdManager * dd )
+{
+    int RetValue;
+    // check for remaining references in the package
+    RetValue = Cudd_CheckZeroRef( dd );
+    if ( RetValue > 0 )
+        printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
+//  Cudd_PrintInfo( dd, stdout );
+    Cudd_Quit( dd );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Outputs the BDD in a readable format.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_bddPrint( DdManager * dd, DdNode * F )
+{
+    DdGen * Gen;
+    int * Cube;
+    CUDD_VALUE_TYPE Value;
+    int nVars = dd->size;
+    int fFirstCube = 1;
+    int i;
+
+    if ( F == NULL )
+    {
+        printf("NULL");
+        return;
+    }
+    if ( F == b0 )
+    {
+        printf("Constant 0");
+        return;
+    }
+    if ( F == b1 )
+    {
+        printf("Constant 1");
+        return;
+    }
+
+    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
+    {
+        if ( fFirstCube )
+            fFirstCube = 0;
+        else
+//          Output << " + ";
+            printf( " + " );
+
+        for ( i = 0; i < nVars; i++ )
+            if ( Cube[i] == 0 )
+                printf( "[%d]'", i );
+//              printf( "%c'", (char)('a'+i) );
+            else if ( Cube[i] == 1 )
+                printf( "[%d]", i );
+//              printf( "%c", (char)('a'+i) );
+    }
+
+//  printf("\n");
+}
+/**Function********************************************************************
+
+  Synopsis    [Returns the size of the support.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp )
+{
+    int Counter = 0;
+    while ( bSupp != b1 )
+    {
+        assert( !Cudd_IsComplement(bSupp) );
+        assert( cuddE(bSupp) == b0 );
+
+        bSupp = cuddT(bSupp);
+        Counter++;
+    }
+    return Counter;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns 1 if the support contains the given BDD variable.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar )   
+{ 
+    for( ; bS != b1; bS = cuddT(bS) )
+        if ( bS->index == bVar->index )
+            return 1;
+    return 0;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns 1 if two supports represented as BDD cubes are overlapping.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 )
+{
+    while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX )
+    {
+        // if the top vars are the same, they intersect
+        if ( S1->index == S2->index )
+            return 1;
+        // if the top vars are different, skip the one, which is higher
+        if ( dd->perm[S1->index] < dd->perm[S2->index] )
+            S1 = cuddT(S1);
+        else
+            S2 = cuddT(S2);
+    }
+    return 0;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of different vars in two supports.]
+
+  Description [Counts the number of variables that appear in one support and 
+  does not appear in other support. If the number exceeds DiffMax, returns DiffMax.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax )
+{
+    int Result = 0;
+    while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX )
+    {
+        // if the top vars are the same, this var is the same
+        if ( S1->index == S2->index )
+        {
+            S1 = cuddT(S1);
+            S2 = cuddT(S2);
+            continue;
+        }
+        // the top var is different
+        Result++;
+
+        if ( Result >= DiffMax )
+            return DiffMax;
+
+        // if the top vars are different, skip the one, which is higher
+        if ( dd->perm[S1->index] < dd->perm[S2->index] )
+            S1 = cuddT(S1);
+        else
+            S2 = cuddT(S2);
+    }
+
+    // consider the remaining variables
+    if ( S1->index != CUDD_CONST_INDEX )
+        Result += Extra_bddSuppSize(dd,S1);
+    else if ( S2->index != CUDD_CONST_INDEX )
+        Result += Extra_bddSuppSize(dd,S2);
+
+    if ( Result >= DiffMax )
+        return DiffMax;
+    return Result;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks the support containment.]
+
+  Description [This function returns 1 if one support is contained in another.
+  In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support.
+  If the supports are identical, return 0 and does not assign the supports!]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall )
+{
+    DdNode * bSL = bL;
+    DdNode * bSH = bH;
+    int fLcontainsH = 1;
+    int fHcontainsL = 1;
+    int TopVar;
+    
+    if ( bSL == bSH )
+        return 0;
+
+    while ( bSL != b1 || bSH != b1 )
+    {
+        if ( bSL == b1 )
+        { // Low component has no vars; High components has some vars
+            fLcontainsH = 0;
+            if ( fHcontainsL == 0 )
+                return 0;
+            else
+                break;
+        }
+
+        if ( bSH == b1 )
+        { // similarly
+            fHcontainsL = 0;
+            if ( fLcontainsH == 0 )
+                return 0;
+            else
+                break;
+        }
+
+        // determine the topmost var of the supports by comparing their levels
+        if ( dd->perm[bSL->index] < dd->perm[bSH->index] )
+            TopVar = bSL->index;
+        else
+            TopVar = bSH->index;
+
+        if ( TopVar == bSL->index && TopVar == bSH->index ) 
+        { // they are on the same level
+            // it does not tell us anything about their containment
+            // skip this var
+            bSL = cuddT(bSL);
+            bSH = cuddT(bSH);
+        }
+        else if ( TopVar == bSL->index ) // and TopVar != bSH->index
+        { // Low components is higher and contains more vars
+            // it is not possible that High component contains Low
+            fHcontainsL = 0;
+            // skip this var
+            bSL = cuddT(bSL);
+        }
+        else // if ( TopVar == bSH->index ) // and TopVar != bSL->index
+        { // similarly
+            fLcontainsH = 0;
+            // skip this var
+            bSH = cuddT(bSH);
+        }
+
+        // check the stopping condition
+        if ( !fHcontainsL && !fLcontainsH )
+            return 0;
+    }
+    // only one of them can be true at the same time
+    assert( !fHcontainsL || !fLcontainsH );
+    if ( fHcontainsL )
+    {
+        *bLarge = bH;
+        *bSmall = bL;
+    }
+    else // fLcontainsH
+    {
+        *bLarge = bL;
+        *bSmall = bH;
+    }
+    return 1;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Finds variables on which the DD depends and returns them as am array.]
+
+  Description [Finds the variables on which the DD depends. Returns an array 
+  with entries set to 1 for those variables that belong to the support; 
+  NULL otherwise. The array is allocated by the user and should have at least
+  as many entries as the maximum number of variables in BDD and ZDD parts of 
+  the manager.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]
+
+******************************************************************************/
+int * 
+Extra_SupportArray(
+  DdManager * dd, /* manager */
+  DdNode * f,     /* DD whose support is sought */
+  int * support ) /* array allocated by the user */
+{
+    int i, size;
+
+    /* Initialize support array for ddSupportStep. */
+    size = ddMax(dd->size, dd->sizeZ);
+    for (i = 0; i < size; i++) 
+        support[i] = 0;
+    
+    /* Compute support and clean up markers. */
+    ddSupportStep(Cudd_Regular(f),support);
+    ddClearFlag(Cudd_Regular(f));
+
+    return(support);
+
+} /* end of Extra_SupportArray */
+
+/**Function********************************************************************
+
+  Synopsis    [Finds the variables on which a set of DDs depends.]
+
+  Description [Finds the variables on which a set of DDs depends.
+  The set must contain either BDDs and ADDs, or ZDDs.
+  Returns a BDD consisting of the product of the variables if
+  successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_Support Cudd_ClassifySupport]
+
+******************************************************************************/
+int *
+Extra_VectorSupportArray( 
+  DdManager * dd, /* manager */ 
+  DdNode ** F, /* array of DDs whose support is sought */ 
+  int n, /* size of the array */  
+  int * support ) /* array allocated by the user */
+{
+    int i, size;
+
+    /* Allocate and initialize support array for ddSupportStep. */
+    size = ddMax( dd->size, dd->sizeZ );
+    for ( i = 0; i < size; i++ )
+        support[i] = 0;
+
+    /* Compute support and clean up markers. */
+    for ( i = 0; i < n; i++ )
+        ddSupportStep( Cudd_Regular(F[i]), support );
+    for ( i = 0; i < n; i++ )
+        ddClearFlag( Cudd_Regular(F[i]) );
+
+    return support;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Find any cube belonging to the on-set of the function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode *  Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
+{
+    char * s_Temp;
+    DdNode * bCube, * bTemp;
+    int v;
+
+    // get the vector of variables in the cube
+    s_Temp = ALLOC( char, dd->size );
+    Cudd_bddPickOneCube( dd, bF, s_Temp );
+
+    // start the cube
+    bCube = b1; Cudd_Ref( bCube );
+    for ( v = 0; v < dd->size; v++ )
+        if ( s_Temp[v] == 0 )
+        {
+//          Cube &= !s_XVars[v];
+            bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        else if ( s_Temp[v] == 1 )
+        {
+//          Cube &=  s_XVars[v];
+            bCube = Cudd_bddAnd( dd, bTemp = bCube,          dd->vars[v]  ); Cudd_Ref( bCube );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+    Cudd_Deref(bCube);
+    free( s_Temp );
+    return bCube;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns one cube contained in the given BDD.]
+
+  Description [This function returns the cube with the smallest 
+  bits-to-integer value.]
+
+  SideEffects []
+
+******************************************************************************/
+DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc )
+{
+    DdNode * bFuncR, * bFunc0, * bFunc1;
+    DdNode * bRes0,  * bRes1,  * bRes;
+
+    bFuncR = Cudd_Regular(bFunc);
+    if ( cuddIsConstant(bFuncR) )
+        return bFunc;
+
+    // cofactor
+    if ( Cudd_IsComplement(bFunc) )
+    {
+        bFunc0 = Cudd_Not( cuddE(bFuncR) );
+        bFunc1 = Cudd_Not( cuddT(bFuncR) );
+    }
+    else
+    {
+        bFunc0 = cuddE(bFuncR);
+        bFunc1 = cuddT(bFuncR);
+    }
+
+    // try to find the cube with the negative literal
+    bRes0 = Extra_bddGetOneCube( dd, bFunc0 );  Cudd_Ref( bRes0 );
+
+    if ( bRes0 != b0 )
+    {
+        bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bRes0 );
+    }
+    else
+    {
+        Cudd_RecursiveDeref( dd, bRes0 );
+        // try to find the cube with the positive literal
+        bRes1 = Extra_bddGetOneCube( dd, bFunc1 );  Cudd_Ref( bRes1 );
+        assert( bRes1 != b0 );
+        bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bRes1 );
+    }
+
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraBddMove( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bF,
+  DdNode * bDist) 
+{
+    DdNode * bRes;
+
+    if ( Cudd_IsConstant(bF) )
+        return bF;
+
+    if ( bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist) )
+        return bRes;
+    else
+    {
+        DdNode * bRes0, * bRes1;             
+        DdNode * bF0, * bF1;             
+        DdNode * bFR = Cudd_Regular(bF); 
+        int VarNew;
+        
+        if ( Cudd_IsComplement(bDist) )
+            VarNew = bFR->index - Cudd_Not(bDist)->index;
+        else
+            VarNew = bFR->index + bDist->index;
+        assert( VarNew < dd->size );
+
+        // cofactor the functions
+        if ( bFR != bF ) // bFunc is complemented 
+        {
+            bF0 = Cudd_Not( cuddE(bFR) );
+            bF1 = Cudd_Not( cuddT(bFR) );
+        }
+        else
+        {
+            bF0 = cuddE(bFR);
+            bF1 = cuddT(bFR);
+        }
+
+        bRes0 = extraBddMove( dd, bF0, bDist );
+        if ( bRes0 == NULL ) 
+            return NULL;
+        cuddRef( bRes0 );
+
+        bRes1 = extraBddMove( dd, bF1, bDist );
+        if ( bRes1 == NULL ) 
+        {
+            Cudd_RecursiveDeref( dd, bRes0 );
+            return NULL;
+        }
+        cuddRef( bRes1 );
+
+        /* only bRes0 and bRes1 are referenced at this point */
+        bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 );
+        if ( bRes == NULL ) 
+        {
+            Cudd_RecursiveDeref( dd, bRes0 );
+            Cudd_RecursiveDeref( dd, bRes1 );
+            return NULL;
+        }
+        cuddRef( bRes );
+        Cudd_RecursiveDeref( dd, bRes0 );
+        Cudd_RecursiveDeref( dd, bRes1 );
+
+        /* insert the result into cache */
+        cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes );
+        cuddDeref( bRes );
+        return bRes;
+    }
+} /* end of extraBddMove */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Finds three cofactors of the cover w.r.t. to the topmost variable.]
+
+  Description [Finds three cofactors of the cover w.r.t. to the topmost variable.
+  Does not check the cover for being a constant. Assumes that ZDD variables encoding 
+  positive and negative polarities are adjacent in the variable order. Is different 
+  from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the 
+  given variable but takes the cofactors with respent to the topmost variable. 
+  This function is more efficient when used in recursive procedures because it does 
+  not require referencing of the resulting cofactors (compare cuddZddProduct() 
+  and extraZddPrimeProduct()).]
+
+  SideEffects [None]
+
+  SeeAlso     [cuddZddGetCofactors3]
+
+******************************************************************************/
+void 
+extraDecomposeCover( 
+  DdManager* dd,    /* the manager */
+  DdNode*  zC,      /* the cover */
+  DdNode** zC0,     /* the pointer to the negative var cofactor */ 
+  DdNode** zC1,     /* the pointer to the positive var cofactor */ 
+  DdNode** zC2 )    /* the pointer to the cofactor without var */ 
+{
+    if ( (zC->index & 1) == 0 ) 
+    { /* the top variable is present in positive polarity and maybe in negative */
+
+        DdNode *Temp = cuddE( zC );
+        *zC1  = cuddT( zC );
+        if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 )
+        {   /* Temp is not a terminal node 
+             * top var is present in negative polarity */
+            *zC2 = cuddE( Temp );
+            *zC0 = cuddT( Temp );
+        }
+        else
+        {   /* top var is not present in negative polarity */
+            *zC2 = Temp;
+            *zC0 = dd->zero;
+        }
+    }
+    else 
+    { /* the top variable is present only in negative */
+        *zC1 = dd->zero;
+        *zC2 = cuddE( zC );
+        *zC0 = cuddT( zC );
+    }
+} /* extraDecomposeCover */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Convert a BDD from a manager to another one.]
+
+  Description [Convert a BDD from a manager to another one. Returns a
+  pointer to the BDD in the destination manager if successful; NULL
+  otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Extra_TransferPermute]
+
+******************************************************************************/
+DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute )
+{
+    DdNode *res;
+    st_table *table = NULL;
+    st_generator *gen = NULL;
+    DdNode *key, *value;
+
+    table = st_init_table( st_ptrcmp, st_ptrhash );
+    if ( table == NULL )
+        goto failure;
+    res = extraTransferPermuteRecur( ddS, ddD, f, table, Permute );
+    if ( res != NULL )
+        cuddRef( res );
+
+    /* Dereference all elements in the table and dispose of the table.
+       ** This must be done also if res is NULL to avoid leaks in case of
+       ** reordering. */
+    gen = st_init_gen( table );
+    if ( gen == NULL )
+        goto failure;
+    while ( st_gen( gen, ( char ** ) &key, ( char ** ) &value ) )
+    {
+        Cudd_RecursiveDeref( ddD, value );
+    }
+    st_free_gen( gen );
+    gen = NULL;
+    st_free_table( table );
+    table = NULL;
+
+    if ( res != NULL )
+        cuddDeref( res );
+    return ( res );
+
+  failure:
+    if ( table != NULL )
+        st_free_table( table );
+    if ( gen != NULL )
+        st_free_gen( gen );
+    return ( NULL );
+
+}                               /* end of extraTransferPermute */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Extra_TransferPermute.]
+
+  Description [Performs the recursive step of Extra_TransferPermute.
+  Returns a pointer to the result if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [extraTransferPermute]
+
+******************************************************************************/
+static DdNode * 
+extraTransferPermuteRecur( 
+  DdManager * ddS, 
+  DdManager * ddD, 
+  DdNode * f, 
+  st_table * table, 
+  int * Permute )
+{
+    DdNode *ft, *fe, *t, *e, *var, *res;
+    DdNode *one, *zero;
+    int index;
+    int comple = 0;
+
+    statLine( ddD );
+    one = DD_ONE( ddD );
+    comple = Cudd_IsComplement( f );
+
+    /* Trivial cases. */
+    if ( Cudd_IsConstant( f ) )
+        return ( Cudd_NotCond( one, comple ) );
+
+
+    /* Make canonical to increase the utilization of the cache. */
+    f = Cudd_NotCond( f, comple );
+    /* Now f is a regular pointer to a non-constant node. */
+
+    /* Check the cache. */
+    if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
+        return ( Cudd_NotCond( res, comple ) );
+
+    /* Recursive step. */
+    if ( Permute )
+        index = Permute[f->index];
+    else
+        index = f->index;
+
+    ft = cuddT( f );
+    fe = cuddE( f );
+
+    t = extraTransferPermuteRecur( ddS, ddD, ft, table, Permute );
+    if ( t == NULL )
+    {
+        return ( NULL );
+    }
+    cuddRef( t );
+
+    e = extraTransferPermuteRecur( ddS, ddD, fe, table, Permute );
+    if ( e == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        return ( NULL );
+    }
+    cuddRef( e );
+
+    zero = Cudd_Not(ddD->one);
+    var = cuddUniqueInter( ddD, index, one, zero );
+    if ( var == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        Cudd_RecursiveDeref( ddD, e );
+        return ( NULL );
+    }
+    res = cuddBddIteRecur( ddD, var, t, e );
+
+    if ( res == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        Cudd_RecursiveDeref( ddD, e );
+        return ( NULL );
+    }
+    cuddRef( res );
+    Cudd_RecursiveDeref( ddD, t );
+    Cudd_RecursiveDeref( ddD, e );
+
+    if ( st_add_direct( table, ( char * ) f, ( char * ) res ) ==
+         ST_OUT_OF_MEM )
+    {
+        Cudd_RecursiveDeref( ddD, res );
+        return ( NULL );
+    }
+    return ( Cudd_NotCond( res, comple ) );
+
+}                               /* end of extraTransferPermuteRecur */
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Cudd_Support.]
+
+  Description [Performs the recursive step of Cudd_Support. Performs a
+  DFS from f. The support is accumulated in supp as a side effect. Uses
+  the LSB of the then pointer as visited flag.]
+
+  SideEffects [None]
+
+  SeeAlso     [ddClearFlag]
+
+******************************************************************************/
+static void
+ddSupportStep(
+  DdNode * f,
+  int * support)
+{
+    if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
+    return;
+    }
+
+    support[f->index] = 1;
+    ddSupportStep(cuddT(f),support);
+    ddSupportStep(Cudd_Regular(cuddE(f)),support);
+    /* Mark as visited. */
+    f->next = Cudd_Not(f->next);
+    return;
+
+} /* end of ddSupportStep */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs a DFS from f, clearing the LSB of the next
+  pointers.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [ddSupportStep ddDagInt]
+
+******************************************************************************/
+static void
+ddClearFlag(
+  DdNode * f)
+{
+    if (!Cudd_IsComplement(f->next)) {
+    return;
+    }
+    /* Clear visited flag. */
+    f->next = Cudd_Regular(f->next);
+    if (cuddIsConstant(f)) {
+    return;
+    }
+    ddClearFlag(cuddT(f));
+    ddClearFlag(Cudd_Regular(cuddE(f)));
+    return;
+
+} /* end of ddClearFlag */
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
new file mode 100644
index 00000000..faf27dc8
--- /dev/null
+++ b/src/misc/extra/extraUtilFile.c
@@ -0,0 +1,382 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilFile.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [File management utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilFile.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Tries to find a file name with a different extension.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, char * pS3, char * pS4, char * pS5 )
+{
+    FILE * pFile;
+    char * pFileNameOther;
+    char * pFileGen;
+
+    if ( pS1 == NULL )
+        return NULL;
+
+    // get the generic file name
+    pFileGen = Extra_FileNameGeneric( pFileNameWrong );
+    pFileNameOther = Extra_FileNameAppend( pFileGen, pS1 );
+    pFile = fopen( pFileNameOther, "r" );
+    if ( pFile == NULL && pS2 )
+    { // try one more
+        pFileNameOther = Extra_FileNameAppend( pFileGen, pS2 );
+        pFile = fopen( pFileNameOther, "r" );
+        if ( pFile == NULL && pS3 )
+        { // try one more
+            pFileNameOther = Extra_FileNameAppend( pFileGen, pS3 );
+            pFile = fopen( pFileNameOther, "r" );
+            if ( pFile == NULL && pS4 )
+            { // try one more
+                pFileNameOther = Extra_FileNameAppend( pFileGen, pS4 );
+                pFile = fopen( pFileNameOther, "r" );
+                if ( pFile == NULL && pS5 )
+                { // try one more
+                    pFileNameOther = Extra_FileNameAppend( pFileGen, pS5 );
+                    pFile = fopen( pFileNameOther, "r" );
+                }
+            }
+        }
+    }
+    FREE( pFileGen );
+    if ( pFile )
+    {
+        fclose( pFile );
+        return pFileNameOther;
+    }
+    // did not find :(
+    return NULL;            
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_FileNameCheckExtension( char * FileName, char * Extension )
+{
+    char * pDot;
+    // find "dot" if it is present in the file name
+//    pDot = strstr( FileName, "." );
+    for ( pDot = FileName + strlen(FileName)-1; pDot >= FileName; pDot-- )
+        if ( *pDot == '.' )
+            break;
+    if ( *pDot != '.' )
+        return 0;
+    // check the extension
+    if ( pDot && strcmp( pDot+1, Extension ) == 0 )
+        return 1;
+    else
+        return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the composite name of the file.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_FileNameAppend( char * pBase, char * pSuffix )
+{
+    static char Buffer[500];
+    sprintf( Buffer, "%s%s", pBase, pSuffix );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_FileNameGeneric( char * FileName )
+{
+    char * pDot;
+    char * pUnd;
+    char * pRes;
+    
+    // find the generic name of the file
+    pRes = util_strsav( FileName );
+    // find the pointer to the "." symbol in the file name
+//  pUnd = strstr( FileName, "_" );
+    pUnd = NULL;
+    pDot = strstr( FileName, "." );
+    if ( pUnd )
+        pRes[pUnd - FileName] = 0;
+    else if ( pDot )
+        pRes[pDot - FileName] = 0;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_FileSize( char * pFileName )
+{
+    FILE * pFile;
+    int nFileSize;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Extra_FileSize(): The file is unavailable (absent or open).\n" );
+        return 0;
+    }
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile ); 
+    fclose( pFile );
+    return nFileSize;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Read the file into the internal buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_FileRead( FILE * pFile )
+{
+    int nFileSize;
+    char * pBuffer;
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = ALLOC( char, nFileSize + 3 );
+    fread( pBuffer, nFileSize, 1, pFile );
+    // terminate the string with '\0'
+    pBuffer[ nFileSize + 0] = '\n';
+    pBuffer[ nFileSize + 1] = '\0';
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the time stamp.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_TimeStamp()
+{
+    static char Buffer[100];
+    time_t ltime;
+    char * TimeStamp;
+    // get the current time
+    time( &ltime );
+    TimeStamp = asctime( localtime( &ltime ) );
+    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
+    strcpy( Buffer, TimeStamp );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Extra_ReadBinary( char * Buffer )
+{
+    unsigned Result;
+    int i;
+
+    Result = 0;
+    for ( i = 0; Buffer[i]; i++ )
+        if ( Buffer[i] == '0' || Buffer[i] == '1' )
+            Result = Result * 2 + Buffer[i] - '0';
+        else
+        {
+            assert( 0 );
+        }
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the bit string.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits )
+{
+    int Remainder, nWords;
+    int w, i;
+
+    Remainder = (nBits%(sizeof(unsigned)*8));
+    nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
+
+    for ( w = nWords-1; w >= 0; w-- )
+        for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
+            fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
+
+//  fprintf( pFile, "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the composite name of the file.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine )
+{
+    int i;
+    for ( i = 0; i < nTimes; i++ )
+        printf( "%c", Char );
+    if ( fPrintNewLine )
+        printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appends the string.]
+
+  Description [Assumes that the given string (pStrGiven) has been allocated
+  before using malloc(). The additional string has not been allocated.
+  Allocs more root, appends the additional part, frees the old given string.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_StringAppend( char * pStrGiven, char * pStrAdd )
+{
+    char * pTemp;
+    if ( pStrGiven )
+    {
+        pTemp = ALLOC( char, strlen(pStrGiven) + strlen(pStrAdd) + 2 );
+        sprintf( pTemp, "%s%s", pStrGiven, pStrAdd );
+        free( pStrGiven );
+    }
+    else
+        pTemp = util_strsav( pStrAdd );
+    return pTemp;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
new file mode 100644
index 00000000..af1128ac
--- /dev/null
+++ b/src/misc/extra/extraUtilMemory.c
@@ -0,0 +1,564 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilMemory.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Memory managers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilMemory.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+struct Extra_MmFixed_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 Extra_MmFlex_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 Extra_MmStep_t_
+{
+    int                nMems;    // the number of fixed memory managers employed
+    Extra_MmFixed_t ** pMems;    // memory managers: 2^1 words, 2^2 words, etc
+    int                nMapSize; // the size of the memory array
+    Extra_MmFixed_t ** pMap;     // maps the number of bytes into its memory manager
+};
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**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     []
+
+***********************************************************************/
+Extra_MmFixed_t * Extra_MmFixedStart( int nEntrySize )
+{
+    Extra_MmFixed_t * p;
+
+    p = ALLOC( Extra_MmFixed_t, 1 );
+    memset( p, 0, sizeof(Extra_MmFixed_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       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_MmFixedStop( Extra_MmFixed_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++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_MmFixedEntryFetch( Extra_MmFixed_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 = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pEntriesFree = 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 Extra_MmFixedEntryRecycle( Extra_MmFixed_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 Extra_MmFixedRestart( Extra_MmFixed_t * p )
+{
+    int i;
+    char * pTemp;
+
+    // delocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        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 Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates entries of flexible size.]
+
+  Description [Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_MmFlex_t * Extra_MmFlexStart()
+{
+    Extra_MmFlex_t * p;
+
+    p = ALLOC( Extra_MmFlex_t, 1 );
+    memset( p, 0, sizeof(Extra_MmFlex_t) );
+
+    p->nEntriesUsed  = 0;
+    p->pCurrent      = NULL;
+    p->pEnd          = NULL;
+
+    p->nChunkSize    = (1 << 12);
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_MmFlexStop( Extra_MmFlex_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++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_MmFlexEntryFetch( Extra_MmFlex_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 = 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 = 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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_MmFlexReadMemUsage( Extra_MmFlex_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+
+
+
+
+/**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 free()ed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_MmStep_t * Extra_MmStepStart( int nSteps )
+{
+    Extra_MmStep_t * p;
+    int i, k;
+    p = ALLOC( Extra_MmStep_t, 1 );
+    p->nMems = nSteps;
+    // start the fixed memory managers
+    p->pMems = ALLOC( Extra_MmFixed_t *, p->nMems );
+    for ( i = 0; i < p->nMems; i++ )
+        p->pMems[i] = Extra_MmFixedStart( (8<<i) );
+    // set up the mapping of the required memory size into the corresponding manager
+    p->nMapSize = (4<<p->nMems);
+    p->pMap = ALLOC( Extra_MmFixed_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 Extra_MmStepStop( Extra_MmStep_t * p, int fVerbose )
+{
+    int i;
+    for ( i = 0; i < p->nMems; i++ )
+        Extra_MmFixedStop( p->pMems[i], fVerbose );
+    free( p->pMems );
+    free( p->pMap );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes )
+{
+    if ( nBytes == 0 )
+        return NULL;
+    if ( nBytes > p->nMapSize )
+    {
+//        printf( "Allocating %d bytes.\n", nBytes );
+        return ALLOC( char, nBytes );
+    }
+    return Extra_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes )
+{
+    if ( nBytes == 0 )
+        return;
+    if ( nBytes > p->nMapSize )
+    {
+        free( pEntry );
+        return;
+    }
+    Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_MmStepReadMemUsage( Extra_MmStep_t * p )
+{
+    int i, nMemTotal = 0;
+    for ( i = 0; i < p->nMems; i++ )
+        nMemTotal += p->pMems[i]->nMemoryAlloc;
+    return nMemTotal;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
new file mode 100644
index 00000000..41c76018
--- /dev/null
+++ b/src/misc/extra/extraUtilMisc.c
@@ -0,0 +1,380 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilMisc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Misc procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+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;
+    assert( Num >= 0 );
+    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.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_Base2LogDouble( double Num )
+{
+    double Res;
+    int ResInt;
+
+    Res    = log(Num)/log(2.0);
+    ResInt = (int)Res;
+    if ( ResInt == Res )
+        return ResInt;
+    else 
+        return ResInt+1;
+}
+
+/**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;
+    assert( Num >= 0 );
+    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 []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+double Extra_Power2( int Degree )
+{
+    double Res;
+    assert( Degree >= 0 );
+    if ( Degree < 32 )
+        return (double)(01<<Degree); 
+    for ( Res = 1.0; Degree; Res *= 2.0, Degree-- );
+    return Res;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_Power3( int Num )
+{
+    int i;
+    int Res;
+    Res = 1;
+    for ( i = 0; i < Num; i++ )
+        Res *= 3;
+    return Res;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Finds the number of combinations of k elements out of n.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_NumCombinations( int k, int n )
+{
+    int i, Res = 1;
+    for ( i = 1; i <= k; i++ )
+            Res = Res * (n-i+1) / i;
+    return Res;
+} /* end of Extra_NumCombinations */
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits )
+{
+    static int Code[100];
+    int i;
+    assert( nDigits < 100 );
+    for ( i = 0; i < nDigits; i++ )
+    {
+        Code[i] = Number % Radix;
+        Number  = Number / Radix;
+    }
+    assert( Number == 0 );
+    return Code;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the factorial.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_Factorial( int n )
+{
+    int i, Res = 1;
+    for ( i = 1; i <= n; i++ )
+        Res *= i;
+    return Res;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the set of all permutations.]
+
+  Description [The number of permutations in the array is n!. The number of
+  entries in each permutation is n. Therefore, the resulting array is a 
+  two-dimentional array of the size: n! x n. To free the resulting array,
+  call free() on the pointer returned by this procedure.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+char ** Extra_Permutations( int n )
+{
+    char Array[50];
+    char ** pRes;
+    char * pBuffer;
+    int nFact, i;
+    // allocate all memory at once
+    nFact   = Extra_Factorial( n );
+    pBuffer = ALLOC( char, nFact * sizeof(char *) + nFact * n * sizeof(char) );
+    // split the chunk
+    pRes = (char **)pBuffer;
+    for ( i = 0; i < nFact; i++ )
+        pRes[i] = pBuffer + nFact * sizeof(char *) + i * n * sizeof(char);
+    // fill in the permutations
+    for ( i = 0; i < n; i++ )
+        Array[i] = i;
+    Extra_Permutations_rec( pRes, nFact, n, Array );
+    // print the permutations
+/*
+    {
+    int i, k;
+    for ( i = 0; i < nFact; i++ )
+    {
+        printf( "{" );
+        for ( k = 0; k < n; k++ )
+            printf( " %d", pRes[i][k] );
+        printf( " }\n" );
+    }
+    }
+*/
+    return pRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Fills in the array of permutations.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
+{
+    char ** pNext;
+    int nFactNext;
+    int iTemp, iCur, iLast, p;
+
+    if ( n == 1 )
+    {
+        pRes[0][0] = Array[0];
+        return;
+    }
+
+    // get the next factorial
+    nFactNext = nFact / n;
+    // get the last entry
+    iLast = n - 1;
+
+    for ( iCur = 0; iCur < n; iCur++ )
+    {
+        // swap Cur and Last
+        iTemp        = Array[iCur];
+        Array[iCur]  = Array[iLast];
+        Array[iLast] = iTemp;
+
+        // get the pointer to the current section
+        pNext = pRes + (n - 1 - iCur) * nFactNext;
+
+        // set the last entry 
+        for ( p = 0; p < nFactNext; p++ )
+            pNext[p][iLast] = Array[iLast];
+
+        // call recursively for this part
+        Extra_Permutations_rec( pNext, nFactNext, n - 1, Array );
+
+        // swap them back
+        iTemp        = Array[iCur];
+        Array[iCur]  = Array[iLast];
+        Array[iLast] = iTemp;
+    }
+}
+
+/**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                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c
new file mode 100644
index 00000000..7b0efb5c
--- /dev/null
+++ b/src/misc/extra/extraUtilProgress.c
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilProgress.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: extraUtilProgress.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "stdio.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct ProgressBarStruct
+{
+    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 Extra_ProgressBarShow( ProgressBar * p, char * pString );
+static void Extra_ProgressBarClean( ProgressBar * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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     []
+
+***********************************************************************/
+ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal )
+{
+    ProgressBar * p;
+    p = ALLOC( ProgressBar, 1 );
+    memset( p, 0, sizeof(ProgressBar) );
+    p->pFile       = pFile;
+    p->nItemsTotal = nItemsTotal;
+    p->posTotal    = 78;
+    p->posCur      = 1;
+    p->nItemsNext  = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+5)+2;
+    Extra_ProgressBarShow( p, NULL );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the progress bar.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString )
+{
+    if ( nItemsCur < p->nItemsNext )
+        return;
+    if ( nItemsCur > p->nItemsTotal )
+        nItemsCur = p->nItemsTotal;
+    p->posCur = (int)((float)nItemsCur * p->posTotal / p->nItemsTotal);
+    p->nItemsNext  = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1;
+    if ( p->posCur == 0 )
+        p->posCur = 1;
+    Extra_ProgressBarShow( p, pString );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the progress bar.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_ProgressBarStop( ProgressBar * p )
+{
+    Extra_ProgressBarClean( p );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the progress bar of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_ProgressBarShow( ProgressBar * p, char * pString )
+{
+    int i;
+    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 Extra_ProgressBarClean( ProgressBar * p )
+{
+    int i;
+    for ( i = 0; i <= p->posTotal; i++ )
+        fprintf( p->pFile, " " );
+    fprintf( p->pFile, "\r" );
+    fflush( stdout );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
new file mode 100644
index 00000000..2dc597bf
--- /dev/null
+++ b/src/misc/extra/extraUtilReader.c
@@ -0,0 +1,367 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilReader.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [File reading utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilReader.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "stdio.h"
+#include "extra.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define EXTRA_BUFFER_SIZE        1048576    // 1M   - size of the data chunk stored in memory
+#define EXTRA_OFFSET_SIZE           4096    // 4K   - load new data when less than this is left
+
+#define EXTRA_MINIMUM(a,b)       (((a) < (b))? (a) : (b))
+
+struct Extra_FileReader_t_
+{
+    // the input file
+    char *           pFileName;     // the input file name
+    FILE *           pFile;         // the input file pointer
+    int              nFileSize;     // the total number of bytes in the file
+    int              nFileRead;     // the number of bytes currently read from file
+    // info about processing different types of input chars
+    char             pCharMap[256]; // the character map
+    // temporary storage for data 
+    char *           pBuffer;       // the buffer
+    int              nBufferSize;   // the size of the buffer
+    char *           pBufferCur;    // the current reading position
+    char *           pBufferEnd;    // the first position not used by currently loaded data
+    char *           pBufferStop;   // the position where loading new data will be done
+    // tokens given to the user
+    Vec_Ptr_t *      vTokens;       // the vector of tokens returned to the user
+    Vec_Int_t *      vLines;        // the vector of line numbers for each token
+    int              nLineCounter;  // the counter of lines processed
+    // status of the parser
+    int              fStop;         // this flag goes high when the end of file is reached
+};
+
+// character types
+typedef enum { 
+    EXTRA_CHAR_COMMENT,  // a character that begins the comment
+    EXTRA_CHAR_NORMAL,   // a regular character
+    EXTRA_CHAR_STOP,     // a character that delimits a series of tokens
+    EXTRA_CHAR_CLEAN     // a character that should be cleaned
+} Extra_CharType_t;
+
+// the static functions
+static void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p );
+static void Extra_FileReaderReload( Extra_FileReader_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName, 
+    char * pCharsComment, char * pCharsStop, char * pCharsClean )
+{
+    Extra_FileReader_t * p;
+    FILE * pFile;
+    char * pChar;
+    int nCharsToRead;
+    // check if the file can be opened
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Extra_FileReaderAlloc(): Cannot open input file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    // start the file reader    
+    p = ALLOC( Extra_FileReader_t, 1 );
+    memset( p, 0, sizeof(Extra_FileReader_t) );
+    p->pFileName   = pFileName;
+    p->pFile       = pFile;
+    // set the character map
+    memset( p->pCharMap, EXTRA_CHAR_NORMAL, 256 );
+    for ( pChar = pCharsComment; *pChar; pChar++ )
+        p->pCharMap[(unsigned char)*pChar] = EXTRA_CHAR_COMMENT;
+    for ( pChar = pCharsStop; *pChar; pChar++ )
+        p->pCharMap[(unsigned char)*pChar] = EXTRA_CHAR_STOP;
+    for ( pChar = pCharsClean; *pChar; pChar++ )
+        p->pCharMap[(unsigned char)*pChar] = EXTRA_CHAR_CLEAN;
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    p->nFileSize = ftell( pFile );  
+    rewind( pFile ); 
+    // allocate the buffer
+    p->pBuffer = ALLOC( char, EXTRA_BUFFER_SIZE+1 );
+    p->nBufferSize = EXTRA_BUFFER_SIZE;
+    p->pBufferCur  = p->pBuffer;
+    // determine how many chars to read
+    nCharsToRead = EXTRA_MINIMUM(p->nFileSize, EXTRA_BUFFER_SIZE);
+    // load the first part into the buffer
+    fread( p->pBuffer, nCharsToRead, 1, p->pFile );
+    p->nFileRead = nCharsToRead;
+    // set the ponters to the end and the stopping point
+    p->pBufferEnd  = p->pBuffer + nCharsToRead;
+    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + EXTRA_BUFFER_SIZE - EXTRA_OFFSET_SIZE;
+    // start the arrays
+    p->vTokens = Vec_PtrAlloc( 100 );
+    p->vLines = Vec_IntAlloc( 100 );
+    p->nLineCounter = 1; // 1-based line counting
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_FileReaderFree( Extra_FileReader_t * p )
+{
+    if ( p->pFile )
+        fclose( p->pFile );
+    FREE( p->pBuffer );
+    Vec_PtrFree( p->vTokens );
+    Vec_IntFree( p->vLines );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_FileReaderGetFileName( Extra_FileReader_t * p )
+{
+    return p->pFileName;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_FileReaderGetFileSize( Extra_FileReader_t * p )
+{
+    return p->nFileSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the current reading position.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_FileReaderGetCurPosition( Extra_FileReader_t * p )
+{
+    return p->nFileRead - (p->pBufferEnd - p->pBufferCur);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the line number for the given token.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_FileReaderGetLineNumber( Extra_FileReader_t * p, int iToken )
+{
+    assert( iToken >= 0 && iToken < p->vTokens->nSize );
+    return p->vLines->pArray[iToken];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the next set of tokens.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Extra_FileReaderGetTokens( Extra_FileReader_t * p )
+{
+    Vec_Ptr_t * vTokens;
+    while ( vTokens = Extra_FileReaderGetTokens_int( p ) )
+        if ( vTokens->nSize > 0 )
+            break;
+    return vTokens;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the next set of tokens.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p )
+{
+    char * pChar;
+    int fTokenStarted, MapValue;
+    if ( p->fStop )
+        return NULL;
+    // reset the token info
+    p->vTokens->nSize = 0;
+    p->vLines->nSize = 0;
+    fTokenStarted = 0;
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Extra_FileReaderReload( p );
+    // process the string starting from the current position
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // switch depending on the character
+        MapValue = p->pCharMap[*pChar];
+        switch ( MapValue )
+        {
+            case EXTRA_CHAR_COMMENT:
+                if ( *pChar != '/' || *(pChar+1) == '/' ) 
+                { // dealing with the need to have // as a comment
+                    // if the token was being written, stop it
+                    if ( fTokenStarted )
+                        fTokenStarted = 0;
+                    // eraze the comment till the end of line
+                    while ( *pChar != '\n' )
+                    {
+                        *pChar++ = 0;
+                        if ( pChar == p->pBufferEnd )
+                        {   // this failure is due to the fact the comment continued 
+                            // through EXTRA_OFFSET_SIZE chars till the end of the buffer
+                            printf( "Extra_FileReader failed to parse the file \"%s\".\n", p->pFileName );
+                            return NULL;
+                        }
+                    }
+                    pChar--;
+                    break;
+                }
+                // otherwise it is a normal character
+            case EXTRA_CHAR_NORMAL:
+                if ( !fTokenStarted )
+                {
+                    Vec_PtrPush( p->vTokens, pChar );
+                    Vec_IntPush( p->vLines, p->nLineCounter );
+                    fTokenStarted = 1;
+                }
+                break;
+            case EXTRA_CHAR_STOP:
+                if ( fTokenStarted )
+                    fTokenStarted = 0;
+                *pChar = 0;
+                // prepare before leaving
+                p->pBufferCur = pChar + 1;
+                return p->vTokens;
+            case EXTRA_CHAR_CLEAN:
+                if ( fTokenStarted )
+                    fTokenStarted = 0;
+                *pChar = 0;
+                break;
+            default:
+                assert( 0 );
+        }
+    }
+    // the file is finished or the last part continued 
+    // through EXTRA_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return p->vTokens;
+    }
+    printf( "Extra_FileReader failed to parse the file \"%s\".\n", p->pFileName );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads new data into the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_FileReaderReload( Extra_FileReader_t * p )
+{
+    int nCharsUsed, nCharsToRead;
+    assert( !p->fStop );
+    assert( p->pBufferCur > p->pBufferStop );
+    assert( p->pBufferCur < p->pBufferEnd );
+    // figure out how many chars are still not processed
+    nCharsUsed = p->pBufferEnd - p->pBufferCur;
+    // move the remaining data to the beginning of the buffer
+    memmove( p->pBuffer, p->pBufferCur, nCharsUsed );
+    p->pBufferCur = p->pBuffer;
+    // determine how many chars we will read
+    nCharsToRead = EXTRA_MINIMUM( p->nBufferSize - nCharsUsed, p->nFileSize - p->nFileRead );
+    // read the chars
+    fread( p->pBuffer + nCharsUsed, nCharsToRead, 1, p->pFile );
+    p->nFileRead += nCharsToRead;
+    // set the ponters to the end and the stopping point
+    p->pBufferEnd  = p->pBuffer + nCharsUsed + nCharsToRead;
+    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + EXTRA_BUFFER_SIZE - EXTRA_OFFSET_SIZE;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
new file mode 100644
index 00000000..0c7d36a2
--- /dev/null
+++ b/src/misc/extra/module.make
@@ -0,0 +1,6 @@
+SRC +=    src/misc/extra/extraUtilBdd.c \
+    src/misc/extra/extraUtilFile.c \
+    src/misc/extra/extraUtilMemory.c \
+    src/misc/extra/extraUtilMisc.c \
+    src/misc/extra/extraUtilProgress.c \
+    src/misc/extra/extraUtilReader.c
diff --git a/src/misc/st/module.make b/src/misc/st/module.make
new file mode 100644
index 00000000..33e442c0
--- /dev/null
+++ b/src/misc/st/module.make
@@ -0,0 +1,2 @@
+SRC +=  src/misc/st/st.c \
+    src/misc/st/stmm.c
diff --git a/src/misc/st/st.c b/src/misc/st/st.c
new file mode 100644
index 00000000..13e9bd6a
--- /dev/null
+++ b/src/misc/st/st.c
@@ -0,0 +1,606 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/st/st.c,v
+ * serdar
+ * 1.1
+ * 1993/07/29 01:00:13
+ *
+ */
+#include <stdio.h>
+#include "util.h"
+#include "st.h"
+
+#define ST_NUMCMP(x,y) ((x) != (y))
+#define ST_NUMHASH(x,size) (ABS((long)x)%(size))
+#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size)
+#define EQUAL(func, x, y) \
+    ((((func) == st_numcmp) || ((func) == st_ptrcmp)) ?\
+      (ST_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))
+
+
+#define do_hash(key, table)\
+    ((table->hash == st_ptrhash) ? ST_PTRHASH((key),(table)->num_bins) :\
+     (table->hash == st_numhash) ? ST_NUMHASH((key), (table)->num_bins) :\
+     (*table->hash)((key), (table)->num_bins))
+
+static int rehash();
+int st_numhash(), st_ptrhash(), st_numcmp(), st_ptrcmp();
+
+st_table *
+st_init_table_with_params(compare, hash, size, density, grow_factor,
+              reorder_flag)
+int (*compare)();
+int (*hash)();
+int size;
+int density;
+double grow_factor;
+int reorder_flag;
+{
+    int i;
+    st_table *new;
+
+    new = ALLOC(st_table, 1);
+    if (new == NIL(st_table)) {
+    return NIL(st_table);
+    }
+    new->compare = compare;
+    new->hash = hash;
+    new->num_entries = 0;
+    new->max_density = density;
+    new->grow_factor = grow_factor;
+    new->reorder_flag = reorder_flag;
+    if (size <= 0) {
+    size = 1;
+    }
+    new->num_bins = size;
+    new->bins = ALLOC(st_table_entry *, size);
+    if (new->bins == NIL(st_table_entry *)) {
+    FREE(new);
+    return NIL(st_table);
+    }
+    for(i = 0; i < size; i++) {
+    new->bins[i] = 0;
+    }
+    return new;
+}
+
+st_table *
+st_init_table(compare, hash)
+int (*compare)();
+int (*hash)();
+{
+    return st_init_table_with_params(compare, hash, ST_DEFAULT_INIT_TABLE_SIZE,
+                     ST_DEFAULT_MAX_DENSITY,
+                     ST_DEFAULT_GROW_FACTOR,
+                     ST_DEFAULT_REORDER_FLAG);
+}
+                
+void
+st_free_table(table)
+st_table *table;
+{
+    register st_table_entry *ptr, *next;
+    int i;
+
+    for(i = 0; i < table->num_bins ; i++) {
+    ptr = table->bins[i];
+    while (ptr != NIL(st_table_entry)) {
+        next = ptr->next;
+        FREE(ptr);
+        ptr = next;
+    }
+    }
+    FREE(table->bins);
+    FREE(table);
+}
+
+#define PTR_NOT_EQUAL(table, ptr, user_key)\
+(ptr != NIL(st_table_entry) && !EQUAL(table->compare, user_key, (ptr)->key))
+
+#define FIND_ENTRY(table, hash_val, key, ptr, last) \
+    (last) = &(table)->bins[hash_val];\
+    (ptr) = *(last);\
+    while (PTR_NOT_EQUAL((table), (ptr), (key))) {\
+    (last) = &(ptr)->next; (ptr) = *(last);\
+    }\
+    if ((ptr) != NIL(st_table_entry) && (table)->reorder_flag) {\
+    *(last) = (ptr)->next;\
+    (ptr)->next = (table)->bins[hash_val];\
+    (table)->bins[hash_val] = (ptr);\
+    }
+
+int
+st_lookup(table, key, value)
+st_table *table;
+register char *key;
+char **value;
+{
+    int hash_val;
+    register st_table_entry *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr, last);
+    
+    if (ptr == NIL(st_table_entry)) {
+    return 0;
+    } else {
+    if (value != NIL(char *)) {
+        *value = ptr->record; 
+    }
+    return 1;
+    }
+}
+
+int
+st_lookup_int(table, key, value)
+st_table *table;
+register char *key;
+int *value;
+{
+    int hash_val;
+    register st_table_entry *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr, last);
+    
+    if (ptr == NIL(st_table_entry)) {
+    return 0;
+    } else {
+    if (value != NIL(int)) {
+        *value = (long) ptr->record;
+    }
+    return 1;
+    }
+}
+
+/* This macro does not check if memory allocation fails. Use at you own risk */
+#define ADD_DIRECT(table, key, value, hash_val, new)\
+{\
+    if (table->num_entries/table->num_bins >= table->max_density) {\
+    rehash(table);\
+    hash_val = do_hash(key,table);\
+    }\
+    \
+    new = ALLOC(st_table_entry, 1);\
+    \
+    new->key = key;\
+    new->record = value;\
+    new->next = table->bins[hash_val];\
+    table->bins[hash_val] = new;\
+    table->num_entries++;\
+}
+
+int
+st_insert(table, key, value)
+register st_table *table;
+register char *key;
+char *value;
+{
+    int hash_val;
+    st_table_entry *new;
+    register st_table_entry *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr, last);
+
+    if (ptr == NIL(st_table_entry)) {
+    if (table->num_entries/table->num_bins >= table->max_density) {
+        if (rehash(table) == ST_OUT_OF_MEM) {
+        return ST_OUT_OF_MEM;
+        }
+        hash_val = do_hash(key, table);
+    }
+    new = ALLOC(st_table_entry, 1);
+    if (new == NIL(st_table_entry)) {
+        return ST_OUT_OF_MEM;
+    }
+    new->key = key;
+    new->record = value;
+    new->next = table->bins[hash_val];
+    table->bins[hash_val] = new;
+    table->num_entries++;
+    return 0;
+    } else {
+    ptr->record = value;
+    return 1;
+    }
+}
+
+int
+st_add_direct(table, key, value)
+st_table *table;
+char *key;
+char *value;
+{
+    int hash_val;
+    st_table_entry *new;
+    
+    hash_val = do_hash(key, table);
+    if (table->num_entries / table->num_bins >= table->max_density) {
+    if (rehash(table) == ST_OUT_OF_MEM) {
+        return ST_OUT_OF_MEM;
+    }
+    }
+    hash_val = do_hash(key, table);
+    new = ALLOC(st_table_entry, 1);
+    if (new == NIL(st_table_entry)) {
+    return ST_OUT_OF_MEM;
+    }
+    new->key = key;
+    new->record = value;
+    new->next = table->bins[hash_val];
+    table->bins[hash_val] = new;
+    table->num_entries++;
+    return 1;
+}
+
+int
+st_find_or_add(table, key, slot)
+st_table *table;
+char *key;
+char ***slot;
+{
+    int hash_val;
+    st_table_entry *new, *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr, last);
+
+    if (ptr == NIL(st_table_entry)) {
+    if (table->num_entries / table->num_bins >= table->max_density) {
+        if (rehash(table) == ST_OUT_OF_MEM) {
+        return ST_OUT_OF_MEM;
+        }
+        hash_val = do_hash(key, table);
+    }
+    new = ALLOC(st_table_entry, 1);
+    if (new == NIL(st_table_entry)) {
+        return ST_OUT_OF_MEM;
+    }
+    new->key = key;
+    new->record = (char *) 0;
+    new->next = table->bins[hash_val];
+    table->bins[hash_val] = new;
+    table->num_entries++;
+    if (slot != NIL(char **)) *slot = &new->record;
+    return 0;
+    } else {
+    if (slot != NIL(char **)) *slot = &ptr->record;
+    return 1;
+    }
+}
+
+int
+st_find(table, key, slot)
+st_table *table;
+char *key;
+char ***slot;
+{
+    int hash_val;
+    st_table_entry *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr, last);
+
+    if (ptr == NIL(st_table_entry)) {
+    return 0;
+    } else {
+    if (slot != NIL(char **)) {
+        *slot = &ptr->record;
+    }
+    return 1;
+    }
+}
+
+static int
+rehash(table)
+register st_table *table;
+{
+    register st_table_entry *ptr, *next, **old_bins;
+    int             i, old_num_bins, hash_val, old_num_entries;
+
+    /* save old values */
+    old_bins = table->bins;
+    old_num_bins = table->num_bins;
+    old_num_entries = table->num_entries;
+
+    /* rehash */
+    table->num_bins = (int)(table->grow_factor * old_num_bins);
+    if (table->num_bins % 2 == 0) {
+    table->num_bins += 1;
+    }
+    table->num_entries = 0;
+    table->bins = ALLOC(st_table_entry *, table->num_bins);
+    if (table->bins == NIL(st_table_entry *)) {
+    table->bins = old_bins;
+    table->num_bins = old_num_bins;
+    table->num_entries = old_num_entries;
+    return ST_OUT_OF_MEM;
+    }
+    /* initialize */
+    for (i = 0; i < table->num_bins; i++) {
+    table->bins[i] = 0;
+    }
+
+    /* copy data over */
+    for (i = 0; i < old_num_bins; i++) {
+    ptr = old_bins[i];
+    while (ptr != NIL(st_table_entry)) {
+        next = ptr->next;
+        hash_val = do_hash(ptr->key, table);
+        ptr->next = table->bins[hash_val];
+        table->bins[hash_val] = ptr;
+        table->num_entries++;
+        ptr = next;
+    }
+    }
+    FREE(old_bins);
+
+    return 1;
+}
+
+st_table *
+st_copy(old_table)
+st_table *old_table;
+{
+    st_table *new_table;
+    st_table_entry *ptr, *newptr, *next, *new;
+    int i, j, num_bins = old_table->num_bins;
+
+    new_table = ALLOC(st_table, 1);
+    if (new_table == NIL(st_table)) {
+    return NIL(st_table);
+    }
+    
+    *new_table = *old_table;
+    new_table->bins = ALLOC(st_table_entry *, num_bins);
+    if (new_table->bins == NIL(st_table_entry *)) {
+    FREE(new_table);
+    return NIL(st_table);
+    }
+    for(i = 0; i < num_bins ; i++) {
+    new_table->bins[i] = NIL(st_table_entry);
+    ptr = old_table->bins[i];
+    while (ptr != NIL(st_table_entry)) {
+        new = ALLOC(st_table_entry, 1);
+        if (new == NIL(st_table_entry)) {
+        for (j = 0; j <= i; j++) {
+            newptr = new_table->bins[j];
+            while (newptr != NIL(st_table_entry)) {
+            next = newptr->next;
+            FREE(newptr);
+            newptr = next;
+            }
+        }
+        FREE(new_table->bins);
+        FREE(new_table);
+        return NIL(st_table);
+        }
+        *new = *ptr;
+        new->next = new_table->bins[i];
+        new_table->bins[i] = new;
+        ptr = ptr->next;
+    }
+    }
+    return new_table;
+}
+
+int
+st_delete(table, keyp, value)
+register st_table *table;
+register char **keyp;
+char **value;
+{
+    int hash_val;
+    char *key = *keyp;
+    register st_table_entry *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr ,last);
+    
+    if (ptr == NIL(st_table_entry)) {
+    return 0;
+    }
+
+    *last = ptr->next;
+    if (value != NIL(char *)) *value = ptr->record;
+    *keyp = ptr->key;
+    FREE(ptr);
+    table->num_entries--;
+    return 1;
+}
+
+int
+st_delete_int(table, keyp, value)
+register st_table *table;
+register long *keyp;
+char **value;
+{
+    int hash_val;
+    char *key = (char *) *keyp;
+    register st_table_entry *ptr, **last;
+
+    hash_val = do_hash(key, table);
+
+    FIND_ENTRY(table, hash_val, key, ptr ,last);
+
+    if (ptr == NIL(st_table_entry)) {
+        return 0;
+    }
+
+    *last = ptr->next;
+    if (value != NIL(char *)) *value = ptr->record;
+    *keyp = (long) ptr->key;
+    FREE(ptr);
+    table->num_entries--;
+    return 1;
+}
+
+int
+st_foreach(table, func, arg)
+st_table *table;
+enum st_retval (*func)();
+char *arg;
+{
+    st_table_entry *ptr, **last;
+    enum st_retval retval;
+    int i;
+
+    for(i = 0; i < table->num_bins; i++) {
+    last = &table->bins[i]; ptr = *last;
+    while (ptr != NIL(st_table_entry)) {
+        retval = (*func)(ptr->key, ptr->record, arg);
+        switch (retval) {
+        case ST_CONTINUE:
+        last = &ptr->next; ptr = *last;
+        break;
+        case ST_STOP:
+        return 0;
+        case ST_DELETE:
+        *last = ptr->next;
+        table->num_entries--;    /* cstevens@ic */
+        FREE(ptr);
+        ptr = *last;
+        }
+    }
+    }
+    return 1;
+}
+
+int
+st_strhash(string, modulus)
+register char *string;
+int modulus;
+{
+    register int val = 0;
+    register int c;
+    
+    while ((c = *string++) != '\0') {
+    val = val*997 + c;
+    }
+
+    return ((val < 0) ? -val : val)%modulus;
+}
+
+int
+st_numhash(x, size)
+char *x;
+int size;
+{
+    return ST_NUMHASH(x, size);
+}
+
+int
+st_ptrhash(x, size)
+char *x;
+int size;
+{
+    return ST_PTRHASH(x, size);
+}
+
+int
+st_numcmp(x, y)
+char *x;
+char *y;
+{
+    return ST_NUMCMP(x, y);
+}
+
+int
+st_ptrcmp(x, y)
+char *x;
+char *y;
+{
+    return ST_NUMCMP(x, y);
+}
+
+st_generator *
+st_init_gen(table)
+st_table *table;
+{
+    st_generator *gen;
+
+    gen = ALLOC(st_generator, 1);
+    if (gen == NIL(st_generator)) {
+    return NIL(st_generator);
+    }
+    gen->table = table;
+    gen->entry = NIL(st_table_entry);
+    gen->index = 0;
+    return gen;
+}
+
+
+int 
+st_gen(gen, key_p, value_p)
+st_generator *gen;
+char **key_p;
+char **value_p;
+{
+    register int i;
+
+    if (gen->entry == NIL(st_table_entry)) {
+    /* try to find next entry */
+    for(i = gen->index; i < gen->table->num_bins; i++) {
+        if (gen->table->bins[i] != NIL(st_table_entry)) {
+        gen->index = i+1;
+        gen->entry = gen->table->bins[i];
+        break;
+        }
+    }
+    if (gen->entry == NIL(st_table_entry)) {
+        return 0;        /* that's all folks ! */
+    }
+    }
+    *key_p = gen->entry->key;
+    if (value_p != 0) {
+    *value_p = gen->entry->record;
+    }
+    gen->entry = gen->entry->next;
+    return 1;
+}
+
+
+int 
+st_gen_int(gen, key_p, value_p)
+st_generator *gen;
+char **key_p;
+long *value_p;
+{
+    register int i;
+
+    if (gen->entry == NIL(st_table_entry)) {
+    /* try to find next entry */
+    for(i = gen->index; i < gen->table->num_bins; i++) {
+        if (gen->table->bins[i] != NIL(st_table_entry)) {
+        gen->index = i+1;
+        gen->entry = gen->table->bins[i];
+        break;
+        }
+    }
+    if (gen->entry == NIL(st_table_entry)) {
+        return 0;        /* that's all folks ! */
+    }
+    }
+    *key_p = gen->entry->key;
+    if (value_p != NIL(long)) {
+       *value_p = (long) gen->entry->record;
+    }
+    gen->entry = gen->entry->next;
+    return 1;
+}
+
+
+void
+st_free_gen(gen)
+st_generator *gen;
+{
+    FREE(gen);
+}
diff --git a/src/misc/st/st.h b/src/misc/st/st.h
new file mode 100644
index 00000000..c51873e9
--- /dev/null
+++ b/src/misc/st/st.h
@@ -0,0 +1,88 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/st/st.h,v
+ * serdar
+ * 1.1
+ * 1993/07/29 01:00:21
+ *
+ */
+/* LINTLIBRARY */
+
+/* /projects/hsis/CVS/utilities/st/st.h,v 1.1 1993/07/29 01:00:21 serdar Exp */
+
+#ifndef ST_INCLUDED
+#define ST_INCLUDED
+
+typedef struct st_table_entry st_table_entry;
+struct st_table_entry {
+    char *key;
+    char *record;
+    st_table_entry *next;
+};
+
+typedef struct st_table st_table;
+struct st_table {
+    int (*compare)();
+    int (*hash)();
+    int num_bins;
+    int num_entries;
+    int max_density;
+    int reorder_flag;
+    double grow_factor;
+    st_table_entry **bins;
+};
+
+typedef struct st_generator st_generator;
+struct st_generator {
+    st_table *table;
+    st_table_entry *entry;
+    int index;
+};
+
+#define st_is_member(table,key) st_lookup(table,key,(char **) 0)
+#define st_count(table) ((table)->num_entries)
+
+enum st_retval {ST_CONTINUE, ST_STOP, ST_DELETE};
+
+typedef enum st_retval (*ST_PFSR)();
+typedef int (*ST_PFI)();
+
+EXTERN st_table *st_init_table_with_params ARGS((ST_PFI, ST_PFI, int, int, double, int));
+EXTERN st_table *st_init_table ARGS((ST_PFI, ST_PFI)); 
+EXTERN void st_free_table ARGS((st_table *));
+EXTERN int st_lookup ARGS((st_table *, char *, char **));
+EXTERN int st_lookup_int ARGS((st_table *, char *, int *));
+EXTERN int st_insert ARGS((st_table *, char *, char *));
+EXTERN int st_add_direct ARGS((st_table *, char *, char *));
+EXTERN int st_find_or_add ARGS((st_table *, char *, char ***));
+EXTERN int st_find ARGS((st_table *, char *, char ***));
+EXTERN st_table *st_copy ARGS((st_table *));
+EXTERN int st_delete ARGS((st_table *, char **, char **));
+EXTERN int st_delete_int ARGS((st_table *, long *, char **));
+EXTERN int st_foreach ARGS((st_table *, ST_PFSR, char *));
+EXTERN int st_strhash ARGS((char *, int));
+EXTERN int st_numhash ARGS((char *, int));
+EXTERN int st_ptrhash ARGS((char *, int));
+EXTERN int st_numcmp ARGS((char *, char *));
+EXTERN int st_ptrcmp ARGS((char *, char *));
+EXTERN st_generator *st_init_gen ARGS((st_table *));
+EXTERN int st_gen ARGS((st_generator *, char **, char **));
+EXTERN int st_gen_int ARGS((st_generator *, char **, long *));
+EXTERN void st_free_gen ARGS((st_generator *));
+
+
+#define ST_DEFAULT_MAX_DENSITY 5
+#define ST_DEFAULT_INIT_TABLE_SIZE 11
+#define ST_DEFAULT_GROW_FACTOR 2.0
+#define ST_DEFAULT_REORDER_FLAG 0
+
+#define st_foreach_item(table, gen, key, value) \
+    for(gen=st_init_gen(table); st_gen(gen,key,value) || (st_free_gen(gen),0);)
+
+#define st_foreach_item_int(table, gen, key, value) \
+    for(gen=st_init_gen(table); st_gen_int(gen,key,value) || (st_free_gen(gen),0);)
+
+#define ST_OUT_OF_MEM -10000
+
+#endif /* ST_INCLUDED */
diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c
new file mode 100644
index 00000000..b75b0134
--- /dev/null
+++ b/src/misc/st/stmm.c
@@ -0,0 +1,683 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/st/st.c,v
+ * serdar
+ * 1.1
+ * 1993/07/29 01:00:13
+ *
+ */
+#include <stdio.h>
+#include "util.h"
+#include "stmm.h"
+
+#define STMM_NUMCMP(x,y) ((x) != (y))
+#define STMM_NUMHASH(x,size) (ABS((long)x)%(size))
+#define STMM_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size)
+#define EQUAL(func, x, y) \
+    ((((func) == stmm_numcmp) || ((func) == stmm_ptrcmp)) ?\
+      (STMM_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))
+
+
+#define do_hash(key, table)\
+    ((table->hash == stmm_ptrhash) ? STMM_PTRHASH((key),(table)->num_bins) :\
+     (table->hash == stmm_numhash) ? STMM_NUMHASH((key), (table)->num_bins) :\
+     (*table->hash)((key), (table)->num_bins))
+
+static int rehash ();
+int stmm_numhash (), stmm_ptrhash (), stmm_numcmp (), stmm_ptrcmp ();
+
+stmm_table *
+stmm_init_table_with_params (compare, hash, size, density, grow_factor,
+                 reorder_flag)
+    int (*compare) ();
+    int (*hash) ();
+    int size;
+    int density;
+    double grow_factor;
+    int reorder_flag;
+{
+    int i;
+    stmm_table *new;
+
+    new = ALLOC (stmm_table, 1);
+    if (new == NIL (stmm_table)) {
+    return NIL (stmm_table);
+    }
+    new->compare = compare;
+    new->hash = hash;
+    new->num_entries = 0;
+    new->max_density = density;
+    new->grow_factor = grow_factor;
+    new->reorder_flag = reorder_flag;
+    if (size <= 0) {
+    size = 1;
+    }
+    new->num_bins = size;
+    new->bins = ALLOC (stmm_table_entry *, size);
+    if (new->bins == NIL (stmm_table_entry *)) {
+    FREE (new);
+    return NIL (stmm_table);
+    }
+    for (i = 0; i < size; i++) {
+    new->bins[i] = 0;
+    }
+
+    // added by alanmi
+    new->pMemMan = Extra_MmFixedStart(sizeof (stmm_table_entry));
+    return new;
+}
+
+stmm_table *
+stmm_init_table (compare, hash)
+    int (*compare) ();
+    int (*hash) ();
+{
+    return stmm_init_table_with_params (compare, hash,
+                    STMM_DEFAULT_INIT_TABLE_SIZE,
+                    STMM_DEFAULT_MAX_DENSITY,
+                    STMM_DEFAULT_GROW_FACTOR,
+                    STMM_DEFAULT_REORDER_FLAG);
+}
+
+void
+stmm_free_table (table)
+    stmm_table *table;
+{
+/*
+    register stmm_table_entry *ptr, *next;
+    int i;
+    for ( i = 0; i < table->num_bins; i++ )
+    {
+        ptr = table->bins[i];
+        while ( ptr != NIL( stmm_table_entry ) )
+        {
+            next = ptr->next;
+            FREE( ptr );
+            ptr = next;
+        }
+    }
+*/
+    // no need to deallocate entries because they are in the memory manager now
+    // added by alanmi
+    if ( table->pMemMan )
+        Extra_MmFixedStop (table->pMemMan, 0);
+    FREE (table->bins);
+    FREE (table);
+}
+
+// this function recycles all the bins
+void
+stmm_clean (table)
+    stmm_table *table;
+{
+    int i;
+    // clean the bins
+    for (i = 0; i < table->num_bins; i++)
+        table->bins[i] = NULL;
+    // reset the parameters
+    table->num_entries = 0;
+    // restart the memory manager
+    Extra_MmFixedRestart (table->pMemMan);
+}
+
+
+#define PTR_NOT_EQUAL(table, ptr, user_key)\
+(ptr != NIL(stmm_table_entry) && !EQUAL(table->compare, user_key, (ptr)->key))
+
+#define FIND_ENTRY(table, hash_val, key, ptr, last) \
+    (last) = &(table)->bins[hash_val];\
+    (ptr) = *(last);\
+    while (PTR_NOT_EQUAL((table), (ptr), (key))) {\
+    (last) = &(ptr)->next; (ptr) = *(last);\
+    }\
+    if ((ptr) != NIL(stmm_table_entry) && (table)->reorder_flag) {\
+    *(last) = (ptr)->next;\
+    (ptr)->next = (table)->bins[hash_val];\
+    (table)->bins[hash_val] = (ptr);\
+    }
+
+int
+stmm_lookup (table, key, value)
+    stmm_table *table;
+    register char *key;
+    char **value;
+{
+    int hash_val;
+    register stmm_table_entry *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    return 0;
+    }
+    else {
+    if (value != NIL (char *))
+    {
+        *value = ptr->record;
+    }
+    return 1;
+    }
+}
+
+int
+stmm_lookup_int (table, key, value)
+    stmm_table *table;
+    register char *key;
+    int *value;
+{
+    int hash_val;
+    register stmm_table_entry *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    return 0;
+    }
+    else {
+    if (value != NIL (int))
+    {
+        *value = (long) ptr->record;
+    }
+    return 1;
+    }
+}
+
+// This macro contained a line
+//    new = ALLOC(stmm_table_entry, 1);
+// which was modified by alanmi
+
+
+/* This macro does not check if memory allocation fails. Use at you own risk */
+#define ADD_DIRECT(table, key, value, hash_val, new)\
+{\
+    if (table->num_entries/table->num_bins >= table->max_density) {\
+    rehash(table);\
+    hash_val = do_hash(key,table);\
+    }\
+    \
+    new = (stmm_table_entry *)Extra_MmFixedEntryFetch( table->pMemMan );\
+    \
+    new->key = key;\
+    new->record = value;\
+    new->next = table->bins[hash_val];\
+    table->bins[hash_val] = new;\
+    table->num_entries++;\
+}
+
+int
+stmm_insert (table, key, value)
+    register stmm_table *table;
+    register char *key;
+    char *value;
+{
+    int hash_val;
+    stmm_table_entry *new;
+    register stmm_table_entry *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    if (table->num_entries / table->num_bins >= table->max_density) {
+        if (rehash (table) == STMM_OUT_OF_MEM) {
+        return STMM_OUT_OF_MEM;
+        }
+        hash_val = do_hash (key, table);
+    }
+
+//              new = ALLOC( stmm_table_entry, 1 );
+    new = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+    if (new == NIL (stmm_table_entry)) {
+        return STMM_OUT_OF_MEM;
+    }
+
+    new->key = key;
+    new->record = value;
+    new->next = table->bins[hash_val];
+    table->bins[hash_val] = new;
+    table->num_entries++;
+    return 0;
+    }
+    else {
+    ptr->record = value;
+    return 1;
+    }
+}
+
+int
+stmm_add_direct (table, key, value)
+    stmm_table *table;
+    char *key;
+    char *value;
+{
+    int hash_val;
+    stmm_table_entry *new;
+
+    hash_val = do_hash (key, table);
+    if (table->num_entries / table->num_bins >= table->max_density) {
+    if (rehash (table) == STMM_OUT_OF_MEM) {
+        return STMM_OUT_OF_MEM;
+    }
+    }
+    hash_val = do_hash (key, table);
+
+//      new = ALLOC( stmm_table_entry, 1 );
+    new = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+    if (new == NIL (stmm_table_entry)) {
+    return STMM_OUT_OF_MEM;
+    }
+
+    new->key = key;
+    new->record = value;
+    new->next = table->bins[hash_val];
+    table->bins[hash_val] = new;
+    table->num_entries++;
+    return 1;
+}
+
+int
+stmm_find_or_add (table, key, slot)
+    stmm_table *table;
+    char *key;
+    char ***slot;
+{
+    int hash_val;
+    stmm_table_entry *new, *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    if (table->num_entries / table->num_bins >= table->max_density) {
+        if (rehash (table) == STMM_OUT_OF_MEM) {
+        return STMM_OUT_OF_MEM;
+        }
+        hash_val = do_hash (key, table);
+    }
+
+    // new = ALLOC( stmm_table_entry, 1 );
+    new = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+    if (new == NIL (stmm_table_entry)) {
+        return STMM_OUT_OF_MEM;
+    }
+
+    new->key = key;
+    new->record = (char *) 0;
+    new->next = table->bins[hash_val];
+    table->bins[hash_val] = new;
+    table->num_entries++;
+    if (slot != NIL (char **))
+         *slot = &new->record;
+    return 0;
+    }
+    else {
+    if (slot != NIL (char **))
+         *slot = &ptr->record;
+    return 1;
+    }
+}
+
+int
+stmm_find (table, key, slot)
+    stmm_table *table;
+    char *key;
+    char ***slot;
+{
+    int hash_val;
+    stmm_table_entry *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    return 0;
+    }
+    else {
+    if (slot != NIL (char **))
+    {
+        *slot = &ptr->record;
+    }
+    return 1;
+    }
+}
+
+static int
+rehash (table)
+    register stmm_table *table;
+{
+    register stmm_table_entry *ptr, *next, **old_bins;
+    int i, old_num_bins, hash_val, old_num_entries;
+
+    /* save old values */
+    old_bins = table->bins;
+    old_num_bins = table->num_bins;
+    old_num_entries = table->num_entries;
+
+    /* rehash */
+    table->num_bins = (int) (table->grow_factor * old_num_bins);
+    if (table->num_bins % 2 == 0) {
+    table->num_bins += 1;
+    }
+    table->num_entries = 0;
+    table->bins = ALLOC (stmm_table_entry *, table->num_bins);
+    if (table->bins == NIL (stmm_table_entry *)) {
+    table->bins = old_bins;
+    table->num_bins = old_num_bins;
+    table->num_entries = old_num_entries;
+    return STMM_OUT_OF_MEM;
+    }
+    /* initialize */
+    for (i = 0; i < table->num_bins; i++) {
+    table->bins[i] = 0;
+    }
+
+    /* copy data over */
+    for (i = 0; i < old_num_bins; i++) {
+    ptr = old_bins[i];
+    while (ptr != NIL (stmm_table_entry)) {
+        next = ptr->next;
+        hash_val = do_hash (ptr->key, table);
+        ptr->next = table->bins[hash_val];
+        table->bins[hash_val] = ptr;
+        table->num_entries++;
+        ptr = next;
+    }
+    }
+    FREE (old_bins);
+
+    return 1;
+}
+
+stmm_table *
+stmm_copy (old_table)
+    stmm_table *old_table;
+{
+    stmm_table *new_table;
+    stmm_table_entry *ptr, /* *newptr, *next, */ *new;
+    int i, /*j, */ num_bins = old_table->num_bins;
+
+    new_table = ALLOC (stmm_table, 1);
+    if (new_table == NIL (stmm_table)) {
+    return NIL (stmm_table);
+    }
+
+    *new_table = *old_table;
+    new_table->bins = ALLOC (stmm_table_entry *, num_bins);
+    if (new_table->bins == NIL (stmm_table_entry *)) {
+    FREE (new_table);
+    return NIL (stmm_table);
+    }
+
+    // allocate the memory manager for the new table
+    new_table->pMemMan =
+    Extra_MmFixedStart (sizeof (stmm_table_entry));
+
+    for (i = 0; i < num_bins; i++) {
+    new_table->bins[i] = NIL (stmm_table_entry);
+    ptr = old_table->bins[i];
+    while (ptr != NIL (stmm_table_entry)) {
+//                      new = ALLOC( stmm_table_entry, 1 );
+        new =
+        (stmm_table_entry *) Extra_MmFixedEntryFetch (new_table->
+                                pMemMan);
+
+        if (new == NIL (stmm_table_entry)) {
+/*
+                for ( j = 0; j <= i; j++ )
+                {
+                    newptr = new_table->bins[j];
+                    while ( newptr != NIL( stmm_table_entry ) )
+                    {
+                        next = newptr->next;
+                        FREE( newptr );
+                        newptr = next;
+                    }
+                }
+*/
+        Extra_MmFixedStop (new_table->pMemMan, 0);
+
+        FREE (new_table->bins);
+        FREE (new_table);
+        return NIL (stmm_table);
+        }
+        *new = *ptr;
+        new->next = new_table->bins[i];
+        new_table->bins[i] = new;
+        ptr = ptr->next;
+    }
+    }
+    return new_table;
+}
+
+int
+stmm_delete (table, keyp, value)
+    register stmm_table *table;
+    register char **keyp;
+    char **value;
+{
+    int hash_val;
+    char *key = *keyp;
+    register stmm_table_entry *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    return 0;
+    }
+
+    *last = ptr->next;
+    if (value != NIL (char *))
+     *value = ptr->record;
+    *keyp = ptr->key;
+//      FREE( ptr );
+    Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+
+    table->num_entries--;
+    return 1;
+}
+
+int
+stmm_delete_int (table, keyp, value)
+    register stmm_table *table;
+    register long *keyp;
+    char **value;
+{
+    int hash_val;
+    char *key = (char *) *keyp;
+    register stmm_table_entry *ptr, **last;
+
+    hash_val = do_hash (key, table);
+
+    FIND_ENTRY (table, hash_val, key, ptr, last);
+
+    if (ptr == NIL (stmm_table_entry)) {
+    return 0;
+    }
+
+    *last = ptr->next;
+    if (value != NIL (char *))
+     *value = ptr->record;
+    *keyp = (long) ptr->key;
+//      FREE( ptr );
+    Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+
+    table->num_entries--;
+    return 1;
+}
+
+int
+stmm_foreach (table, func, arg)
+    stmm_table *table;
+    enum stmm_retval (*func) ();
+    char *arg;
+{
+    stmm_table_entry *ptr, **last;
+    enum stmm_retval retval;
+    int i;
+
+    for (i = 0; i < table->num_bins; i++) {
+    last = &table->bins[i];
+    ptr = *last;
+    while (ptr != NIL (stmm_table_entry)) {
+        retval = (*func) (ptr->key, ptr->record, arg);
+        switch (retval) {
+        case STMM_CONTINUE:
+        last = &ptr->next;
+        ptr = *last;
+        break;
+        case STMM_STOP:
+        return 0;
+        case STMM_DELETE:
+        *last = ptr->next;
+        table->num_entries--;    /* cstevens@ic */
+//                              FREE( ptr );
+        Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+
+        ptr = *last;
+        }
+    }
+    }
+    return 1;
+}
+
+int
+stmm_strhash (string, modulus)
+    register char *string;
+    int modulus;
+{
+    register int val = 0;
+    register int c;
+
+    while ((c = *string++) != '\0') {
+    val = val * 997 + c;
+    }
+
+    return ((val < 0) ? -val : val) % modulus;
+}
+
+int
+stmm_numhash (x, size)
+    char *x;
+    int size;
+{
+    return STMM_NUMHASH (x, size);
+}
+
+int
+stmm_ptrhash (x, size)
+    char *x;
+    int size;
+{
+    return STMM_PTRHASH (x, size);
+}
+
+int
+stmm_numcmp (x, y)
+    char *x;
+    char *y;
+{
+    return STMM_NUMCMP (x, y);
+}
+
+int
+stmm_ptrcmp (x, y)
+    char *x;
+    char *y;
+{
+    return STMM_NUMCMP (x, y);
+}
+
+stmm_generator *
+stmm_init_gen (table)
+    stmm_table *table;
+{
+    stmm_generator *gen;
+
+    gen = ALLOC (stmm_generator, 1);
+    if (gen == NIL (stmm_generator)) {
+    return NIL (stmm_generator);
+    }
+    gen->table = table;
+    gen->entry = NIL (stmm_table_entry);
+    gen->index = 0;
+    return gen;
+}
+
+
+int
+stmm_gen (gen, key_p, value_p)
+    stmm_generator *gen;
+    char **key_p;
+    char **value_p;
+{
+    register int i;
+
+    if (gen->entry == NIL (stmm_table_entry)) {
+    /* try to find next entry */
+    for (i = gen->index; i < gen->table->num_bins; i++) {
+        if (gen->table->bins[i] != NIL (stmm_table_entry)) {
+        gen->index = i + 1;
+        gen->entry = gen->table->bins[i];
+        break;
+        }
+    }
+    if (gen->entry == NIL (stmm_table_entry)) {
+        return 0;        /* that's all folks ! */
+    }
+    }
+    *key_p = gen->entry->key;
+    if (value_p != 0) {
+    *value_p = gen->entry->record;
+    }
+    gen->entry = gen->entry->next;
+    return 1;
+}
+
+
+int
+stmm_gen_int (gen, key_p, value_p)
+    stmm_generator *gen;
+    char **key_p;
+    long *value_p;
+{
+    register int i;
+
+    if (gen->entry == NIL (stmm_table_entry)) {
+    /* try to find next entry */
+    for (i = gen->index; i < gen->table->num_bins; i++) {
+        if (gen->table->bins[i] != NIL (stmm_table_entry)) {
+        gen->index = i + 1;
+        gen->entry = gen->table->bins[i];
+        break;
+        }
+    }
+    if (gen->entry == NIL (stmm_table_entry)) {
+        return 0;        /* that's all folks ! */
+    }
+    }
+    *key_p = gen->entry->key;
+    if (value_p != NIL (long))
+    {
+    *value_p = (long) gen->entry->record;
+    }
+    gen->entry = gen->entry->next;
+    return 1;
+}
+
+
+void
+stmm_free_gen (gen)
+    stmm_generator *gen;
+{
+    FREE (gen);
+}
diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h
new file mode 100644
index 00000000..1fe3dfd2
--- /dev/null
+++ b/src/misc/st/stmm.h
@@ -0,0 +1,119 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/st/st.h,v
+ * serdar
+ * 1.1
+ * 1993/07/29 01:00:21
+ *
+ */
+/* LINTLIBRARY */
+
+/* /projects/hsis/CVS/utilities/st/st.h,v 1.1 1993/07/29 01:00:21 serdar Exp */
+
+#ifndef STMM_INCLUDED
+#define STMM_INCLUDED
+
+#include "extra.h"
+
+typedef struct stmm_table_entry stmm_table_entry;
+typedef struct stmm_table stmm_table;
+typedef struct stmm_generator stmm_generator;
+
+struct stmm_table_entry
+{
+    char *key;
+    char *record;
+    stmm_table_entry *next;
+};
+
+struct stmm_table
+{
+    int (*compare) ();
+    int (*hash) ();
+    int num_bins;
+    int num_entries;
+    int max_density;
+    int reorder_flag;
+    double grow_factor;
+    stmm_table_entry **bins;
+    // memory manager to improve runtime and prevent memory fragmentation
+    // added by alanmi - January 16, 2003
+    Extra_MmFixed_t *pMemMan;
+};
+
+struct stmm_generator
+{
+    stmm_table *table;
+    stmm_table_entry *entry;
+    int index;
+};
+
+#define stmm_is_member(table,key) stmm_lookup(table,key,(char **) 0)
+#define stmm_count(table) ((table)->num_entries)
+
+enum stmm_retval
+{ STMM_CONTINUE, STMM_STOP, STMM_DELETE };
+
+typedef enum stmm_retval (*STMM_PFSR) ();
+typedef int (*STMM_PFI) ();
+
+EXTERN stmm_table *stmm_init_table_with_params
+ARGS ((STMM_PFI, STMM_PFI, int, int, double, int));
+EXTERN stmm_table *stmm_init_table ARGS ((STMM_PFI, STMM_PFI));
+EXTERN void stmm_free_table ARGS ((stmm_table *));
+EXTERN int stmm_lookup ARGS ((stmm_table *, char *, char **));
+EXTERN int stmm_lookup_int ARGS ((stmm_table *, char *, int *));
+EXTERN int stmm_insert ARGS ((stmm_table *, char *, char *));
+EXTERN int stmm_add_direct ARGS ((stmm_table *, char *, char *));
+EXTERN int stmm_find_or_add ARGS ((stmm_table *, char *, char ***));
+EXTERN int stmm_find ARGS ((stmm_table *, char *, char ***));
+EXTERN stmm_table *stmm_copy ARGS ((stmm_table *));
+EXTERN int stmm_delete ARGS ((stmm_table *, char **, char **));
+EXTERN int stmm_delete_int ARGS ((stmm_table *, long *, char **));
+EXTERN int stmm_foreach ARGS ((stmm_table *, STMM_PFSR, char *));
+EXTERN int stmm_strhash ARGS ((char *, int));
+EXTERN int stmm_numhash ARGS ((char *, int));
+EXTERN int stmm_ptrhash ARGS ((char *, int));
+EXTERN int stmm_numcmp ARGS ((char *, char *));
+EXTERN int stmm_ptrcmp ARGS ((char *, char *));
+EXTERN stmm_generator *stmm_init_gen ARGS ((stmm_table *));
+EXTERN int stmm_gen ARGS ((stmm_generator *, char **, char **));
+EXTERN int stmm_gen_int ARGS ((stmm_generator *, char **, long *));
+EXTERN void stmm_free_gen ARGS ((stmm_generator *));
+// additional functions
+EXTERN void stmm_clean ARGS ((stmm_table *));
+
+
+
+#define STMM_DEFAULT_MAX_DENSITY        5
+#define STMM_DEFAULT_INIT_TABLE_SIZE   11
+#define STMM_DEFAULT_GROW_FACTOR      2.0
+#define STMM_DEFAULT_REORDER_FLAG       0
+
+// added by Zhihong: no need for memory allocation
+#define stmm_foreach_item2(tb, /* stmm_generator */gen, key, value) \
+    for(gen.table=(tb), gen.entry=NIL(stmm_table_entry), gen.index=0; \
+        stmm_gen(&(gen),key,value);)
+
+#define stmm_foreach_item(table, gen, key, value) \
+    for(gen=stmm_init_gen(table); stmm_gen(gen,key,value) || (stmm_free_gen(gen),0);)
+
+#define stmm_foreach_item_int(table, gen, key, value) \
+    for(gen=stmm_init_gen(table); stmm_gen_int(gen,key,value) || (stmm_free_gen(gen),0);)
+
+#define STMM_OUT_OF_MEM -10000
+
+/*
+
+// consider adding these other other similar definitions
+#define st_table       stmm_table
+#define st_insert      stmm_insert
+#define st_delete      stmm_delete
+#define st_lookup      stmm_lookup
+#define st_init_table  stmm_init_table
+#define st_free_table  stmm_free_table
+
+*/
+
+#endif /* STMM_INCLUDED */
diff --git a/src/misc/util/cpu_stats.c b/src/misc/util/cpu_stats.c
new file mode 100644
index 00000000..aa2d18ef
--- /dev/null
+++ b/src/misc/util/cpu_stats.c
@@ -0,0 +1,122 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/util/cpu_stats.c,v
+ * rajeev
+ * 1.4
+ * 1995/08/08 22:41:17
+ *
+ */
+/* LINTLIBRARY */
+
+#include <stdio.h>
+#include "util.h"
+
+
+#include <sys/types.h>
+//#include <sys/time.h>
+#ifdef HAVE_SYS_RESOURCE_H
+#  include <sys/resource.h>
+#endif
+
+#if defined(_IBMR2)
+#define etext _etext
+#define edata _edata
+#define end _end
+#endif
+
+#ifndef __CYGWIN32__
+extern int end, etext, edata;
+#endif
+
+void
+util_print_cpu_stats(fp)
+FILE *fp;
+{
+    (void) fprintf(fp, "Usage statistics not available\n");
+}
+
+#if 0
+
+void
+util_print_cpu_stats(fp)
+FILE *fp;
+{
+#if HAVE_SYS_RESOURCE_H && !defined(__CYGWIN32__)
+    struct rusage rusage;
+#ifdef RLIMIT_DATA
+    struct rlimit rlp;
+#endif
+    int text, data, vm_limit, vm_soft_limit;
+    double user, system, scale;
+    char hostname[257];
+    int vm_text, vm_init_data, vm_uninit_data, vm_sbrk_data;
+
+    /* Get the hostname */
+    (void) gethostname(hostname, 256);
+    hostname[256] = '\0';        /* just in case */
+
+    /* Get the virtual memory sizes */
+    vm_text = ((int) (&etext)) / 1024.0 + 0.5;
+    vm_init_data = ((int) (&edata) - (int) (&etext)) / 1024.0 + 0.5;
+    vm_uninit_data = ((int) (&end) - (int) (&edata)) / 1024.0 + 0.5;
+    vm_sbrk_data = (sizeof(char) * ((char *) sbrk(0) - (char *) (&end))) / 1024.0 + 0.5; 
+
+    /* Get virtual memory limits */
+#ifdef RLIMIT_DATA /* In HP-UX, with cc, this constant does not exist */
+    (void) getrlimit(RLIMIT_DATA, &rlp);
+    vm_limit = rlp.rlim_max / 1024.0 + 0.5;
+    vm_soft_limit = rlp.rlim_cur / 1024.0 + 0.5;
+#else
+    vm_limit = -1;
+    vm_soft_limit = -1;
+#endif      
+
+    /* Get usage stats */
+    (void) getrusage(RUSAGE_SELF, &rusage);
+    user = rusage.ru_utime.tv_sec + rusage.ru_utime.tv_usec/1.0e6;
+    system = rusage.ru_stime.tv_sec + rusage.ru_stime.tv_usec/1.0e6;
+    scale = (user + system)*100.0;
+    if (scale == 0.0) scale = 0.001;
+
+    (void) fprintf(fp, "Runtime Statistics\n");
+    (void) fprintf(fp, "------------------\n");
+    (void) fprintf(fp, "Machine name: %s\n", hostname);
+    (void) fprintf(fp, "User time   %6.1f seconds\n", user);
+    (void) fprintf(fp, "System time %6.1f seconds\n\n", system);
+
+    text = rusage.ru_ixrss / scale + 0.5;
+    data = (rusage.ru_idrss + rusage.ru_isrss) / scale + 0.5;
+    (void) fprintf(fp, "Average resident text size       = %5dK\n", text);
+    (void) fprintf(fp, "Average resident data+stack size = %5dK\n", data);
+    (void) fprintf(fp, "Maximum resident size            = %5ldK\n\n", 
+    rusage.ru_maxrss/2);
+    (void) fprintf(fp, "Virtual text size                = %5dK\n", 
+    vm_text);
+    (void) fprintf(fp, "Virtual data size                = %5dK\n", 
+    vm_init_data + vm_uninit_data + vm_sbrk_data);
+    (void) fprintf(fp, "    data size initialized        = %5dK\n", 
+    vm_init_data);
+    (void) fprintf(fp, "    data size uninitialized      = %5dK\n", 
+    vm_uninit_data);
+    (void) fprintf(fp, "    data size sbrk               = %5dK\n", 
+    vm_sbrk_data);
+    /* In some platforms, this constant does not exist */
+#ifdef RLIMIT_DATA 
+    (void) fprintf(fp, "Virtual memory limit             = %5dK (%dK)\n\n", 
+    vm_soft_limit, vm_limit);
+#endif
+    (void) fprintf(fp, "Major page faults = %ld\n", rusage.ru_majflt);
+    (void) fprintf(fp, "Minor page faults = %ld\n", rusage.ru_minflt);
+    (void) fprintf(fp, "Swaps = %ld\n", rusage.ru_nswap);
+    (void) fprintf(fp, "Input blocks = %ld\n", rusage.ru_inblock);
+    (void) fprintf(fp, "Output blocks = %ld\n", rusage.ru_oublock);
+    (void) fprintf(fp, "Context switch (voluntary) = %ld\n", rusage.ru_nvcsw);
+    (void) fprintf(fp, "Context switch (involuntary) = %ld\n", rusage.ru_nivcsw);
+#else /* Do not have sys/resource.h */
+    (void) fprintf(fp, "Usage statistics not available\n");
+#endif
+}
+
+#endif
+
diff --git a/src/misc/util/cpu_time.c b/src/misc/util/cpu_time.c
new file mode 100644
index 00000000..d264bdc9
--- /dev/null
+++ b/src/misc/util/cpu_time.c
@@ -0,0 +1,128 @@
+/**CFile***********************************************************************
+
+  FileName    [ cpu_time.c ]
+
+  PackageName [ util ]
+
+  Synopsis    [ System time calls ]
+
+  Description [ The problem is that all unix systems have a different notion
+        of how fast time goes (i.e., the units returned by).  This
+        returns a consistent result. ]
+
+  Author      [ Stephen Edwards <sedwards@eecs.berkeley.edu> and others ]
+
+  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
+  All rights reserved.
+
+  Permission is hereby granted, without written agreement and without license
+  or royalty fees, to use, copy, modify, and distribute this software and its
+  documentation for any purpose, provided that the above copyright notice and
+  the following two paragraphs appear in all copies of this software.
+
+  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
+  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
+  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
+  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
+  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
+  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
+  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
+
+******************************************************************************/
+
+#include "util.h"
+
+#if HAVE_SYS_TYPES_H
+#  include<sys/types.h>
+#endif
+
+#if HAVE_SYS_TIMES_H
+#  include<sys/times.h>
+#endif
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+/**Function********************************************************************
+
+  Synopsis           [ Return elapsed time in milliseconds ]
+
+  Description        [ Return a long which represents the elapsed time in
+               milliseconds since some constant reference. <P>
+
+               There are two possibilities:
+               <OL>
+               <LI> The system is non-POSIX compliant, so unistd.h
+                    and hence sysconf() can't tell us the clock tick
+                speed.  At this point, we have to resort to
+                using the user-settable CLOCK_RESOLUTION definition
+                to get the right speed
+               <LI> The system is POSIX-compliant.  unistd.h gives
+                    us sysconf(), which tells us the clock rate.
+               </OL>
+ ]
+
+  SideEffects        [ none ]
+
+******************************************************************************/
+
+/*
+long 
+util_cpu_time()
+{
+    long t = 0;
+
+#if HAVE_SYSCONF == 1
+
+    // Code for POSIX systems 
+
+    struct tms buffer;
+    long nticks;                // number of clock ticks per second 
+
+    nticks = sysconf(_SC_CLK_TCK);
+    times(&buffer);
+    t = buffer.tms_utime * (1000.0/nticks);
+
+#else
+#  ifndef vms
+
+    // Code for non-POSIX systems 
+
+    struct tms buffer;
+
+    time(&buffer);
+    t = buffer.tms_utime * 1000.0 / CLOCK_RESOLUTION;
+
+#  else
+
+    // Code for VMS (?) 
+
+    struct {int p1, p2, p3, p4;} buffer;
+    static long ref_time;
+    times(&buffer);
+    t = buffer.p1 * 10;
+    if (ref_time == 0)
+      ref_time = t;
+    t = t - ref_time;
+
+#  endif // vms 
+#endif // _POSIX_VERSION 
+
+    return t;
+}
+*/
+
+
+long 
+util_cpu_time()
+{
+    return clock();
+}
diff --git a/src/misc/util/datalimit.c b/src/misc/util/datalimit.c
new file mode 100644
index 00000000..96c2ce95
--- /dev/null
+++ b/src/misc/util/datalimit.c
@@ -0,0 +1,95 @@
+/**CFile************************************************************************
+
+  FileName    [datalimit.c]
+
+  PackageName [util]
+
+  Synopsis [Routine to obtain the maximum data size available to a program. The
+  routine is based on "getrlimit". If the system does not have this function,
+  the default value RLIMIT_DATA_DEFAULT is assumed. This function provides an
+  informative value, it does not restrict the size of the program in any way.]
+
+  Author      [Fabio Somenzi <fabio@colorado.edu>]
+
+  Copyright   [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include "util.h"
+
+static char rcsid[] UNUSED = "$Id: datalimit.c,v 1.1.1.1 2003/02/24 22:24:04 wjiang Exp $";
+
+#if HAVE_SYS_RESOURCE_H
+#if HAVE_SYS_TIME_H
+#include <sys/time.h>
+#endif
+#include <sys/resource.h>
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations                                                    */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+#ifndef RLIMIT_DATA_DEFAULT
+#define RLIMIT_DATA_DEFAULT 67108864    /* assume 64MB by default */
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis           [Function that computes the data limit of the process.]
+
+  SideEffects        []
+
+******************************************************************************/
+int
+getSoftDataLimit()
+{
+#if HAVE_SYS_RESOURCE_H && HAVE_GETRLIMIT && defined(RLIMIT_DATA)
+    struct rlimit rl;
+    int result;
+
+    result = getrlimit(RLIMIT_DATA, &rl);
+    if (result != 0 || rl.rlim_cur == RLIM_INFINITY)
+    return(RLIMIT_DATA_DEFAULT);
+    else
+    return(rl.rlim_cur);
+#else
+    return(RLIMIT_DATA_DEFAULT);
+#endif
+
+} /* end of getSoftDataLimit */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
diff --git a/src/misc/util/getopt.c b/src/misc/util/getopt.c
new file mode 100644
index 00000000..778c34d6
--- /dev/null
+++ b/src/misc/util/getopt.c
@@ -0,0 +1,84 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/util/getopt.c,v
+ * rajeev
+ * 1.3
+ * 1995/08/08 22:41:22
+ *
+ */
+/* LINTLIBRARY */
+
+#include <stdio.h>
+#include "util.h"
+
+
+/*  File   : getopt.c
+ *  Author : Henry Spencer, University of Toronto
+ *  Updated: 28 April 1984
+ *
+ *  Changes: (R Rudell)
+ *    changed index() to strchr();
+ *    added getopt_reset() to reset the getopt argument parsing
+ *
+ *  Purpose: get option letter from argv.
+ */
+
+char *util_optarg;    /* Global argument pointer. */
+int util_optind = 0;    /* Global argv index. */
+static char *scan;
+
+
+void
+util_getopt_reset()
+{
+    util_optarg = 0;
+    util_optind = 0;
+    scan = 0;
+}
+
+
+
+int 
+util_getopt(argc, argv, optstring)
+int argc;
+char *argv[];
+char *optstring;
+{
+    register int c;
+    register char *place;
+
+    util_optarg = NIL(char);
+
+    if (scan == NIL(char) || *scan == '\0') {
+    if (util_optind == 0) util_optind++;
+    if (util_optind >= argc) return EOF;
+    place = argv[util_optind];
+    if (place[0] != '-' || place[1] == '\0') return EOF;
+    util_optind++;
+    if (place[1] == '-' && place[2] == '\0') return EOF;
+    scan = place+1;
+    }
+
+    c = *scan++;
+    place = strchr(optstring, c);
+    if (place == NIL(char) || c == ':') {
+    (void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
+    return '?';
+    }
+    if (*++place == ':') {
+    if (*scan != '\0') {
+        util_optarg = scan;
+        scan = NIL(char);
+    } else {
+        if (util_optind >= argc) {
+        (void) fprintf(stderr, "%s: %c requires an argument\n", 
+            argv[0], c);
+        return '?';
+        }
+        util_optarg = argv[util_optind];
+        util_optind++;
+    }
+    }
+    return c;
+}
diff --git a/src/misc/util/leaks.h b/src/misc/util/leaks.h
new file mode 100644
index 00000000..daa628b1
--- /dev/null
+++ b/src/misc/util/leaks.h
@@ -0,0 +1,30 @@
+///////////////////////////////////////////////////////////////////////
+// This file is used to detect memory leaks using Visual Studio 6.0
+// The idea comes from the following webpage:
+// http://www.michaelmoser.org/memory.htm
+//////////////////////////////////////
+
+#ifndef __LEAKS_H__
+#define __LEAKS_H__
+
+#ifdef _DEBUG
+#define _CRTDBG_MAP_ALLOC // include Microsoft memory leak detection procedures
+//#define _INC_MALLOC         // exclude standard memory alloc procedures
+
+#define   malloc(s)         _malloc_dbg(s, _NORMAL_BLOCK, __FILE__, __LINE__)
+#define   calloc(c, s)      _calloc_dbg(c, s, _NORMAL_BLOCK, __FILE__, __LINE__)
+#define   realloc(p, s)     _realloc_dbg(p, s, _NORMAL_BLOCK, __FILE__, __LINE__)
+//#define   _expand(p, s)     _expand_dbg(p, s, _NORMAL_BLOCK, __FILE__, __LINE__)
+//#define   free(p)           _free_dbg(p, _NORMAL_BLOCK)
+//#define   _msize(p)         _msize_dbg(p, _NORMAL_BLOCK)
+
+//#include <stdlib.h>
+#include <stdlib_hack.h>
+#include <crtdbg.h>
+#endif
+
+#endif
+
+//////////////////////////////////////
+
+
diff --git a/src/misc/util/module.make b/src/misc/util/module.make
new file mode 100644
index 00000000..06eba7e4
--- /dev/null
+++ b/src/misc/util/module.make
@@ -0,0 +1,8 @@
+SRC +=  src/misc/util/cpu_stats.c \
+    src/misc/util/cpu_time.c \
+    src/misc/util/datalimit.c \
+    src/misc/util/getopt.c \
+    src/misc/util/pathsearch.c \
+    src/misc/util/safe_mem.c \
+    src/misc/util/strsav.c \
+    src/misc/util/texpand.c
diff --git a/src/misc/util/pathsearch.c b/src/misc/util/pathsearch.c
new file mode 100644
index 00000000..d4d845eb
--- /dev/null
+++ b/src/misc/util/pathsearch.c
@@ -0,0 +1,131 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/util/pathsearch.c,v
+ * rajeev
+ * 1.3
+ * 1995/08/08 22:41:24
+ *
+ */
+/* LINTLIBRARY */
+
+#if HAVE_SYS_FILE_H
+#  include <sys/file.h>
+#endif
+
+#if HAVE_SYS_STAT_H
+#  include <sys/stat.h>
+#endif
+
+#include "util.h"
+
+/**Function********************************************************************
+
+  Synopsis           [ Check that a given file is present and accessible ]
+
+  SideEffects        [none]
+******************************************************************************/
+static int
+check_file(filename, mode)
+char *filename;
+char *mode;
+{
+#if defined(HAVE_SYS_STAT_H)
+    struct stat stat_rec;
+    int access_char = mode[0];
+    int access_mode = R_OK;
+
+    /* First check that the file is a regular file. */
+
+    if (stat(filename,&stat_rec) == 0
+            && (stat_rec.st_mode&S_IFMT) == S_IFREG) {
+    if (access_char == 'w') {
+        access_mode = W_OK;
+    } else if (access_char == 'x') {
+        access_mode = X_OK;
+    }
+    return access(filename,access_mode) == 0;
+    }
+    return 0;
+
+#else
+
+    FILE *fp;
+    int got_file;
+
+    if (strcmp(mode, "x") == 0) {
+    mode = "r";
+    }
+    fp = fopen(filename, mode);
+    got_file = (fp != 0);
+    if (fp != 0) {
+    (void) fclose(fp);
+    }
+    return got_file;
+
+#endif
+}
+
+/**Function********************************************************************
+
+  Synopsis           [ Search for a program in all possible paths ]
+
+  SideEffects        [none]
+
+******************************************************************************/
+char *
+util_path_search(prog)
+char *prog;
+{
+#ifdef HAVE_GETENV
+    return util_file_search(prog, getenv("PATH"), "x");
+#else
+    return util_file_search(prog, NIL(char), "x");
+#endif
+}
+
+char *
+util_file_search(file, path, mode)
+char *file;            /* file we're looking for */
+char *path;            /* search path, colon separated */
+char *mode;            /* "r", "w", or "x" */
+{
+    int quit;
+    char *buffer, *filename, *save_path, *cp;
+
+    if (path == 0 || strcmp(path, "") == 0) {
+    path = ".";        /* just look in the current directory */
+    }
+
+    save_path = path = util_strsav(path);
+    quit = 0;
+    do {
+    cp = strchr(path, ':');
+    if (cp != 0) {
+        *cp = '\0';
+    } else {
+        quit = 1;
+    }
+
+    /* cons up the filename out of the path and file name */
+    if (strcmp(path, ".") == 0) {
+        buffer = util_strsav(file);
+    } else {
+        buffer = ALLOC(char, strlen(path) + strlen(file) + 4);
+        (void) sprintf(buffer, "%s/%s", path, file);
+    }
+    filename = util_tilde_expand(buffer);
+    FREE(buffer);
+
+    /* see if we can access it */
+    if (check_file(filename, mode)) {
+        FREE(save_path);
+        return filename;
+    }
+    FREE(filename);
+    path = ++cp;
+    } while (! quit); 
+
+    FREE(save_path);
+    return 0;
+}
diff --git a/src/misc/util/safe_mem.c b/src/misc/util/safe_mem.c
new file mode 100644
index 00000000..5a8a5de8
--- /dev/null
+++ b/src/misc/util/safe_mem.c
@@ -0,0 +1,104 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/util/safe_mem.c,v
+ * rajeev
+ * 1.3
+ * 1995/08/08 22:41:29
+ *
+ */
+/* LINTLIBRARY */
+
+#include "util.h"
+
+/*
+ *  These are interface routines to be placed between a program and the
+ *  system memory allocator.  
+ *
+ *  It forces well-defined semantics for several 'borderline' cases:
+ *
+ *    malloc() of a 0 size object is guaranteed to return something
+ *        which is not 0, and can safely be freed (but not dereferenced)
+ *    free() accepts (silently) an 0 pointer
+ *    realloc of a 0 pointer is allowed, and is equiv. to malloc()
+ *    For the IBM/PC it forces no object > 64K; note that the size argument
+ *        to malloc/realloc is a 'long' to catch this condition
+ *
+ *  The function pointer MMoutOfMemory() contains a vector to handle a
+ *  'out-of-memory' error (which, by default, points at a simple wrap-up 
+ *  and exit routine).
+ */
+
+extern char *MMalloc();
+extern void MMout_of_memory();
+extern char *MMrealloc();
+
+
+void (*MMoutOfMemory)() = MMout_of_memory;
+
+
+/* MMout_of_memory -- out of memory for lazy people, flush and exit */
+void 
+MMout_of_memory(size)
+long size;
+{
+    (void) fflush(stdout);
+    (void) fprintf(stderr, "\nout of memory allocating %u bytes\n",
+           (unsigned) size);
+    assert( 0 );
+    exit(1);
+}
+
+
+char *
+MMalloc(size)
+long size;
+{
+    char *p;
+
+#ifdef IBMPC
+    if (size > 65000L) {
+    if (MMoutOfMemory != (void (*)()) 0 ) (*MMoutOfMemory)(size);
+    return NIL(char);
+    }
+#endif
+    if (size == 0) size = sizeof(long);
+    if ((p = (char *) malloc((unsigned) size)) == NIL(char)) {
+    if (MMoutOfMemory != (void (*)()) 0 ) (*MMoutOfMemory)(size);
+    return NIL(char);
+    }
+    return p;
+}
+
+
+char *
+MMrealloc(obj, size)
+char *obj;
+long size;
+{
+    char *p;
+
+#ifdef IBMPC
+    if (size > 65000L) {
+    if (MMoutOfMemory != (void (*)()) 0 ) (*MMoutOfMemory)(size);
+    return NIL(char);
+    }
+#endif
+    if (obj == NIL(char)) return MMalloc(size);
+    if (size <= 0) size = sizeof(long);
+    if ((p = (char *) realloc(obj, (unsigned) size)) == NIL(char)) {
+    if (MMoutOfMemory != (void (*)()) 0 ) (*MMoutOfMemory)(size);
+    return NIL(char);
+    }
+    return p;
+}
+
+
+void
+MMfree(obj)
+char *obj;
+{
+    if (obj != 0) {
+    free(obj);
+    }
+}
diff --git a/src/misc/util/stdlib_hack.h b/src/misc/util/stdlib_hack.h
new file mode 100644
index 00000000..2ddf73d1
--- /dev/null
+++ b/src/misc/util/stdlib_hack.h
@@ -0,0 +1,4 @@
+
+#include <stdlib.h>
+
+
diff --git a/src/misc/util/strsav.c b/src/misc/util/strsav.c
new file mode 100644
index 00000000..8da1f0c9
--- /dev/null
+++ b/src/misc/util/strsav.c
@@ -0,0 +1,157 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/util/strsav.c,v
+ * shiple
+ * 1.4
+ * 1995/08/30 17:37:58
+ *
+ */
+/* LINTLIBRARY */
+
+#include <stdio.h>
+#include "util.h"
+
+
+/*
+ *  util_strsav -- save a copy of a string
+ */
+char *
+util_strsav(s)
+char *s;
+{
+    if(s == NIL(char)) {  /* added 7/95, for robustness */
+       return s;
+    }
+    else {
+       return strcpy(ALLOC(char, strlen(s)+1), s);
+    }
+}
+
+/*
+ * util_inttostr -- converts an integer into a string
+ */
+char *
+util_inttostr(i)
+  int i;
+{
+  unsigned int mod, len;
+  char *s;
+  
+  if (i == 0)
+    len = 1;
+  else {
+    if (i < 0) {
+      len = 1;
+      mod = -i;
+    }
+    else {
+      len = 0;
+      mod = i;
+    }
+    len += (unsigned)floor(log10(mod)) + 1;
+  }
+
+  s = ALLOC(char, len + 1);
+  sprintf(s, "%d", i);
+  
+  return s;
+}
+
+/*
+ * util_strcat3 -- Creates a new string which is the concatenation of 3
+ *    strings. It is the responsibility of the caller to free this string
+ *    using FREE.
+ */
+char *
+util_strcat3(
+  char * str1,
+  char * str2,
+  char * str3)
+{
+  char *str = ALLOC(char, strlen(str1) + strlen(str2) + strlen(str3) + 1);
+  
+  (void) strcpy(str, str1);
+  (void) strcat(str, str2);
+  (void) strcat(str, str3);
+
+  return (str);
+}
+
+/*
+ * util_strcat4 -- Creates a new string which is the concatenation of 4
+ *    strings. It is the responsibility of the caller to free this string
+ *    using FREE.
+ */
+char *
+util_strcat4(
+  char * str1,
+  char * str2,
+  char * str3,
+  char * str4)
+{
+  char *str = ALLOC(char, strlen(str1) + strlen(str2) + strlen(str3) +
+                    strlen(str4) + 1);
+  
+  (void) strcpy(str, str1);
+  (void) strcat(str, str2);
+  (void) strcat(str, str3);
+  (void) strcat(str, str4);
+
+  return (str);
+}
+
+
+#if !HAVE_STRSTR
+/**Function********************************************************************
+
+  Synopsis    [required]
+
+  Description [optional]
+
+  SideEffects [required]
+
+  SeeAlso     [optional]
+
+******************************************************************************/
+char *
+strstr(
+  const char * s,
+  const char * pat)
+{
+  int len;
+
+  len = strlen(pat);
+  for (; *s != '\0'; ++s)
+    if (*s == *pat && memcmp(s, pat, len) ==  0) {
+      return (char *)s; /* UGH */
+    }
+  return NULL;
+}
+#endif /* !HAVE_STRSTR */
+
+#if !HAVE_STRCHR
+/**Function********************************************************************
+
+  Synopsis    [required]
+
+  Description [optional]
+
+  SideEffects [required]
+
+  SeeAlso     [optional]
+
+******************************************************************************/
+char *
+strchr(const char * s,
+       int c)
+{
+   for (; *s != '\0'; s++) {
+     if (*s == c) {
+       return (char *)s;
+     }
+   }
+   return NULL;
+   
+}
+#endif /* !HAVE_STRCHR */
diff --git a/src/misc/util/texpand.c b/src/misc/util/texpand.c
new file mode 100644
index 00000000..37f71cbd
--- /dev/null
+++ b/src/misc/util/texpand.c
@@ -0,0 +1,66 @@
+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/util/texpand.c,v
+ * rajeev
+ * 1.3
+ * 1995/08/08 22:41:36
+ *
+ */
+
+#include "util.h"
+
+#if HAVE_PWD_H
+#  include <pwd.h>
+#endif
+
+
+char *
+util_tilde_expand(fname)
+char *fname;
+{
+#if HAVE_PWD_H
+    struct passwd *userRecord;
+    char username[256], *filename, *dir;
+    register int i, j;
+
+    filename = ALLOC(char, strlen(fname) + 256);
+
+    /* Clear the return string */
+    i = 0;
+    filename[0] = '\0';
+
+    /* Tilde? */
+    if (fname[0] == '~') {
+    j = 0;
+    i = 1;
+    while ((fname[i] != '\0') && (fname[i] != '/')) {
+        username[j++] = fname[i++];
+    }
+    username[j] = '\0';
+    dir = (char *)0;
+    if (username[0] == '\0') {
+        /* ~/ resolves to home directory of current user */
+        userRecord = getpwuid(getuid());
+        if (userRecord) dir = userRecord->pw_dir;
+    } else {
+        /* Special check for ~octtools */
+        if (!strcmp(username,"octtools"))
+            dir = getenv("OCTTOOLS");
+        /* ~user/ resolves to home directory of 'user' */
+        if (!dir) {
+            userRecord = getpwnam(username);
+        if (userRecord) dir = userRecord->pw_dir;
+        }
+    }
+    if (dir) (void) strcat(filename, dir);
+    else i = 0;    /* leave fname as-is */
+    } /* if tilde */
+
+    /* Concantenate remaining portion of file name */
+    (void) strcat(filename, fname + i);
+    return filename;
+#else
+    return util_strsav(fname);
+#endif
+}
diff --git a/src/misc/util/util.h b/src/misc/util/util.h
new file mode 100644
index 00000000..0b147347
--- /dev/null
+++ b/src/misc/util/util.h
@@ -0,0 +1,331 @@
+/**CHeaderFile*****************************************************************
+
+  FileName    [ util.h ]
+
+  PackageName [ util ]
+
+  Synopsis    [ Very low-level utilities ]
+
+  Description [ Includes file access, pipes, forks, time, and temporary file
+          access. ]
+
+  Author      [ Stephen Edwards <sedwards@eecs.berkeley.edu> and many others]
+
+  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
+  All rights reserved.
+
+  Permission is hereby granted, without written agreement and without license
+  or royalty fees, to use, copy, modify, and distribute this software and its
+  documentation for any purpose, provided that the above copyright notice and
+  the following two paragraphs appear in all copies of this software.
+
+  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
+  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
+  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
+  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
+  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
+  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
+  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
+
+  Revision    [$Id: util.h,v 1.11 1998/05/04 02:05:08 hsv Exp $]
+
+******************************************************************************/
+
+#ifndef _UTIL
+#define _UTIL
+
+////////////////////////////////////////////
+#include "leaks.h"
+////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <math.h>
+
+//////////////// added by alanmi, November 22, 2001 ////////////////
+//#include <ctype.h>
+#include <time.h>
+#include <signal.h>
+
+#ifndef SIGALRM
+#define SIGALRM SIGINT
+#endif
+
+#ifndef SIGSTOP
+#define SIGSTOP SIGINT
+#endif
+
+#ifndef SIGXCPU
+#define SIGXCPU SIGINT
+#endif
+
+#ifndef SIGUSR1
+#define SIGUSR1 SIGINT
+#endif
+
+#ifndef SIGKILL
+#define SIGKILL SIGINT
+#endif
+
+#ifndef HUGE
+#define HUGE HUGE_VAL
+#endif
+
+#if defined(__STDC__)
+#define SIGNAL_FN       void
+#endif
+
+#define alarm(n)    ((void)0)
+#define kill(a,b)   ((void)0)
+
+#define  random  rand
+#define srandom srand
+////////////////////////////////////////////////////////////////////
+
+
+#if HAVE_UNISTD_H
+#  include <unistd.h>
+#endif
+
+#if HAVE_SYS_TYPES_H
+#  include <sys/types.h>
+#endif
+
+#if HAVE_VARARGS_H
+///////////////////////////////////////
+#undef __STDC__
+#  include <varargs.h>
+#define __STDC__ 1
+////////////////// alanmi Feb 03, 2001
+#endif
+
+#ifndef STDC_HEADERS
+#define STDC_HEADERS 1
+#endif
+
+#ifndef HAVE_STRCHR
+#define HAVE_STRCHR 1
+#endif
+
+#ifndef HAVE_GETENV
+#define HAVE_GETENV 1
+#endif
+
+#if STDC_HEADERS
+//#  include <stdlib.h>
+#  include <string.h>
+#else
+#  ifdef HAVE_STRCHR
+char * strchr();
+int strcmp();
+#  else
+#    define strchr index
+#  endif
+#  ifdef HAVE_GETENV
+char * getenv();
+#  endif
+#endif /* STDC_HEADERS */
+
+#if HAVE_ERRNO_H
+#  include <errno.h>
+#endif
+
+/*
+ * Ensure we have reasonable assert() and fail() functions
+ */
+
+#ifndef HAVE_ASSERT_H
+#define HAVE_ASSERT_H 1
+#endif
+
+#if HAVE_ASSERT_H
+#  include <assert.h>
+#else
+#  ifdef NDEBUG
+#    define assert(ex) ;
+#  else
+#    define assert(ex) {\
+    if (! (ex)) {\
+    (void) fprintf(stderr,\
+        "Assertion failed: file %s, line %d\n\"%s\"\n",\
+        __FILE__, __LINE__, "ex");\
+    (void) fflush(stdout);\
+    abort();\
+    }\
+}
+#  endif
+#endif
+
+#define fail(why) {\
+    (void) fprintf(stderr, "Fatal error: file %s, line %d\n%s\n",\
+    __FILE__, __LINE__, why);\
+    (void) fflush(stdout);\
+    abort();\
+}
+
+/*
+ * Support for ANSI function prototypes in non-ANSI compilers
+ *
+ * Usage:
+ *   extern int foo ARGS((char *, double))
+ */
+
+#ifndef ARGS
+#  ifdef __STDC__
+#     define ARGS(args)    args
+#  else
+#     define ARGS(args) ()
+# endif
+#endif
+
+#ifndef NULLARGS
+#  ifdef __STDC__
+#    define NULLARGS    (void)
+#  else
+#    define NULLARGS    ()
+#  endif
+#endif
+
+/*
+ * A little support for C++ compilers
+ */
+
+#ifdef __cplusplus
+#  define EXTERN    extern "C"
+#else
+#  define EXTERN    extern
+#endif
+
+/* 
+ * Support to define unused varibles
+ */
+#if (__GNUC__ >2 || __GNUC_MINOR__ >=7) && !defined(UNUSED)
+#define UNUSED __attribute__ ((unused))
+#else
+#define UNUSED
+#endif
+
+/*
+ * A neater way to define zero pointers
+ *
+ * Usage:
+ *  int * fred;
+ *  fred = NIL(int);
+ */
+
+#define NIL(type)        ((type *) 0)
+
+/*
+ * Left over from SIS and Octtools:
+ */
+
+//#define USE_MM
+// uncommented this line,
+// because to detect memory leaks, we need to work with malloc(), etc directly
+#define USE_MM
+
+
+
+#ifdef USE_MM
+/*
+ *  assumes the memory manager is libmm.a (a deprecated (?) Octtools library)
+ *    - allows malloc(0) or realloc(obj, 0)
+ *    - catches out of memory (and calls MMout_of_memory())
+ *    - catch free(0) and realloc(0, size) in the macros
+ */
+#  define ALLOC(type, num)    \
+    ((type *) malloc(sizeof(type) * (num)))
+#  define REALLOC(type, obj, num)    \
+    (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num)))
+#  define FREE(obj)        \
+    ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#else
+/*
+ *  enforce strict semantics on the memory allocator
+ */
+#  define ALLOC(type, num)    \
+    ((type *) MMalloc((long) sizeof(type) * (long) (num)))
+#  define REALLOC(type, obj, num)    \
+    ((type *) MMrealloc((char *) (obj), (long) sizeof(type) * (long) (num)))
+#  define FREE(obj)        \
+    ((obj) ? (free((void *) (obj)), (obj) = 0) : 0)
+EXTERN void MMout_of_memory ARGS((long));
+EXTERN char *MMalloc ARGS((long));
+EXTERN char *MMrealloc ARGS((char *, long));
+EXTERN void MMfree ARGS((char *));
+#endif
+
+#ifndef TRUE
+#  define TRUE 1
+#endif
+
+#ifndef FALSE
+#  define FALSE 0
+#endif
+
+#ifndef ABS
+#  define ABS(a)            ((a) < 0 ? -(a) : (a))
+#endif
+
+#ifndef MAX
+#  define MAX(a,b)        ((a) > (b) ? (a) : (b))
+#endif
+
+#ifndef MIN
+#  define MIN(a,b)        ((a) < (b) ? (a) : (b))
+#endif
+
+#define ptime()         util_cpu_time()
+#define print_time(t)   util_print_time(t)
+
+#ifndef HUGE_VAL
+#  ifndef HUGE
+#    define HUGE  8.9884656743115790e+307
+#  endif
+#  define HUGE_VAL HUGE
+#endif
+
+#ifndef MAXINT
+#  define MAXINT (1 << 30)
+#endif
+
+EXTERN void util_print_cpu_stats ARGS((FILE *));
+EXTERN long util_cpu_time ARGS((void));
+EXTERN void util_getopt_reset ARGS((void));
+EXTERN int util_getopt ARGS((int, char **, char *));
+EXTERN char *util_path_search ARGS((char *));
+EXTERN char *util_file_search ARGS((char *, char *, char *));
+EXTERN char *util_print_time ARGS((long));
+EXTERN int util_save_image ARGS((char *, char *));
+EXTERN char *util_strsav ARGS((char *));
+EXTERN char *util_inttostr ARGS((int));
+EXTERN char *util_strcat3 ARGS((char *, char *, char *));
+EXTERN char *util_strcat4 ARGS((char *, char *, char *, char *));
+EXTERN int util_do_nothing ARGS((void));
+EXTERN char *util_tilde_expand ARGS((char *));
+EXTERN char *util_tempnam ARGS((char *, char *));
+EXTERN FILE *util_tmpfile ARGS((void));
+EXTERN void util_srandom ARGS((long));
+EXTERN long util_random ARGS(());
+EXTERN int getSoftDataLimit ARGS(());
+
+/*
+ * Global variables for util_getopt()
+ */
+
+extern int util_optind;
+extern char *util_optarg;
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Function prototypes                                                       */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* _UTIL */
diff --git a/src/misc/vec/module.make b/src/misc/vec/module.make
new file mode 100644
index 00000000..d6d908e7
--- /dev/null
+++ b/src/misc/vec/module.make
@@ -0,0 +1 @@
+SRC += 
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
new file mode 100644
index 00000000..34b0bfa2
--- /dev/null
+++ b/src/misc/vec/vec.h
@@ -0,0 +1,58 @@
+/**CFile****************************************************************
+
+  FileName    [vec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_H__
+#define __VEC_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "vecFan.h"
+#include "vecInt.h"
+#include "vecPtr.h"
+#include "vecStr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan.h
new file mode 100644
index 00000000..7bfded4a
--- /dev/null
+++ b/src/misc/vec/vecFan.h
@@ -0,0 +1,361 @@
+/**CFile****************************************************************
+
+  FileName    [vecFan.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of integers (fanins/fanouts) with memory management.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecFan.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_FAN_H__
+#define __VEC_FAN_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_Fan_t_       Abc_Fan_t;
+struct Abc_Fan_t_ // 1 word
+{
+    unsigned         iFan    : 21;  // the ID of the object
+    unsigned         nLats   :  3;  // the number of latches (up to 7)
+    unsigned         Inits   :  7;  // the initial values of the latches
+    unsigned         fCompl  :  1;  // the complemented attribute
+};
+
+typedef struct Vec_Fan_t_       Vec_Fan_t;
+struct Vec_Fan_t_ 
+{
+    int              nSize;
+    int              nCap;
+    Abc_Fan_t *      pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts an integer into the simple fanin structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Fan_t Vec_Int2Fan( int iFan )
+{
+    return *((Abc_Fan_t *)&iFan);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Fan_t * Vec_FanArray( Vec_Fan_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_FanSize( Vec_Fan_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Fan_t Vec_FanEntry( Vec_Fan_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_FanWriteEntry( Vec_Fan_t * p, int i, Abc_Fan_t Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Fan_t Vec_FanEntryLast( Vec_Fan_t * p )
+{
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_FanShrink( Vec_Fan_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_FanClear( Vec_Fan_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_FanPush( Extra_MmStep_t * pMemMan, Vec_Fan_t * p, Abc_Fan_t Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        Abc_Fan_t * pArray;
+        int i;
+
+        if ( p->nSize == 0 )
+            p->nCap = 1;
+        pArray = (Abc_Fan_t *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
+//        pArray = ALLOC( int, p->nCap * 2 );
+        if ( p->pArray )
+        {
+            for ( i = 0; i < p->nSize; i++ )
+                pArray[i] = p->pArray[i];
+            Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
+//            free( p->pArray );
+        }
+        p->nCap *= 2;
+        p->pArray = pArray;
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Fan_t Vec_FanPop( Vec_Fan_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_FanFindEntry( Vec_Fan_t * p, unsigned iFan )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i].iFan == iFan )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_FanDeleteEntry( Vec_Fan_t * p, unsigned iFan )
+{
+    int i, k, fFound = 0;
+    for ( i = k = 0; i < p->nSize; i++ )
+    {
+        if ( p->pArray[i].iFan == iFan )
+            fFound = 1;
+        else
+            p->pArray[k++] = p->pArray[i];
+    }
+    p->nSize = k;
+    return fFound;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_FanSortCompare1( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_FanSortCompare2( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_FanSort( Vec_Fan_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_FanSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_FanSortCompare1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
new file mode 100644
index 00000000..8cca2b29
--- /dev/null
+++ b/src/misc/vec/vecInt.h
@@ -0,0 +1,496 @@
+/**CFile****************************************************************
+
+  FileName    [vecInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of integers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_INT_H__
+#define __VEC_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Int_t_       Vec_Int_t;
+struct Vec_Int_t_ 
+{
+    int              nSize;
+    int              nCap;
+    int *            pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 = ALLOC( Vec_Int_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    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 = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntAllocArrayCopy( int * pArray, int nSize )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( int, nSize );
+    memcpy( p->pArray, pArray, sizeof(int) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFree( Vec_Int_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int * Vec_IntReleaseArray( Vec_Int_t * p )
+{
+    int * pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int * Vec_IntArray( Vec_Int_t * p )
+{
+    return p->pArray;
+}
+
+/**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 int Vec_IntEntryLast( Vec_Int_t * p )
+{
+    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 = REALLOC( int, p->pArray, nCapMin ); 
+    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 Entry )
+{
+    int i;
+    Vec_IntGrow( p, nSize );
+    p->nSize = nSize;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[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    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
+{
+    int i;
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->nSize++;
+    for ( i = p->nSize-2; i >= 0; i-- )
+        if ( p->pArray[i] > Entry )
+            p->pArray[i+1] = p->pArray[i];
+        else
+            break;
+    p->pArray[i+1] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntPop( Vec_Int_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSortCompare1( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSortCompare2( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_IntSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_IntSortCompare1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
new file mode 100644
index 00000000..0ba1bdc5
--- /dev/null
+++ b/src/misc/vec/vecPtr.h
@@ -0,0 +1,461 @@
+/**CFile****************************************************************
+
+  FileName    [vecPtr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of generic pointers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecPtr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_PTR_H__
+#define __VEC_PTR_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Ptr_t_       Vec_Ptr_t;
+struct Vec_Ptr_t_ 
+{
+    int              nSize;
+    int              nCap;
+    void **          pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    if ( nCap > 0 && nCap < 8 )
+        nCap = 8;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocArray( void ** pArray, int nSize )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( void *, nSize );
+    memcpy( p->pArray, pArray, sizeof(void *) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(void *) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFree( Vec_Ptr_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void ** Vec_PtrReleaseArray( Vec_Ptr_t * p )
+{
+    void ** pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void ** Vec_PtrArray( Vec_Ptr_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrSize( Vec_Ptr_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_PtrEntryLast( Vec_Ptr_t * p )
+{
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( void *, p->pArray, nCapMin ); 
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFill( Vec_Ptr_t * p, int nSize, void * Entry )
+{
+    int i;
+    Vec_PtrGrow( p, nSize );
+    p->nSize = nSize;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrShrink( Vec_Ptr_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrClear( Vec_Ptr_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrPush( Vec_Ptr_t * p, void * Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_PtrGrow( p, 16 );
+        else
+            Vec_PtrGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrPushUnique( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_PtrPush( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_PtrPop( Vec_Ptr_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves the first nItems to the end.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems )
+{
+    assert( nItems < p->nSize );
+    Vec_PtrGrow( p, nItems + p->nSize );
+    memmove( (char **)p->pArray + p->nSize, p->pArray, nItems * sizeof(void*) );
+    memmove( p->pArray, (char **)p->pArray + nItems, p->nSize * sizeof(void*) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
+{
+    qsort( (void *)p->pArray, p->nSize, sizeof(void *), 
+            (int (*)(const void *, const void *)) Vec_PtrSortCompare );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
new file mode 100644
index 00000000..367304d4
--- /dev/null
+++ b/src/misc/vec/vecStr.h
@@ -0,0 +1,466 @@
+/**CFile****************************************************************
+
+  FileName    [vecStr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of characters.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecStr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_STR_H__
+#define __VEC_STR_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Str_t_       Vec_Str_t;
+struct Vec_Str_t_ 
+{
+    int              nSize;
+    int              nCap;
+    char *           pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 = ALLOC( Vec_Str_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAllocArrayCopy( char * pArray, int nSize )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( char, nSize );
+    memcpy( p->pArray, pArray, sizeof(char) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrDup( Vec_Str_t * pVec )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(char) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrDupArray( Vec_Str_t * pVec )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrFree( Vec_Str_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Vec_StrReleaseArray( Vec_Str_t * p )
+{
+    char * pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Vec_StrArray( Vec_Str_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSize( Vec_Str_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char Vec_StrEntry( Vec_Str_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrWriteEntry( Vec_Str_t * p, int i, char Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char Vec_StrEntryLast( Vec_Str_t * p )
+{
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( char, p->pArray, nCapMin ); 
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Entry )
+{
+    int i;
+    Vec_StrGrow( p, nSize );
+    p->nSize = nSize;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrShrink( Vec_Str_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrClear( Vec_Str_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_StrGrow( p, 16 );
+        else
+            Vec_StrGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char Vec_StrPop( Vec_Str_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSortCompare1( char * pp1, char * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSortCompare2( char * pp1, char * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_StrSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+