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

5 files changed, 613 insertions, 35 deletions

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);