Version abc50729

8 files changed, 3101 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