Merge remote-tracking branch 'upstream/master' into yosys-experimental

19 files changed, 1353 insertions, 46 deletions

diff --git a/src/misc/bzlib/decompress.c b/src/misc/bzlib/decompress.c
index 47dd98e4..4b7370f1 100644
--- a/src/misc/bzlib/decompress.c
+++ b/src/misc/bzlib/decompress.c
@@ -21,6 +21,10 @@
 
 #include "bzlib_private.h"
 
+#if (__GNUC__ >= 8)
+  #pragma GCC diagnostic ignored "-Wimplicit-fallthrough"
+#endif
+
 ABC_NAMESPACE_IMPL_START
 
 
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 2f38692d..3ab09965 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -106,6 +106,7 @@ extern char *       Extra_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern void         Extra_FileNameCorrectPath( char * FileName );
 extern char *       Extra_FileNameWithoutPath( char * FileName );
 extern char *       Extra_FilePathWithoutName( char * FileName );
+extern char *       Extra_FileInTheSameDir( char * pPathFile, char * pFileName );
 extern char *       Extra_FileDesignName( char * pFileName );
 extern int          Extra_FileCheck( char * pFileName );
 extern int          Extra_FileSize( char * pFileName );
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 38192c71..54e6efc2 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -240,13 +240,25 @@ char * Extra_FilePathWithoutName( char * FileName )
     for ( pRes = FileName + strlen(FileName) - 1; pRes >= FileName; pRes-- )
         if ( *pRes == '\\' || *pRes == '/' )
         {
-           *pRes = 0;
+           pRes[1] = '\0';
            Extra_FileNameCorrectPath( FileName );
            return FileName;
         }
     ABC_FREE( FileName );
     return NULL;
 }
