7 files changed, 700 insertions, 8 deletions

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