+char * Extra_FileInTheSameDir( char * pPathFile, char * pFileName )
+{
+    static char pBuffer[1000]; char * pThis;
+    assert( strlen(pPathFile) + strlen(pFileName) < 990 );
+    memmove( pBuffer, pPathFile, strlen(pPathFile) );
+    for ( pThis = pBuffer + strlen(pPathFile) - 1; pThis >= pBuffer; pThis-- )
+        if ( *pThis == '\\' || *pThis == '/' )
+            break;
+    memmove( ++pThis, pFileName, strlen(pFileName) );
+    pThis[strlen(pFileName)] = '\0';
+    return pBuffer;
+}
 char * Extra_FileDesignName( char * pFileName )
 {
     char * pBeg, * pEnd, * pStore, * pCur;
diff --git a/src/misc/extra/extraUtilPrime.c b/src/misc/extra/extraUtilPrime.c
index 215de367..13558092 100644
--- a/src/misc/extra/extraUtilPrime.c
+++ b/src/misc/extra/extraUtilPrime.c
@@ -583,7 +583,7 @@ void Tab_DecomposeTest()
     Vec_Int_t * vPrimes = Abc_GenPrimes( nVars );
     Tab_Man_t * p = Tab_ManAlloc( nVars, Vec_IntSize(vPrimes) );
     Tab_ManStart( p, vPrimes );
-    printf( "Created %d cubes dependent on %d variables with %d literals.\n", p->nCubes, p->nVars );
+    printf( "Created %d cubes dependent on %d variables.\n", p->nCubes, p->nVars );
     vPairs = Tab_ManCollectDist1( p, 0 );
     printf( "Collected %d pairs.\n", Vec_IntSize(vPairs)/2 );
     Vec_IntFree( vPairs );
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
index db604396..7ee3ddc3 100644
--- a/src/misc/extra/extraUtilReader.c
+++ b/src/misc/extra/extraUtilReader.c
@@ -22,8 +22,11 @@
 #include "extra.h"
 #include "misc/vec/vec.h"
 
-ABC_NAMESPACE_IMPL_START
+#if (__GNUC__ >= 8)
+  #pragma GCC diagnostic ignored "-Wimplicit-fallthrough"
+#endif
 
+ABC_NAMESPACE_IMPL_START
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/misc/mem/mem.c b/src/misc/mem/mem.c
index 23d8d7ec..347d0130 100644
--- a/src/misc/mem/mem.c
+++ b/src/misc/mem/mem.c
@@ -156,6 +156,22 @@ void Mem_FixedStop( Mem_Fixed_t * p, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Wrapper for Mem_FlexStop for use in Vec_AttAlloc]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FlexStop2( Mem_Flex_t * p )
+{
+     Mem_FlexStop( p, 0 );  
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/misc/mem/mem.h b/src/misc/mem/mem.h
index 4c0aa038..7bc5306c 100644
--- a/src/misc/mem/mem.h
+++ b/src/misc/mem/mem.h
@@ -50,6 +50,7 @@ extern int           Mem_FixedReadMaxEntriesUsed( Mem_Fixed_t * p );
 // flexible-size-block memory manager
 extern Mem_Flex_t *  Mem_FlexStart();
 extern void          Mem_FlexStop( Mem_Flex_t * p, int fVerbose );
+extern void          Mem_FlexStop2( Mem_Flex_t * p );
 extern char *        Mem_FlexEntryFetch( Mem_Flex_t * p, int nBytes );
 extern void          Mem_FlexRestart( Mem_Flex_t * p );
 extern int           Mem_FlexReadMemUsage( Mem_Flex_t * p );
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index d7c5bea7..d1a9b4d3 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -288,6 +288,8 @@ static inline int      Abc_Base2Log( unsigned n )             { int r; if ( n <
 static inline int      Abc_Base10Log( unsigned n )            { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; }
 static inline int      Abc_Base16Log( unsigned n )            { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; }
 static inline char *   Abc_UtilStrsav( char * s )             { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL;  }
+static inline char *   Abc_UtilStrsavTwo( char * s, char * a ){ char * r; if (!a) return Abc_UtilStrsav(s); r = ABC_ALLOC(char, strlen(s)+strlen(a)+1); sprintf(r, "%s%s", s, a ); return r; }
+static inline char *   Abc_UtilStrsavNum( char * s, int n )   { char * r; if (!s) return NULL;              r = ABC_ALLOC(char, strlen(s)+12+1);        sprintf(r, "%s%d", s, n ); return r; }
 static inline int      Abc_BitByteNum( int nBits )            { return (nBits>>3) + ((nBits&7)  > 0);                       }
 static inline int      Abc_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);                       }
 static inline int      Abc_Bit6WordNum( int nBits )           { return (nBits>>6) + ((nBits&63) > 0);                       }
@@ -327,7 +329,12 @@ static inline int      Abc_Lit2Att4( int Lit )                { assert(Lit >= 0)
 typedef ABC_INT64_T abctime;
 static inline abctime Abc_Clock()
 {
-#if (defined(LIN) || defined(LIN64)) && !(__APPLE__ & __MACH__) && !defined(__MINGW32__)
+#if defined(__APPLE__) && defined(__MACH__)
+  #define APPLE_MACH (__APPLE__ & __MACH__)
+#else
+  #define APPLE_MACH 0
+#endif
+#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__)
     struct timespec ts;
     if ( clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts) < 0 ) 
         return (abctime)-1;
@@ -513,6 +520,8 @@ static inline void Abc_ReverseOrder( int * pA, int nA )
 // sorting
 extern void   Abc_MergeSort( int * pInput, int nSize );
 extern int *  Abc_MergeSortCost( int * pCosts, int nSize );
+extern void   Abc_MergeSortCost2( int * pInput, int nSize, int * pCost );
+extern void   Abc_MergeSortCost2Reverse( int * pInput, int nSize, int * pCost );
 extern void   Abc_QuickSort1( word * pData, int nSize, int fDecrease );
 extern void   Abc_QuickSort2( word * pData, int nSize, int fDecrease );
 extern void   Abc_QuickSort3( word * pData, int nSize, int fDecrease );
diff --git a/src/misc/util/utilNam.c b/src/misc/util/utilNam.c
index 30a68c63..f6539f03 100644
--- a/src/misc/util/utilNam.c
+++ b/src/misc/util/utilNam.c
@@ -144,6 +144,45 @@ void Abc_NamPrint( Abc_Nam_t * p, char * pFileName )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes into a file and reads from a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NamSave( Abc_Nam_t * p, char * pFileName )
+{
+    FILE * pFile = fopen( pFileName, "wb" ); int h, i;
+    if ( pFile == NULL ) { printf( "Count node open input file %s\n", pFileName ); return; }
+    Vec_IntForEachEntryStart( &p->vInt2Handle, h, i, 1 )
+        fprintf( pFile, "%s\n", Abc_NamHandleToStr(p, h) );
+    fclose(pFile);
+}
+Abc_Nam_t * Abc_NamLoad( char * pFileName )
+{
+    Abc_Nam_t * p;
+    int fFound, NameId = -1, nLineSize = 1 << 20;
+    char * pBuffer = ABC_ALLOC( char, nLineSize+1 );
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL ) { printf( "Count node open output file %s\n", pFileName ); return NULL; }
+    p = Abc_NamStart( 1000, 20 );
+    while ( fgets( pBuffer, nLineSize, pFile ) != NULL )
+    {
+        pBuffer[strlen(pBuffer)-1] = 0;
+        NameId = Abc_NamStrFindOrAdd( p, pBuffer, &fFound );
+        assert( !fFound );
+    }
+    assert( NameId+1 == Abc_NamObjNumMax(p) );
+    fclose( pFile );
+    ABC_FREE( pBuffer );
+    return p;
+}
+
+/**Function*************************************************************
+
   Synopsis    [References the manager.]
 
   Description []
diff --git a/src/misc/util/utilNam.h b/src/misc/util/utilNam.h
index 8e054fc1..cf2d27e7 100644
--- a/src/misc/util/utilNam.h
+++ b/src/misc/util/utilNam.h
@@ -53,6 +53,8 @@ typedef struct Abc_Nam_t_           Abc_Nam_t;
 extern Abc_Nam_t *     Abc_NamStart( int nObjs, int nAveSize );
 extern void            Abc_NamStop( Abc_Nam_t * p );
 extern void            Abc_NamPrint( Abc_Nam_t * p, char * pFileName );
+extern void            Abc_NamSave( Abc_Nam_t * p, char * pFileName );
+extern Abc_Nam_t *     Abc_NamLoad( char * pFileName );
 extern Abc_Nam_t *     Abc_NamRef( Abc_Nam_t * p );
 extern void            Abc_NamDeref( Abc_Nam_t * p );
 extern int             Abc_NamObjNumMax( Abc_Nam_t * p );
diff --git a/src/misc/util/utilSort.c b/src/misc/util/utilSort.c
index 31890503..a748caf9 100644
--- a/src/misc/util/utilSort.c
+++ b/src/misc/util/utilSort.c
@@ -137,6 +137,210 @@ void Abc_MergeSort( int * pInput, int nSize )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Merging two lists of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SortMergeCost2( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut, int * pCost )
+{
+    int nEntries = (p1End - p1Beg) + (p2End - p2Beg);
+    int * pOutBeg = pOut;
+    while ( p1Beg < p1End && p2Beg < p2End )
+    {
+        if ( pCost[*p1Beg] == pCost[*p2Beg] )
+            *pOut++ = *p1Beg++, *pOut++ = *p2Beg++; 
+        else if ( pCost[*p1Beg] < pCost[*p2Beg] )
+            *pOut++ = *p1Beg++; 
+        else // if ( pCost[*p1Beg] > pCost[*p2Beg] )
+            *pOut++ = *p2Beg++; 
+    }
+    while ( p1Beg < p1End )
+        *pOut++ = *p1Beg++; 
+    while ( p2Beg < p2End )
+        *pOut++ = *p2Beg++;
+    assert( pOut - pOutBeg == nEntries );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursive sorting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SortCost2_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost )
+{
+    int nSize = pInEnd - pInBeg;
+    assert( nSize > 0 );
+    if ( nSize == 1 )
+        return;
+    if ( nSize == 2 )
+    {
+         if ( pCost[pInBeg[0]] > pCost[pInBeg[1]] )
+         {
+             pInBeg[0] ^= pInBeg[1];
+             pInBeg[1] ^= pInBeg[0];
+             pInBeg[0] ^= pInBeg[1];
+         }
+    }
+    else if ( nSize < 8 )
+    {
+        int temp, i, j, best_i;
+        for ( i = 0; i < nSize-1; i++ )
+        {
+            best_i = i;
+            for ( j = i+1; j < nSize; j++ )
+                if ( pCost[pInBeg[j]] < pCost[pInBeg[best_i]] )
+                    best_i = j;
+            temp = pInBeg[i]; 
+            pInBeg[i] = pInBeg[best_i]; 
+            pInBeg[best_i] = temp;
+        }
+    }
+    else
+    {
+        Abc_SortCost2_rec( pInBeg, pInBeg + nSize/2, pOutBeg, pCost );
+        Abc_SortCost2_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2, pCost );
+        Abc_SortMergeCost2( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg, pCost );
+        memcpy( pInBeg, pOutBeg, sizeof(int) * nSize );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the sorted array of integers.]
+
+  Description [This procedure is about 10% faster than qsort().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MergeSortCost2( int * pInput, int nSize, int * pCost )
+{
+    int * pOutput;
+    if ( nSize < 2 )
+        return;
+    pOutput = (int *) malloc( sizeof(int) * nSize );
+    Abc_SortCost2_rec( pInput, pInput + nSize, pOutput, pCost );
+    free( pOutput );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merging two lists of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SortMergeCost2Reverse( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut, int * pCost )
+{
+    int nEntries = (p1End - p1Beg) + (p2End - p2Beg);
+    int * pOutBeg = pOut;
+    while ( p1Beg < p1End && p2Beg < p2End )
+    {
+        if ( pCost[*p1Beg] == pCost[*p2Beg] )
+            *pOut++ = *p1Beg++, *pOut++ = *p2Beg++; 
+        else if ( pCost[*p1Beg] > pCost[*p2Beg] )
+            *pOut++ = *p1Beg++; 
+        else // if ( pCost[*p1Beg] < pCost[*p2Beg] )
+            *pOut++ = *p2Beg++; 
+    }
+    while ( p1Beg < p1End )
+        *pOut++ = *p1Beg++; 
+    while ( p2Beg < p2End )
+        *pOut++ = *p2Beg++;
+    assert( pOut - pOutBeg == nEntries );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursive sorting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SortCost2Reverse_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost )
+{
+    int nSize = pInEnd - pInBeg;
+    assert( nSize > 0 );
+    if ( nSize == 1 )
+        return;
+    if ( nSize == 2 )
+    {
+         if ( pCost[pInBeg[0]] < pCost[pInBeg[1]] )
+         {
+             pInBeg[0] ^= pInBeg[1];
+             pInBeg[1] ^= pInBeg[0];
+             pInBeg[0] ^= pInBeg[1];
+         }
+    }
+    else if ( nSize < 8 )
+    {
+        int temp, i, j, best_i;
+        for ( i = 0; i < nSize-1; i++ )
+        {
+            best_i = i;
+            for ( j = i+1; j < nSize; j++ )
+                if ( pCost[pInBeg[j]] > pCost[pInBeg[best_i]] )
+                    best_i = j;
+            temp = pInBeg[i]; 
+            pInBeg[i] = pInBeg[best_i]; 
+            pInBeg[best_i] = temp;
+        }
+    }
+    else
+    {
+        Abc_SortCost2Reverse_rec( pInBeg, pInBeg + nSize/2, pOutBeg, pCost );
+        Abc_SortCost2Reverse_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2, pCost );
+        Abc_SortMergeCost2Reverse( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg, pCost );
+        memcpy( pInBeg, pOutBeg, sizeof(int) * nSize );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the sorted array of integers.]
+
+  Description [This procedure is about 10% faster than qsort().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MergeSortCost2Reverse( int * pInput, int nSize, int * pCost )
+{
+    int * pOutput;
+    if ( nSize < 2 )
+        return;
+    pOutput = (int *) malloc( sizeof(int) * nSize );
+    Abc_SortCost2Reverse_rec( pInput, pInput + nSize, pOutput, pCost );
+    free( pOutput );
+}
+
+
 
 /**Function*************************************************************
 
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index e0ee1720..d9efa55f 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -35,6 +35,22 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static unsigned s_Truths5[6] = {
+    0xAAAAAAAA,
+    0xCCCCCCCC,
+    0xF0F0F0F0,
+    0xFF00FF00,
+    0xFFFF0000
+};
+
+static unsigned s_Truths5Neg[6] = {
+    0x55555555,
+    0x33333333,
+    0x0F0F0F0F,
+    0x00FF00FF,
+    0x0000FFFF
+};
+
 static word s_Truths6[6] = {
     ABC_CONST(0xAAAAAAAAAAAAAAAA),
     ABC_CONST(0xCCCCCCCCCCCCCCCC),
@@ -216,6 +232,12 @@ static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Abc_TtVec( word * pOut, int nWords, word Entry )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = Entry;
+}
 static inline void Abc_TtConst( word * pOut, int nWords, int fConst1 )
 {
     int w;
@@ -256,6 +278,12 @@ static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
         for ( w = 0; w < nWords; w++ )
             pOut[w] = pIn[w];
 }
+static inline word * Abc_TtDup( word * pIn, int nWords, int fCompl )
+{
+    word * pOut = ABC_ALLOC( word, nWords );
+    Abc_TtCopy( pOut, pIn, nWords, fCompl );
+    return pOut;
+}
 static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
@@ -316,6 +344,24 @@ static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWord
     for ( w = 0; w < nWords; w++ )
         pOut[w] |= pIn1[w] ^ pIn2[w];
 }
+static inline void Abc_TtAndXor( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] &= pIn1[w] ^ pIn2[w];
+}
+static inline void Abc_TtOrAnd( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] |= pIn1[w] & pIn2[w];
+}
+static inline void Abc_TtSharpOr( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = (pOut[w] & ~pIn1[w]) | pIn2[w];
+}
 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
@@ -365,6 +411,157 @@ static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCo
     }
     return 0;
 }
+static inline int Abc_TtIntersectCare( word * pIn1, word * pIn2, word * pCare, int nWords, int fCompl )
+{
+    int w;
+    if ( fCompl )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pIn1[w] & pIn2[w] & pCare[w] )
+                return 1;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pIn1[w] & pIn2[w] & pCare[w] )
+                return 1;
+    }
+    return 0;
+}static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords )
+{
+    int w;
+    if ( fComp0 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
+static inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords )
+{
+    int w;
+    if ( fComp0 && fComp1 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & ~pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else if ( fComp0 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else if ( fComp1 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & ~pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & ~pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else 
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
+static inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords )
+{
+    int w;
+    if ( fComp01 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] )
+                    return 1;
+        }
+        else 
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] )
+                    return 1;
+        }
+    }
+    else
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] )
+                    return 1;
+        }
+        else 
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( (pIn0[w] ^ pIn1[w]) & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
 static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
 {
     int w;
@@ -373,6 +570,23 @@ static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
             return 0;
     return 1;
 }
+static inline int Abc_TtEqualCare( word * pIn1, word * pIn2, word * pCare, int fComp, int nWords )
+{
+    int w;
+    if ( fComp )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( (~pIn1[w] ^ pIn2[w]) & pCare[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( (pIn1[w] ^ pIn2[w]) & pCare[w] )
+                return 0;
+    }
+    return 1;
+}
 static inline int Abc_TtOpposite( word * pIn1, word * pIn2, int nWords )
 {
     int w;
@@ -683,6 +897,33 @@ static inline void Abc_TtElemInit2( word * pTtElems, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Abc_Tt5HasVar( unsigned t, int iVar )
+{
+    return ((t << (1<<iVar)) & s_Truths5[iVar]) != (t & s_Truths5[iVar]);
+}
+static inline unsigned Abc_Tt5Cofactor0( unsigned t, int iVar )
+{
+    assert( iVar >= 0 && iVar < 5 );
+    return (t &s_Truths5Neg[iVar]) | ((t &s_Truths5Neg[iVar]) << (1<<iVar));
+}
+static inline unsigned Abc_Tt5Cofactor1( unsigned t, int iVar )
+{
+    assert( iVar >= 0 && iVar < 5 );
+    return (t & s_Truths5[iVar]) | ((t & s_Truths5[iVar]) >> (1<<iVar));
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline word Abc_Tt6Cofactor0( word t, int iVar )
 {
     assert( iVar >= 0 && iVar < 6 );
@@ -1478,31 +1719,6 @@ static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
-static inline word Abc_Tt6Permute_rec( word t, int * pPerm, int nVars )
-{
-    word uRes0, uRes1; int Var;
-    if (  t == 0 ) return 0;
-    if ( ~t == 0 ) return ~(word)0;
-    for ( Var = nVars-1; Var >= 0; Var-- )
-        if ( Abc_Tt6HasVar( t, Var ) )
-             break;
-    assert( Var >= 0 );
-    uRes0 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor0(t, Var), pPerm, Var );
-    uRes1 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor1(t, Var), pPerm, Var );
-    return (uRes0 & s_Truths6Neg[pPerm[Var]]) | (uRes1 & s_Truths6[pPerm[Var]]);
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar )
 {
     return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar));
@@ -1609,6 +1825,69 @@ static inline word Abc_Tt6RemoveVar( word t, int iVar )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word Abc_Tt6Permute_rec( word t, int * pPerm, int nVars )
+{
+    word uRes0, uRes1; int Var;
+    if (  t == 0 ) return 0;
+    if ( ~t == 0 ) return ~(word)0;
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Abc_Tt6HasVar( t, Var ) )
+             break;
+    assert( Var >= 0 );
+    uRes0 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor0(t, Var), pPerm, Var );
+    uRes1 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor1(t, Var), pPerm, Var );
+    return (uRes0 & s_Truths6Neg[pPerm[Var]]) | (uRes1 & s_Truths6[pPerm[Var]]);
+}
+static inline void Abc_TtPermute( word * p, int * pPerm, int nVars )
+{
+    int v, UnPerm[16], Perm[16];
+    assert( nVars <= 16 );
+    for ( v = 0; v < nVars; v++ )
+        UnPerm[v] = Perm[v] = v;
+    for ( v = nVars-1; v >= 0; v-- )
+    {
+        int Lev = UnPerm[pPerm[v]];
+        if ( v == Lev )
+            continue;
+        Abc_TtSwapVars( p, nVars, v, Lev );
+        ABC_SWAP( int, Perm[v], Perm[Lev] );
+        UnPerm[Perm[Lev]] = Lev;
+        UnPerm[Perm[v]] = v;
+    }
+    for ( v = 0; v < nVars; v++ )
+        assert( Perm[v] == pPerm[v] );
+}
+static inline void Abc_TtUnpermute( word * p, int * pPerm, int nVars )
+{
+    int v, Perm[16];
+    assert( nVars <= 16 );
+    for ( v = 0; v < nVars; v++ )
+        Perm[v] = pPerm[v];
+    for ( v = nVars-1; v >= 0; v-- )
+    {
+        while ( v != Perm[v] )
+        {
+            int vCur = Perm[v];
+            Abc_TtSwapVars( p, nVars, v, vCur );
+            Perm[v] = Perm[vCur];
+            Perm[vCur]= vCur;
+        }
+    }
+    for ( v = 0; v < nVars; v++ )
+        assert( Perm[v] == v );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Support minimization.]
 
   Description []
@@ -1827,22 +2106,30 @@ static inline int Abc_TtCountOnes( word x )
     x = x + (x >> 32); 
     return (int)(x & 0xFF);
 }
+static inline int Abc_TtCountOnes2( word x )
+{
+    return x ? Abc_TtCountOnes(x) : 0;
+}
 static inline int Abc_TtCountOnesVec( word * x, int nWords )
 {
     int w, Count = 0;
     for ( w = 0; w < nWords; w++ )
-        Count += Abc_TtCountOnes( x[w] );
+        Count += Abc_TtCountOnes2( x[w] );
     return Count;
 }
 static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl )
 {
     int w, Count = 0;
     if ( fCompl )
+    {
         for ( w = 0; w < nWords; w++ )
-            Count += Abc_TtCountOnes( pMask[w] & ~x[w] );
+            Count += Abc_TtCountOnes2( pMask[w] & ~x[w] );
+    }
     else
+    {
         for ( w = 0; w < nWords; w++ )
-            Count += Abc_TtCountOnes( pMask[w] & x[w] );
+            Count += Abc_TtCountOnes2( pMask[w] & x[w] );
+    }
     return Count;
 }
 static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords )
@@ -1850,23 +2137,34 @@ static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int
     int w, Count = 0;
     if ( !fComp0 && !fComp1 )
         for ( w = 0; w < nWords; w++ )
-            Count += Abc_TtCountOnes( pMask[w] &  x0[w] &  x1[w] );
+            Count += Abc_TtCountOnes2( pMask[w] &  x0[w] &  x1[w] );
     else if (  fComp0 && !fComp1 )
         for ( w = 0; w < nWords; w++ )
-            Count += Abc_TtCountOnes( pMask[w] & ~x0[w] &  x1[w] );
+            Count += Abc_TtCountOnes2( pMask[w] & ~x0[w] &  x1[w] );
     else if ( !fComp0 &&  fComp1 )
         for ( w = 0; w < nWords; w++ )
-            Count += Abc_TtCountOnes( pMask[w] &  x0[w] & ~x1[w] );
+            Count += Abc_TtCountOnes2( pMask[w] &  x0[w] & ~x1[w] );
     else 
         for ( w = 0; w < nWords; w++ )
-            Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & ~x1[w] );
+            Count += Abc_TtCountOnes2( pMask[w] & ~x0[w] & ~x1[w] );
     return Count;
 }
 static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
 {
     int w, Count = 0;
     for ( w = 0; w < nWords; w++ )
-        Count += Abc_TtCountOnes( x[w] ^ y[w] );
+        Count += Abc_TtCountOnes2( x[w] ^ y[w] );
+    return Count;
+}
+static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords )
+{
+    int w, Count = 0;
+    if ( fCompl )
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes2( pMask[w] & (x[w] ^ ~y[w]) );
+    else
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes2( pMask[w] & (x[w] ^ y[w]) );
     return Count;
 }
 static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nWords )
@@ -1875,10 +2173,20 @@ static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nW
     for ( w = 0; w < nWords; w++ )
     {
         pOut[w] &= pIn1[w] ^ pIn2[w];
-        Count += Abc_TtCountOnes( pOut[w] );
+        Count += Abc_TtCountOnes2( pOut[w] );
     }
     return Count;
 }
+static inline void Abc_TtIsfPrint( word * pOff, word * pOn, int nWords )
+{
+    int nTotal  = 64*nWords;
+    int nOffset = Abc_TtCountOnesVec(pOff, nWords);
+    int nOnset  = Abc_TtCountOnesVec(pOn, nWords);
+    int nDcset  = nTotal - nOffset - nOnset;
+    printf( "OFF =%6d (%6.2f %%)  ", nOffset, 100.0*nOffset/nTotal );
+    printf( "ON =%6d (%6.2f %%)  ",  nOnset,  100.0*nOnset/nTotal );
+    printf( "DC =%6d (%6.2f %%)",    nDcset,  100.0*nDcset/nTotal );
+}
 
 /**Function*************************************************************
 
@@ -1979,6 +2287,22 @@ static inline int Abc_TtFindLastDiffBit2( word * pIn1, word * pIn2, int nWords )
             return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
     return -1;
 }
+static inline int Abc_TtFindFirstAndBit2( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn1[w] & pIn2[w] )
+            return 64*w + Abc_Tt6FirstBit(pIn1[w] & pIn2[w]);
+    return -1;
+}
+static inline int Abc_TtFindLastAndBit2( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = nWords - 1; w >= 0; w-- )
+        if ( pIn1[w] & pIn2[w] )
+            return 64*w + Abc_Tt6LastBit(pIn1[w] & pIn2[w]);
+    return -1;
+}
 static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
 {
     int w, nWords = Abc_TtWordNum(nVars);
diff --git a/src/misc/vec/vecHsh.h b/src/misc/vec/vecHsh.h
index 00da8450..b87904a2 100644
--- a/src/misc/vec/vecHsh.h
+++ b/src/misc/vec/vecHsh.h
@@ -492,6 +492,10 @@ static inline int Hsh_VecSize( Hsh_VecMan_t * p )
 {
     return Vec_IntSize(p->vMap);
 }
+static inline double Hsh_VecManMemory( Hsh_VecMan_t * p )
+{
+    return !p ? 0.0 : Vec_IntMemory(p->vTable) + Vec_IntMemory(p->vData) + Vec_IntMemory(p->vMap);
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 514ce455..c15369d2 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -63,6 +63,8 @@ struct Vec_Int_t_
     for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
 #define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i )                           \
     for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
+#define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start )               \
+    for ( i = Start; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
 #define Vec_IntForEachEntryDouble( vVec, Entry1, Entry2, i )                                \
     for ( i = 0; (i+1 < Vec_IntSize(vVec)) && (((Entry1) = Vec_IntEntry(vVec, i)), 1) && (((Entry2) = Vec_IntEntry(vVec, i+1)), 1); i += 2 )
 #define Vec_IntForEachEntryDoubleStart( vVec, Entry1, Entry2, i, Start )                    \
@@ -148,6 +150,23 @@ static inline Vec_Int_t * Vec_IntStartRange( int First, int Range )
         p->pArray[i] = First + i;
     return p;
 }
+static inline Vec_Int_t * Vec_IntStartRandomLimit( int nSize, int Upper, int Lower )
+{
+    Vec_Int_t * p = Vec_IntAlloc( nSize );
+    int i, Gap = Upper - Lower + 1;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = Lower + Abc_Random(0) % Gap;
+    return p;
+}
+static inline void Vec_IntRandomizeOrder( Vec_Int_t * p )
+{
+    int v;
+    for ( v = 0; v < p->nSize; v++ )
+    {
+        int vRand = Abc_Random(0) % p->nSize;
+        ABC_SWAP( int, p->pArray[vRand], p->pArray[v] );
+    }
+}
 
 /**Function*************************************************************
 
@@ -732,6 +751,11 @@ static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
     }
     p->pArray[p->nSize++] = Entry;
 }
+static inline int Vec_IntPushReturn( Vec_Int_t * p, int Entry )
+{
+    Vec_IntPush( p, Entry );
+    return Entry;
+}
 static inline void Vec_IntPushTwo( Vec_Int_t * p, int Entry1, int Entry2 )
 {
     Vec_IntPush( p, Entry1 );
@@ -756,6 +780,12 @@ static inline void Vec_IntPushArray( Vec_Int_t * p, int * pEntries, int nEntries
     for ( i = 0; i < nEntries; i++ )
         Vec_IntPush( p, pEntries[i] );
 }
+static inline void Vec_IntShift( Vec_Int_t * p, int Shift )
+{
+    p->nSize  -= Shift;
+    p->nCap   -= Shift;
+    p->pArray += Shift;
+}
 
 /**Function*************************************************************
 
@@ -834,6 +864,52 @@ static inline void Vec_IntPushOrderCost( Vec_Int_t * p, int Entry, Vec_Int_t * v
 
 /**Function*************************************************************
 
+  Synopsis    [Check if the array is ordered.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntIsOrdered( Vec_Int_t * p, int fReverse )
+{
+    int i;
+    if ( fReverse )
+    {
+        for ( i = 1; i < p->nSize; i++ )
+            if ( p->pArray[i-1] < p->pArray[i] )
+                return 0;
+    }
+    else
+    {
+        for ( i = 1; i < p->nSize; i++ )
+            if ( p->pArray[i-1] > p->pArray[i] )
+                return 0;
+    }
+    return 1;
+}
+static inline int Vec_IntIsOrderedCost( Vec_Int_t * p, Vec_Int_t * vCost, int fReverse )
+{
+    int i;
+    if ( fReverse )
+    {
+        for ( i = 1; i < p->nSize; i++ )
+            if ( Vec_IntEntry(vCost, p->pArray[i-1]) < Vec_IntEntry(vCost, p->pArray[i]) )
+                return 0;
+    }
+    else
+    {
+        for ( i = 1; i < p->nSize; i++ )
+            if ( Vec_IntEntry(vCost, p->pArray[i-1]) > Vec_IntEntry(vCost, p->pArray[i]) )
+                return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Inserts the entry while preserving the increasing order.]
 
   Description []
@@ -1078,6 +1154,17 @@ static inline int Vec_IntFindMax( Vec_Int_t * p )
             Best = p->pArray[i];
     return Best;
 }
+static inline int Vec_IntArgMax( Vec_Int_t * p )
+{
+    int i, Best, Arg = 0;
+    if ( p->nSize == 0 )
+        return -1;
+    Best = p->pArray[0];
+    for ( i = 1; i < p->nSize; i++ )
+        if ( Best < p->pArray[i] )
+            Best = p->pArray[i], Arg = i;
+    return Arg;
+}
 
 /**Function*************************************************************
 
@@ -1101,6 +1188,17 @@ static inline int Vec_IntFindMin( Vec_Int_t * p )
             Best = p->pArray[i];
     return Best;
 }
+static inline int Vec_IntArgMin( Vec_Int_t * p )
+{
+    int i, Best, Arg = 0;
+    if ( p->nSize == 0 )
+        return 0;
+    Best = p->pArray[0];
+    for ( i = 1; i < p->nSize; i++ )
+        if ( Best > p->pArray[i] )
+            Best = p->pArray[i], Arg = i;
+    return Arg;
+}
 
 /**Function*************************************************************
 
@@ -1277,6 +1375,26 @@ static inline int Vec_IntCountZero( Vec_Int_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntAddPositive( Vec_Int_t * p ) 
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] > 0 )
+            Counter += p->pArray[i];
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if two vectors are equal.]
 
   Description []
@@ -1296,6 +1414,19 @@ static inline int Vec_IntEqual( Vec_Int_t * p1, Vec_Int_t * p2 )
             return 0;
     return 1;
 }
+static inline int Vec_IntContained( Vec_Int_t * pSmall, Vec_Int_t * pLarge ) 
+{
+    int i, k;
+    for ( i = 0; i < pSmall->nSize; i++ )
+    {
+        for ( k = 0; k < pLarge->nSize; k++ )
+            if ( pSmall->pArray[i] == pLarge->pArray[k] )
+                break;
+        if ( k == pLarge->nSize )
+            return 0;
+    }
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -1397,6 +1528,14 @@ static inline void Vec_IntSortMulti( Vec_Int_t * p, int nMulti, int fReverse )
         qsort( (void *)p->pArray, (size_t)(p->nSize/nMulti), nMulti*sizeof(int), 
                 (int (*)(const void *, const void *)) Vec_IntSortCompare1 );
 }
+static inline int Vec_IntIsSorted( Vec_Int_t * p, int fReverse )
+{
+    int i;
+    for ( i = 1; i < p->nSize; i++ )
+        if ( fReverse ? (p->pArray[i-1] < p->pArray[i]) : (p->pArray[i-1] > p->pArray[i]) )
+            return 0;
+    return 1;            
+}
 
 /**Function*************************************************************
 
@@ -1795,6 +1934,70 @@ static inline int Vec_IntTwoRemove( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
 
   Synopsis    [Returns the result of merging the two vectors.]
 
+  Description [Keeps only those entries of vArr1, which are in vArr2.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntTwoMerge1( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+{
+    int * pBeg  = vArr1->pArray;
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            pBeg1++;
+        else 
+            pBeg2++;
+    }
+    assert( vArr1->nSize >= pBeg - vArr1->pArray );
+    vArr1->nSize = pBeg - vArr1->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the result of subtracting for two vectors.]
+
+  Description [Keeps only those entries of vArr1, which are not in vArr2.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntTwoRemove1( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+{
+    int * pBeg  = vArr1->pArray;
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg++ = *pBeg1++;
+        else 
+            pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg++ = *pBeg1++;
+    assert( vArr1->nSize >= pBeg - vArr1->pArray );
+    vArr1->nSize = pBeg - vArr1->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the result of merging the two vectors.]
+
   Description [Assumes that the vectors are sorted in the increasing order.]
                
   SideEffects []
@@ -2032,6 +2235,13 @@ static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntClearAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
+{
+    int Entry, i;
+    Vec_IntClear( vVec1 );
+    Vec_IntForEachEntry( vVec2, Entry, i )
+        Vec_IntPush( vVec1, Entry );
+}
 static inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
 {
     int Entry, i;
@@ -2075,6 +2285,67 @@ static inline void Vec_IntRemapArray( Vec_Int_t * vOld2New, Vec_Int_t * vOld, Ve
             Vec_IntWriteEntry( vNew, iNew, Vec_IntEntry(vOld, iOld) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [File interface.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntDumpBin( char * pFileName, Vec_Int_t * p, int fVerbose )
+{
+    int RetValue;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    RetValue = fwrite( Vec_IntArray(p), 1, sizeof(int)*Vec_IntSize(p), pFile );
+    fclose( pFile );
+    if ( RetValue != (int)sizeof(int)*Vec_IntSize(p) )
+        printf( "Error reading data from file.\n" );
+    if ( fVerbose )
+        printf( "Written %d integers into file \"%s\".\n", Vec_IntSize(p), pFileName );
+}
+static inline Vec_Int_t * Vec_IntReadBin( char * pFileName, int fVerbose )
+{
+    Vec_Int_t * p = NULL; int nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    fseek( pFile, 0, SEEK_END );
+    nSize = ftell( pFile );
+    if ( nSize == 0 )
+    {
+        printf( "The input file is empty.\n" );
+        fclose( pFile );
+        return NULL;
+    }
+    if ( nSize % sizeof(int) > 0 )
+    {
+        printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", (int)(nSize % sizeof(int)) );
+        fclose( pFile );
+        return NULL;
+    }
+    rewind( pFile );
+    p = Vec_IntStart( (int)(nSize/sizeof(int)) );
+    RetValue = fread( Vec_IntArray(p), 1, nSize, pFile );
+    fclose( pFile );
+    if ( RetValue != nSize )
+        printf( "Error reading data from file.\n" );
+    if ( fVerbose )
+        printf( "Read %d integers from file \"%s\".\n", (int)(nSize/sizeof(int)), pFileName );
+    return p;
+}
+
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index ed2a481e..0f024f68 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -607,6 +607,26 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Vec_PtrFreeFunc( Vec_Ptr_t * p, void (*pFuncItemFree)(void *) ) ___unused;
+static void Vec_PtrFreeFunc( Vec_Ptr_t * p, void (*pFuncItemFree)(void *) )
+{
+    void * pItem; int i;
+    Vec_PtrForEachEntry( void *, p, pItem, i )
+        if ( pItem ) pFuncItemFree( pItem );
+    Vec_PtrFree( p );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Copies the interger array.]
 
   Description []
@@ -626,6 +646,26 @@ static inline void Vec_PtrCopy( Vec_Ptr_t * pDest, Vec_Ptr_t * pSour )
 
 /**Function*************************************************************
 
+  Synopsis    [Print names stored in the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrPrintNames( Vec_Ptr_t * p )
+{
+    char * pName; int i;
+    printf( "Vector has %d entries: {", Vec_PtrSize(p) );
+    Vec_PtrForEachEntry( char *, p, pName, i )
+        printf( "%s ", pName );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -651,6 +691,12 @@ static inline void Vec_PtrPushTwo( Vec_Ptr_t * p, void * Entry1, void * Entry2 )
     Vec_PtrPush( p, Entry1 );
     Vec_PtrPush( p, Entry2 );
 }
+static inline void Vec_PtrAppend( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2 )
+{
+    void * Entry; int i;
+    Vec_PtrForEachEntry( void *, vVec2, Entry, i )
+        Vec_PtrPush( vVec1, Entry );
+}
 
 /**Function*************************************************************
 
@@ -912,8 +958,8 @@ static int Vec_PtrSortComparePtr( void ** pp1, void ** pp2 )
   SeeAlso     []
 
 ***********************************************************************/
-static void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() ) ___unused;
-static void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
+static void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(const void *, const void *) ) ___unused;
+static void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(const void *, const void *) )
 {
     if ( p->nSize < 2 )
         return;
@@ -936,8 +982,8 @@ static void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
   SeeAlso     []
 
 ***********************************************************************/
-static void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() ) ___unused;
-static void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
+static void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(const void *, const void *) ) ___unused;
+static void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(const void *, const void *) )
 {
     int i, k;
     if ( p->nSize < 2 )
@@ -948,15 +994,15 @@ static void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
             p->pArray[k++] = p->pArray[i];
     p->nSize = k;
 }
-static void Vec_PtrUniqify2( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(void**, void**), void (*Vec_PtrObjFree)(void*), Vec_Int_t * vCounts ) ___unused;
-static void Vec_PtrUniqify2( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(void**, void**), void (*Vec_PtrObjFree)(void*), Vec_Int_t * vCounts )
+static void Vec_PtrUniqify2( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(const void *, const void *), void (*Vec_PtrObjFree)(void*), Vec_Int_t * vCounts ) ___unused;
+static void Vec_PtrUniqify2( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)(const void *, const void *), void (*Vec_PtrObjFree)(void*), Vec_Int_t * vCounts )
 {
     int i, k;
     if ( vCounts )
         Vec_IntFill( vCounts, 1, 1 );
     if ( p->nSize < 2 )
         return;
-    Vec_PtrSort( p, (int (*)())Vec_PtrSortCompare );
+    Vec_PtrSort( p, Vec_PtrSortCompare );
     for ( i = k = 1; i < p->nSize; i++ )
         if ( Vec_PtrSortCompare(p->pArray+i, p->pArray+k-1) != 0 )
         {
diff --git a/src/misc/vec/vecQue.h b/src/misc/vec/vecQue.h
index 54a10a29..6a8a68d0 100644
--- a/src/misc/vec/vecQue.h
+++ b/src/misc/vec/vecQue.h
@@ -119,6 +119,10 @@ static inline void Vec_QueClear( Vec_Que_t * p )
     }
     p->nSize = 1;
 }
+static inline double Vec_QueMemory( Vec_Que_t * p )
+{
+    return !p ? 0.0 : 2.0 * sizeof(int) * (size_t)p->nCap + sizeof(Vec_Que_t) ;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 12053d3d..16e15761 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -561,6 +561,11 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
     }
     p->pArray[p->nSize++] = Entry;
 }
+static inline void Vec_StrPushTwo( Vec_Str_t * p, char Entry1, char Entry2 )
+{
+    Vec_StrPush( p, Entry1 );
+    Vec_StrPush( p, Entry2 );
+}
 static inline void Vec_StrPushBuffer( Vec_Str_t * p, char * pBuffer, int nSize )
 {
     if ( p->nSize + nSize > p->nCap )
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index fdbded9c..cd463e01 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -275,6 +275,13 @@ static inline void Vec_WecClear( Vec_Wec_t * p )
         Vec_IntClear( vVec );
     p->nSize = 0;
 }
+static inline void Vec_WecClearLevels( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i;
+    Vec_WecForEachLevel( p, vVec, i )
+        Vec_IntClear( vVec );
+}
 
 /**Function*************************************************************
 
@@ -296,6 +303,15 @@ static inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry )
     }
     Vec_IntPush( Vec_WecEntry(p, Level), Entry );
 }
+static inline void Vec_WecPushTwo( Vec_Wec_t * p, int Level, int Entry1, int Entry2 )
+{
+    if ( p->nSize < Level + 1 )
+    {
+        Vec_WecGrow( p, Abc_MaxInt(2*p->nSize, Level + 1) );
+        p->nSize = Level + 1;
+    }
+    Vec_IntPushTwo( Vec_WecEntry(p, Level), Entry1, Entry2 );
+}
 static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p )
 {
     if ( p->nSize == p->nCap )
@@ -422,7 +438,7 @@ static inline Vec_Wec_t * Vec_WecDup( Vec_Wec_t * p )
     Vec_Wec_t * vNew;
     Vec_Int_t * vVec;
     int i, k, Entry;
-    vNew = Vec_WecAlloc( Vec_WecSize(p) );
+    vNew = Vec_WecStart( Vec_WecSize(p) );
     Vec_WecForEachLevel( p, vVec, i )
         Vec_IntForEachEntry( vVec, Entry, k )
             Vec_WecPush( vNew, i, Entry );
@@ -552,6 +568,29 @@ static inline void Vec_WecSortByLastInt( Vec_Wec_t * p, int fReverse )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_WecKeepLevels( Vec_Wec_t * p, int Limit )
+{
+    Vec_Int_t * vLevel; int i, k = 0;
+    Vec_WecForEachLevel( p, vLevel, i )
+        if ( Vec_IntSize(vLevel) > Limit )
+        {
+            ABC_SWAP( Vec_Int_t, Vec_WecArray(p)[i], Vec_WecArray(p)[k] );
+            k++;
+        }
+    Vec_WecShrink( p, k );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
 {
     Vec_Int_t * vVec;
@@ -637,6 +676,25 @@ static inline int Vec_WecCountNonTrivial( Vec_Wec_t * p, int * pnUsed )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_WecMaxLevelSize( Vec_Wec_t * p )
+{
+    Vec_Int_t * vTemp; int i, Res = 0;
+    Vec_WecForEachLevel( p, vTemp, i )
+        Res = Abc_MaxInt( Res, Vec_IntSize(vTemp) );
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline Vec_Int_t * Vec_WecCollectFirsts( Vec_Wec_t * p )
 {
     Vec_Int_t * vFirsts, * vLevel;
@@ -733,6 +791,83 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [File interface.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecDumpBin( char * pFileName, Vec_Wec_t * p, int fVerbose )
+{
+    Vec_Int_t * vLevel;
+    int i, nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    nSize = Vec_WecSize(p);
+    RetValue = fwrite( &nSize, 1, sizeof(int), pFile );
+    Vec_WecForEachLevel( p, vLevel, i )
+    {
+        nSize = Vec_IntSize(vLevel);
+        RetValue += fwrite( &nSize, 1, sizeof(int), pFile );
+        RetValue += fwrite( Vec_IntArray(vLevel), 1, sizeof(int)*nSize, pFile );
+    }
+    fclose( pFile );
+    if ( RetValue != (int)sizeof(int)*(Vec_WecSizeSize(p)+Vec_WecSize(p)+1) )
+        printf( "Error writing data into file.\n" );
+    if ( fVerbose )
+        printf( "Written %d integer arrays into file \"%s\".\n", Vec_WecSize(p), pFileName );
+}
+static inline Vec_Wec_t * Vec_WecReadBin( char * pFileName, int fVerbose )
+{
+    Vec_Wec_t * p = NULL; Vec_Int_t * vLevel; int i, nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    fseek( pFile, 0, SEEK_END );
+    nSize = ftell( pFile );
+    if ( nSize == 0 )
+    {
+        printf( "The input file is empty.\n" );
+        fclose( pFile );
+        return NULL;
+    }
+    if ( nSize % sizeof(int) > 0 )
+    {
+        printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", (int)(nSize % sizeof(int)) );
+        fclose( pFile );
+        return NULL;
+    }
+    rewind( pFile );
+    RetValue = fread( &nSize, 1, sizeof(int), pFile );
+    assert( RetValue == 4 );
+    p = Vec_WecStart( nSize );
+    Vec_WecForEachLevel( p, vLevel, i )
+    {
+        RetValue = fread( &nSize, 1, sizeof(int), pFile );
+        assert( RetValue == 4 );
+        Vec_IntFill( vLevel, nSize, 0 );
+        RetValue = fread( Vec_IntArray(vLevel), 1, sizeof(int)*nSize, pFile );
+        assert( RetValue == 4*nSize );
+    }
+    fclose( pFile );
+    if ( fVerbose )
+        printf( "Read %d integer arrays from file \"%s\".\n", Vec_WecSize(p), pFileName );
+    return p;
+}
+
+
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index e123c054..8275702a 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -61,6 +61,8 @@ struct Vec_Wrd_t_
     for ( i = Start; (i < Stop) && (((Entry) = Vec_WrdEntry(vVec, i)), 1); i++ )
 #define Vec_WrdForEachEntryReverse( vVec, pEntry, i )                                       \
     for ( i = Vec_WrdSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_WrdEntry(vVec, i)), 1); i-- )
+#define Vec_WrdForEachEntryDouble( vVec, Entry1, Entry2, i )                                \
+    for ( i = 0; (i+1 < Vec_WrdSize(vVec)) && (((Entry1) = Vec_WrdEntry(vVec, i)), 1) && (((Entry2) = Vec_WrdEntry(vVec, i+1)), 1); i += 2 )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -167,6 +169,32 @@ static inline Vec_Wrd_t * Vec_WrdStartRandom( int nSize )
         vSims->pArray[i] = Abc_RandomW(0);
     return vSims;
 }
+static inline Vec_Wrd_t * Vec_WrdStartTruthTables( int nVars )
+{
+    Vec_Wrd_t * p;
+    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    int i, k, nWords;
+    nWords = nVars <= 6 ? 1 : (1 << (nVars - 6));
+    p = Vec_WrdStart( nWords * nVars );
+    for ( i = 0; i < nVars; i++ )
+    {
+        unsigned * pTruth = (unsigned *)(p->pArray + nWords * i);
+        if ( i < 5 )
+        {
+            for ( k = 0; k < 2*nWords; k++ )
+                pTruth[k] = Masks[i];
+        }
+        else
+        {
+            for ( k = 0; k < 2*nWords; k++ )
+                if ( k & (1 << (i-5)) )
+                    pTruth[k] = ~(unsigned)0;
+                else
+                    pTruth[k] = 0;
+        }
+    }
+    return p;
+}
 
 /**Function*************************************************************
 
@@ -354,6 +382,10 @@ static inline int Vec_WrdSize( Vec_Wrd_t * p )
 {
     return p->nSize;
 }
+static inline int Vec_WrdChangeSize( Vec_Wrd_t * p, int Shift )
+{
+    return p->nSize += Shift;
+}
 
 /**Function*************************************************************
 
@@ -643,6 +675,30 @@ static inline void Vec_WrdPush( Vec_Wrd_t * p, word Entry )
     }
     p->pArray[p->nSize++] = Entry;
 }
+static inline void Vec_WrdPushTwo( Vec_Wrd_t * p, word Entry1, word Entry2 )
+{
+    Vec_WrdPush( p, Entry1 );
+    Vec_WrdPush( p, Entry2 );
+}
+static inline void Vec_WrdPushThree( Vec_Wrd_t * p, word Entry1, word Entry2, word Entry3 )
+{
+    Vec_WrdPush( p, Entry1 );
+    Vec_WrdPush( p, Entry2 );
+    Vec_WrdPush( p, Entry3 );
+}
+static inline void Vec_WrdPushFour( Vec_Wrd_t * p, word Entry1, word Entry2, word Entry3, word Entry4 )
+{
+    Vec_WrdPush( p, Entry1 );
+    Vec_WrdPush( p, Entry2 );
+    Vec_WrdPush( p, Entry3 );
+    Vec_WrdPush( p, Entry4 );
+}
+static inline void Vec_WrdPushArray( Vec_Wrd_t * p, word * pEntries, int nEntries )
+{
+    int i;
+    for ( i = 0; i < nEntries; i++ )
+        Vec_WrdPush( p, pEntries[i] );
+}
 
 /**Function*************************************************************
 
@@ -851,6 +907,14 @@ static inline void Vec_WrdInsert( Vec_Wrd_t * p, int iHere, word Entry )
         p->pArray[i] = p->pArray[i-1];
     p->pArray[i] = Entry;
 }
+static inline void Vec_WrdDrop( Vec_Wrd_t * p, int i )
+{
+    int k;
+    assert( i >= 0 && i < Vec_WrdSize(p) );
+    p->nSize--;
+    for ( k = i; k < p->nSize; k++ )
+        p->pArray[k] = p->pArray[k+1];
+}
 
 /**Function*************************************************************
 
@@ -1201,6 +1265,169 @@ static inline void Vec_WrdAppend( Vec_Wrd_t * vVec1, Vec_Wrd_t * vVec2 )
         Vec_WrdPush( vVec1, Entry );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords )
+{
+    int k, Digit, nDigits = nWords*16;
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15);
+        if ( Digit < 10 )
+            fprintf( pFile, "%d", Digit );
+        else
+            fprintf( pFile, "%c", 'A' + Digit-10 );
+    }
+    fprintf( pFile, "\n" );
+}
+static inline void Vec_WrdPrintHex( Vec_Wrd_t * p, int nWords )
+{
+    int i, nNodes = Vec_WrdSize(p) / nWords;
+    assert( Vec_WrdSize(p) % nWords == 0 );
+    for ( i = 0; i < nNodes; i++ )
+        Gia_ManSimPatWriteOne( stdout, Vec_WrdEntryP(p, i*nWords), nWords );
+}
+static inline void Vec_WrdDumpHex( char * pFileName, Vec_Wrd_t * p, int nWords, int fVerbose )
+{
+    int i, nNodes = Vec_WrdSize(p) / nWords;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    assert( Vec_WrdSize(p) % nWords == 0 );
+    for ( i = 0; i < nNodes; i++ )
+        Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(p, i*nWords), nWords );
+    fclose( pFile );
+    if ( fVerbose )
+        printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(p)/nWords, pFileName );
+}
+static inline int Vec_WrdReadHexOne( char c )
+{
+    int Digit = 0;
+    if ( c >= '0' && c <= '9' )
+        Digit = c - '0';
+    else if ( c >= 'A' && c <= 'F' )
+        Digit = c - 'A' + 10;
+    else if ( c >= 'a' && c <= 'f' )
+        Digit = c - 'a' + 10;
+    else assert( 0 );
+    assert( Digit >= 0 && Digit < 16 );
+    return Digit;
+}
+static inline Vec_Wrd_t * Vec_WrdReadHex( char * pFileName, int * pnWords, int fVerbose )
+{
+    Vec_Wrd_t * p = NULL; 
+    int c, nWords = -1, nChars = 0; word Num = 0;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    p = Vec_WrdAlloc( 1000 );
+    while ( (c = fgetc(pFile)) != EOF )
+    {
+        if ( c == '\r' || c == '\t' || c == ' ' )
+            continue;
+        if ( c == '\n' )
+        {
+            if ( nChars > 0 )
+            {
+                Vec_WrdPush( p, Num );
+                nChars = 0; 
+                Num = 0;
+            }
+            if ( nWords == -1 && Vec_WrdSize(p) > 0 )
+                nWords = Vec_WrdSize(p);
+            continue;
+        }
+        Num |= (word)Vec_WrdReadHexOne((char)c) << (nChars * 4);
+        if ( ++nChars < 16 )
+            continue;
+        Vec_WrdPush( p, Num );
+        nChars = 0; 
+        Num = 0;
+    }
+    assert( Vec_WrdSize(p) % nWords == 0 );
+    fclose( pFile );
+    if ( pnWords )
+        *pnWords = nWords;
+    if ( fVerbose )
+        printf( "Read %d words of simulation data for %d objects.\n", nWords, Vec_WrdSize(p)/nWords );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WrdDumpBin( char * pFileName, Vec_Wrd_t * p, int fVerbose )
+{
+    int RetValue;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    RetValue = fwrite( Vec_WrdArray(p), 1, 8*Vec_WrdSize(p), pFile );
+    fclose( pFile );
+    if ( RetValue != 8*Vec_WrdSize(p) )
+        printf( "Error reading data from file.\n" );
+    if ( fVerbose )
+        printf( "Written %d words of simulation data into file \"%s\".\n", Vec_WrdSize(p), pFileName );
+}
+static inline Vec_Wrd_t * Vec_WrdReadBin( char * pFileName, int fVerbose )
+{
+    Vec_Wrd_t * p = NULL; int nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    fseek( pFile, 0, SEEK_END );
+    nSize = ftell( pFile );
+    if ( nSize == 0 )
+    {
+        printf( "The input file is empty.\n" );
+        fclose( pFile );
+        return NULL;
+    }
+    if ( nSize % 8 > 0 )
+    {
+        printf( "Cannot read file with simulation data that is not aligned at 8 bytes (remainder = %d).\n", nSize % 8 );
+        fclose( pFile );
+        return NULL;
+    }
+    rewind( pFile );
+    p = Vec_WrdStart( nSize/8 );
+    RetValue = fread( Vec_WrdArray(p), 1, nSize, pFile );
+    fclose( pFile );
+    if ( RetValue != nSize )
+        printf( "Error reading data from file.\n" );
+    if ( fVerbose )
+        printf( "Read %d words of simulation data from file \"%s\".\n", nSize/8, pFileName );
+    return p;
+}
 
 ABC_NAMESPACE_HEADER_END